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

[mo jia‏]

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.

[mo jia‏]

I offer the total debug output run in console  by this commond

/usr/local/bin/tlapm --toolbox 0 0 --isaprove -I /usr/local/lib/tlaps/ /home/jiamo/tlaspecs/Euclid/euclid.tla

[Stephan Merz‏]

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

--
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...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
<tla-first-example.png>

[mo jia‏]

I install ls4 in /usr/local/bin

The example you give me can be proved. I upload the picture.
The euclid failed may be it need more time to be proved.
While I don't know how to give a long time to ls4.
"The Additional Preference" just have SMT slover to add.


Here is the help . It seem fine.
----------------------------------------------------------
jiamo@allstoalls:~$ /usr/local/bin/ls4 --help
USAGE: /usr/local/bin/ls4 [options] <input-file>


AIGER OPTIONS:

-r2l, -no-r2l (default: off)
-pg, -no-pg (default: on)

-id = <int32> [ -2 .. imax] (default: -1)

CORE OPTIONS:

-rnd-init, -no-rnd-init (default: off)
-luby, -no-luby (default: on)

-gc-frac = <double> ( 0 .. inf) (default: 0.2)
-var-decay = <double> ( 0 .. 1) (default: 0.95)
-cla-decay = <double> ( 0 .. 1) (default: 0.999)
-rinc = <double> ( 1 .. inf) (default: 2)
-rnd-seed = <double> ( 0 .. inf) (default: 9.16483e+07)
-rnd-freq = <double> [ 0 .. 1] (default: 0)

-ccmin-mode = <int32> [ 0 .. 2] (default: 2)
-rfirst = <int32> [ 1 .. imax] (default: 100)
-phase-saving = <int32> [ 0 .. 2] (default: 2)

INPUT OPTIONS:

-format = <string>

MAIN OPTIONS:

-verbose, -no-verbose (default: on)
-simp, -no-simp (default: on)

SIMP OPTIONS:

-asymm, -no-asymm (default: off)
-rcheck, -no-rcheck (default: off)
-elim, -no-elim (default: on)

-simp-gc-frac = <double> ( 0 .. inf) (default: 0.5)

-cl-lim = <int32> [ -1 .. imax] (default: 20)
-sub-lim = <int32> [ -1 .. imax] (default: 1000)
-grow = <int32> [imin .. imax] (default: 0)

HELP OPTIONS:

--help Print help message.
--help-verb Print verbose help message.



----------------------------------------------------------

On Mon, Aug 14, 2017 at 3:09 AM, Stephan Merz <stepha...@gmail.com> wrote:
> 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

While I install Xming with WSL. So the environment is like the ubuntu
16.04 64bit.

> You received this message because you are subscribed to a topic in the
> Google Groups "tlaplus" group.
> To unsubscribe from this topic, visit
> https://groups.google.com/d/topic/tlaplus/HsTEFVmDn9Q/unsubscribe.
> To unsubscribe from this group and all its topics, send an email to

[mo jia‏]

I re do it all on a real ubuntu 16.04 using the same step I used in WSL. 

This time It works fine.

So it is environment depended error. 

This time the prover 'zenon' can prove it.  So I decide not use WSL when at the begging time of my study. 
​

> email to tlaplus+unsubscribe@googlegroups.com.

> To post to this group, send email to tla...@googlegroups.com.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.
> <tla-first-example.png>
>
>
> --
> You received this message because you are subscribed to a topic in the
> Google Groups "tlaplus" group.
> To unsubscribe from this topic, visit
> https://groups.google.com/d/topic/tlaplus/HsTEFVmDn9Q/unsubscribe.
> To unsubscribe from this group and all its topics, send an email to

> tlaplus+unsubscribe@googlegroups.com.

[Stephan Merz‏]

Thanks for the follow-up. If we get access to a Windows 10 box with WSL, we'll investigate if we can reproduce the issue and report back. If you find a clue to what goes wrong, we'd be happy to hear about it. (The PTL backend shouldn't take long, so increasing the timeout is unlikely to help.)

Thanks,

Stephan

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.

To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

<linux.png>