Difference between => and <=>

=> ("if") is an Implication. Here's an example: If the door opens, sound the alarm.
Note that the alarm can still be triggered because of something other than the door opening (e.g. a window opening).

Here's its truth table. Think you are programming an alarm system for a customer. x represents the door opening, y the alarm sounding.

x | y | x => y | Explanation
0 | 0 |   1    | The door doesn't open, the alarm doesn't sound (You don't want the alarm to go off for nothing)
0 | 1 |   1    | The door doesn't open, but the alarm still sounds (e.g. because a window was opened)
1 | 0 |   0    | The door opens, but the alarm doesn't sound (That is not how you want to protect your house)
1 | 1 |   1    | The door opens and the alarm sounds (What else would you have an alarm for)

Let's go to the Equation (<=> or "only if"). This is only true when both options are the same value. This example keeps the alarm but changes it to Only if the door opens, sound the alarm.
Note: This time an opening window should not trigger the alarm, only the door should.

x | y | x => y | Explanation
0 | 0 |   1    | The door doesn't open, the alarm doesn't sound
0 | 1 |   0    | The door doesn't open, the alarm sounds (That's a false positive, that window opening is not what your alarm should cover)
1 | 0 |   0    | The door opens, but the alarm doesn't sound (That is not how you want to protect your house)
1 | 1 |   1    | The door opens and the alarm sounds (What else would you have an alarm for)

This is something often mixed up and written wrongly in specifications (It also conveniently is a legal defense if you know it).

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.

THEOREM TRUE = \A x:  (x \in {1, 2})  =>  (x \in {1, 2, 3})

in contrast to

THEOREM FALSE = \A x:  (x \in {1, 2})  <=> (x \in {1, 2, 3})

which does not hold, because \E x: (x \in {1, 2, 3}) /\ ~ (x \in {1, 2}) (namely x = 3).

The identifier x could represent which room the system is in.

The value of the expression A <=> B is defined for A \in BOOLEAN /\ B \in BOOLEAN. For non-Boolean values of A and B, the meaning of the operator <=> is unspecified by TLA+. With the moderate interpretation of Boolean operators, A <=> B may be non-Boolean for non-Boolean A, B. With the liberal interpretation, A <=> B is Boolean-valued, though the value is unspecified for non-Boolean A, B.

Section 16.1.3 "Interpretations of Boolean Operators" on pages 296--297 and Section 1.1 "Propositional Logic" on pages 9--11 (in particular page 9) from [1] are the most relevant to what the operators <=> and => mean.

[1] Leslie Lamport, "Specifying systems", Addison-Wesley, 2002