| Hello, PlusCal expressions are the same as those in TLA+, and if your question is if the formulas in the definitions below: Reverse(s) == [i \in 1 .. Len(s) |-> s[Len(s)-i+1] IsMirrorSeq(seq) == \E s \in Seq(Nat) : seq = s \o Reverse(s) are well-formed TLA+ formulas, the answer is yes. Tools for TLA+ impose different restrictions on what kind of formulas they can handle. For example, TLC will not be able to evaluate the formula IsMirrorSeq(<<0,1,1,0>>) out of the box, but you can override the Seq operator to impose a bound on the length of sequences. More information on how to do this is available in the Help pages. Hope this helps, 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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/9B4878A6-3141-4D83-AA54-DF2762A26412%40gmail.com. |