I'm using Alloy 4.2 to define the scope of Int using the 'for ... but...' syntax, however it seems
that it is ignoring my request. For example, given the following simple model:
sig A {
y : seq A
}
run { some a : A | #(a.y) = 4} for 3 but 4 Int
run { some a : A | #(a.y) = 4} for 4 Int, 3 A
the first run finds no instance while the second finds an instance. As far as I understand these
two commands are equivalent (unless there is some hidden signature whose scope is deduced automatically).
Could someone shed light on this behavior?
Those two run commands would be equivalent under the assumption that the atoms used to "index" the A-atoms of the sequence y are typed by the signature Int.
Though this assumption seems legit enough, it is not the case, as the index of sequences is typed by the signature "seq/Int".
Increasing the scope of Int will thus have no effect on the maximal length of the sequence.
To accomplish what you intend to do, you can assign a scope to the "sequence itself".
This is done as follows :
run { some a : A | #(a.y) = 4} for 3 but 4 seq
The answer and other information about sequences can be found at this address :
http://alloy.mit.edu/alloy/documentation/quickguide/seq.html
EDIT: (more readable than in comments)
Note that
1.run { some a : A | #(a.y) = 4} for 4
works, and
2.run { some a : A | #(a.y) = 4} for 3
doesn't work.
Now the interesting thing is that
3.run { some a : A | #(a.y) = 4}
works , even if the default scope is known to be 3.
From those experimentation we can conclude that :
- 1 and 2 shows us that the fact instances are found or no, does not depend on the scope you assign to the signature Int
- 3 makes me guess that the Analyzer is "smart enough" to adapt the scope of seq/Int given the predicate you are running if you do not EXPLICITLY define a global scope.
