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

[tlaplus] Re: what's possibly wrong with this simple pluscal?



OK. Seems I am messing tla with pcal.

On Thursday, 7 March 2019 15:22:50 UTC+8, Shiyao MA wrote:
The error message is 
pcal.trans Version 1.8 of 16 May 2016

Unrecoverable error:
 -- Expected "end" but found "if"
    line 10, column 18.


---- MODULE manual ----
EXTENDS Integers, TLC

(* --algorithm manual

variables x = 5, a \in BOOLEAN;

define
    (* IsEven(x) == if x % 2 = 0 then TRUE end if; *)
    IsEven(x) == if x % 2 = 0 then TRUE end if; 
end define;

begin
    x := 3;
    a := TRUE;
    (* print IsEven(2); *)
end algorithm; *)

\* BEGIN TRANSLATION
VARIABLES x, a, pc

(* define statement *)
IsEven(x) == TRUE


vars == << x, a, pc >>

Init == (* Global variables *)
        /\ x = 5
        /\ a \in BOOLEAN
        /\ pc = "Lbl_1"

Lbl_1 == /\ pc = "Lbl_1"
         /\ x' = 3
         /\ a' = TRUE
         /\ pc' = "Done"

Next == Lbl_1
           \/ (* Disjunct to prevent deadlock on termination *)
              (pc = "Done" /\ UNCHANGED vars)

Spec == Init /\ [][Next]_vars

Termination == <>(pc = "Done")

\* END TRANSLATION

====

--
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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.