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

Question

我用PlusCal编写的基本代码如下所示。

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

====

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; *)
====