Re: [tlaplus] Yet another stuttering question

[Luca Tumedei <luca@xxxxxxxxxxxxxxxxx>]

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.

Luca

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`.

Markus

> 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.