如何在合金中运行谓词和断言

Question

我来自 C/C++ 背景，并试图了解谓词/断言是如何在 Alloy 中运行/检查的。 (a) 如果我有多个谓词并且我想同时运行它们，当我运行第一个谓词时，如何确保与另一个谓词中的约束相关的条件保持不变？我只是对如何运行多个谓词感到困惑。 (b) 断言也一样。我必须检查每个断言吗？

感谢您对此的任何反馈。

Answer 1

您可以在“运行”命令中使用任意公式，因此您可以在其中连接任意数量的谓词。这是一个例子：

one sig S {
  x: Int
}

pred gt[n: Int] { S.x > n }
pred lt[n: Int] { S.x < n }

run { gt[2] and lt[4] }

对于断言，我认为你必须一一检查它们，例如，

one sig S {
  x: Int
}

assert plus_1  { plus[S.x, 1] > S.x }
assert minus_1 { minus[S.x, 1] < S.x }

check plus_1
check minus_1
// doesn't compile: check { plus_1 and minus_1 } 

但是，您可以将断言转换为谓词，然后您可以在“检查”命令的主体中从它们形成任意公式，例如，

one sig S {
  x: Int
}

pred plus_1[]  { plus[S.x, 1] > S.x }
pred minus_1[] { minus[S.x, 1] < S.x }

check { plus_1 and minus_1 }