Re: [tlaplus] LearnTLA+ "anything can crash" not fixed by fairness

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

Replace INIT and NEXT with SPECIFICATION Spec (assuming Spec == Init /\ [][Next]_vars).

M.

> On Feb 9, 2025, at 9:05 AM, Frederic Marand (FGM) <fgmarand@xxxxxxxxx> wrote:
> 
> FWIW, here is my CFG file:
> 
> INIT Init
> NEXT Next
> CONSTANT NULL = NULL
> PROPERTY Liveness


-- 
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 visit https://groups.google.com/d/msgid/tlaplus/C2A2E2C6-C5F8-47BB-9834-F99FD2E8A885%40lemmster.de.