[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Yet another stuttering question
- From: Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>
- Date: Thu, 14 Apr 2022 10:21:14 -0700
- Ironport-data: A9a23:ikZJmaon1c+EDqDupts5XfI1qsReBmK0YBIvgKrLsJaIsI4StFCzt garIBmFO/nbMWanfd8jaI619ksH7ZbVy4BkQAFuqX03Qy4X+OPIVI+TRqvSF3PLf5ebFCqLz O1HN4KedJhsJpP4jk3wWlQ0hSAkjclkfpKlVKicfHkZqTZMEE/Nszo68wICqtMu0IDR7z+l4 4uo+ZWDYQP9gVaYD0pNg069gEM31BjNkGhA1rAOTagjUIj2yhH5pLpGTU2AByOQrrt8RoZWd M6fpF2NxV41yj92Yj+TfhkXRWVRKlLaFVDmZnO7wMFOiDAazsA5+v5T2Pbx9S67hh3R9+2dx umhurS5RTc3FfX0w988CTp7N3tlNvwd3aTYdC3XXcy7lyUqclPpyvRqSV4zZMgWpL0xDmZJ+ vgVbjsKa3hvhcrsmOP9GrQq355zapewVG8ckikIITXxEfIvWZTeWObA49Ry9xcCvu9+Mcb3T vAzRBRWMDviSjhgA3o0OMwZpN+Zrnb4dDJcpV2Porcv+C7YywkZPL3FaYOIJoPTGps9ckCwv FnK30jERREgK9HDzxXcy3iw1+iRgnauMG4VPOTgqqQCbEeo7mASExYLTkCTvf2wzEulQZdeL VYV82wvq7Iz/QqlVLHAswaQpXeFulsDXoMVHbNhrg6KzaXQ7kCSAW1soiN9hMIOvcMGWxdy7 gSyvonKJhg1q7bEEleG6eLBxd+tAhQ9IWgHbC4CaAIK5dj/vY0+5i4jqP4zQMZZafWlSVnNL yC2QDsW2+xO3JFVv0mv1RWY2GL898Whohsdv12PBgqYAhVFiJlJjmBCwWfS9e5BKomUVELJk nEAn9P2AAsmVMvQxXTlrAklOry2r8eCKj60vLKCN5wo9jDo5Hv6OI4Ou3dxI0BmNstCcjjsC KMyhe+zzMEPVJdJRfUvC25UNyjM5fW6fTgCfq2OBueimrArKGe6ENhGPCZ8JVzFnkk2ir0YM pyGa8uqBntyIf05kGvmHrZCj+Jwn39WKYbvqXbTn0TPPV22NC79dFv5GAbmgh0RsPvU8VyNr b6zyePTk04ECLGWjtbrHX47dAhWdxDX9Lj5rMtYcuPrH+aVMDBJNhMl+ptwK+RNxvwL/s+Rp yHVchIGlTLX2COWQS3XOiELQO6+Af5X8CNrVQRyZwrA8yZ4O+6HsvxPH6bbiJF7nACV5aMvE altlgTpKq8ndwkrDBxENMem/d0+Lknz7e9MVgL8CAUCk1dbb1Sh0rfZksHHrUHi1wK76pkzp aOOzATeTcZRTghuFp+IOv2oyFy1sHcHn/9qRA3DJdwKIBfg941jKirQiP4rIpBcck6anWTEi AvGUw0FoeTtopMu9IWbj66zqYr0QfB1GVBXHjWG4LvvbXva82OvzJVuSuGNeTyBBmr49L/7P LdRwvT5K+EKhhBGvtMkQbpsyKs/4frppqNbl1g1Qi+UMg7zUr45eyuIx8hCsKFJ14R1gwruV xLd4MReNJWIJNjhTAwbKj0jY7nRzvoTgDTTsak4LUijv3138bOLXF9oMgGImTBaKLcpYoopz f145pwZ7AuwjhclKNGbljsS/GOJdyRSX6Iiv5AcIYnqlgt6mgoZOMeDVHD7sMOVdtFBEkg2O TvI1qDMsLJRmxjZeH0pGHmRgOdQiMhcuB1Oy1NedV2FlsCf3a0y1RxVtCsyF0FbkE4B3OV0N WxmcUZyIPzWrTtvgcFCWUGqGh1AVELFoB2vkwNRmT2LVVSsW0zMMHY5ZbSH8ncf/j8OZTNc5 ryZlDvoXGe4eMDqwhY0QlNvr/C/H9V9+hecyJKiFsWBA55obj3ijaujanAPtgP8RMY4gkTIq Koxo7YhNfClZXFJ+vN4Fo+ByL4LQwqFLmFqTvZm86cEEnvbZSmpnzOJLhnpKM9KIvXL926+C tBvd5IUDE3li3jRo2BJH7MILp91gOUtuIgIdITtKDNUqLCYtDdo7M/d+ySi1mYnT88ywJQ9N p/JbGDFVWOKgmZMgCnCq85LPmf+at4BIwLm2/2tt/kNHooHrforalw4ybCuvn+YPQY7rQiYu hjPO/3fw+B4k98+moLtFuBcAlzxJ42oEuuP9w+3vpJFataWaZXCsAYcq1/GOQVKPOtOB44my +zV6NOnjlnYuLsWUnzCn8XTHad+48jvDvFcNdj6LSUHkCaPMCM2D8DvJ4xlxV11fNJhCg2PQ gK5bI6vcIdQVYkGgnJSbCdaHlAWDKGfgmIMY8+ih6zkN/Tf+VWvwBCbGbvBYmZceSsFNIf5F xfv/f2p47i0aaxSUQQcCagO74BQeTfetGhPSzE1nTafCWasj1yYvab6jlwr7jSj5rxo1irly cqteyUSvyhedE0FIB+1fmCyUtAq4K5BvNQN
- Ironport-hdrordr: A9a23:smbh367RJs5fABpu8wPXwGrXdLJyesId70hD6qkvc3AlCvBwxv rC7Y0mPEHP4kd2ZJhAo6H+BEDkexzhHPFOkPks1NuZLXXbUS6TXfRfBWWL+UygJ8XRntQtm5 uIMJIOQuEZNDBB/InHCXCDYpYdKGztytHiuQ6h9QYYcegaUdAf0+4jMHfSLqQefmAvbutcZe Hsm/arvwDQA0j/LP7LdUXtOdKz7uEju6iGXfdsPW9X1ODht0Lb1FY6eyLouyv2kAku/V7hyw b4e7yT3NTujxh28G6+64ffhK4m7ucIOrB4dbuxYwEuW1ec7TqAVcBaQrWH+Bo1rOus5FtvsN 6JjQwnI90b0QKdQl2I
- Ironport-sdr: OZa7kpchjyu2QL6kUF3p1y8EgKmZUgEEcw7mfMqTBiSMABT0KJUjghPYP1Jki43OocWgb5JJfE H1nl3g7badvaLyjfMCR5RySfOh1NKm3a94dJeL861Dr/wYkC7XNseGpC6ZTMMwvH5xN5qQseC0 c5UKaDFocCeUVVqDzPVgLWI8v/+1ivaC/87pcPnOtvGN5dCP60Gl1k9g+OncnKv2xP2qGF9Qy3 MAFmoioNB1/C3d3msN2n3X8MF12lpXdxWA+G+fzjVzmZE0wmcVGXYIiVhf81x+uh3mFSWfnDjf U99wnF6HG15W0coW5bo7Vzu1
- References: <6f31d511-b6cf-488b-ac30-bcfbb42bda85n@googlegroups.com> <60B4EC04-193E-4946-917F-827F55A10A77@gmail.com> <85bf9a23-4739-4637-91ed-8ff39b290e16n@googlegroups.com>
Hi Luca,
replace `INIT Init NEXT Next` with `SPECIFICATION Spec`.
Markus
> On Apr 14, 2022, at 10:08 AM, Luca Tumedei <luca@xxxxxxxxxxxxxxxxx> wrote:
>
> I've simplified it a bit and removed what redundancy there was.
> Running the above specification with the ParallelismRespected invariant and AllWorkDone property does not fail in the TLA+ toolbox, but keeps failing with stuttering in VSCode with the following .cfg file:
>
> ```
> INIT Init
> NEXT Next
>
> INVARIANT ParallelismRespected
> PROPERTY AllWorkDone
> ```
--
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/3779E4B0-0C9F-4E98-81B8-EA29BC451B80%40lemmster.de.