Duplicate models when enumerating

[edmcman]

I am using Alloy to enumerate models, and it is returning the same model more than once. That is, if I write the models to XML files, the resulting files are identical. Is this a bug?

It's easy for me to work around this behavior, but I am a little surprised by it.

[nmacedo]

Can you provide an example where this is happening?

[edmcman]

I'll work on minimizing this to a small example that I can share.

[edmcman]

So the following Alloy program causes the problem, but I couldn't trigger the problem from the GUI interface:

sig c {}
sig m extends c {}
pred features {}
run features

These are the instances that get returned when iterating over the answers:

---INSTANCE---
integers={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
univ={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
Int={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
seq/Int={0, 1, 2, 3}
String={}
none={}
this/m={}
this/c={}

---INSTANCE---
integers={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
univ={m$0, -8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
Int={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
seq/Int={0, 1, 2, 3}
String={}
none={}
this/m={m$0}
this/c={m$0}

---INSTANCE---
integers={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
univ={m$0, c$0, -8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
Int={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
seq/Int={0, 1, 2, 3}
String={}
none={}
this/m={m$0}
this/c={m$0, c$0}

---INSTANCE---
integers={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
univ={m$0, m$1, -8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
Int={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
seq/Int={0, 1, 2, 3}
String={}
none={}
this/m={m$0, m$1}
this/c={m$0, m$1}

---INSTANCE---
integers={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
univ={c$0, -8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
Int={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
seq/Int={0, 1, 2, 3}
String={}
none={}
this/m={}
this/c={c$0}

---INSTANCE---
integers={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
univ={m$0, -8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
Int={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
seq/Int={0, 1, 2, 3}
String={}
none={}
this/m={m$0}
this/c={m$0}

I'll work on minimizing and sharing the offending Scala program.

[nmacedo]

I see, that happens because that problem is trivially satisfiable, Alloy doesn't even launch the underlying solver where symmetry breaking is implemented, it just iterates over all possible assignments of atoms. (Without going into details, internally those instances are not the same, they have different atoms assigned, but Alloy has a renaming procedure to paint atoms in a more friendly way that has tricky results when symmetry breaking is not performed.)

[edmcman]

This is also happening in a fairly non-trivial model. This is just the program that that reduced down to. Is there an easy trick to ensure the solver will be used (to prevent the minimizer from getting rid of too much)?

[nmacedo]

Ok, that's stranger since models quickly become non-trivial. The easiest way to identify a trivial execution is that they always report "0 vars" in the log.

[edmcman]

I reminimized to a non-trivial model, but the result was only slightly different:

sig a{b : c} sig d {}
sig c extends d {}
pred features {}
run features

Debug: Generating facts...                                                                                                                                                                                                                                                                                                                   [40/1780]

Debug: Simplifying the bounds...

Debug: Generating the solution...

127 vars
---INSTANCE---
integers={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
univ={a$0, a$1, c$0, c$1, c$2, -8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
Int={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
seq/Int={0, 1, 2, 3}
String={}
none={}
this/a={a$0, a$1}
this/a<:b={a$0->c$1, a$1->c$0}
this/c={c$0, c$1, c$2}
this/d={c$0, c$1, c$2}

---INSTANCE---
integers={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
univ={a$0, c$0, c$1, -8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
Int={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
seq/Int={0, 1, 2, 3}
String={}
none={}
this/a={a$0}
this/a<:b={a$0->c$0}
this/c={c$0, c$1}
this/d={c$0, c$1}

---INSTANCE---
integers={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
univ={a$0, d$0, c$0, c$1, -8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
Int={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
seq/Int={0, 1, 2, 3}
String={}
none={}
this/a={a$0}
this/a<:b={a$0->c$0}
this/c={c$0, c$1}
this/d={d$0, c$0, c$1}

---INSTANCE---
integers={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
univ={a$0, c$0, c$1, c$2, -8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
Int={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
seq/Int={0, 1, 2, 3}
String={}
none={}
this/a={a$0}
this/a<:b={a$0->c$1}
this/c={c$0, c$1, c$2}
this/d={c$0, c$1, c$2}

---INSTANCE---
integers={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
univ={a$0, a$1, c$0, c$1, -8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
Int={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
seq/Int={0, 1, 2, 3}
String={}
none={}
this/a={a$0, a$1}
this/a<:b={a$0->c$1, a$1->c$0}
this/c={c$0, c$1}
this/d={c$0, c$1}

---INSTANCE---
integers={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
univ={a$0, a$1, d$0, c$0, c$1, -8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
Int={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
seq/Int={0, 1, 2, 3}
String={}
none={}
this/a={a$0, a$1}
this/a<:b={a$0->c$1, a$1->c$0}
this/c={c$0, c$1}
this/d={d$0, c$0, c$1}

---INSTANCE---
integers={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
univ={a$0, a$1, c$0, c$1, c$2, -8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
Int={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
seq/Int={0, 1, 2, 3}
String={}
none={}
this/a={a$0, a$1}
this/a<:b={a$0->c$2, a$1->c$1}
this/c={c$0, c$1, c$2}
this/d={c$0, c$1, c$2}

---INSTANCE---
integers={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
univ={a$0, a$1, c$0, c$1, -8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
Int={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}
seq/Int={0, 1, 2, 3}
String={}
none={}
this/a={a$0, a$1}
this/a<:b={a$0->c$1, a$1->c$0}
this/c={c$0, c$1}
this/d={c$0, c$1}

REPEAT

[edmcman]

I just added a full reproducer for this here: https://github.com/edmcman/alloy-issue142

[pkriens]

@nmacedo what do we do with this issue?

(I also noticed that using the API returned a lot of identical solutions)

[grayswandyr]

ping @nmacedo @pkriens

[nmacedo]

I confirm that this is still an issue, but I still haven't been able to fix it. It seems to have something to do with how the remainder of a non-abstract signature with sub-signatures is encoded. Here's an even smaller example that just returns 2 isomorphic solutions:

sig A {}
sig B extends A {}
run {some A-B and some B} for 2

This issue was already present in previous releases (at least Alloy 5).