[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

Hi Andrew,

Thanks for the clarification!

On Sunday, May 19, 2024 at 9:29:08 PM UTC+2 Andrew Helwer wrote:
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.


On 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 --------------------------------

TwiceOutsice(x) == x * 2  

(*--algorithm example
  x = 2,
  m = 3,
  y = 0,
  d = 0,
  res = 0;

  ThriceInside(i) == i * m
end define

macro TwiceMacro(i) begin
  \* localVariable = i not allowed
  res := i * 2;
  i := i * 2;
end macro;

    y := TwiceOutsice(2);
    d := ThriceInside(2);
    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/325f88a6-6a9f-4138-84d5-027ea058d4cfn%40googlegroups.com.