ltldo.org 18.2 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1 2
# -*- coding: utf-8 -*-
#+TITLE: =ltldo=
3
#+DESCRIPTION: Spot's wrapper for third-party LTL translators
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
#+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
23
[[https://sourceforge.net/projects/ltl3ba/][=ltl3ba=]] on a set of 10 formulas stored in a file.  For each formula
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
24 25 26 27 28
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:

29
#+BEGIN_SRC sh :results silent :exports both
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84
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
85
ltldo 'ltl3ba -f %s>%O' -F sample.ltl --stats='%f,%s,%t'
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104
#+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.

105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125
In fact, as we will discuss below, =ltl3ba= is a tool that =ltldo=
already knows about, so there is a shorter way to run the above
command:

#+BEGIN_SRC sh :results verbatim :exports code
ltldo ltl3ba -F sample.ltl --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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
126 127 128 129 130 131
* 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.

132
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
133
ltldo -f a -f GFa 'spin -f %s>%O'
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
134 135 136
#+END_SRC

#+RESULTS:
137
#+BEGIN_SRC hoa
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
138 139 140 141 142 143
HOA: v1
States: 2
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
144 145
properties: trans-labels explicit-labels state-acc colored
properties: deterministic
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165
--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--
166
#+END_SRC
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
167

168 169 170
Again, using the shorthands defined below, the previous command can be
simplified to just this:

171 172 173
#+BEGIN_EXAMPLE sh
  ltldo spin -f a -f GFa
#+END_EXAMPLE
174

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
175 176 177 178 179 180 181 182 183 184
* 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:
185
:   %%                         a single %
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
186 187 188 189
:   %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
190 191
:   %O                         the automaton output in HOA, never claim, LBTT, or
:                              ltl2dstar's format
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
192

193 194 195 196
Contrarily to =ltlcross=, it this not mandatory to specify an output
filename using one of the sequence for that last line.  For instance
we could simply run a formula though =echo= to compare different
output syntaxes:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214

#+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
215
ltldo -F sample.ltl 'spin -f %s>%O' 'ltl3ba -f %s>%O' --stats=%T,%f,%s,%e
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
216 217 218 219
#+END_SRC

#+RESULTS:
#+begin_example
220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239
spin -f %s>%O,1,2,2
ltl3ba -f %s>%O,1,1,1
spin -f %s>%O,1 U a,2,3
ltl3ba -f %s>%O,1 U a,2,3
spin -f %s>%O,!(!((a U Gb) U b) U GFa),23,86
ltl3ba -f %s>%O,!(!((a U Gb) U b) U GFa),2,3
spin -f %s>%O,(b <-> Xc) xor Fb,12,23
ltl3ba -f %s>%O,(b <-> Xc) xor Fb,7,11
spin -f %s>%O,FXb R (a R (1 U b)),28,176
ltl3ba -f %s>%O,FXb R (a R (1 U b)),6,20
spin -f %s>%O,Ga,1,1
ltl3ba -f %s>%O,Ga,1,1
spin -f %s>%O,G(!(c | (a & (a W Gb))) M Xa),15,51
ltl3ba -f %s>%O,G(!(c | (a & (a W Gb))) M Xa),1,0
spin -f %s>%O,GF((b R !a) U (Xc M 1)),12,60
ltl3ba -f %s>%O,GF((b R !a) U (Xc M 1)),2,4
spin -f %s>%O,G(Xb | Gc),4,8
ltl3ba -f %s>%O,G(Xb | Gc),3,5
spin -f %s>%O,XG!F(a xor Gb),8,21
ltl3ba -f %s>%O,XG!F(a xor Gb),4,7
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
240 241 242 243 244 245 246 247 248 249 250 251 252
#+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 \
253
      'echo "#" %f' '{spin}spin -f %s>%O' '{ltl3ba}ltl3ba -f %s>%O'
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291
#+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!

292 293 294 295
#+BEGIN_SRC sh :results silent :exports results
rm -f sample.ltl
#+END_SRC

296 297 298 299 300 301 302 303 304 305 306 307 308 309
* Shorthands for existing tools

There is a list of existing tools for which =ltldo= (and =ltlcross=)
have built-in specifications.  This list can be printed using the
=--list-shorthands= option:

#+BEGIN_SRC sh :results verbatim :exports both
ltldo --list-shorthands
#+END_SRC
#+RESULTS:
#+begin_example
If a COMMANDFMT does not use any %-sequence, and starts with one of
the following words, then the string on the right is appended.

310 311
  lbt          <%L>%O
  ltl2ba       -f %s>%O
312 313 314
  ltl2da       %f>%O
  ltl2dpa      %f>%O
  ltl2ldba     %f>%O
315
  ltl2dstar    --output-format=hoa %[MW]L %O
316 317
  ltl2tgba     -H %f>%O
  ltl3ba       -f %s>%O
318
  ltl3dra      -f %s>%O
319 320
  ltl3hoa      -f %f>%O
  modella      %[MWei^]L %O
321
  spin         -f %s>%O
322 323 324 325 326

Any {name} and directory component is skipped for the purpose of
matching those prefixes.  So for instance
  '{DRA} ~/mytools/ltl2dstar-0.5.2'
will changed into
327
  '{DRA} ~/mytools/ltl2dstar-0.5.2 --output-format=hoa %[MR]L %O'
328 329
#+end_example

330
Therefore you can type just
331

332
#+BEGIN_SRC sh :results verbatim :exports code
333
ltldo ltl2ba -f a -d
334 335
#+END_SRC

336 337
to obtain a Dot output (as requested with =-d=) for the neverclaim
produced by =ltl2ba -f a=.
338

339
#+BEGIN_SRC sh :results verbatim :exports results
340 341
SPOT_DOTEXTRA= ltldo ltl2ba -f a --dot=
#+END_SRC
342
#+RESULTS:
343 344 345 346 347 348 349 350 351 352 353 354
#+begin_example
digraph G {
  rankdir=LR
  node [shape="circle"]
  I [label="", style=invis, width=0]
  I -> 0
  0 [label="0", peripheries=2]
  0 -> 1 [label="a"]
  1 [label="1", peripheries=2]
  1 -> 1 [label="1"]
}
#+end_example
355 356

The =ltl2ba= argument passed to =ltldo= was interpreted as if you had
357
typed ={ltl2ba}ltl2ba -f %s>%O=.
358 359 360 361 362 363 364 365 366 367 368 369 370

The shorthand is only used if it is the first word of an command
string that does not use any =%= character.  This makes it possible to
add options:

#+BEGIN_SRC sh :results verbatim :exports both
ltldo ltl3ba 'ltl3ba -H2' -f GFa --stats='%T, %s states, %e edges'
#+END_SRC

#+RESULTS:
: ltl3ba, 2 states, 4 edges
: ltl3ba -H2, 1 states, 2 edges

371 372
* Transparent renaming

373
If you have ever tried to use =spin=, =ltl2ba=, or =ltl3ba=, to translate
374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394
a formula such as =[]!Error=, you have noticed that it does not work:

#+BEGIN_SRC sh :results verbatim :exports code
spin -f '[]!Error'
#+END_SRC
#+RESULTS:

#+BEGIN_SRC sh :results verbatim :exports results
spin -f '[]!Error' 2>&1 || exit 0
#+END_SRC
#+RESULTS:
: tl_spin: expected predicate, saw 'E'
: tl_spin: []!Error
: -------------^

All these tools are based on the same LTL parser, that allows
only atomic propositions starting with a lowercase letter.

Running the same command through =ltldo= will work:

#+BEGIN_SRC sh :results verbatim :exports both
395
ltldo spin -f '[]!Error' -s
396 397 398 399 400 401 402 403 404
#+END_SRC
#+RESULTS:
: never {
: accept_init:
:   if
:   :: ((!(Error))) -> goto accept_init
:   fi;
: }

405
(We need the =-s= option to obtain a never claim, instead of the
406
default HOA output.)
407

408 409
What happened is that =ltldo= renamed the atomic propositions in the
formula before calling =spin=.  So =spin= actually received the
410
formula =[]!p0= and produced a never claim using =p0=.  That never
411 412 413 414
claim was then relabeled by =ltldo= to use =Error= instead of =p0=.

This renaming occurs any time some command uses =%s= or =%S= and the
formula has atomic propositions incompatible with Spin's conventions;
415
or when some command uses =%l= or =%L=, and the formula has
416 417
atomic propositions incompatible with [[http://www.tcs.hut.fi/Software/maria/tools/lbt/][LBT's conventions]].

418 419 420 421
For =%f=, =%w=, =%F=, and =%W=, no relabeling is automatically
performed, but you can pass option =--relabel= if you need to force it
for some reason (e.g., if you have a tool that uses almost Spot's
syntax, but cannot cope with double-quoted atomic propositions).
422 423 424 425 426 427 428 429 430

There are some cases where the renaming is not completely transparent.
For instance if a translator tool outputs some HOA file named after
the formula translated, the name will be output unmodified (since this
can be any text string, there is not way for =ltldo= to assume it is
an LTL formula).  In the following example, you can see that the
automaton uses the atomic proposition =Error=, but its name contains a
reference to =p0=.

431
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
432
ltldo 'ltl3ba -H' -f '[]!Error'
433 434
#+END_SRC
#+RESULTS:
435
#+BEGIN_SRC hoa
436
HOA: v1
437
name: "BA for [](!(p0))"
438 439 440 441 442
States: 1
Start: 0
AP: 1 "Error"
acc-name: Buchi
Acceptance: 1 Inf(0)
443 444
properties: trans-labels explicit-labels state-acc colored
properties: deterministic
445 446 447 448
--BODY--
State: 0 "accept_init" {0}
[!0] 0
--END--
449
#+END_SRC
450 451 452 453

If this is a problem, you can always force a new name with the
=--name= option:

454
#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
455
ltldo 'ltl3ba -H' -f '[]!Error' --name='BA for %f'
456 457 458
#+END_SRC

#+RESULTS:
459
#+BEGIN_SRC hoa
460 461 462 463 464 465 466
HOA: v1
name: "BA for []!Error"
States: 1
Start: 0
AP: 1 "Error"
acc-name: Buchi
Acceptance: 1 Inf(0)
467 468
properties: trans-labels explicit-labels state-acc colored
properties: deterministic
469 470 471 472
--BODY--
State: 0 "accept_init" {0}
[!0] 0
--END--
473
#+END_SRC
474

475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618
* Acting as a portfolio of translators
   :PROPERTIES:
   :CUSTOM_ID: portfolio
   :END:

Here is a formula on which different translators produce Büchi automata of
different sizes (states and edges):

#+BEGIN_SRC sh :results verbatim :exports both
ltldo ltl2ba ltl3ba 'ltl2tgba -s' -f 'F(a & Xa | FGa)' \
      --stats='%T: %s st. (%n non-det.), %e ed.'
#+END_SRC

#+RESULTS:
: ltl2ba: 5 st. (2 non-det.), 9 ed.
: ltl3ba: 3 st. (1 non-det.), 4 ed.
: ltl2tgba -s: 3 st. (0 non-det.), 5 ed.

Instead of outputting the result of the translation of each formula by each
translator, =ltldo= can also be configured to output the smallest
automaton obtained for each formula:

#+BEGIN_SRC sh :results verbatim :exports both
ltldo ltl2ba ltl3ba 'ltl2tgba -s' -f 'F(a & Xa | FGa)' --smallest
#+END_SRC

#+RESULTS:
#+begin_example
HOA: v1
States: 3
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc
--BODY--
State: 0
[t] 0
[0] 1
State: 1
[0] 2
State: 2 {0}
[t] 2
--END--
#+end_example

Therefore, in practice, =ltldo --smallest trans1 trans2 trans3...=
acts like a portfolio of translators, always returning the smallest
produced automaton.

The sorting criterion can be specified using =--smallest= or
=--greatest=, optionally followed by a format string with
=%=-sequences.  The default criterion is =%s,%e=, so the number of
states will be compared first, and in case of equality the number of
edges.  If we desire the automaton that has the fewest states, and in
case of equality the smallest number of non-deterministic states, we
can use the following command instead.

#+BEGIN_SRC sh :results verbatim :exports both
ltldo ltl2ba ltl3ba 'ltl2tgba -s' -f 'F(a & Xa | FGa)' --smallest=%s,%n
#+END_SRC

#+RESULTS:
#+begin_example
HOA: v1
name: "F(a & Xa)"
States: 3
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic terminal
--BODY--
State: 0
[!0] 0
[0] 1
State: 1
[!0] 0
[0] 2
State: 2 {0}
[t] 2
--END--
#+end_example

We can of course apply this on a large number of formulas.  For
instance here is a more complex pipeline, where we take 11 patterns
from Dwyer et al. (FMSP'98), and print which translator among
=ltl2ba=, =ltl3ba=, and =ltl2tgba -s= would produce the smallest
automaton.

#+BEGIN_SRC sh :results verbatim :exports both
genltl --dac=10..20 --format=%F:%L,%f |
  ltldo -F-/2 ltl2ba ltl3ba 'ltl2tgba -s' --smallest --stats='%<,%T'
#+END_SRC
#+RESULTS:
#+begin_example
dac-patterns:10,ltl2ba
dac-patterns:11,ltl3ba
dac-patterns:12,ltl2tgba -s
dac-patterns:13,ltl2tgba -s
dac-patterns:14,ltl2tgba -s
dac-patterns:15,ltl2tgba -s
dac-patterns:16,ltl2ba
dac-patterns:17,ltl2tgba -s
dac-patterns:18,ltl2ba
dac-patterns:19,ltl3ba
dac-patterns:20,ltl2ba
#+end_example

Note that in case of equality, only the first translator is returned.
So when =ltl2ba= is output above, it could be the case that =ltl3ba=
or =ltl2tgba -s= are also producing automata of equal size.

To understand the above pipeline, remove the =ltldo= invocation.  The
[[file:genltl.org][=genltl=]] command outputs this:

#+BEGIN_SRC sh :results verbatim :exports both
genltl --dac=10..20 --format=%F:%L,%f
#+END_SRC
#+RESULTS:
#+begin_example
dac-patterns:10,G((p0 & !p1) -> (!p1 U (!p1 & p2)))
dac-patterns:11,!p0 W (p0 W (!p0 W (p0 W G!p0)))
dac-patterns:12,Fp0 -> ((!p0 & !p1) U (p0 | ((!p0 & p1) U (p0 | ((!p0 & !p1) U (p0 | ((!p0 & p1) U (p0 | (!p1 U p0)))))))))
dac-patterns:13,Fp0 -> (!p0 U (p0 & (!p1 W (p1 W (!p1 W (p1 W G!p1))))))
dac-patterns:14,G((p0 & Fp1) -> ((!p1 & !p2) U (p1 | ((!p1 & p2) U (p1 | ((!p1 & !p2) U (p1 | ((!p1 & p2) U (p1 | (!p2 U p1))))))))))
dac-patterns:15,G(p0 -> ((!p1 & !p2) U (p2 | ((p1 & !p2) U (p2 | ((!p1 & !p2) U (p2 | ((p1 & !p2) U (p2 | (!p1 W p2) | Gp1)))))))))
dac-patterns:16,Gp0
dac-patterns:17,Fp0 -> (p1 U p0)
dac-patterns:18,G(p0 -> Gp1)
dac-patterns:19,G((p0 & !p1 & Fp1) -> (p2 U p1))
dac-patterns:20,G((p0 & !p1) -> (p2 W p1))
#+end_example

This is a two-column CSV file where each line is a description of the
origin of the formula (=%F:%L=), followed by the formula itself
(=%f=).  The =ltldo= from the previous pipeline simply takes its input
from the second column of its standard input (=-F-/2=), run that
formula through the three translator, pick the smallest automaton
(=--smallest=), and for this automaton, it display the translator that
was used (=%T=) along with the portion of the CSV file that was before
the input column (=%<=).

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
619 620 621 622 623 624 625 626 627 628
* 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
629 630 631
on the exit status of =ltldo=.  This behavior can be changed with
option =--fail-on-timeout=, in which case timeouts are considered
as errors.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
632 633 634 635 636

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.