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

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



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.

Andrew

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:

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/40d88f8f-2828-4a7d-9a77-1fee74631382n%40googlegroups.com.