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
}

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

// Model used by the textbook
// But in the textbook: t, t'  (written as t prime)
// WARNING: manually change the prime t2 instead of t'
pred deleteFile(f: File, t1, t2: Trash) {
  f not in t1.files // You can't delete something already in the trash, t1 is "before"
  // 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
}

// Restore should move a file *out* of the trash
pred restoreFile(f: File, t1, t2: Trash) {
  f not in t2.files // redundant with the final line
  f in t1.files
  t2.files = t1.files - f
}

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

// Run this to see examples
// Make it a pred, run that pred
// It's perfectly fine for Alloy to find instances of the predicate that do not 
// delete then restore any file
run { 
  some t1, t2, t3: Trash, f: File | {
     deleteFile[f, t1, t2] and restoreFile[f, t2, t3]
  } 
} for 3 but exactly 3 Trash

// Assert then check this to actually search for counterexamples up to the scope
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)
  }  
}

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

Part 2 code: Trash with Alloy 6 temporal logic

// Model: using temporal Alloy
// Just define as a signature "sig X": same set in every state in the trace
// "var sig X": this can change throughout the trace
var sig File {}

// If I kept this model: 
// sig Trash {
//  files: set File
// }
// This would allow multiple trashes in a given state
// "in" lets us talk about non-mutually-exclusive subsets
var sig Trash in File {}


// With a variable signature, non-temporal pred/facts now refer to the starting state
// of that signature
pred emptyStartingTrash {
  no Trash // the first moment/state
  // always no Trash  : uninteresting world where trash is always empty
}


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
  //f not in Trash'
  Trash' = Trash - f
  // Obligated to talk about every "var sig" that I do not want to change
  File' = File
}

pred doNothing {
  // All the "var" sigs, don't change
  File' = File
  Trash' = Trash
}

fact validTraces {
  emptyStartingTrash
  always (doNothing or (some f: File | restoreFile[f] or deleteFile[f]))
}

assert restoreComesAfterDelete {
  // A restored file has to have been previously deleted
  always (all f: File | restoreFile[f] => once deleteFile[f])
}

// As expected, this does not have a counterexample
check restoreComesAfterDelete

assert deletedFilesGetRestored {
  // All deleted files get restored: should have a counterexample
  always (all f: File | deleteFile[f] => eventually restoreFile[f])
}

// As expected, this DOES have a counterexample: in a trace, we can have
// a file be deleted, then have all "noNothing" steps
check deletedFilesGetRestored

// Now: we want to check deleting then restoring a file

// Before we assert, let's just see some examples with run

run {
  some disj f1, f2: File | {
    (deleteFile[f1] and after restoreFile[f1])
    // Need the eventually here because we can't delete two files in one step
    eventually (deleteFile[f2] and after restoreFile[f2])
  }
} for 5

// Now, go from just examples to an actual assertion that we can check
assert deleteThenRestore {
  always {
    all f: File |
      (deleteFile[f] and after restoreFile[f]) =>
      // The trash two steps in the future should be equal to the current trash
      { 
        Trash'' = Trash
        File'' = File
      }
  }
}

check deleteThenRestore

// tangent about scope
//   no Trash // "Trash" means the starting state
//   always { no Trash and no Trash' } // looks at every step, and its next step
//   eventually { no Trash } // look at every step, stops when it finds one  

Part 3 code: Counter example

one sig Counter {
  var counter: one Int
}

run {
  Counter.counter = 0 // Not temporal: starting state
  // Is temporal, applying to every state
  // Can't use +: 1 + 1 = {1}
   // Other option: either reset
   //  OR: doNothing
  always {
     (Counter.counter' = add[Counter.counter, 1])
     -- or (Counter.counter'  = Counter.counter )
     or (Counter.counter = 3 and Counter.counter' = 0)
  }
} for 3 Int

Correction from class: to implement the student suggest to reset to 0, I wrote (Counter.counter = 3 => Counter.counter' = 0) instead of the correct (Counter.counter = 3 and Counter.counter' = 0). The => does not work as I wanted it to, because the implication is true wheever the counter is not 3, allowing a sort of back-door into a "doNothing" transition in that case as well.