Re: [tlaplus] New to TLA, Can't figure out the example work

Hello,

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:

LEMMA 

  ASSUME NEW TEMPORAL P, NEW TEMPORAL Q

  PROVE  []P /\ [](P => Q) => []Q

BY PTL

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?

Regards,

Stephan

On 12 Aug 2017, at 16:36, mo jia <life....@xxxxxxxxx> wrote:

I am using WSL on windows10.

And some step following https://groups.google.com/forum/#!searchin/tlaplus/%22cvc3%22$20not$20found$20in$20this$20PATH$3A%7Csort:relevance/tlaplus/zrKSDGA9yZ4/UgHm0iLRAwAJ

It work right but not totally right.

The picture is what I have done:
I am following the http://tla.msr-inria.inria.fr/tlaps/content/Documentation/Tutorial/Hierarchical_proofs.html
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.
<tla-first-example.png>