Scopes for sigs constrained by the ordering module

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!