Dynamic Models¶
A dynamic model represents something changing over time. Alloy does not have a first-class notion of time, and dynamics must be encoded as part of the relationships. This is normally done by placing an ordering on some signature, which then used to emulate time. There are several common ways of doing this.
Changing Object Signature¶
When only one entity is changing and there is only one instance of the signature to consider, we can place the ordering on the signature itself. Then each atom of that signature represents the state of the entity at a different point in time.
open util/ordering[Light] as ord
abstract sig Color {}
one sig Red, Yellow, Green extends Color {}
sig Light {
color: Color
}
While there are multiple Light atoms, they all represent the same physical “traffic light”, just at different points in time.
The dynamic model is modeled by a state change predicate, which relates each light to the next light in the sequence.
pred change_light[l: Light] {
let l" = l.(ord/next) {
l.color = Red => l".color = Green
l.color = Green => l".color = Yellow
l.color = Yellow => l".color = Red
}
}
Conventionally ordering is not namespaced. We do it here to make the imported functions clearer.
Traces¶
A trace is a fact that describes how the system will evolve, by constraining “valid models” to ones where the system evolves properly.
fact Trace {
ord/first.color = Red
all l: Light - ord/last |
change_light[l]
}
first and last are from the ordering module. This sets the first light to red and every subsequent light to the next color in the chain.
Note
We write Light - last because no last.next, so the predicate would be false.
Time Signatures¶
For more complex specifications we use a Time signature. This is useful if we have multiple things that are changing or multiple properties that can change. The ordering is placed on Time and the signature fields are all related to that time.
Representing Boolean Properties¶
If the changing value is a boolean, the best way to represent that is to have a field that is set Time, which represents the times where that field is true:
sig Key {
pressed: set Time
}
pred press[k: Key, t: Time] {
t not in k.pressed
t.next in k.pressed
}
pred release[k: Key, t: Time] {
t in k.pressed
t.next not in k.pressed
}
pred changed[k: Key, t: Time] {
press[k, t] or release[k, t]
}
We will assume that only one key can be pressed or released at a given time. This means that the trace must specify that some key changes and also that no other key changes.
fact Trace {
no first.~pressed
all t: Time - last |
some k: Key {
changed[k, t]
all k": Key - k |
not changed[k, t]
}
}
Note
We could have instead written it this way, using one instad of some:
all t: Time - last |
one k: Key |
changed[k, t]
Which would have enforced that no other keys changed by default. Using one in these contexts can be error-prone, so it’s avoided for the purposes of this page.
Conventionally, state-change predicates are written to take two time parameters, where the trace then passes in both t and t.next.
pred release[k: Key, t, t": Time] {
t in k.pressed
t" not in k.pressed
}
Representing Arbitrary Properties¶
Information beyond booleans can be encoded with Multirelations.
open util/ordering[Time]
sig Time {}
sig User {
-- current place in time
, at: Page one -> Time
-- all visited pages
, history: Page -> Time
}
Writing Page one -> Time indicates that for every User and Time, there is exactly one page. Writing Page -> Time also any number of pages per user/time.
Note
There’s no innate reason why we use Page -> Time instead of Time -> Page. However, making Time the end of the multirelation is conventional.
sig Page {
-- pages reachable from this page
link: set Page
}
pred goto[u: User, p: Page, t, t": Time] {
-- valid page to change to
p in u.at.t.link
-- change pages
p = u.at.t"
-- save new page in history
u.history.t" = u.history.t + p
}
When using multirelations of form rel = A -> B -> Time, we get the value of b at time t with a.rel.t
pred stay[u: User, t, t": Time] {
u.at.t" = u.at.t
u.history.t" = u.history.t
}
stay is a “stuttering” predicate which makes it valid for a user to not change at the next time step. Without it goto would have to be true for every single user at every time in the trace.
Common Issues¶
Incomplete Trace¶
The trace must fully cover what happens to all dynamic signatures. If not, weird things happen. Consider the following alternate trace for the browsing model:
fact Trace {
at.first = history.first -- everybody starts with their initial page in history
all t: Time - last |
let t" = t.next {
one u: User |
u.stay[t, t"] or
some p: Page | u.goto[p, t, t"]
}
}
This is true iff exactly one User either stays or goes to a valid page. This allows them to do anything that’s not covered by the two predicates. A user may go to an unlinked page, or stay on the same page but change their history to include a page they never visited.
Limitations¶
There are some limitations to what we can model in a dynamic system.
Alloy cannot tell if a system has deadlocked. A deadlock is when there is no valid next state as part of the trace. If the trace is encoded as a fact, then the entire model is discarded. If the trace is encoded as a predicate, Alloy will provide any model that doesn’t match the trace as a counterexample.
Alloy cannot test that some property is guaranteed to happen in infinite time, aka liveness.
Alloy cannot emulate fair dynamic systems.