A run command with growing scopes should stop once an instance is found

[SteveZhangBit]

Here is a minimal test scenario:

sig A {}

run {} for 3..5 A

My question is what is the expected semantic for a scoped command? I expect that the model gradually increases the bound for A to find a solution. This is useful when I don't know the possible minimum bound for a signature.

So I expect that when 3 atoms of A would be satisfiable, the solver returns a solution. However, the actual behavior is it searches for 3, 4, and 5 As.

This is the line of code that I think causes this "issue":
https://github.com/AlloyTools/org.alloytools.alloy/blame/654e00b0338985c85457b246d154a9457c4a3299/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/TranslateAlloyToKodkod.java#L509

[nmacedo]

This feature was never officially documented (as far as I know), so I'm not sure what was the initial intention. But I agree that a run command with growing scopes should stop once an instance is found. That's actually what happens in check commands with growing scopes, it stops at the first counter-example found.

[grayswandyr]

Renamed the issue.
Setting it as a possible enhancement.