Defining an operator in TLA+ PLusCal does not work

Question

My elementary code in PlusCal is as follows.

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

====

Line IsFive(5) is highlighted in the toolbox and when I try to run the model, I get an error that macro IsFive is undefined.

On the similar note, https://learntla.com/tla/operators/ says operator are functions and then proceeds to define functions in next chapters.

Say I need to check a functionality of verifying if argument is five. What should I use, operator or function?

Answer 1

The PlusCal translator expects the text between the begin and end algorithm to contain an assignment of values to variables (e.g., x := 3), or an invocation of a PlusCal macro (that assigns to variables), defined using the macro keyboard.

In your example code, the PlusCal translator doesn't see an assignment statement, so it assumes that IsFive is a macro, and then complains.

If you define a variable and use your operator to calculate the value of the variable in your algorithm, then the toolbox will be able to parse your code.

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