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

Re: [tlaplus] Yet another stuttering question

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.