"New" results in 'there are no more satisfying instances', but re-executing nets more examples

[eoliphan]

Hi, new to Alloy and working through the "Formal Design with Alloy 6" online book. I'm running 6.1.0 on an M1 Mac

So for a simple spec like

sig Object {}
sig File in Object {}
sig Dir in Object {}

run example {}

I get the instance found message, click on that and see the visualization. However clicking New seems to always pop the "There are no more satisfying instances.." dialog, but i can in fact just rerun it to see more. Is this the expected behavior?

[grayswandyr]

Hi, the expected behavior is as follows: if you run example and then immediately open the Visualizer, clicking New over and over again will yield lots of instances until you get the said dialog (and you decide to close the Visualizer). THEN, if you re-run example (meaning clicking again on the Execute button), this whole process is reset and you start again from the first instance found. If this is not what you observe, then there is an issue.

[eoliphan]

Hi, that's what I thought, so i think there may be an issue. In the above example, I never get new instances when I click "New", I always get the dialog on the first click.

I've attached a screen shot with stats from the run, etc. I execute, open up the instance, hit "New" and get the dialog

[eoliphan]

Hi, I also tried this example:

abstract sig Object {}

sig File extends Object {}

sig Dir extends Object {
  entries : set Entry
}

one sig Root extends Dir {}

sig Entry {
  name : one Name,
  object : one Object
}

sig Name {}

Same thing happens when I hit "New". Since this is a static/structural model, I also installed Alloy 5 to see what would happen. 'Next' works as expected in Alloy 5. One thing I noticed was a difference in the "Executing..." output. I got this for Alloy 6:

Executing "Run Default for 4 but 4 int, 4 seq expect 1"
   Solver=sat4j Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=OFF Mode=parallel
   0 vars. 0 primary vars. 372ms.
   . found. Predicate is consistent, as expected. 45ms.

And this for Alloy 5:

Executing "Run Default for 4 but 4 int, 4 seq expect 1"
   Solver=sat4j Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=OFF
   222 vars. 62 primary vars. 305 clauses. 112ms.
   . found. Predicate is consistent, as expected. 24ms.

Not sure if the "0" for vars, etc in version 6 is part of the problem

[grayswandyr]

OK got it: this is because the Decompose strategy is set to parallel. In that case, you're asking for Alloy to decompose the problem, which features many configurations (ways to populate the static sigs), into all possible subproblems with a fixed configuration; and then to run example on every such fixed configuration and stop as soon as one instance is found (and trash all other ongoing runs (on other fixed configurations)). For this reason, there's indeed no other instance in the sense that the popup is about a subproblem with a fixed configuration, not the "general" problem you originally wrote. To fix this, please set the mode to batch (this is the "historical" way of working for Alloy).

So, this is not a bug, but I agree we should find a way to be more explicit about this, because one can easily forget that the mode has been set to parallel. @nmacedo

[eoliphan]

Ah that makes total sense, I should have included that output in my original post. Thanks!