Scopes for sigs constrained by the ordering module

Questions
1

I’ve been looking at the following small Alloy model trying to understand how scopes are chosen for sigs constrained by the ordering module:

open util/ordering[A1]
open util/ordering[A2]

sig A {}

sig A1,A2 extends A {}

run {} for exactly 2 A1,  4 A

This model has only one instance (after symmetry breaking) where A has a scope of 6 in AA6.2. A1 has a scope of 2 and A2 gets a scope of 4. I’m rather baffled about why A2 gets a scope of 4. Giving A2 an exact scope of 2 would make sense to me.

In the following

open util/ordering[A1]
open util/ordering[A2]
open util/ordering[A3]

sig A {}

sig A1,A2,A3 extends A {}

run {} for exactly 3 A1,  4 A

A1 has 3, A2 has 4 and A3 has 4 in the instance. It seems that when a scope is not given for a subsig constrained by the ordering module, the subsig has scope equal to the scope given for the parent sig (explicitly or by a default 'for x`), which increases the scope of the parent sig.

Thanks for any pointers on what the scope computation algorithm is here!

1 Like
2

Hi,

I think this is true for any subsig, not only for those constrained by the ordering module. The ordering makes the scope exact, which triggers a curious cascading effect: A2 has no scope so it gets the same scope as A; A1 and A2 are constrained by ordering so their scope becomes exact; A scope has to grow to 6 to accommodate the exact scope of the subsigs.

Best,
Alcino

1 Like