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.