The following model is ok, Alloy finds instances.
abstract sig A{}
sig B extends A{}
sig C extends A{}
run {} for 1 but exactly 1 B, exactly 1 C
That makes me understand that the scope is not limited by the top-level signature A, but by its extensions, B and C.
However, I have a large model (no sense posting it here) that can only be satisfied with the scope of 14. With a scope of 13 the analyzer finds no instances.
When I analyze the instance found, using the evaluator to request 'univ', I get a solution that has about 5 atoms of each signature. Only the top-level abstract signatures have 14 atoms.
Am I missing something about scope? Does it affect something else besides the signatures (such as predicates)? Does it behave differently than what I assumed with the toy example?
Why won't my model simulate with a scope of 5?
edit: here is my model if anyone is interested in taking a look. It is the result of model transformation, that's why legibility is an issue http://pastebin.com/17Z00wV4
edit2: the predicate below works. If I run the predicate for 5 but don't specify the other ranges explicitly, it doesn't find instances.
run story3 for 5 but exactly 4 World, exactly 4 kPerson,
exactly 0 kSoftwareTool, exactly 1 kSourceCode,
exactly 1 kDocument, exactly 1 kDiagram, exactly 3 kChange,
exactly 1 kProject, exactly 2 coBranch, exactly 1 coRepository,
exactly 3 modeConfiguration, exactly 2 modeAtomicVersion,
exactly 2 relatorChangeRequest, exactly 0 relatorVerification,
exactly 1 relatorCheckIn, exactly 1 relatorCheckOut,
exactly 2 relatorConfigurationSelection,
exactly 1 relatorModification,
exactly 0 relatorRequestEvaluation, exactly 2 relatorMarkup
this one does not (it's the same predicate, but without the "exactly" keywords
run story3 for 5 but exactly 4 World, 4 kPerson, 1 kSourceCode,
1 kDocument, 1 kDiagram, 3 kChange, 1 kProject, 2 coBranch,
1 coRepository, 3 modeConfiguration, 2 modeAtomicVersion,
2 relatorChangeRequest, 1 relatorCheckIn, 1 relatorCheckOut,
2 relatorConfigurationSelection, 1 relatorModification,
2 relatorMarkup
I was told Alloy would find any possible instances within the defined scope so
run story3 for 5
should work too!
If each of the signature extending another one have a well defined scope, (it is the case for the small exemple you gave, then the the analyzer is "smart enough" to understand that the scope of the top level signature is at least equal to the some of the scopes of the signatures partitionning it.
In the case now you do not give any scopes to specific signatures, I assume that the analyzer won't be able to process the scope of the top signature as detailed bellow, the top level signature hence will have as scope the global one you gave.