显示合金中的反例

Question

也许这是一个愚蠢的问题，但是我正在尝试使用允许来测试FOL公式的等效性。对于反模型，有什么方法可以显示它们吗？例如

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

说

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.

但是当我单击Counterexample时，它将打开一个没有实例的窗口。

Answer 1

我为您运行了模型。有一个实例。请注意，它说“由于主题设置，每个原子都被隐藏了。请单击主题并调整设置”。这意味着正在显示一个实例，并且如果它包含任何原子，则由于自定义可视化的主题而不会显示它们。在这种情况下，这是因为默认主题中未显示未连接的整数。您可以通过以其他方式查看实例（其他任何选项-Txt，表格，树）或更改主题来查看实例。