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

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

 Hello,operator definitions appearing in the define' section of a PlusCal algorithm must adhere to TLA+ syntax. Moreover, your definition of IsEven(x)' is incomplete because you don't specify the result if x%2 is different from 0. Finally, x cannot be used as a parameter in a scope where x is already declared as a variable.The following is probably what you intended to write:(* --algorithm manualvariables x = 5, a \in BOOLEAN;define    (* IsEven(z) == IF z % 2 = 0 THEN TRUE ELSE FALSE *)    IsEven(z) == z % 2 = 0 end define;begin    x := 3;    a := TRUE;    (* print IsEven(2); *)end algorithm; *)Regards,StephanOn 7 Mar 2019, at 13:30, Shiyao MA wrote: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 2016Unrecoverable error: -- Expected "end" but found "if"    line 10, column 18.---- MODULE manual ----EXTENDS Integers, TLC(* --algorithm manualvariables 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 TRANSLATIONVARIABLES x, a, pc(* define statement *)IsEven(x) == TRUEvars == << 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]_varsTermination == <>(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. -- 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.