Yes, it is mostly a stylistic difference. Generally speaking I put definitions needed for the algorithm to function inside the algorithm, while definitions about the algorithm (like to show that it's correct) I put outside the algorithm.AndrewOn Sunday, May 19, 2024 at 11:54:24 AM UTC-4 Max Neverov wrote:Hi everyone,
I have a beginner's question: What is the fundamental difference between definitions outside and inside an algorithm, and macros?
My interpretation is as follows:
- Definitions outside an algorithm are plain TLA+ operators that cannot: a) Modify arguments b) Reference the algorithm variables
- Definitions inside an algorithm are also TLA+ operators that cannot modify arguments but can reference the algorithm variables, although they cannot change them.
- Macros can change arguments and reference and change the algorithm variables.
My understanding is that apart from what I mentioned, it is a matter of preference which to use. Is this correct?
Please check the module below:
-------------------------------- MODULE tmp --------------------------------
EXTENDS Integers, TLC
TwiceOutsice(x) == x * 2
(*--algorithm example
variables
x = 2,
m = 3,
y = 0,
d = 0,
res = 0;
define
ThriceInside(i) == i * m
end define
macro TwiceMacro(i) begin
\* localVariable = i not allowed
res := i * 2;
i := i * 2;
end macro;
begin
y := TwiceOutsice(2);
d := ThriceInside(2);
TwiceMacro(x);
assert y = 4;
assert d = 6;
assert res = 4;
assert x = res;
end algorithm; *)
====