[tlaplus] Re: Where does assert go in Euclid Algorithm of Chapter 4.5

[Samuel Miller <samuel.s.miller@xxxxxxxxx>]

The translator finds an error on the line before the assert, with "};". The while brackets require a semi-colon because it is after a sequence of statements, but the process-level brackets (wrapping the "while") do not.

To properly place the assert, remove the ";" above. Move the assert line inside the procedure-level brackets. Then add a semi-colon to the end of the assert. The below works for me. I always struggle with the syntax, so including a few links at the bottom for reference.

(*--algorithm Euclid {

 variables x \in 1..N, y \in 1..N, x0=x, y0=y;

 { while (x # y) { if (x < y) { y := y - x }

                   else       { x := x - y }

                 };

    assert (x = y) /\ (x = GCD(x0, y0));

    }

}

- Pluscal C-Syntax -- https://lamport.azurewebsites.net/tla/c-manual.pdf (Euclid example, p 7)

- Euclid Writes an Algorithm -- https://lamport.azurewebsites.net/pubs/euclid.pdf

On Tuesday, December 26, 2023 at 9:27:25 AM UTC-5 Linyu Zhu wrote:

Here is my code:

------------------------------- MODULE EUCLID -------------------------------

EXTENDS GCD, Integers,TLC

CONSTANT M,N

ASSUME {M, N} \subseteq Nat \ {0}

(***************************************************************************

--algorithm Euclid {

 variables x \in 1..N, y \in 1..N, x0=x, y0=y;

 { while (x # y) { if (x < y) { y := y - x }

                   else       { x := x - y }

                 };

};

assert (x = y) /\ (x = GCD(x0, y0))

}

***************************************************************************)

Translator reports "Expected "}" but found ";" line 11, column2

Is it a translator bug?

Tool kit version:

This is Version 1.7.1 of 31 December 2020 and includes:

  - SANY Version 2.2 of 20 April 2020

  - TLC Version 2.16 of 31 December 2020

  - PlusCal Version 1.11 of 31 December 2020

  - TLATeX Version 1.0 of 20 September 2017

-- 
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/61b1b68d-b5d9-4d33-896b-f9d46f324d38n%40googlegroups.com.