So far, we've modeled static models in Alloy: we've described states of systems at single moments in time.

This can be useful for many systems; but often, we want to actually described changes to systems over time.

Explicit/manual event predicates and traces (all version of Alloy)

We'll start with a model of an operating system's Trash bin (where files go when you delete them). Your computer knows about the set of all file, and some subset of those files are in the trash at a given moment in time. "In the trash" is different from permanently gone: the bytes defining the file contents are still around, but your computer has marked them as in the trash. Only once you "empty" the trash are the files contents permanently deleted.

Example inspired by the Electrum 2 tutorial.

Initial static model

We'll start with the initial components of the model: we'll need some Files and Trashs.

sig File {}

sig Trash {
  files: set File
}

We can say that some particular trash is empty with a predicate:

pred emptyStartingTrash(t: Trash) {
  no t.files
}

Modeling time with explicit/manual events and traces

One way to model time is to define explicit predicates for each event that can happen over time. In this strategy, we have multiple atoms of the Trash sig that model the evolution over time.

We can relate two particular Trash atoms as being changed by a given event, e.g., by a file being deleted, with the following predicate signature:

// Model used by the textbook: two Trash instances
// t1, t2 will be related by deleteFile if t2 is the state
// of the trash after File f is deleted from t1.
pred deleteFile(f: File, t1, t2: Trash) {
    // TODO
}

To fill in the body of this predicate, we should think about how deleting a file changes the state of the trash.

pred deleteFile(f: File, t1, t2: Trash) {
  // You can't delete something already in
  // the trash, t1 is "before"
  f not in t1.files 
  // Let's try this, t1 is "after":
  f in t2.files 
}

Modeling what does not change over time

When we run the Analyzer with just these two constraints, some instances look ok, but in other instances, other files that were previously in the trash at t1 disappear at t2!

This is because the under-constrained model allows more behavior: we have not made our predicate strong enough to say anything about the state of the rest of the files in the universe. In the trash example, this is bad: deleting file foo should not cause a different file bar to be permanently deleted or restored from the trash.

Let's update our predicate to specifically use the + or union model to relate the contents of t1 and t2. In general, +, -, and & will be useful in modeling changes over time, since they are all in a sense "more strict" than just the subset operator in.

pred deleteFile(f: File, t1, t2: Trash) {
  // You can't delete something already in
  // the trash, t1 is "before"
  f not in t1.files 
  // Could try this, doesn't work because other files disappear
  // f in t2.files // t1 is "after"
  // Instead: make the "after" state be a specific
  // union (or intersection)
  t2.files = f + t1.files
}

We can check that we now avoid the case of disappearing files with an assert and check:

assert noDisappearing {
  all disj f1, f2 : File, t1, t2: Trash |
    (f1 in t1.files and deleteFile[f2, t1, t2]) 
      => f1 in t2.files
}

check noDisappearing // implicit bound: 3

As we hoped, there are no counterexamples: up to our scope, the Analyzer finds no bad disappearing cases, so it appears our updated model is a better model.

Next, we can model the "opposite" predicate: how the state of the trash should change when we restore a file.

// Restore should move a file *out* of the trash
pred restoreFile(f: File, t1, t2: Trash) {
  // f not in t2.files // True, but redundant with the final line
  // File must be in the trash to be restored
  f in t1.files 

  // Again, '-' is more strict than just subset
  t2.files = t1.files - f
}

Checking for specific traces

We can now check the outcome for a specific "trace", or series of events.

Here's an idea for an interesting trace that we can expect a certain outcome after: if we delete a file and then restore it (without anything else happening in between), the starting state and the ending state should be the same.

To just see examples of this trace, we can just ask the Analyzer for some examples:

run { 
  some t1, t2, t3: Trash, f: File | {
     deleteFile[f, t1, t2] and restoreFile[f, t2, t3]
  } 
} for 3 but exactly 3 Trash

As expected, we see an instance that does what we want: we have an empty trash, then a single file is deleted and shown in a non-empty trash, and finally there is another empty trash for after the file is restored.

Next, we can check whether the outcome we expect always holds (up to the Analyzer's small scope).

We'll now define this as a named assert and ask the Analyzer to check for counterexamples:

assert deleteThenRestore {
  all t1, t2, t3: Trash | {
     all f: File |
       // Sequence of state we're interested in 
       //    => condition we care about
       (deleteFile[f, t1, t2] and restoreFile[f, t2, t3]) 
         => (t1.files = t3.files)
  }  
}

check deleteThenRestore for 3 but exactly 3 Trash

As we hoped, we get "no counterexamples found", which means the Analyzer did not find any problems with this assertion up to its scope.

Downsides to the explicit event/trace model

There are several downsides to modeling each moment in time as a distinct Trash:

1. As we add more events, we want to let the analyzer interweave events in arbitrary ways. To allow this, we need to make Event itself a sig and then say that Events happen in a single linear trace.
2. As we cover more events, each instance in the Analyzer becomes harder to understand, single each moment in time is shown simultaneously (and the order in which Alloy numbers atoms does not always match the linear progression of time).
3. We have no built-in support for saying some property should "eventually" be true. In general, we have to do a lot of manual modeling to talk about changes over time.

Modeling changes over time in Alloy 6 with temporal logic

In Alloy 6, you can still use almost all of the Alloy features documented in the textbook to describe static systems or to manually specify explicit events and traces.

However, you can now also model systems that change over time by marking certain sigs as variable. Once any sig in a model is marked var, the instances the Analyzer finds will be traces that describe infinite sequences of states. Each state is like an instance in static Alloy, in that it is an assignment of specific atoms to all sigs and fields.

Use of in vs extends

Now, we only want there to be a single concept of "trash" in our model that is variable over time.

Rather than saying one sig Trash and keeping files as a field, we can instead just make Trash a single subset of all files. This is useful because the subset will be distinct in each state, without having to indirect through a field.

In Alloy, extends between two sig names indicates an exclusive subset, whereas an in indicates a non-exclusive subset. E.g., Student extends Person and Professor extends Person make sense, but if we want to allow a person to be both a student and an employee, we could use:Student in Person and Professor in Person. This are shown in the Analyzer as additional labels on boxes, rather than new boxes.

We'll change our file model to use this update, also marking both Files and Trash as var (since the trash changing is the whole point, and the total set of files our computer knows about will change as we empty the trash).

var sig File {}

// Defines a single, non-exclusive subset.
var sig Trash in File {} 

Our predicates for delete and restore now look similar, but we don't have two copies of each arguments for var sigs. Instead, we can just talk about the state's global Trash subset.

We use the tick, ', pronounced "Trash prime", to talk about the trash in the state immediately after the current state.

pred deleteFile(f: File) {
  f not in Trash
  Trash' = f + Trash
  // Obligated to talk about every "var sig" that I do not want to change
  File' = File
}

pred restoreFile(f: File) {
  f in Trash
  Trash' = Trash - f
  // Obligated to talk about every "var sig" that I do not want to change
  File' = File
}

Since Alloy expects there to be an infinite series of possible events modeled by transitions that loop back onto prior states (known as "lasso traces", which will will talk about more next time), we often will want to define a sort of "no-op" predicate where nothing happens between two states.

Here, this looks like:

pred doNothing {
  // Specify that all the "var" sigs don't change
  File' = File
  Trash' = Trash
}

Traces with temporal logic

Now, we can create traces where these 3 events (delete, restore, or do nothing) happen in arbitrary order, without needing to explicitly model an event sig. Instead, we'll use temporal operators: always here says that in every state, one of these three predicates relates the current state and the state immediately following that state.

fact validTraces {
  // With no temporal operator, "emptyStartingTrash" just applied to 
  // the FIRST state
  emptyStartingTrash

  // "always" means this is true in every state
  always (doNothing or (some f: File | restoreFile[f] or deleteFile[f]))
}

Part 1 code: Trash with explicit event predicates

// Model: operating system's Trash
// Explicit/manual event model

sig File {}

sig Trash {
    files : set File, // default w/o: "one" File
                    // instead, pick something else
}

// all possible trashes: empty
pred emptyStartingTrashAll {
  no files
}

// pass a particular trash
pred emptyStartingTrash(t: Trash) {
   no t.files
}

run emptyStartingTrash 

// In this file: modeling time *explicitly* with events
// Context: textbook uses to model time
// Second half: built-in temporal support (Alloy 6)

// Takes in two Trash instances (before and an after)
// and one File instance (the file being deleted)
// t1 is before
// t2 is after
pred deleteFile(f: File, t1, t2: Trash) {
   f not in t1.files
   // Initial attempt
   f in t2.files
   // does not quite work because it ignores the 
   // other contents of t1.files
         // doesn't work: f in t2.files
   // does work: the after state should be specific. 
  // we use set union to make the set exactly grow
  // by the newly-deleted data
  t2.files = t1.files + f
 // f in t2.files
}
// f in t2.files was *underconstrained*: it was not specific
// enough to rule out behaviors we wanted to be 
// impossible

// Rule of thumb: when modeling changes over time,
// we need to think about what should *not* change
// in a given event and constrain that, in addition to 
// what should change 

// in terms of operators: +, -, & 
//              union, difference, intersection
//   are useful in not under-constraining our models

run deleteFile

// Check if our model is consistent with some property
assert noDisappearingFiles {
//   all t1, t2: Trash | all disj f1, f2: File 
     all disj f1, f2: File, t1, t2: Trash |
	deleteFile[f1, t1, t2] and f2 in t1.files
          => f2 in t2.files
}

// Common pattern:
// quantify over what you care about (all, some)
// set up conditions you care about (combined with
// and)
// implies
// thing you expect to be true under those conditions

check noDisappearingFiles // implicit size up to 3

// Restore takes something out of the trash
pred restoreFile(f: File, t1, t2: Trash) {
   f in t1.files

   // t2.files = t1.files - f
   // f not in t2.files
   f not in t1.files
}

run {
   some t1, t2, t3: Trash, f: File |
      deleteFile[f, t1, t2] and restoreFile[f, t2, t3]
}

assert deleteThenRestore {
  all t1, t2, t3: Trash | {
      all f: File | {
         (deleteFile[f, t1, t2] and restoreFile[f, t2, t3])
         => (t1.files = t3.files)
    }
  }
}

// No counterexample, Alloy did not find any VIOLATIONS of the assertion
check deleteThenRestore for 5 but exactly 3 Trash


// Downsides to explicit event model:
// 1. as we add more events, becomes difficult to track
//  what happens when
// 2. visualizer gets harder to understand
// 3. no built in support for "eventually"

Part 2 code: Trash with Alloy 6 temporal logic

var sig File {} // var: set changes over time

var sig Trash in File {}

pred deleteFile(f: File) {
   f not in Trash // this trash is the current moment
   Trash'  = f +Trash   // trash prime, trash tick
                                 // refers to the state immediately
                                 // after the current state
  // simplify: no new files added/perm deleted while
  // this is happening
  File' = File
  // obligated to talk about every var sig or field
}

// the prime ' syntax is used in the textbook, but 
// before it was a keyword

pred restoreFile(f: File) {
   f in Trash
   Trash' = Trash - f
   File' = File
}

pred doNothing {
  File' = File
  Trash' = Trash
}

pred emptyStartingTrash(t: Trash) {
   no t
}

fact validTraces {
    // not invoking time: this applies to the initial state
   emptyStartingTrash[Trash]
   always (doNothing or (some f: File | 
         deleteFile[f] or restoreFile[f]))

}

run { eventually some f: File | restoreFile[f] }