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
