| In principle, TLC should not see the difference between these ASCII representations because the lexer should map them to the same token. Due to concurrency effects, TLC may report different statistics or counter-examples for subsequent runs that lead to invariant or property violations. (You can force TLC to use a single core using the "How to run?" options in the Model Overview pane.) If you see repeatable discrepancies, we'd be interested in seeing the TLA+ module that causes this effect – feel free to send it by private email.
Regards, Stephan
I haven't found the definition in p.273 of specifying systems. I have looked at pages 344, 348 and 237 (suggested by the index) and non of them seem to mention the ASCII representation of the "less than or equal" operator. Please can you explain the difference in TLC's behavior depending on the version of the operator used? In particular these differ: counter example generated, number of states and diameter of state-space. On Tuesday, 9 January 2018 07:34:30 UTC, Stephan Merz wrote: Hello,
<=, =<, and \leq are different ASCII representations of the same operator: the "numbers" modules (Naturals, Integers, Reals) defines that operator to denote "less than or equal" – see "Specifying Systems", p. 273.
Regards, Stephan
What's the difference between these two operators? I could not find any definition for the former (even though it looks similar to => which is used for logical implication).
I had mistakenly typed <= for less than or equal in the definition of SmallToBig while going through video 4 (Die Hard) of the video lecture series.
The parser and model checkers did not complain: I even got a valid counter-example for the invariant big#4. However, the behaviour of the model checker using '<=' seems to be different. It explores a different number of states, and the state-space has a different diameter.
--
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+u...@googlegroups.com.
To post to this group, send email to tla...@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+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
|