Re: [tlaplus] TLC bug or TLA+ subtlety?

[Alexander Bakst <alexander.bakst@xxxxxxxxx>]

I’m no TLA+/TLC expert, but I think in the second version, since the second conjunct must be parsed as (y' = x) \/ x’, y’ could be anything (which would satisfy the  since there is no type invariant. In the first version, y’ must be TRUE or FALSE. So it seems there is a semantic difference.

—Alexander

> On Mar 6, 2022, at 10:09 AM, Hillel Wayne <hwayne@xxxxxxxxx> wrote:
> 
> Take the following spec:
> 
> VARIABLES x, y
> 
> vars == <<x, y>>
> 
> Init ==
>   /\ x = FALSE
>   /\ y = FALSE
> 
> Next ==
>   /\ x' \in BOOLEAN
>   /\ y' = (x \/ x')
> 
> Spec == /\ Init /\ [][Next]_vars
> 
> This checks with 7 states generated. Now remove the parenthesis in Next, giving
> 
> Next ==
>   /\ x' \in BOOLEAN
>   /\ y' = x \/ x'
> 
> This now fails, with a not fully specified successor state:
> 
> State 2: <Next line 11, col 3 to line 12, col 17 of module problem>
> /\ x = TRUE
> /\ y = null
> 
> This seems to me like a bug with TLC, but I wanted to check if the two Nexts aren't actually different semantically, and if so, what makes them different.
> 
> H
> 
> -- 
> 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+unsubscribe@xxxxxxxxxxxxxxxx.
> To view this discussion on the web visit https://urldefense.proofpoint.com/v2/url?u=https-3A__groups.google.com_d_msgid_tlaplus_b2139e63-2D9e12-2Df82c-2D4935-2D2077a148f7ef-2540gmail.com&d=DwIFaQ&c=-35OiAkTchMrZOngvJPOeA&r=K2l4mPc1D0iv68sbdBufTMtzoJU_1KNLlayaL2SDXyM&m=8LYpsEoab1BwkFSb0asQPySqAcjrT4e8LOpWxVsSXn6o2ItRMoDUKXXH57UBZe1-&s=WBDXH0D7duJXGwd7L__dZJIR6RymR5fEaJSyT6TmLm8&e= .

-- 
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/690ABB47-97F4-43D7-819F-E1ACFDEF37BB%40gmail.com.