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

*From*: Shiyao MA <i@xxxxxxxxx>*Date*: Thu, 7 Mar 2019 04:30:53 -0800 (PST)*References*: <d6e69f72-55b3-4b4a-a336-5d54ffcaeb5c@googlegroups.com>

OK. Seems I am messing tla with pcal.

On Thursday, 7 March 2019 15:22:50 UTC+8, Shiyao MA wrote:

-- On Thursday, 7 March 2019 15:22:50 UTC+8, Shiyao MA wrote:

The error message ispcal.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;beginx := 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.

**Follow-Ups**:**Re: [tlaplus] Re: what's possibly wrong with this simple pluscal?***From:*Stephan Merz

- Prev by Date:
**[tlaplus] How to understand the concept "step simulation"** - Next by Date:
**Re: [tlaplus] Re: what's possibly wrong with this simple pluscal?** - Previous by thread:
**[tlaplus] Re: How to understand the concept "step simulation"** - Next by thread:
**Re: [tlaplus] Re: what's possibly wrong with this simple pluscal?** - Index(es):