Re: [tlaplus] new to TLA: difference between if-then-else and logic or

[Stephan Merz <stepha...@xxxxxxxxx>]

"<=>" expects Boolean arguments and denotes equivalence, you want to write "=" instead.

Regards,
Stephan

> On 19 Feb 2018, at 07:31, Yong Liu <liuy...@xxxxxxxxx> wrote:
> 
> 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   
> 
> =============================================================================
> 
> -- 
> 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...@xxxxxxxxxxxxxxxx.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.