10903

# how to define scope of Int

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 ```

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 :

<li>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</li> <li>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.</li> </ul>