verification - 在 TLA+ PLusCal 中定义运算符不起作用
问题描述
我在 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 的功能。我应该使用什么,运算符或函数?
解决方案
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; *)
====
推荐阅读
- responsive-design - Bootstrap 5 - 在移动设备上更改 FORM 宽度
- c++ - std::string_view rvalue from macro not a constant expression when building on aarch64 using GCC
- java - 将四元数从当前旋转角度旋转一定角度的正确方法是什么?
- azure - Unable to query 'principalName' via azure-cli when authenticated as a Service Principal
- php - Getting radio input from selection in table
- php - Laravel Blade using default variable
- python - Unable to dockerize rails container, while using python
- text - Proper Aggregate Measure of Cosine Similarity? (based on text similarity)
- hadoop - Why Namenode is not coming UP in HDFS on kubernetes
- android - Appium - 遇到内部错误运行命令:错误:无法启动
应用