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

46 views
Skip to first unread message

Yong Liu

unread,
Feb 19, 2018, 2:20:58 AM2/19/18
to tlaplus
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

=============================================================================

Stephan Merz

unread,
Feb 19, 2018, 2:59:43 AM2/19/18
to tla...@googlegroups.com
"<=>" expects Boolean arguments and denotes equivalence, you want to write "=" instead.

Regards,
Stephan
> --
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
> To post to this group, send email to tla...@googlegroups.com.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.

Yong Liu

unread,
Feb 19, 2018, 12:56:58 PM2/19/18
to tlaplus
Thanks Stephan. After I replace <=> to =, it works.

Regards,
Yong
Reply all
Reply to author
Forward
0 new messages