Per page 271 in Specifying Systems the \/ operator has precedence 3-3 and the = operator has precedence 5-5, so the = binds more tightly to the _expression_ and it is parsed ((y = x) \/ x').
On Sunday, March 6, 2022 at 3:10:48 PM UTC-5 Markus Alexander Kuppe wrote:
----- MODULE Foo -----
VARIABLES x, y
A ==
/\ x' \in BOOLEAN
/\ y' = x \/ x'
B ==
/\ x' \in BOOLEAN
/\ \/ y' = x
\/ x'
THEOREM A <=> B BY DEF A, B
=================
-> % tlapm Foo.tla
** Unexpanded symbols: ---
(* created new "Foo.tla.tlaps/Foo.tla.thy" *)
(* fingerprints written in "Foo.tla.tlaps/fingerprints" *)
M.
> On Mar 6, 2022, at 10:38 AM, Alexander Bakst <alexand...@xxxxxxxxx> wrote:
>
> 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 <hwa...@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+u...@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+u...@xxxxxxxxxxxxxxxx.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/690ABB47-97F4-43D7-819F-E1ACFDEF37BB%40gmail.com.