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

New to TLA, Can't figure out the example work

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.

Attachment: tla-first-example.png
Description: PNG image