<=, =<, 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.
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...@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