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

[Stephan Merz <stepha...@xxxxxxxxx>]

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

On 14 Aug 2017, at 11:39, mo jia <life....@xxxxxxxxx> wrote:

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.

--
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.
<linux.png>