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!