new to TLA: difference between if-then-else and logic or

[Yong Liu <liuy...@xxxxxxxxx>]

Hi all,

I'm new to TLA+.

I tried the HourClock example, and found it will fail after I replace:
HCnxt == hr' = IF hr # 12 THEN hr + 1 ELSE 1
to
HCnxt == \/ hr # 12      /\ hr' = hr + 1
                 \/ hr <=> 12 /\ hr' = 1
I think above statements are equivalent, if not, please kindly let me know the difference.

Below is my HourClock for your reference.

----------------------------- MODULE HourClock -----------------------------

EXTENDS Naturals
VARIABLE hr

HCini == hr \in 1..12

\*HCnxt == hr' = IF hr # 12 THEN hr + 1 ELSE 1

HCnxt == \/ hr # 12   /\ hr' = hr + 1
         \/ hr <=> 12 /\ hr' = 1

HC == HCini /\ [][HCnxt]_hr

-----------------------------------------------------------------------------
THEOREM HC   
 
=============================================================================