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