Equivalent expressions
Use <=> to check whether two expressions are equivalent.
Blog¶
MECE Principle (mutually exclusive and collectively exhaustive)
In Alloy, it is very handy to check whether MECE establishes or not.
Substitutable Syntax
|, { } and ( ) when they are substitutable and when not.
Assertion and Counterexample
List the truth table of facts and assertion corresponding to whether counterexample found or not.
It is commonly noted that when there is no counterexample, it may be because of scope too small. However, not so commonly noted, it may be because of the facts are False.
Whenever the facts are False, no matter what assertion it is, there would be no counterexample found. See sample code #2 and #3 below.