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

117 views
Skip to first unread message

mo jia

unread,
Aug 12, 2017, 10:36:11 AM8/12/17
to tlaplus
I am using WSL on windows10.


It work right but not totally right.

The picture is what I have done:
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.


tla-first-example.png

mo jia

unread,
Aug 12, 2017, 10:42:11 AM8/12/17
to tlaplus
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
in_termilator.txt

Stephan Merz

unread,
Aug 13, 2017, 3:09:57 PM8/13/17
to tla...@googlegroups.com
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

unread,
Aug 13, 2017, 4:02:26 PM8/13/17
to tla...@googlegroups.com
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
simple_proved_by_ls4.png

mo jia

unread,
Aug 14, 2017, 5:39:49 AM8/14/17
to tla...@googlegroups.com
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. 



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

Stephan Merz

unread,
Aug 15, 2017, 12:20:54 PM8/15/17
to tla...@googlegroups.com
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>

Reply all
Reply to author
Forward
0 new messages