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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Thu, 7 Mar 2019 13:48:18 +0100*References*: <d6e69f72-55b3-4b4a-a336-5d54ffcaeb5c@googlegroups.com> <99d16589-6ac4-401a-ad21-a1f4e1e6ff6a@googlegroups.com>

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
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. |

**References**:**[tlaplus] Re: what's possibly wrong with this simple pluscal?***From:*Shiyao MA

- Prev by Date:
**[tlaplus] Re: what's possibly wrong with this simple pluscal?** - Next by Date:
**[tlaplus] Re: Seeking advice about principles of translating TLA+ spec to real code** - Previous by thread:
**[tlaplus] Re: what's possibly wrong with this simple pluscal?** - Next by thread:
**[tlaplus] problems with the command-line tools** - Index(es):