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

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



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+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.
> <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+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.

Attachment: simple_proved_by_ls4.png
Description: PNG image