On Sunday, February 18, 2018 at 11:59:43 PM UTC-8, Stephan Merz wrote:
"<=>" expects Boolean arguments and denotes equivalence, you want to write "=" instead.
Regards,
Stephan
> On 19 Feb 2018, at 07:31, Yong Liu <liu...@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...@googlegroups.com.
> 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.