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

*From*: Max Neverov <neverov.max@xxxxxxxxx>*Date*: Sun, 19 May 2024 08:54:24 -0700 (PDT)

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.

**Follow-Ups**:**[tlaplus] Re: Definitions inside and outside of an algorithm and macros***From:*Andrew Helwer

- Prev by Date:
**Re: [tlaplus] Statements in TLA** - Next by Date:
**Re: [tlaplus] Statements in TLA** - Previous by thread:
**Re: [tlaplus] Statements in TLA** - Next by thread:
**[tlaplus] Re: Definitions inside and outside of an algorithm and macros** - Index(es):