[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] TLC bug or TLA+ subtlety?
- From: tlaplus-google-group@xxxxxxxxxxx
- Date: Sun, 6 Mar 2022 12:10:37 -0800
- Ironport-data: A9a23:5OZ9U6+nRi9Dx5vJlUK6DrUDBHuTJUtcMsCJ2f8bNWPcYEJGY0x3n DMZXT2CbP+IZWuke9ggao/kpB5VvJ/RzdQ1QAVs+CBEQiMRo6IpJ/zJdxaqZ3v6wu7rFR88s Z1GMrEsCOhuExcwcz/0auCJQUFUjP3OHvylYAL9EngZqTVMEU/Nsjo+3b9h6mJUqYLhWVnV4 ous+5e31GKNglaYDEpEs8pvlzs05JweiBtA1rDpTa0jUPf2zhH5PbpHTU2DByOQrrp8QoZWc 93+IISRpQs1yfuC5uSNyd4XemVSKlLb0JPnZnB+A8BOiTAazsA+PzpS2Pc0MS9qZzu1c99Zy MxJn7yXeTUTZ7TupPUTbkN1OgFOFPgTkFPHCSDXXc27ykTHdz7owawrAhhmbcsX/eF4BWwI/ vsdQNwPRkrb1qTmnfThErkq35RzRCXoFNt3VnVI0TXQFfI7WtPJRa7gzv9q5BgAqvBnNMz0X fQ6UgFOVTHvWjBlZn4uN6MHtOivgXb7fjJCr0+Nvuw85G27IAlZj+exa4GLJLRmQ+12sXrHo V3Yz1jSExw+He6U+Quor2+F07qncSTTAdpOTtVU7MVCjFyIzXEIEzUKUVL9pOKjz0+4QdNWb U0S4Csn66YonHFHVfH4Vhy85XqG51sSAooAVeI97w6Jx+zf5APx6nU4oiBpaMUinu8RdQ4Qj 0aro8LnOGZCmZ2lYCfInluLlg+aNS8QJG4EQCYLSwoZ/tXuyL3faDqfEb6P94bl3rXI9SHML yOi93dh2u1C5SIf/+DqogCd2mPESo3hF1Ztvm3qsnSZAhSVjbNJiqSt4FnfqPJCdcOXFwnR+ ncDnMea4aYFCpTleM2xrAclQ+3BCxWtamW0bbtT838Jqm3FF5mLINk43d2GDB01WvvogBewC KMphStf5YVIIFyhZrJtboS6BqwClPa8S4m9C6iMNoYXPPCdkTNrGgk+OiZ8OEi9wCARfV0XZ P93jO7wVy9BUf0/pNZIb75Ej+FwrszB+Y8jbcmjk07PPUu2a3mSRrMIWGZinchohJ5oVD79q o4FX+PTkk03eLSnMkH/rNBPRXhXcylTLc2n86R/K7/fSiI7STFJI6GKm9sJJdc695m5Y8+Zl p1LchIAkAKXaLyuAV7iV02Pn5u0Bccv9S9gZHd0VbtqslB6CbuSAG4kX8NfVdEaGCZLlpaYl tEJJJeNBOphUDPC92hPZJXxttU8Jhusgg2KMiW/ZyUnZNhrQAmQoo3oeQ7m9S8vCCurtJpu+ Ob5jVyFHpdTFR5/CMv2ae60yw/jt3Yqnu8vDVDDJcNeeRmx/YUzc37xg/Y7LtsiMxLGwjfGh Q+aDQ1B/LvJroow68XEn+aIot7xQed5G0NbGUjd7Kq3bHWLoDD8nNUYCOvRJGLTTmL5/qmmd N559fCkPa1VhktOvqp9D61vkfA06ezpquII1Q9jBnjKMwmmB745eSuG0MBDu7d3y6ddqBexX k7TqNBWNa/QZpHqF1keIAcqdOOezepSkT7XtKxnLEL/7S5x3byGTUQDb0LX0XcCcuR4YNE/3 OMsmM8K8Ajj2BAkBdCL03JP/GOWI31cDqgqu81IAILvjQZ3mFhObYaGVn3z6ZCLLtFOawwke 2/EwqXFgLtYywzJdH9qTSrB2u9UhJIvvhFWzQ9dew7YxIKd3vJnjgdM9TkXTxhOykkV2exEP GU2ZVZ+Ir+D/ms1icUSDWStAB18AgaE8Ej9lwkAmGHDERn6U2XMKHE6a+mK+08d/m1GeSVD5 /SdwWDsXjupJ56hj3dvBx468qW9DsF37RDIg8u9Hs6IN5Y9ZjXhj6C0YncQsF3sBsZo3B/Lo uxj/eBRb6znNH9A+PZiUNbEirlAGgqZIGFiQO16+P9bF2/rfjzviyOFLFq8e58QKvHGrR2xB 8B0epMdVwiizD3c6XcUH6kRO6Qyk/ku694PPLjsICkJqbyCtn11tJvI8jXlw3Q2Sc5li8c3J 47cK2CYHmqLiScGkmPBtpMYaG+xYN1BYA+lme7soLVPGJUEv+VhN0o11+Ls7XmSNQJm+TOSv R/CN/CKlb08kdw0ktu+CLhHCiW1Ncj3CLaC/je1vokcdtjIK8rP614Yp1SP09665lfNtwmbV IhhseIbGGvAtbcyFmTbwtyPTvkZo8q1W+VTP4T8K3wyce5uniPzy0Nrxox6AcUhfBBhCg2PS Ay/Z8+9esQSRs9GgnZSbkCy1j4DXr/vYP6ISTyV9pyx59t07eADBNyg8nDtYG5BcTIQINv1D QqcVzNCIDxHhNwkOSLozM2Kz3O1zJEPlEfmmxDMWeGkM1SV
- Ironport-hdrordr: A9a23:bwrp5KNjqPkhK8BcT5n155DYdb4zR+YMi2TDiHocOGRom52j+r HWoB1E73WE7gr5P0tQ5+xoWZPwPk80kKQb3WB/B8bQYOCLghrVEGgm1/qX/9UPcxeOttK0+8 9bAulD4Z7LfBVHZf+T2nj3Lz9Y+qjFzEgc7t2uhUuFMzsaHJ2Inj0JezpzSXcGDzWubKBRfP Hsgrs91kedlGwsH76G7zs+Lpr+Trvw5drbiDE9ZiLPgzP+/Q9AhoSKZiRxH38lIlZyKHQZkV QtUTaW2k0S2MvLhSM0G1WjjKi/lbDau5J+7DzmsLliFtwksHfLFeNccozHhik8pKWE6Vohkt XA5zcme+pp7W/JF1vF7SfQ5w==
- Ironport-sdr: QQzssmpCAFooUIWKz+aA7es/Oahhk/47CKZnwSYtJ6cfsmJ49w8pol5FjgaFIPqHXK0Qs6+vmR hVSfnOzSaX6QAmMlrMjnSgldz1IOiWz3DZxE7wUUkXGTCZCnhUy8nfZYeftkJhPvAlu0LpR3mZ MmeuwpDLUTUlVfs6i56mj6U1XNGdHKLaHDA/UJCkOEDgNTgP9fqymu5ITohFwIasOgIx0qL29O vKwGrpdfjUfOJeOuEiAlRfNOt0H///15MMS0NU3mtS1GUz99VIqGb6oi/c7tlJGIL6sVrfB2FC FXsVqHWmy1VA+202Jb7crBGW
- References: <b2139e63-9e12-f82c-4935-2077a148f7ef@gmail.com> <690ABB47-97F4-43D7-819F-E1ACFDEF37BB@gmail.com>
----- 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.