Reputation: 211
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?
Upvotes: 2
Views: 363
Reputation: 1
I was curious about this as well, so I looked at the source code. It turns out that the default scope for seq/Int
is just hard coded as 4; it's also limited to the maximum value representable in two's complement for a given bitwidth -- the bitwidth is the scope of Int
, whose default value is also 4, unlike the default scope of signatures, which is 3.
/**
* The maximum sequence length; always between 0 and (2^(bitwidth-1))-1.
*/
private int maxseq = 4;
Upvotes: 0
Reputation: 4171
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 :
Upvotes: 5