Commands in detail¶
Commands are an essential feature of an Alloy model, since they are what
triggers the automatic analyses of our model by the Analyzer. There are two
types of commands in Alloy: run commands search for instances that satisfy
certain constraints, while check commands search for
counter-examples that violate assertions. Commands also
include the scope of the analyses, which determines the maximum size of the
signatures and of the universe of discourse. In the Structural modeling chapter we have already seen the fundamentals of command
declaration. This chapter explores commands in more detail.
Alternative command syntaxes¶
Both run and check commands can take two different syntaxes. In the first commands have an optional label and a constraint to be enforced/checked
between braces. Between the braces any arbitrary constraint can be written. In the Structural modeling chapter we have defined run commands of this shape, but this could
also be done for check commands. For instance, below is a
check command equivalent to the one defined in the Structural modeling chapter to check that the file system has no partitions, given as a contraint in the command rather than defined in an assertion.
check no_partitions {
all o : Object | reachable[o]
} for 6
In the second alternative syntax, a command cannot be labelled and just calls a re-usable formula defined
elsewhere. For check commands we’ve already seen in the Structural modeling chapter
how that can be done through the definition of assertions; the
check command will then search for counter-examples that violate that
assertion. For run commands, they can be instructed to generate
instances for which a certain predicate holds. An advantage of these
versions is that they ease the definition of multiple commands for the same
property with different scopes. For instance, let’s say that we want to explore
instances that have a file hierarchy of at least depth 2 but with different
scopes for File. We could do something like the following.
pred depth2 {
some Root.entries.object.entries.object
}
run depth2 for 4 but 0 File
run depth2 for 4 but 1 File
run depth2 for 4 but 2 File
An interesting feature of this kind of commands is that, if you run a
predicate with parameters, they will be automatically quantified and show an
instance for which there is some atom that makes the predicate true. For
instance, let us define a predicate that tests whether a directory is empty, and
then ask for instances where there is some empty directory.
pred empty_dir [d : Dir] {
no d.entries
}
run empty_dir for 3
This will result in instances such as the one below. Notice that there is now a
subset $empty_dir_d in the instances, identifying the quantified
variable that made predicate empty_dir true. This is because the
Analyzer performs a process called Skolemization whenever outermost
existential quantifications occur in run commands (or universal
quantifications for check commands), creating additional free relations to represent the quantified variables. This improves the
efficiency of the analysis procedures, and as a side-effect such relations are
now also part of the generated instance and can be depicted.
Although less common, run commands can also call a function rather than a predicate. In that case Alloy will search for input variables for which the function is well defined (i.e., it returns a value within its return type).
Note that once you specify a constraint in the command, you are no longer calling an assertion or predicate and just labelling the command. Since commands can have the same label as a predicate name, this can sometime lead to confusions. For instance, the command below is not really checking assertion no_partitions, but instead the empty constraint within brackets (which is equivalent to true) and obviously never finds any counter-example, possibly leading the distracted user to a false sense of confidence.
check no_partitions {}
Controlling scopes¶
When the Analyzer is launched, a non-negative scope must be assigned to every signature of the model that determines the maximum number of atoms for that signature. These scopes are declared in the analysis commands.
The overall scope of a command is specified with the keyword for which
is applied to all top-level signatures. If omitted, a default overall scope of 3
is used. Since overall scopes apply only to top-level signatures, they may have
some unintended results when the signature hierarchy becomes more complex, in
particular when singleton signatures are introduced and consume part of the
scope of a top-level signature. For instance, in our running example, a command
with a overall scope of 3 like the one below will never generate instances with
3 files. This is because the scope for Object is 3, but one of those
atoms is the Root, so only 2 atoms are free to become files or non-root
directories.
run scope_3 {} for 3
After the overall scope, we can assign additional scopes to specific top-level
and extension sub-signatures that override the overall scope (you cannot assign
scopes to subset signatures). These additional scopes are declared after the
overall scope with a keyword but and separated by commas. For instance,
the following command overrides the overall scope for signature Name.
run names_2 {} for 3 but 2 Name
If you declare a scope for a specific signature that conflicts with its
multiplicity constraint, you’ll get an error. Namely, one signatures
must have scope 1, lone signatures scope less than or equal to 1, and
some signatures greater than 0. Also, you can never declare a scope for
an enumeration signature.
In general, assigning a specific scope to a signature does not affect the scope
of its parent nor its siblings. There are however exceptions, namely when specific scopes are assigned to the extensions of a signature. If the extensions have exact scopes (if they are singleton signatures or, as will be explained later, have an exact scope defined in a command) than the scope of the parent signature is automatically increased so be at least the sum of the scopes of the extensions. If the parent signature is abstract and does not have a specified scope then the overall scope will also be automatically overrided to be the sum of the specified scopes of the extensions (even if these scopes are not exact). For example, in the following command, the scope of
Object is actually increased from the overall specified scope of 3 up to 6.
run files_3_dirs_3 {} for 3 but 3 Dir, 3 File
Note that this second case only happens if all extensions signatures are assigned a specific scope.
Moreover, there is another corner case implemented in calculating the scope of
abstract signatures: if all extension signatures are assigned a specific scope except
one, then that one gets the scope remaining from the abstract parent signature,
which is not increased. This may have unexpected consequences. For instance, the
following command yields no instance, because there is a single extension signature of
Object without a specific scope assigned, namely File, so it gets what
remains of the scope on Object minus the scope on Dir, which is
0.
run dirs_3 { some File } for 3 but 3 Dir
The actual scopes being used by the Analyzer can be consulted in the information reported by the Analyzer. For instance, for the two commands above, the following information would be reported.
More information about how these scopes were calculated is provided if the logging verbosity is increased through menu option .
If you assign a specific scope for every top-level signature of the model, you can actually omit the overall scope; otherwise, an error is thrown. For instance, the following command is valid in our running example.
run no_overall {} for 3 Object, 2 Name, 2 Entry
All scopes considered until now impose an upper-bound on the number of atoms.
Specific signature scopes can also be marked with keyword exactly,
which forces them to contain exactly that amount of atoms. For instance, the
following command guarantees that there exist exactly 2 files in every instance.
run files_exact2 {} for 3 but exactly 2 File
Documenting expected outcomes¶
A complex model often contains several run and check commands.
Sometimes we want to encode negative run commands to show that a certain
class of instances is disallowed, or invalid check commands to register
some known issues. We could use comments to annotate which is the case, but
Alloy allows the user to register what is the expected outcome of a command
using a keyword expect after the scope declaration. The expectation is
that the command is either satisfiable (1) or unsatisfiable (0). A command is
satisfiable when it is able to generate an instance. So a run command that
yields instances is satisfiable, and a valid check command that finds no
counter-examples is unsatisfiable. When executing such commands, the Analyzer
will inform the user whether the result was the expected.
Let us recall the file system example developed in the
Structural modeling chapter. Let us say that, for demonstration purposes we want
to be able execute the invalid version of the no_partitions assertion
that we encountered when the incorrect fact no_self_containment was
enforced rather than the stronger, fixed no_indirect_containment. This
would require those constraints to no longer be enforced as a fact (which would
apply to all commands), but as a predicate that is only enforced in the
appropriate command. Likewise, we won’t be able to use a single assert
since we now have two distinct properties to check. A possibility is to encode
them as follows.
pred no_self_containment {
// Directories cannot contain themselves
all d : Dir | d not in d.entries.object
}
pred no_indirect_containment {
// Directories cannot contain themselves directly or indirectly
all d : Dir | d not in descendants[d]
}
pred no_partitions {
// Every object is reachable from the root
all o : Object | reachable[o]
}
Then we can call the appropriate restriction as a premise to checking
no_partitions. This would be done as follows.
check bad_containment {
no_self_containment implies no_partitions
} for 6 expect 1
check good_containment {
no_indirect_containment implies no_partitions
} for 6 expect 0
The first command is expected to generate a counter-example, but not the second one, as stated by the expected outcome. After execution, the Analyzer would report the results as follows.
Recall, however, that once no_self_containment becomes a predicate, it is no longer enforced in any command. For instance, to generate valid file systems without any additional constraint, one would have to adapt the example run command as follows.
run example { no_self_containment }
Alloy model
Download and explore the files relevant for the model at this point of the book.
Further reading
run commands can be used to encode unit tests for our specification.
Learn how to write commands of that kind.