Mutable top-level signatures¶

In the specification of our file sharing app in chapter Behavioral modeling: we’ve seen mutable signature as subsets of static signatures. In Alloy it is also possible to declare mutable top-level signatures. Although this sometimes makes for more natural models, there are some nuances of these signatures that must be taken into consideration.

Declaring top-level signatures¶

In our file sharing model, uploaded files were modelled using a mutable subset of File, the top-level signature that contains the universe of all possible files that can exist in a trace. Instead, we could argue that the universe of files known to the system is exactly the set of uploaded files, and that the value of File itself in each state corresponds to the set of uploaded files. In that case, we could have declared File itself as mutable instead of adding a new mutable subset signature. The signature declarations would then look as follows.

sig Token {}
var sig File {
  var shared : set Token
}
var sig trashed in File {}

There are some important points to note when top-level signatures are used:

The scope of a mutable top-level signature is the maximum number of different atoms it can contain in the full trace, and not the maximum at each different state. For example, with the default scope of 3, we can have at most 3 different uploaded files in each trace. For example, if at some state File contains 3 uploaded files, no more different files can be uploaded (of course, we can delete a file a re-uploaded it again later).
In Alloy all top-level and extension signatures are disjoint. The same is true for mutable top-level and extension signatures: they are always disjoint, even at different points in time, meaning that an atom cannot move from one top-level signature to another one in a state transition. For example, if Token was also mutable, an atom contained in File at some state could never be part of Token in a different state.
When there are mutable top-level signatures the univ is mutable as well, containing, in each state, all atoms contained in all signatures at that state. Similarly, the iden relation also becomes mutable.

Updating the rest of the specification to accommodate this change is not just a matter of replacing uploaded with File. In most formulas that will be the case, but in some formulas the changes are more subtle. As an example of the former case, consider fact init after replacing uploaded with File, that specifies the valid initial states.

fact init {
  // Initially there are no files uploaded nor shared
  no File
  no shared
}

Although this is a correct specification, the second constraint is now redundant. If in the initial state there are no atoms in File it will be impossible for relation shared between files and tokens to have any tuples, so we can can simplify it as follows.

fact init {
  // Initially there are no files uploaded nor shared
  no File
}

Alloy model

Full model for the section

Download and explore the files relevant for the model at this point of the book.

Adding new atoms to the universe¶

In the file sharing example, for most action predicates we get the intended specification by just replacing uploaded by File. As an example, consider action predicate empty, that specifies the action of emptying the trash bin.

pred empty {
  no trashed'              // effect on trashed
  File' = File - trashed   // effect on File
  shared' = shared         // no effect on shared
}

Here, the effect on uploaded was just replaced by the same effect on File.

However, specifying action predicate upload is a bit more tricky, and cannot be updated by simply replacing uploaded by File. In particular, it no longer makes sense to parametrize it by the file that will be uploaded, since that file will not even exist before the action occurs. Instead, we can have a non-parametrized predicate whose effect is to upload any new file. To enforce that signature File will contain a new uploaded file in the post-state we could, for example, use constraint one File' - File or, alternatively, some f : File' | File' = File + f. The latter version is more convenient if we need to refer to the newly created atom in later effects, but that is not the case of upload. The new specification of upload could thus be as follows.

pred upload {
  one File' - File     // effect on File
  trashed' = trashed   // no effect on trashed
  shared' = shared     // no effect on shared
}

The fact that specifies the valid transitions will then look as follows.

fact transitions {
  // The system must only evolve according to the defined actions
  always (
    upload or
    (some f : File | delete[f] or restore[f]) or
    (some f : File, t : Token | share[f, t]) or
    (some t : Token | download[t]) or
    empty or
    stutter
  )
}

Alloy model

Full model for the section

Download and explore the files relevant for the model at this point of the book.

Quantifying over mutable signatures¶

Concerning assertions, again it might not suffice to just replace uploaded by File. In particular, special care is needed with quantifications over mutable signatures. For example, consider assertion restore_undoes_delete.

assert restore_undoes_delete {
  all f : File | always (
    delete[f] and after restore[f] implies
    File'' = File and trashed'' = trashed and shared'' = shared
  )
}
check restore_undoes_delete

This assertion is now trivially true, because the quantification all f : File is outside any temporal operator, and thus only needs to hold in the initial state where File is still empty because no files were yet uploaded, as enforced by fact init. To correctly specify the desired assertion we need to move the quantification inside the always temporal operator, as follows.

assert restore_undoes_delete {
  always all f : File | (
    delete[f] and after restore[f] implies
    File'' = File and trashed'' = trashed and shared'' = shared
  )
}
check restore_undoes_delete

Now, at each state the quantified property must hold for all files that are currently uploaded at that state.

The specification of assertion one_download_per_token used function downloaded shown below, to compute the set of files that were once downloaded with a given token. For similar reasons, its specification no longer makes sense, because the function will now only return the files that are also currently uploaded.

fun downloaded [t : Token] : set File {
  { f : File | once (download[t] and t in f.shared) }
}

As an alternative, for this assertion we can still use the first formulation from the Behavioral modeling chapter that did not use this function.

assert one_download_per_token {
  all t : Token | always (
    download[t] implies
    after always not download[t]
  )
}
check one_download_per_token

Here the quantification all t : Token can still be outside always, because Token is immutable and thus already contains all possible tokens in the initial state. Of course, it could also be moved inside the always because its value is the same in every state.

Alloy model

Full model for the section

Download and explore the files relevant for the model at this point of the book.