如何在合金中运行谓词和断言-Java 学习之路

我来自C / C背景，并试图了解如何在Alloy中运行/检查谓词/断言 . （a）如果我有多个谓词，并且我想运行它们，当我运行第一个谓词时，如何确保与其他谓词中的约束相关的条件保持静态？我很困惑你如何运行多个谓词 . （b）断言也是如此 . 我是否必须检查每个断言？

感谢您的任何反馈 .

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 }

回复于 2024-04-26T19:35:37+08:00

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

1 回答

相关问题