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

*From*: Andrew Helwer <andrew.helwer@xxxxxxxxx>*Date*: Sun, 19 May 2024 12:29:08 -0700 (PDT)*References*: <ba43c57b-6688-4908-9c01-23ff03c7bb3an@googlegroups.com>

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:

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

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

**References**:**[tlaplus] Definitions inside and outside of an algorithm and macros***From:*Max Neverov

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