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