according to the screen shot, the temporal proof obligations fail when you run the proof. It looks like the ls4 executable doesn't run successfully on your installation. Unfortunately, I do not have any experience with Windows 10 – has anybody run ls4 successfully on this platform? (The log simply says "failed", which is not very helpful.)
I presume the following also fails for you:
ASSUME NEW TEMPORAL P, NEW TEMPORAL Q
PROVE P /\ (P => Q) => Q
What happens if you launch "/usr/local/lib/tlaps/bin/ls4 --help" (or whatever the correct path on your installation is) from the command line?
I am using WSL on windows10.
It work right but not totally right.
The picture is what I have done:
While I can't figure out why this
<1>2 Spec => InductiveInvariant
BY PTL, InitProperty, NextProperty, <1>1 DEF Spec
can be proved.
The debug msg in console don't helped me to debug.
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+u...@xxxxxxxxxxxxxxxx
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx
Visit this group at https://groups.google.com/group/tlaplus
For more options, visit https://groups.google.com/d/optout