[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Yet another stuttering question

Thanks Markus for your reply, that did it: now the specification is passing the model check without issues.

I'm good now to iterate over the specification and complicate it in incremental steps.


On Thursday, April 14, 2022 at 7:21:21 PM UTC+2 Markus Alexander Kuppe wrote:
Hi Luca,

replace `INIT Init NEXT Next` with `SPECIFICATION Spec`.


> On Apr 14, 2022, at 10:08 AM, Luca Tumedei <lu...@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/e6f66162-57f8-4789-964d-7553d62d941dn%40googlegroups.com.