[tlaplus] Definitions inside and outside of an algorithm and macros

[Max Neverov <neverov.max@xxxxxxxxx>]

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

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ba43c57b-6688-4908-9c01-23ff03c7bb3an%40googlegroups.com.