Legacy Dynamic Models

A dynamic model represents something changing over time. As of Alloy 6, you can model dynamic systems with the Time functions. This page is about how dynamics used to be modeled in Alloy, in case you need to read an old spec.

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.

See also

time

A module with some utility macros to better model time.

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.

Full spec downloadable here
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.

Full spec downloadable here
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.

Full spec downloadable here
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.

Full spec downloadable here
open util/ordering[Time]

sig 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:

Full spec downloadable here
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.

Full spec downloadable here
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.

Full spec downloadable here
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.

Full spec downloadable here
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

Full spec downloadable here
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.

Full spec downloadable here
fact trace {
  -- everybody starts with their initial page in history
  at.first = history.first 
  all t: Time - last |
    let t" = t.next {
      all u: User |
        u.stay[t, t"] or
        some p: Page | u.goto[p, t, t"]
    }
}

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.

“No Models Found”

ordering implicity makes the ordered signature exact and this cannot be overridden. If a dynamic spec does not exist, it’s likely due to this.

open util/ordering[State]

sig State {}

run {#State = 2} -- no models

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.