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

[tlaplus] Checking Liveness on Windows

Hi everyone,

I am using toolbox version 1.6.0 of 10 July on Windows 10 1909.

I have defined my spec to be like this:
MySpec ==
/\ SpecInit
/\ [][SpecNext]_vars
/\ SpecLiveness

The problem is that the model checker does not check liveness at all, unless I remove /\ SpecLiveness from the spec definition above!!!

Why is this happening? Please help me.


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/CAKxfy0sttw3%3DZvLT2LU4n%3Ddi8zSW633Cs6wvtHk39EhjAqFsGw%40mail.gmail.com.