With Alloy, you can automatically verify (up to a specified scope)
or falsify (with a counterexample) an assert statement,
by using a check command.
check name-of-assert for integer
The integer defines the scope -- the maximum size of each set in the model that will be considered. Specifically, it is the maximum size of the top-level signatures (sets). If there is any solution in that scope or less, Alloy is guaranteed to find it. Thus, we say Alloy is 'complete up to scope'.
For example, the statement
check acyclic for 5
checks the acyclic assertion, and tells Alloy to only examine cases where there are at most 5 top level sigs/sets.
Larger scopes take longer to solve, and often result in more complicated examples. Thus it is good practice to reduce the scope as low as it can go but still get a solution, before trying to visualize solutions.
You can refine you definition of scope with the
but keyword. For example:
check acyclic for 5 but 1 fileSystem, 7 FSObject
The but command lets you specify exceptions to the main scope. In this case, Alloy will only examine 1 file system, up to 7 file system objects, and up to 5 of any other set.