如何在alloy中运行谓词和断言

Question

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

感谢您对此的反馈。

Answer 1

您可以在"run"命令中有一个任意的公式，因此您可以在其中连接任意数量的谓词。这里有一个例子：

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 } 

然而，您可以将断言转换为谓词，然后可以在"check"命令的主体中根据它们形成任意公式，例如

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 }