Search code examples
logicboolean-logicboolean-operationstla+

Difference between => and <=>


I am learning TLA+ from this great "Learn TLA+" page.

I cannot get the practical difference between => and <=>. I get it in terms of "truth table", but I cannot really grasp it.

Could one provide a practical TLA+ example highlighting the difference between those two?

Related:


Solution

  • Imagine we have a bounded queue q with max size MAX, a reader process that pops messages from the queue , a writer process that adds messages to the queue, and a queue_maxed_flag that is either true or false. Here's four possible invariants:

    • (len(q) = MAX) => queue_maxed_flag means (in addition to other possible things, depending on the spec) that if a writer adds a message when q has MAX-1 messages it must also set the queue_maxed_flag, otherwise the invariant is violated. However, if the reader pops from a maxed queue, it does not need to unset queue_maxed_flag.
    • queue_maxed_flag => (len(q) = MAX) means (in addition to, etc) that if a reader pops a message when q has MAX messages it must also unset the queue_maxed_flag. However, if the writer adds a message when q has MAX-1 messages, it does not need to set queue_maxed_flag.
    • (len(q) = MAX) <=> queue_maxed_flag and queue_maxed_flag <=> (len(q) = MAX) mean the same thing: the prior two invariants both hold. If the writer writes the last message to a queue, it must set the flag, and if the reader reads from a full queue, it must unset the flag.

    So why A <=> B and not A = B? A <=> B is stricter in that it expects both A and B to be booleans. TLC evaluates 5 = 6 as FALSE, but it raises an error on 5 <=> 6.