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

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.

On Mon, Aug 14, 2017 at 4:02 AM, mo jia <life....@xxxxxxxxx> wrote:

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...@xxxxxxxxx> 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.

> "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+unsubscribe@googlegroups.com.
> 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>
>
>
> --
> 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.
> 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.