search

AlloyTools / org.alloytools.alloy

Alloy is a language for describing structures and a tool for exploring them. It has been used in a wide range of applications from finding holes in security mechanisms to designing telephone switching networks. This repository contains the code for the tool.
Other
712 stars 123 forks source link

Duplicate models when enumerating #142

Open edmcman opened 3 years ago

edmcman commented 3 years ago

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 commented 3 years ago

Can you provide an example where this is happening?

edmcman commented 3 years ago

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

edmcman commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

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

pkriens commented 2 years ago

@nmacedo what do we do with this issue?

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

grayswandyr commented 1 year ago

ping @nmacedo @pkriens

nmacedo commented 1 year ago

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).

DanieleMarchei commented 3 months ago

I am having this problem as well. Here is a quick non-trivial example that enumerates all binary trees with 3 nodes and 2 leaves

sig Node{
    parent: set Node
}

fun Leaves: set Node {
    Node - Node.parent
}

fun Root: set Node {
    Node - Node.~parent
}

fun NonRoot: set Node {
    Node - Root
}

fact "All non-root nodes have only one parent"{
    all l:NonRoot | one l.parent
}

fact "No cycles"{
    no n:Node | n in n.^parent
}

fact "Only one root"{
    #Root = 1
}

fact "Two children or no children" {
    all n:Node | #n.~parent = 2 || #n.~parent = 0
}

run {#Leaves = 2} for exactly 3 Node

Trivially the answer should be 1, but Alloy returns 2 isomorphic trees.

image