alloy

How to debug Alloy if the outcome is not as expected?

When Alloy says 'No instance found.' How can I look for some more detail to know why the outcome is not as expected?

I am using Alloy Analyzer 6.1.0

My code is,

sig State, Node {}
sig List {
  header: Node ->one State
}
pred test( l: List, n: Node ){
 #l.header = 1 and #n.(l.header) = 1
}
run test for  exactly 2 List, exactly 2 State, exactly 2 Node

My expect is,

my expect

But Alloy's output is,

Executing "Run run$1 for exactly 2 List, exactly 2 State, exactly 2 Node" Solver=sat4j Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=20 Mode=batch 106 vars. 8 primary vars. 195 clauses. 124ms. No instance found. Predicate may be inconsistent. 3ms.

I looked the Parse Tree, but still having no idea why no instance found.

However, if I change the exactly 2 Node to exactly 1 Node, then Alloy says, Instance found. Like this, enter image description here

I do not understand how to explain this difference.

Solution

  • There are mainly two approaches to "debugging" in Alloy.

    I'm going with the most important one first, which is like being a detective: you must look by yourself for constraints that are sufficient to make your model inconsistent:

    For instance, your model can be rewritten as follows:

    sig State, Node {}
sig List {
  header: Node ->one State
}
pred test( l: List, n: Node ){
 one l.header 
 one l.header[n] // can be removed
}
run test for  exactly 2 List, exactly 2 State, exactly 2 Node

    Then you may realize that one l.header[n] isn't useful as the type of header already says that there's exactly one state for every pair of list and node. So you can remove it and see that it is still UNSAT.

    Now, you have essentially 3 constraints: one in the type of header, one in test and the scope specification. The type of header says that every combination of list and node is mapped to a unique state. Due to the scope, it means header should be equal to, up to permutations, { l1->n1->?, l1->n2->?, l2->n1->?, l2->n2->? } (with ? being s1 or s2 for every tuple). Then, in test, you're saying that l (be it l1 or l2) is associated to a single pair of node and state. Bang!

    So we see the issue comes from a combination of 3 constraints.

    If indeed you consider only one node instead, then header will only contain tuples of the shape { l1->n1->?, l2->n1->? }, which will -this time- satisfy test.

    But another way to solve the issue would be to remove test! Or to remove one in the type of header! There are often several ways to solve an inconsistency. It's your knowledge of the domain that will make you favor one solution over another.

    For completeness, there is a second approach which complements the former and is automated, but it's sometimes difficult to interpret. The idea is to ask Alloy to produce a so-called UNSAT core, that is a set of constraints that is sufficient to lead to inconsistency. To do so, you must rely on a SAT solver that can produce such cores, e.g. "Minisat with Unsat Cores" in the Options menu. Then, you run the analysis and, if it's inconsistent as in your example, a Core clickable text will appear that will highlight "suspicious" parts in your model. Depending on options, the computation of the core will be more or less fast and the scope of highlighting will be more or less large.

    In your example, if I use Slow minimization and granularity Expand quantifiers, then Alloy will only highlight one l.header. And indeed, you may relax or remove this constraint to make the model satisfiable. But as you can see from the above discussion, other modifications might work too, and UNSAT core extraction with these options doesn't show them. At the very least, using this technique should by no means prevent you to rely on your own analysis of the situation!