Maybe it is a silly question, but I am trying to use Allow for testing equivalence of FOL formulas. In the case of counter-models, is there any way to show them? For instance
sig Value {}
pred p [x: Value] {
// ...
}
assert bla {
(all x: Value | p [x]) iff (some x: Value | p [x])
}
// run p for 2 Value
check bla for 5 Value
It says
Executing "Check bla for 5 Value"
Solver=minisat(jni) Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20
16 vars. 5 primary vars. 15 clauses. 1ms.
Counterexample found. Assertion is invalid. 2ms.
But when I click in Counterexample, it opens a window with no instances.
I ran your model for you. There is an instance. Notice that it says "Due to your theme settings, every atom is hidden. Please click Theme and adjust your settings". This means that an instance is being shown, and that if it contains any atoms, they're not shown because of the theme that customizes the visualization. In this case, it's because unconnected integers are not shown in the default theme. You can see the instance either by viewing it in a different way (any of the other options -- Txt, Table, Tree), or by changing the theme.