verification - 在 TLA+ PLusCal 中定义运算符不起作用

Question

我在 PlusCal 中的基本代码如下。

---- MODULE flags ----
EXTENDS TLC, Integers
(* --algorithm flags
define
    IsFive(z) == z = 5
end define
begin
IsFive(5)
end algorithm; *)

====

线IsFive(5)在工具箱中突出显示，当我尝试运行模型时，我收到一个错误，即宏 IsFive 未定义。

在类似的注释中，https ://learntla.com/tla/operators/说操作符是函数，然后在接下来的章节中继续定义函数。

假设我需要检查验证参数是否为 5 的功能。我应该使用什么，运算符或函数？

Answer 1

PlusCal 翻译器期望 和 之间的文本begin包含end algorithm对变量的赋值（例如，x := 3），或对 PlusCal 宏（赋值给变量）的调用，使用macro键盘定义。

在您的示例代码中，PlusCal 翻译器没有看到赋值语句，因此它假定 IsFive 是一个宏，然后抱怨。

如果您定义一个变量并使用您的运算符计算算法中变量的值，那么工具箱将能够解析您的代码。

---- MODULE flags ----
EXTENDS TLC, Integers
(* --algorithm flags
variable x;
define
    IsFive(z) == z = 5
end define
begin
x := IsFive(5)
end algorithm; *)
====