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

[tlaplus-google-group@xxxxxxxxxxx]

----- 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 <alexander.bakst@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 <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.

-- 
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/8F4A6DC7-AE28-422A-824C-08FEC69F179C%40lemmster.de.