在 Alloy 中显示反例

Question

也许这是一个愚蠢的问题，但我正在尝试使用 Allow 来测试 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 时，它会打开一个没有实例的 window。

Answer 1

我运行你的模特给你。有一个例子。请注意，它显示 "Due to your theme settings, every atom is hidden. Please click Theme and adjust your settings"。这意味着正在显示一个实例，并且如果它包含任何原子，它们不会显示，因为自定义可视化的主题。在这种情况下，这是因为未连接的整数未显示在默认主题中。您可以通过以不同方式查看实例（任何其他选项 -- Txt、Table、Tree）或更改主题来查看实例。

在 Alloy 中显示反例

show counterexample in Alloy

alloy