[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] TLC bug or TLA+ subtlety?
- From: Hillel Wayne <hwayne@xxxxxxxxx>
- Date: Sun, 6 Mar 2022 12:09:11 -0600
- Ironport-data: A9a23:+I2LP6COLzexlRVW/7bmw5YqxClBgxIJ4kV8jS/XYbTApDsi3jQEn TQcXmvXaa3bYGCgft5/YNi39E8BucfRyINjOVdlrnsFo1Bi+ZOUX4zBRqvTF3rPdZObFBoPA +E2MISowBUcFyeEzvuVGuG96yE6jMlkf5KkYAL+EnkZqTRMFWFw0XqPp8Zj2tQy2YPhXVvX0 T/Pi5S31GGNi2Yc3l08sPrrRCNH5JwebxtF1rCWTakjUG72zxH5PrpHTU2CByeQrr1vIwKPb 72rIIdVUY/u10xF5tuNyt4Xe6CRK1LYFVDmZnF+A8BOjvXez8A/+v5TCRYSVatYo22mpoBW4 tFSj4CtRwISNKT+uL1MchYNRkmSPYUekFPGCX22sMjW1lGfNnW1kq8oA0YxMokVvO1wBAmi9 9RCcGFLPk3F3rzuhuvqEIGAhex7RCXvFJ8bs2lk0CqaB/Ata7vyHv7q2/AE8RIarPt2J835R vM8RgNCTDLmWUAUA38YD5UxmOqnnH7iayYeo1WQzUYyyzeMkFQtgOGF3Nz9Vta1SOFojEWho Unk0WX/HDhLc+KO4G/Qmp6rrraXwXmTtJgpPLG57fV3m0a72mgaThgNTx66p+O4gwi/XcheI goa4EITQbMa8UWqSpzkQ0T9rifV5FgTXN1fF+B84waIokbJ3+qHLjArd25mQtg5jtMrSzkR3 Fa7v4q4JDM65dV5Vkmh3ruTqDqzPw0cImkDeTIIQGM5Dz/L8N5bYvXnHoYLLUKlsjHmMWqvn G3S/UDSk51W3JFbjfzqlbzSq2v0/sChc+Ij2unAsouYAu5RYYekY8mx9QGe468RdsCWSV6Ou HVCkM+bhAzvMX1vvHPQKAnuNOvzjxpgDNE6qQI+d3XG32j8k0NPhagKvFlDyL5Ba67ogwPBb k7Joh9275ROJnasZqIfS9vvV5p3lfW4TYy5D668gj9yjn5ZJFDvEMZGNR744owRuBVEfVwXZ c3CKp71VR7294w+lWToHI/xLoPHNghnnT+JLXwK5xug1rWaaRaopUQtYTOzghQCxPrc+G39q o8HX+PTkkU3eLCgP0H/rNBCRXhXfSlTLc2n96R/K7/TSiI4QztJI6GKkdscl3lNw8y5YM+Vp S/tMqKZoXKk7UD6xfKiMSgyOOuyBs8k9RrW/0UEZD6V5pTqWq73hI93Snf9VeBPGDVLwaEmQ v8bVd+HB/gTGD3L9y5EM8vyq4ttcBmknwWTJzHjaz86JsYySwvM897iXw3u6ChfXnHs7JBh/ eKthlHBXJ4OZwV+F8KKOvih+FW84CoGk+VoUkqUf9ReIR2+8IVjJyHroOUwJsUAdUfKyjeAh lSZBB4Zoa/GpIpsqIvFgqWNroGIFepiHxoCTzOLs+rubSSDpzit245NVuqMbAvxbmKs9fXwf /hRwtH9LOYDwwRHvo96JLBhkvAz6t7pkLlFl1g2EXjOaWOrPbNuOHyx28dC6/9WzbhDtArqA 0+C94ABa7WEMc/oCmQcPA40cuOH2a1GkzXe961rckr94yBz8bWdVlhKJF+HjykEdOl5N4Ysw OEAvs8K6l3v0UFzaYnY0S0EpX6RKnEgUrk8ss1ICoHcjAd2mEpJZobRC3Or7ZyCN4dMP00tL mPGjabOne4AlE/Lcn52DGSUmOQE1M5ItxdNw1sPYV+On4Od1PMw2RRQ9xUxTxhUnkobibMtY jAzOh0nP7iK8hdpmNNHAzKmFTZHCUDL4Uf20VYIyDDUQhj6Um3WMFA7IvuH+ExFoWtQciIFr OOdwWfhTTG4c8b20S8/VlRituT4CNl48ATNlYP8QJTUQ8RkMWW82/HteGwTthH8CtkwjkDvq u5t8+J9Zrf8KDYL5aY8DtDCh7gXTRmFIk1EQO1grfNSRjiHJ2/t1GjcMV21d+NMO+fOrR2yB ftoK58dTB+5ziuP8m0WCKJQcbZ4kOR1tYgCZq/zPjxB9LSFqSdxq9Tf8S/xgGJtSNJr1sknL Z7JMC6GG3SUmGATgHLHt8JeO2C1bNRYNhfw2vu5rLcAG54Z6r0+dEgz1v6toyzQPlI2pVSbu wTMY6KQxOtnkNw+k4zpG6RFJgO1NdKjC7jSoV7r64xDPYHVLMPDlwIJsV27bQ5YCr0cBoZsn rOXvd+rgU7Isd7aiYwCd0VtykWI2SmzYAaTGsf+LX0fhDfbHcG1skFF9Ge/JphE1tha46FLg ud+hNSYLbYotxV1nRW5qBSy1z4SDKP4aqrvvySgt+/KAR8YueACBM3y7mfnNAm3aQdRU6ATy WbIVzKG6ddfo4BBCwUDGul9RZR/JTcPnEfgm8LZ7VGlM4Vjvr9OVnYOW/btBfEnx0RoyPrH3 K8=
- Ironport-hdrordr: A9a23:DNgHxalznRb1LL2hjl7KSyZ+hPfpDfN0imdD5ihNYBxZY6Wkfp +V8IVh6fakslthIE3Ix+rrSdC9qBTnhNdICOgqTMGftWzd1wWVxe5ZnPvfKlHbalnDHgA079 YjT0BRYOeATmSSzvyKrzVRKr4bsZm6GdmT9KLjJhRWPHJXgxQK1XY0Nu/4KDwGeOAcP+t1KH P03KMuzEvGCA5nErXEOpQcZZm/mzSsruOtXfcoPX4aAWK1/ESVAdDBYm2lN1slIkFyKXZLyx mgr+U73NTBjxh48H7hP9+51eUWpDIs8KogOCSA4fJlYQkFem2TFcxcsnS5zVVFxpDR1H8a1O PUqxNlFcV+4XHccyWUpl/CwA/9yV8VmjHf9WM=
- Ironport-sdr: ltxRl9yA9Qt0tZwhnJ2s5FjBKUjvlfFf4f4eIH13FdW+fwn0Ab/QeLF2YYfmC949bFiw8mk0cV E9UxpA4vPZaPP3br6MHsPA5imKSqIh4kdkxHQS/6blOKIApGn1vGP0oQ0IyPqtXn30Bb92hApj BEsQ94ZwNyUL0fUzCuw0WPMIvbFmzl1Yi0MgWMb9MJt2S2+AYDbnMBgfqlMABbRQF5WW2MQjOR AvVBuU7eAcF3ig7R9iOS4WsRPtRU2+87y2nxHgnUDd6m7gefyP33TNZBFMdDF3979aAHNN/XgE HFCi98IUEk3CnCpzjpukiUYh
- User-agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101 Thunderbird/91.6.1
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://groups.google.com/d/msgid/tlaplus/b2139e63-9e12-f82c-4935-2077a148f7ef%40gmail.com.