ltldo: new binary
* src/bin/common_trans.cc, src/bin/common_trans.hh: New files, extracted from... * src/bin/ltlcross.cc: ... here, so that ltldo can use them. * src/bin/ltldo.cc: New file. * src/bin/Makefile.am: Adjust. * src/bin/common_aoutput.cc, src/bin/common_aoutput.hh: Make it possible to add new statistics. * doc/org/ltldo.org: New file. * doc/Makefile.am, doc/org/tools.org: Adjust. * src/bin/man/ltldo.x: New file. * src/bin/man/Makefile.am: Adjust. * src/bin/man/ltlcross.x, src/bin/man/ltlfilt.x: Mention ltldo(1). * src/tgbatest/ltldo.test, src/tgbatest/ltldo2.test: New files. * src/tgbatest/Makefile.am: Add them. * NEWS: Mention ltldo.
This commit is contained in:
Alexandre Duret-Lutz
parent
e5294aac21
commit
16a8c03143
20 changed files with 1294 additions and 392 deletions
275
doc/org/ltldo.org
Normal file
275
doc/org/ltldo.org
Normal file
|
|
@ -0,0 +1,275 @@
|
|||
# -*- coding: utf-8 -*-
|
||||
#+TITLE: =ltldo=
|
||||
#+SETUPFILE: setup.org
|
||||
#+HTML_LINK_UP: tools.html
|
||||
|
||||
This tool is a wrapper for tools that read LTL/PSL formulas and
|
||||
(optionally) output automata.
|
||||
|
||||
It reads formulas specified using the [[file:ioltl.org][common options for specifying
|
||||
input]] and passes each formula to a tool (or a list of tools) specified
|
||||
using options similar to those of [[file:ltlcross.org][=ltlcross=]]. In case that tool
|
||||
returns an automaton, the resulting automaton is read back by =ltldo=
|
||||
and is finally output as specified using the [[file:oaut.org][common options for
|
||||
outputing automata]].
|
||||
|
||||
In effect, =ltldo= wraps the I/O interface of the Spot tools on top of
|
||||
any other tool.
|
||||
|
||||
* Example: computing statistics for =ltl3ba=
|
||||
|
||||
As a motivating example, consider a scenario where we want to run
|
||||
[[http://sourceforge.net/projects/ltl3ba/][=ltl3ba=]] on a set of 10 formulas stored in a file. For each formula
|
||||
we would like to compute compute the number of states and edges in the
|
||||
Büchi automaton produced by =ltl3ba=.
|
||||
|
||||
Here is the input file:
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports code
|
||||
cat >sample.ltl <<EOF
|
||||
1
|
||||
1 U a
|
||||
!(!((a U Gb) U b) U GFa)
|
||||
(b <-> Xc) xor Fb
|
||||
FXb R (a R (1 U b))
|
||||
Ga
|
||||
G(!(c | (a & (a W Gb))) M Xa)
|
||||
GF((b R !a) U (Xc M 1))
|
||||
G(Xb | Gc)
|
||||
XG!F(a xor Gb)
|
||||
EOF
|
||||
#+END_SRC
|
||||
#+RESULTS:
|
||||
|
||||
We will first implement this scenario without =ltldo=.
|
||||
|
||||
A first problem that the input is not in the correct syntax: although
|
||||
=ltl3ba= understands =G= and =F=, it does not support =xor= or =M=,
|
||||
and requires the Boolean operators =||= and =&&=. This syntax
|
||||
issue can be fixed by processing the input with [[file:ltlfilt.org][=ltlfilt -s=]].
|
||||
|
||||
A second problem is that =ltl3ba= (at least version 1.1.1) can only
|
||||
process one formula at a time. So we'll need to call =ltl3ba= in a
|
||||
loop.
|
||||
|
||||
Finally, one way to compute the size of the resulting Büchi automaton
|
||||
is to pipe the output of =ltl3ba= through [[file:autfilt.org][=autfilt=]].
|
||||
|
||||
Here is how the shell command could look like:
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
ltlfilt -F sample.ltl -s |
|
||||
while read f; do
|
||||
ltl3ba -f "$f" | autfilt --stats="$f,%s,%t"
|
||||
done
|
||||
#+END_SRC
|
||||
#+RESULTS:
|
||||
#+begin_example
|
||||
true,1,1
|
||||
true U a,2,4
|
||||
!(!((a U []b) U b) U []<>a),2,4
|
||||
(((!b && !Xc) || (b && Xc)) && !<>b) || (<>b && !((!b && !Xc) || (b && Xc))),7,21
|
||||
<>Xb V (a V (true U b)),6,28
|
||||
[]a,1,1
|
||||
[](Xa U (Xa && !(c || (a && ([]b V (a || []b)))))),1,0
|
||||
[]<>((b V !a) U (true U Xc)),2,4
|
||||
[](Xb || []c),3,11
|
||||
X[]!<>((a && ![]b) || (!a && []b)),4,10
|
||||
#+end_example
|
||||
|
||||
|
||||
Using =ltldo= the above command can be reduced to this:
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
ltldo -F sample.ltl 'ltl3ba -f %s>%N' --stats='%f,%s,%t'
|
||||
#+END_SRC
|
||||
#+RESULTS:
|
||||
#+begin_example
|
||||
1,1,1
|
||||
1 U a,2,4
|
||||
!(!((a U Gb) U b) U GFa),2,4
|
||||
(b <-> Xc) xor Fb,7,21
|
||||
FXb R (a R (1 U b)),6,28
|
||||
Ga,1,1
|
||||
G(!(c | (a & (a W Gb))) M Xa),1,0
|
||||
GF((b R !a) U (Xc M 1)),2,4
|
||||
G(Xb | Gc),3,11
|
||||
XG!F(a xor Gb),4,10
|
||||
#+end_example
|
||||
|
||||
Note that the formulas look different in both cases, because in the
|
||||
=while= loop the formula printed has already been processed with
|
||||
=ltlfilt=, while =ltldo= emits the input string untouched.
|
||||
|
||||
* Example: running =spin= and producing HOA
|
||||
|
||||
Here is another example, where we use Spin to produce two automata in
|
||||
the [[http://adl.github.io/hoaf/][HOA format]]. Spin has no support for HOA, but =ltldo= simply
|
||||
converts the never claim produced by =spin= into this format.
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
ltldo -f a -f GFa 'spin -f %s>%N' -H
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
#+begin_example
|
||||
HOA: v1
|
||||
States: 2
|
||||
Start: 0
|
||||
AP: 1 "a"
|
||||
acc-name: Buchi
|
||||
Acceptance: 1 Inf(0)
|
||||
properties: trans-labels explicit-labels state-acc deterministic
|
||||
--BODY--
|
||||
State: 0 {0}
|
||||
[0] 1
|
||||
State: 1 {0}
|
||||
[t] 1
|
||||
--END--
|
||||
HOA: v1
|
||||
States: 2
|
||||
Start: 0
|
||||
AP: 1 "a"
|
||||
acc-name: Buchi
|
||||
Acceptance: 1 Inf(0)
|
||||
properties: trans-labels explicit-labels state-acc complete
|
||||
--BODY--
|
||||
State: 0
|
||||
[0] 1
|
||||
[t] 0
|
||||
State: 1 {0}
|
||||
[t] 0
|
||||
--END--
|
||||
#+end_example
|
||||
|
||||
* Syntax for specifying tools to call
|
||||
|
||||
The syntax for specifying how a tool should be called is the same as
|
||||
in [[file:ltlcross.org][=ltlcross=]]. Namely, the following sequences are available.
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports results
|
||||
ltldo --help | sed -n '/character sequences:/,/^$/p' | sed '1d;$d'
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
: %f,%s,%l,%w the formula as a (quoted) string in Spot, Spin,
|
||||
: LBT, or Wring's syntax
|
||||
: %F,%S,%L,%W the formula as a file in Spot, Spin, LBT, or
|
||||
: Wring's syntax
|
||||
: %N,%T,%D,%H the automaton is output as a Never claim, or in
|
||||
: LBTT's, in LTL2DSTAR's, or in the HOA format
|
||||
|
||||
Contrarily to =ltlcross=, it this not mandatory to specify an output filename
|
||||
using one of the sequence for that later lines. For instance we could
|
||||
simply run a formula though =echo= to compare different output syntaxes:
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
ltldo -f 'p0 U p1' -f 'GFp0' 'echo %f, %s, %l, %w'
|
||||
#+END_SRC
|
||||
#+RESULTS:
|
||||
: (p0) U (p1), (p0) U (p1), U p0 p1, (p0=1) U (p1=1)
|
||||
: (G(F(p0))), ([](<>(p0))), G F p0, (G(F(p0=1)))
|
||||
|
||||
In this case (i.e., when the command does not specify any output
|
||||
filename), =ltldo= will not output anything.
|
||||
|
||||
|
||||
As will =ltlcross=, multiple commands can be given, and they will be
|
||||
executed on each formula in the same order.
|
||||
|
||||
A typical use-case is to compare statistics of different tools:
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
ltldo -F sample.ltl 'spin -f %s>%N' 'ltl3ba -f %s>%N' --stats=%T,%f,%s,%e
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
#+begin_example
|
||||
spin -f %s>%N,1,2,2
|
||||
ltl3ba -f %s>%N,1,1,1
|
||||
spin -f %s>%N,1 U a,2,3
|
||||
ltl3ba -f %s>%N,1 U a,2,3
|
||||
spin -f %s>%N,!(!((a U Gb) U b) U GFa),23,86
|
||||
ltl3ba -f %s>%N,!(!((a U Gb) U b) U GFa),2,3
|
||||
spin -f %s>%N,(b <-> Xc) xor Fb,12,23
|
||||
ltl3ba -f %s>%N,(b <-> Xc) xor Fb,7,11
|
||||
spin -f %s>%N,FXb R (a R (1 U b)),28,176
|
||||
ltl3ba -f %s>%N,FXb R (a R (1 U b)),6,20
|
||||
spin -f %s>%N,Ga,1,1
|
||||
ltl3ba -f %s>%N,Ga,1,1
|
||||
spin -f %s>%N,G(!(c | (a & (a W Gb))) M Xa),15,51
|
||||
ltl3ba -f %s>%N,G(!(c | (a & (a W Gb))) M Xa),1,0
|
||||
spin -f %s>%N,GF((b R !a) U (Xc M 1)),12,60
|
||||
ltl3ba -f %s>%N,GF((b R !a) U (Xc M 1)),2,4
|
||||
spin -f %s>%N,G(Xb | Gc),4,8
|
||||
ltl3ba -f %s>%N,G(Xb | Gc),3,5
|
||||
spin -f %s>%N,XG!F(a xor Gb),8,21
|
||||
ltl3ba -f %s>%N,XG!F(a xor Gb),4,7
|
||||
#+end_example
|
||||
|
||||
Here we used =%T= to output the name of the tool used to translate the
|
||||
formula =%f= as an automaton with =%s= states and =%e= edges.
|
||||
If you feel that =%T= has too much clutter, you can give each tool
|
||||
a shorter name by prefixing its command with ={name}=.
|
||||
|
||||
In the following example, we moved the formula used on its own line
|
||||
using the trick that the command =echo %f= will not be subject to
|
||||
=--stats= (since it does not declare any output automaton).
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
ltldo -F sample.ltl --stats=%T,%s,%e \
|
||||
'echo "#" %f' '{spin}spin -f %s>%N' '{ltl3ba}ltl3ba -f %s>%N'
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
#+begin_example
|
||||
# (1)
|
||||
spin,2,2
|
||||
ltl3ba,1,1
|
||||
# (1) U (a)
|
||||
spin,2,3
|
||||
ltl3ba,2,3
|
||||
# (!((!(((a) U (G(b))) U (b))) U (G(F(a)))))
|
||||
spin,23,86
|
||||
ltl3ba,2,3
|
||||
# ((b) <-> (X(c))) xor (F(b))
|
||||
spin,12,23
|
||||
ltl3ba,7,11
|
||||
# (F(X(b))) R ((a) R ((1) U (b)))
|
||||
spin,28,176
|
||||
ltl3ba,6,20
|
||||
# (G(a))
|
||||
spin,1,1
|
||||
ltl3ba,1,1
|
||||
# (G((!((c) | ((a) & ((a) W (G(b)))))) M (X(a))))
|
||||
spin,15,51
|
||||
ltl3ba,1,0
|
||||
# (G(F(((b) R (!(a))) U ((X(c)) M (1)))))
|
||||
spin,12,60
|
||||
ltl3ba,2,4
|
||||
# (G((X(b)) | (G(c))))
|
||||
spin,4,8
|
||||
ltl3ba,3,5
|
||||
# (X(G(!(F((a) xor (G(b)))))))
|
||||
spin,8,21
|
||||
ltl3ba,4,7
|
||||
#+end_example
|
||||
|
||||
Much more readable!
|
||||
|
||||
* Controlling and measuring time
|
||||
|
||||
The run time of each command can be restricted with the =-T NUM=
|
||||
option. The argument is the maximum number of seconds that each
|
||||
command is allowed to run.
|
||||
|
||||
When a timeout occurs a warning is printed on stderr, and no automaton
|
||||
(or statistic) is output by =ltdo= for this specific pair of
|
||||
command/formula. The processing then continue with other formulas and
|
||||
tools. Timeouts are not considered as errors, so they have no effect
|
||||
on the exit status of =ltldo=.
|
||||
|
||||
For each command (that does not terminate with a timeout) the runtime
|
||||
can be printed using the =%r= escape sequence. This makes =ltldo= an
|
||||
alternative to [[file:ltlcross.org][=ltlcross=]] for running benchmarks without any
|
||||
verification.
|
||||
Loading…
Add table
Add a link
Reference in a new issue