[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] TLC bug or TLA+ subtlety?
- From: Alexander Bakst <alexander.bakst@xxxxxxxxx>
- Date: Sun, 6 Mar 2022 10:38:50 -0800
- Ironport-data: A9a23:Qm6T66Kf1/UBFugSFE+RR5AlxSXFcZb7ZxGr2PjKsXjdYENS1TEGz GBJXTyCbvmMNGX2LYt/bovloEsE6sLSztNiTwYd+CA2RRqmi+KVXIXDdh+Y0wC6d5CYEho/t 63yTvGacajYm1eF/k/F3oDJ9CU6jefRLlbFILas1hpZHGeIcw98z0M78wIFqtQw24LhWFvT4 YmaT/D3YTdJ5RYkagr41IrY8HuDjNyq0N/PlgFWiVhj5TcyplFNZH4tDfnZw0jQHuG4KtWHq 9Prl9lVyI92EyAFUbtJmp6jGqEDryW70QKm0hK6UID66vROS7BbPqsTbJIhhUlrZzqhotd34 cRz6JOKbUQiH6HHvbg0Wkh4DHQrVUFG0OevzXmXtMWSywjecSKpzas0Sk4xOoIc96B8BmQmG f4wcmhcKEDewbjvnvTlEIGAhex7RCXvFJ8bs2lk0CqaB/Ata7vhcouXyvxm+RAarPh2Qs35R vM8RgNCQj3/TCVqA38YD5UxmOqnnH7iayYeo1WQzUYyyzeMkFUojeaF3Nz9QIG1SupxjHuhh GPerl/aBBUaPfeZxm/Qmp6rrraXwXmTtJgpPLG57fV3m0a72mgaThgNTx66p+O4gwi/XcheI goa4EITQbMa8UWqSpzlXUT9riDe+BEbXNVUHqsx7wTlJrfoDxixO28CZy9/NdMckIw9ZDAh8 wOgloLJGmk62FGKck61+rCRpDK0HCEaK24eeCMJJTfpBfGz/+nfaTqfHr5e/L6JYs7dQm6vn mjbxMQqr/BC0p5RjvTTEUXv2mr0/vD0ohgJChI7t19JAyt8bY+hIpSqsB3Vs6wGI4GeQV2M+ nMDnqByDdzi77nSyERho81XRNlFAspp1hWA0DaD+LF9plyQF4aLJ9w43d2HDB4B3jw4UTHoe lTPngha+YVeOnCnBYcuPd7vVpx3lfC4SY27PhwxUjaoSsguHONg1HE+DXN8I0iw+KTRuf1lY MzDKJ7E4YgyUP05kmHeqxghPU8Dn3hinws/tLj0yBOo1bf2WZJmYeZtDbd6VchovMus+VyNm /4Gbpvi40gBDYXWP3eGmaZOfQFiBSVqWPje9p0HHsbdeVAOMD96W5fsLUYJPtINc1J9yLeSp xlQmyZwkzLCuJEwAV7SOyA7Nei2Bs4XQLBSFXVEAGtEEkMLOe6HhJrzvbNuFVX+3OA8n/NyU dcffMCMXqZGRjjdompPYp76o4hvew6smBqVeSGiZWFnLZJnQgXI/P7ifxfupXlVVXPs6pVhr u3yzB7fTLoCWx9mUJTcZsWpwg7jpnMagu9zAxbFL4ALKkXh+YRnMQLrifozL51eIBnP3GrI2 AOfABNeru7I+tdn/N7MjKGCjoGoD+ouRhoATzeHte67bHCI8HCizIlMVPezUQrcDG6kqr+/Y eh1zu3nNKJVkVtPtb16Gek5wK874ezpuOYGnAlpGXP8b2OrBKllFX+I0JQdraZK3LJY5VK7V 0/WoYtaNLyFNdnfHUYVNRYiaujfh/gYliOLs6Y6J0L14CJ45r2aSV4UNB6J0XQPILxwOYIj4 OEgpM9Hu1fk00F1bImL3nJO6mCBDn0cSKF75JsUN4nm11gwwVZYbJ2AVyL77c3da9hINUV2c DaYiLCY3OZZz0vGNmIxTD3Dg7AbipMJtxRHilQFIg3RyNbCg/Y22jxX8Cg2HlsJlEQZi7orN zg5LVBxKIWP4yxs2JpJUVeqFlwTHxae4EHwlwYEmTyLS0izSlHLN3A3PerRrkkV/3gCLmpe9 bCc1GG3XjHtc8X80TE1RFZ+7vnqS9V++06Zx5D2Q5nbT8ZjOGSmn6m1eGAToAHmC84Zi0rAq u1n8/x3dLXgcyUXpvRjWYWd0L0RTjGCJXBDEKE6p/pSQj+DdWHgwyWKJmCwZthJe67A/3i+B pE8PclITRm/iHuDozxHV6cAL6Uozawp+MYaYeGsYmEctKaHtXxmt5Xf8iW4j2guBNp0ltslb Z/VfiqGD3fXnmZegGTXrcNJN2fkM8MIYhbwgLK8/OkTTclRtehtdQQq0OLxsSvPdgRg+B2Qs UXIYKqPl75uzoFlno3NFKRfBlXrdYmiCrzQqA3j4c5Tad7vMNvVs19HoFfQOQkLb6AaXM56l OjQvdP6tK8fUG3aj4wEd1i9+6h1CQGaWeNWNofvLiAfk3XYHsDr5BQH9iazLpkhfBaxICW4b 1PQVSdyXYd9txRhKLl9ZC9ZHBIQBL7wc7/74yi6qpxgzzADhBffIorPGWDBNAlmm+xhB3E6I gDzvPmq699Cq5lUH1kPAPQO71qU5rP8cfNOSuAdfgV0woVlbp1ud1ciedcdBen3N0S5
- Ironport-hdrordr: A9a23:FsN92aj6o711/Sj46Q3zIZgZsHBQX4513DAbv31ZSRFFG/FwyP rD7Y8mPE7P5UdoZJh/o7rwQZVoJkmshqKdgLNhTYtKOTOI1ldAQ7sSmbcKrweQahEWs9QtnJ uJncBFeZnN5XYTt7e+3OD6Kadg/DG/mJrYx9s2tk0dCj2D3spbnklE43igYwVLrXh9dOgE/c Gnl4V6TlObEBx9H6PLfAh4Lpb+SsXw5e/biFw9dmkaAW+1/H+VAZHBcyRwtS1uJg+nr41Sh1 QsUmTCl8GeWjKAu3zhPq3ojqi/KLDau5h+7QC3+6oow03X+02VjIkLYczOgNjEy9vfomrCWe O8xmZHTrtOwkKURHi8pV/G2gXr0joir1/kjXGCh2f7yPaJBA4HNw==
- Ironport-sdr: 8KzsCR6P8GMfSIc1gPqWKeKZIJs+n3D2oJ72HfyrfFOL8hb3jOgJAoivdUqJFvSFg9QsPP5VGk J3TFJwECnVhDF5Gg9obnMOrvuwlXEDHMBH4QkGenDNEgLigafU6kMN4UTpOgucrFb0SNAanYBU ybdMXqJ9B5OBXDxsq9IVOpp20aP+Ncyixj3njnb5LokFi9gZ6kZ9Q1/6KiwjaIB/N6zsudN0mW x4ronYYNfd/cXb5QB3TlokhSlogcUDOGrhId5wg1ATT/Fkxqsjayzr9u6oocWMhwkZ4azd9Y/l Wcq0kx0Fah+ZoaSSrL7XdQLZ
- References: <b2139e63-9e12-f82c-4935-2077a148f7ef@gmail.com>
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.