| 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 manual
variables 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, Stephan On 7 Mar 2019, at 13:30, Shiyao MA < i@xxxxxxxxx> 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 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.
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.
|