Определение оператора в 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/ говорит, что оператором являются функции, а затем приступает к определению функций в следующих главах.

Скажем, мне нужно проверить функциональность проверки, если аргумент равен пяти.Что я должен использовать, оператор или функцию?

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