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.
