1# -*- coding: utf-8 -*- 2#+TITLE: =ltldo= 3#+DESCRIPTION: Spot's wrapper for third-party LTL translators 4#+INCLUDE: setup.org 5#+HTML_LINK_UP: tools.html 6#+PROPERTY: header-args:sh :results verbatim :exports both 7 8This tool is a wrapper for tools that read LTL/PSL formulas and 9(optionally) output automata. 10 11It reads formulas specified using the [[file:ioltl.org][common options for specifying 12input]] and passes each formula to a tool (or a list of tools) specified 13using options similar to those of [[file:ltlcross.org][=ltlcross=]]. In case that tool 14returns an automaton, the resulting automaton is read back by =ltldo= 15and is finally output as specified using the [[file:oaut.org][common options for 16outputing automata]]. 17 18In effect, =ltldo= wraps the I/O interface of the Spot tools on top of 19any other tool. 20 21* Example: computing statistics for =ltl3ba= 22 23As a motivating example, consider a scenario where we want to run 24[[https://sourceforge.net/projects/ltl3ba/][=ltl3ba=]] on a set of 10 formulas stored in a file. For each formula 25we would like to compute compute the number of states and edges in the 26Büchi automaton produced by =ltl3ba=. 27 28Here is the input file: 29 30#+BEGIN_SRC sh :results silent 31cat >sample.ltl <<EOF 321 331 U a 34!(!((a U Gb) U b) U GFa) 35(b <-> Xc) xor Fb 36FXb R (a R (1 U b)) 37Ga 38G(!(c | (a & (a W Gb))) M Xa) 39GF((b R !a) U (Xc M 1)) 40G(Xb | Gc) 41XG!F(a xor Gb) 42EOF 43#+END_SRC 44#+RESULTS: 45 46We will first implement this scenario without =ltldo=. 47 48A first problem that the input is not in the correct syntax: although 49=ltl3ba= understands =G= and =F=, it does not support =xor= or =M=, 50and requires the Boolean operators =||= and =&&=. This syntax 51issue can be fixed by processing the input with [[file:ltlfilt.org][=ltlfilt -s=]]. 52 53A second problem is that =ltl3ba= (at least version 1.1.1) can only 54process one formula at a time. So we'll need to call =ltl3ba= in a 55loop. 56 57Finally, one way to compute the size of the resulting Büchi automaton 58is to pipe the output of =ltl3ba= through [[file:autfilt.org][=autfilt=]]. 59 60Here is how the shell command could look like: 61 62#+BEGIN_SRC sh 63ltlfilt -F sample.ltl -s | 64while read f; do 65 ltl3ba -f "$f" | autfilt --stats="$f,%s,%t" 66done 67#+END_SRC 68#+RESULTS: 69#+begin_example 70true,1,1 71true U a,2,4 72!(!((a U []b) U b) U []<>a),2,4 73(((!b && !Xc) || (b && Xc)) && !<>b) || (<>b && !((!b && !Xc) || (b && Xc))),7,21 74<>Xb V (a V (true U b)),6,28 75[]a,1,1 76[](Xa U (Xa && !(c || (a && ([]b V (a || []b)))))),1,0 77[]<>((b V !a) U (true U Xc)),2,4 78[](Xb || []c),3,11 79X[]!<>((a && ![]b) || (!a && []b)),4,10 80#+end_example 81 82 83Using =ltldo= the above command can be reduced to this: 84 85#+BEGIN_SRC sh 86ltldo 'ltl3ba -f %s>%O' -F sample.ltl --stats='%f,%s,%t' 87#+END_SRC 88#+RESULTS: 89#+begin_example 901,1,1 911 U a,2,4 92!(!((a U Gb) U b) U GFa),2,4 93(b <-> Xc) xor Fb,7,21 94FXb R (a R (1 U b)),6,28 95Ga,1,1 96G(!(c | (a & (a W Gb))) M Xa),1,0 97GF((b R !a) U (Xc M 1)),2,4 98G(Xb | Gc),3,11 99XG!F(a xor Gb),4,10 100#+end_example 101 102Note that the formulas look different in both cases, because in the 103=while= loop the formula printed has already been processed with 104=ltlfilt=, while =ltldo= emits the input string untouched. 105 106In fact, as we will discuss below, =ltl3ba= is a tool that =ltldo= 107already knows about, so there is a shorter way to run the above 108command: 109 110#+BEGIN_SRC sh :exports code 111ltldo ltl3ba -F sample.ltl --stats='%f,%s,%t' 112#+END_SRC 113#+RESULTS: 114#+begin_example 1151,1,1 1161 U a,2,4 117!(!((a U Gb) U b) U GFa),2,4 118(b <-> Xc) xor Fb,7,21 119FXb R (a R (1 U b)),6,28 120Ga,1,1 121G(!(c | (a & (a W Gb))) M Xa),1,0 122GF((b R !a) U (Xc M 1)),2,4 123G(Xb | Gc),3,11 124XG!F(a xor Gb),4,10 125#+end_example 126 127* Example: running =spin= and producing HOA 128 129Here is another example, where we use Spin to produce two automata in 130the [[http://adl.github.io/hoaf/][HOA format]]. Spin has no support for HOA, but =ltldo= simply 131converts the never claim produced by =spin= into this format. 132 133#+BEGIN_SRC sh :wrap SRC hoa 134ltldo 'spin -f %s>%O' -f a -f GFa 135#+END_SRC 136 137#+RESULTS: 138#+BEGIN_SRC hoa 139HOA: v1 140States: 2 141Start: 0 142AP: 1 "a" 143acc-name: Buchi 144Acceptance: 1 Inf(0) 145properties: trans-labels explicit-labels state-acc colored 146properties: deterministic 147--BODY-- 148State: 0 {0} 149[0] 1 150State: 1 {0} 151[t] 1 152--END-- 153HOA: v1 154States: 2 155Start: 0 156AP: 1 "a" 157acc-name: Buchi 158Acceptance: 1 Inf(0) 159properties: trans-labels explicit-labels state-acc complete 160--BODY-- 161State: 0 162[0] 1 163[t] 0 164State: 1 {0} 165[t] 0 166--END-- 167#+END_SRC 168 169Again, using the shorthands defined below, the previous command can be 170simplified to just this: 171 172#+BEGIN_EXAMPLE sh 173 ltldo spin -f a -f GFa 174#+END_EXAMPLE 175 176* Syntax for specifying tools to call 177 178The syntax for specifying how a tool should be called is the same as 179in [[file:ltlcross.org][=ltlcross=]]. Namely, the following sequences are available. 180 181#+BEGIN_SRC sh :exports results 182ltldo --help | sed -n '/character sequences:/,/^$/p' | sed '1d;$d' 183#+END_SRC 184 185#+RESULTS: 186: %% a single % 187: %f,%s,%l,%w the formula as a (quoted) string in Spot, Spin, 188: LBT, or Wring's syntax 189: %F,%S,%L,%W the formula as a file in Spot, Spin, LBT, or 190: Wring's syntax 191: %O the automaton output in HOA, never claim, LBTT, or 192: ltl2dstar's format 193 194Contrarily to =ltlcross=, it this not mandatory to specify an output 195filename using one of the sequence for that last line. For instance 196we could simply run a formula though =echo= to compare different 197output syntaxes: 198 199#+BEGIN_SRC sh 200ltldo -f 'p0 U p1' -f 'GFp0' 'echo %f, %s, %l, %w' 201#+END_SRC 202#+RESULTS: 203: (p0) U (p1), (p0) U (p1), U p0 p1, (p0=1) U (p1=1) 204: (G(F(p0))), ([](<>(p0))), G F p0, (G(F(p0=1))) 205 206In this case (i.e., when the command does not specify any output 207filename), =ltldo= will not output anything. 208 209 210As will =ltlcross=, multiple commands can be given, and they will be 211executed on each formula in the same order. 212 213A typical use-case is to compare statistics of different tools: 214 215#+BEGIN_SRC sh 216ltldo -F sample.ltl 'spin -f %s>%O' 'ltl3ba -f %s>%O' --stats=%T,%f,%s,%e 217#+END_SRC 218 219#+RESULTS: 220#+begin_example 221spin -f %s>%O,1,2,2 222ltl3ba -f %s>%O,1,1,1 223spin -f %s>%O,1 U a,2,3 224ltl3ba -f %s>%O,1 U a,2,3 225spin -f %s>%O,!(!((a U Gb) U b) U GFa),23,86 226ltl3ba -f %s>%O,!(!((a U Gb) U b) U GFa),2,3 227spin -f %s>%O,(b <-> Xc) xor Fb,12,23 228ltl3ba -f %s>%O,(b <-> Xc) xor Fb,7,11 229spin -f %s>%O,FXb R (a R (1 U b)),28,176 230ltl3ba -f %s>%O,FXb R (a R (1 U b)),6,20 231spin -f %s>%O,Ga,1,1 232ltl3ba -f %s>%O,Ga,1,1 233spin -f %s>%O,G(!(c | (a & (a W Gb))) M Xa),15,51 234ltl3ba -f %s>%O,G(!(c | (a & (a W Gb))) M Xa),1,0 235spin -f %s>%O,GF((b R !a) U (Xc M 1)),12,60 236ltl3ba -f %s>%O,GF((b R !a) U (Xc M 1)),2,4 237spin -f %s>%O,G(Xb | Gc),4,8 238ltl3ba -f %s>%O,G(Xb | Gc),3,5 239spin -f %s>%O,XG!F(a xor Gb),8,21 240ltl3ba -f %s>%O,XG!F(a xor Gb),4,7 241#+end_example 242 243Here we used =%T= to output the name of the tool used to translate the 244formula =%f= as an automaton with =%s= states and =%e= edges. 245If you feel that =%T= has too much clutter, you can give each tool 246a shorter name by prefixing its command with ={name}=. 247 248In the following example, we moved the formula used on its own line 249using the trick that the command =echo %f= will not be subject to 250=--stats= (since it does not declare any output automaton). 251 252#+BEGIN_SRC sh 253ltldo -F sample.ltl --stats=%T,%s,%e \ 254 'echo "#" %f' '{spin}spin -f %s>%O' '{ltl3ba}ltl3ba -f %s>%O' 255#+END_SRC 256 257#+RESULTS: 258#+begin_example 259# (1) 260spin,2,2 261ltl3ba,1,1 262# (1) U (a) 263spin,2,3 264ltl3ba,2,3 265# (!((!(((a) U (G(b))) U (b))) U (G(F(a))))) 266spin,23,86 267ltl3ba,2,3 268# ((b) <-> (X(c))) xor (F(b)) 269spin,12,23 270ltl3ba,7,11 271# (F(X(b))) R ((a) R ((1) U (b))) 272spin,28,176 273ltl3ba,6,20 274# (G(a)) 275spin,1,1 276ltl3ba,1,1 277# (G((!((c) | ((a) & ((a) W (G(b)))))) M (X(a)))) 278spin,15,51 279ltl3ba,1,0 280# (G(F(((b) R (!(a))) U ((X(c)) M (1))))) 281spin,12,60 282ltl3ba,2,4 283# (G((X(b)) | (G(c)))) 284spin,4,8 285ltl3ba,3,5 286# (X(G(!(F((a) xor (G(b))))))) 287spin,8,21 288ltl3ba,4,7 289#+end_example 290 291Much more readable! 292 293#+BEGIN_SRC sh :results silent :exports results 294rm -f sample.ltl 295#+END_SRC 296 297* Shorthands for existing tools 298 299There is a list of existing tools for which =ltldo= (and =ltlcross=) 300have built-in specifications. This list can be printed using the 301=--list-shorthands= option: 302 303#+BEGIN_SRC sh 304ltldo --list-shorthands 305#+END_SRC 306#+RESULTS: 307#+begin_example 308If a COMMANDFMT does not use any %-sequence, and starts with one of 309the following regexes, then the string on the right is appended. 310 311 delag %f>%O 312 lbt <%L>%O 313 ltl2ba -f %s>%O 314 ltl2(da|dgra|dpa|dra|ldba|na|nba|ngba) %f>%O 315 ltl2dstar --output-format=hoa %[MW]L %O 316 ltl2tgba -H %f>%O 317 ltl3(ba|dra|hoa|tela) -f %s>%O 318 modella %[MWei^]L %O 319 spin -f %s>%O 320 owl.* ltl2[bdeglnpr]+a\b -f %f>%O 321 owl.* ltl2delta2\b -f %f 322 owl.* ltl-utilities\b -f %f 323 324Any {name} and directory component is skipped for the purpose of 325matching those prefixes. So for instance 326 '{DRA} ~/mytools/ltl2dstar-0.5.2' 327will be changed into 328 '{DRA} ~/mytools/ltl2dstar-0.5.2 --output-format=hoa %[MW]L %O' 329#+end_example 330 331Therefore you can type the following to obtain a Dot output (as 332requested with =-d=) for the neverclaim produced by =ltl2ba -f a=. 333 334#+BEGIN_SRC sh :prologue export SPOT_DOTEXTRA= SPOT_DOTDEFAULT= 335ltldo ltl2ba -f a -d 336#+END_SRC 337#+RESULTS: 338#+begin_example 339digraph "" { 340 rankdir=LR 341 label="\n[Büchi]" 342 labelloc="t" 343 node [shape="circle"] 344 I [label="", style=invis, width=0] 345 I -> 0 346 0 [label="0", peripheries=2] 347 0 -> 1 [label="a"] 348 1 [label="1", peripheries=2] 349 1 -> 1 [label="1"] 350} 351#+end_example 352 353The =ltl2ba= argument passed to =ltldo= was interpreted as if you had 354typed ={ltl2ba}ltl2ba -f %s>%O=. 355 356Those shorthand patterns are only tested if the command string does 357not contains any =%= character. They should always patch a prefix of 358the command, ignoring any leading directory. This makes it possible 359to add options: 360 361#+BEGIN_SRC sh 362ltldo ltl3ba 'ltl3ba -H2' -f GFa --stats='%T, %s states, %e edges' 363#+END_SRC 364#+RESULTS: 365: ltl3ba, 2 states, 4 edges 366: ltl3ba -H2, 1 states, 2 edges 367 368* Transparent renaming 369 370If you have ever tried to use =spin=, =ltl2ba=, or =ltl3ba=, to translate 371a formula such as =[]!Error=, you have noticed that it does not work: 372 373#+BEGIN_SRC sh :prologue "exec 2>&1" :epilogue true 374spin -f '[]!Error' 375#+END_SRC 376#+RESULTS: 377: tl_spin: expected predicate, saw 'E' 378: tl_spin: []!Error 379: -------------^ 380 381All these tools are based on the same LTL parser, that allows 382only atomic propositions starting with a lowercase letter. 383 384Running the same command through =ltldo= will work: 385 386#+BEGIN_SRC sh 387ltldo spin -f '[]!Error' -s 388#+END_SRC 389#+RESULTS: 390: never { 391: accept_init: 392: if 393: :: (!(Error)) -> goto accept_init 394: fi; 395: } 396 397(We need the =-s= option to obtain a never claim, instead of the 398default HOA output.) 399 400What happened is that =ltldo= renamed the atomic propositions in the 401formula before calling =spin=. So =spin= actually received the 402formula =[]!p0= and produced a never claim using =p0=. That never 403claim was then relabeled by =ltldo= to use =Error= instead of =p0=. 404 405This renaming occurs any time some command uses =%s= or =%S= and the 406formula has atomic propositions incompatible with Spin's conventions; 407or when some command uses =%l= or =%L=, and the formula has 408atomic propositions incompatible with [[http://www.tcs.hut.fi/Software/maria/tools/lbt/][LBT's conventions]]. 409 410For =%f=, =%w=, =%F=, and =%W=, no relabeling is automatically 411performed, but you can pass option =--relabel= if you need to force it 412for some reason (e.g., if you have a tool that uses almost Spot's 413syntax, but cannot cope with double-quoted atomic propositions). 414 415There are some cases where the renaming is not completely transparent. 416For instance if a translator tool outputs some HOA file named after 417the formula translated, the name will be output unmodified (since this 418can be any text string, there is not way for =ltldo= to assume it is 419an LTL formula). In the following example, you can see that the 420automaton uses the atomic proposition =Error=, but its name contains a 421reference to =p0=. 422 423#+BEGIN_SRC sh :wrap SRC hoa 424ltldo 'ltl3ba -H' -f '[]!Error' 425#+END_SRC 426#+RESULTS: 427#+BEGIN_SRC hoa 428HOA: v1 429name: "BA for [](!(p0))" 430States: 1 431Start: 0 432AP: 1 "Error" 433acc-name: Buchi 434Acceptance: 1 Inf(0) 435properties: trans-labels explicit-labels state-acc colored 436properties: deterministic 437--BODY-- 438State: 0 "accept_init" {0} 439[!0] 0 440--END-- 441#+END_SRC 442 443If this is a problem, you can always force a new name with the 444=--name= option: 445 446#+BEGIN_SRC sh :wrap SRC hoa 447ltldo 'ltl3ba -H' -f '[]!Error' --name='BA for %f' 448#+END_SRC 449 450#+RESULTS: 451#+BEGIN_SRC hoa 452HOA: v1 453name: "BA for []!Error" 454States: 1 455Start: 0 456AP: 1 "Error" 457acc-name: Buchi 458Acceptance: 1 Inf(0) 459properties: trans-labels explicit-labels state-acc colored 460properties: deterministic 461--BODY-- 462State: 0 "accept_init" {0} 463[!0] 0 464--END-- 465#+END_SRC 466 467* Acting as a portfolio of translators 468 :PROPERTIES: 469 :CUSTOM_ID: portfolio 470 :END: 471 472Here is a formula on which different translators produce Büchi automata of 473different sizes (states and edges): 474 475#+BEGIN_SRC sh 476ltldo ltl2ba ltl3ba 'ltl2tgba -s' -f 'F(a & Xa | FGa)' \ 477 --stats='%T: %s st. (%n non-det.), %e ed.' 478#+END_SRC 479 480#+RESULTS: 481: ltl2ba: 5 st. (2 non-det.), 9 ed. 482: ltl3ba: 3 st. (1 non-det.), 4 ed. 483: ltl2tgba -s: 3 st. (0 non-det.), 5 ed. 484 485Instead of outputting the result of the translation of each formula by each 486translator, =ltldo= can also be configured to output the smallest 487automaton obtained for each formula: 488 489#+BEGIN_SRC sh :wrap SRC hoa 490ltldo ltl2ba ltl3ba 'ltl2tgba -s' -f 'F(a & Xa | FGa)' --smallest 491#+END_SRC 492 493#+RESULTS: 494#+begin_SRC hoa 495HOA: v1 496States: 3 497Start: 0 498AP: 1 "a" 499acc-name: Buchi 500Acceptance: 1 Inf(0) 501properties: trans-labels explicit-labels state-acc 502--BODY-- 503State: 0 504[t] 0 505[0] 1 506State: 1 507[0] 2 508State: 2 {0} 509[t] 2 510--END-- 511#+end_SRC 512 513Therefore, in practice, =ltldo --smallest trans1 trans2 trans3...= 514acts like a portfolio of translators, always returning the smallest 515produced automaton. 516 517The sorting criterion can be specified using =--smallest= or 518=--greatest=, optionally followed by a format string with 519=%=-sequences. The default criterion is =%s,%e=, so the number of 520states will be compared first, and in case of equality the number of 521edges. If we desire the automaton that has the fewest states, and in 522case of equality the smallest number of non-deterministic states, we 523can use the following command instead. 524 525#+BEGIN_SRC sh 526ltldo ltl2ba ltl3ba 'ltl2tgba -s' -f 'F(a & Xa | FGa)' --smallest=%s,%n 527#+END_SRC 528 529#+RESULTS: 530#+begin_example 531HOA: v1 532name: "F(a & Xa)" 533States: 3 534Start: 0 535AP: 1 "a" 536acc-name: Buchi 537Acceptance: 1 Inf(0) 538properties: trans-labels explicit-labels state-acc complete 539properties: deterministic terminal 540--BODY-- 541State: 0 542[!0] 0 543[0] 1 544State: 1 545[!0] 0 546[0] 2 547State: 2 {0} 548[t] 2 549--END-- 550#+end_example 551 552We can of course apply this on a large number of formulas. For 553instance here is a more complex pipeline, where we take 11 patterns 554from Dwyer et al. (FMSP'98), and print which translator among 555=ltl2ba=, =ltl3ba=, and =ltl2tgba -s= would produce the smallest 556automaton. 557 558#+BEGIN_SRC sh 559genltl --dac=10..20 --format=%F:%L,%f | 560 ltldo -F-/2 ltl2ba ltl3ba 'ltl2tgba -s' --smallest --stats='%<,%T' 561#+END_SRC 562#+RESULTS: 563#+begin_example 564dac-patterns:10,ltl2ba 565dac-patterns:11,ltl3ba 566dac-patterns:12,ltl2tgba -s 567dac-patterns:13,ltl2tgba -s 568dac-patterns:14,ltl2tgba -s 569dac-patterns:15,ltl2tgba -s 570dac-patterns:16,ltl2ba 571dac-patterns:17,ltl2tgba -s 572dac-patterns:18,ltl2ba 573dac-patterns:19,ltl3ba 574dac-patterns:20,ltl2ba 575#+end_example 576 577Note that in case of equality, only the first translator is returned. 578So when =ltl2ba= is output above, it could be (and it probably is, see 579below) the case that =ltl3ba= or =ltl2tgba -s= are also producing 580automata of equal size. 581 582To understand the above pipeline, remove the =ltldo= invocation. The 583[[file:genltl.org][=genltl=]] command outputs this: 584 585#+BEGIN_SRC sh 586genltl --dac=10..20 --format=%F:%L,%f 587#+END_SRC 588#+RESULTS: 589#+begin_example 590dac-patterns:10,G((p0 & !p1) -> (!p1 U (!p1 & p2))) 591dac-patterns:11,!p0 W (p0 W (!p0 W (p0 W G!p0))) 592dac-patterns:12,Fp0 -> ((!p0 & !p1) U (p0 | ((!p0 & p1) U (p0 | ((!p0 & !p1) U (p0 | ((!p0 & p1) U (p0 | (!p1 U p0))))))))) 593dac-patterns:13,Fp0 -> (!p0 U (p0 & (!p1 W (p1 W (!p1 W (p1 W G!p1)))))) 594dac-patterns:14,G((p0 & Fp1) -> ((!p1 & !p2) U (p1 | ((!p1 & p2) U (p1 | ((!p1 & !p2) U (p1 | ((!p1 & p2) U (p1 | (!p2 U p1)))))))))) 595dac-patterns:15,G(p0 -> ((!p1 & !p2) U (p2 | ((p1 & !p2) U (p2 | ((!p1 & !p2) U (p2 | ((p1 & !p2) U (p2 | (!p1 W p2) | Gp1))))))))) 596dac-patterns:16,Gp0 597dac-patterns:17,Fp0 -> (p1 U p0) 598dac-patterns:18,G(p0 -> Gp1) 599dac-patterns:19,G((p0 & !p1 & Fp1) -> (p2 U p1)) 600dac-patterns:20,G((p0 & !p1) -> (p2 W p1)) 601#+end_example 602 603This is a two-column CSV file where each line is a description of the 604origin of the formula (=%F:%L=), followed by the formula itself 605(=%f=). The =ltldo= from the previous pipeline simply takes its input 606from the second column of its standard input (=-F-/2=), run that 607formula through the three translator, pick the smallest automaton 608(=--smallest=), and for this automaton, it display the translator that 609was used (=%T=) along with the portion of the CSV file that was before 610the input column (=%<=). 611 612 613If you are curious about the actually size of the automata produced by 614=ltl2ba=, =ltl3ba=, and =ltl2tgba -s= in the above example, you can 615quickly build a CSV file using the following pipeline where each 616command append a new column. We wrap =ltl2ba= and =ltl3ba= with 617=ltldo= so that they can process one column of the CSV that is input, 618and output statistics in CSV as output. =ltl2tgba= does not need 619that, as it already supports those features. In the resulting CSV 620file, displayed as a table below, entries like =2s 4e 0d= represent an 621automaton with 2 states, 4 edges, and that is not deterministic. . 622(We have a [[file:csv.org][separate page]] with more examples of reading and writing CSV 623files.) 624 625#+NAME: small-bench 626#+BEGIN_SRC sh :exports code 627echo input,ltl2ba,ltl3ba,ltl2tgba -s 628genltl --dac=10..20 --format=%F:%L,%f | 629 ltldo -F-/2 ltl2ba --stats '%<,%f,%ss %ee %dd' | 630 ltldo -F-/2 ltl3ba --stats '%<,%f,%>,%ss %ee %dd' | 631 ltl2tgba -s -F-/2 --stats '%<,%>,%ss %ee %dd' 632#+END_SRC 633 634#+BEGIN_SRC sh :results output raw :exports results :noweb yes 635sed ' 636$d 637s/|/\\vert{}/g 638s/--/@@html:--@@/g 639s/^/| / 640s/$/ |/ 641s/,/|/g 642s/"//g 6431a\ 644|-|\ 645|<c>|<r>|<r>|<r>| 646' <<EOF 647<<small-bench()>> 648EOF 649#+END_SRC 650 651#+ATTR_HTML: :class table-pre 652#+RESULTS: 653| input | ltl2ba | ltl3ba | ltl2tgba -s | 654|-----------------+------------+------------+-------------| 655| <c> | <r> | <r> | <r> | 656| dac-patterns:10 | 2s 4e 0d | 2s 4e 1d | 2s 4e 1d | 657| dac-patterns:11 | 5s 9e 1d | 5s 9e 1d | 5s 9e 1d | 658| dac-patterns:12 | 8s 29e 0d | 8s 20e 0d | 7s 17e 1d | 659| dac-patterns:13 | 8s 17e 0d | 8s 17e 0d | 6s 12e 1d | 660| dac-patterns:14 | 16s 62e 0d | 11s 33e 0d | 7s 19e 1d | 661| dac-patterns:15 | 10s 47e 0d | 10s 41e 0d | 6s 17e 1d | 662| dac-patterns:16 | 1s 1e 1d | 1s 1e 1d | 1s 1e 1d | 663| dac-patterns:17 | 4s 7e 0d | 4s 7e 0d | 3s 5e 1d | 664| dac-patterns:18 | 2s 3e 0d | 2s 3e 1d | 2s 3e 1d | 665| dac-patterns:19 | 4s 8e 0d | 3s 6e 0d | 3s 7e 1d | 666| dac-patterns:20 | 2s 4e 0d | 2s 4e 1d | 2s 4e 1d | 667 668#+ATTR_HTML: :class table-pre 669#+RESULTS: 670 671* Controlling and measuring time 672 673The run time of each command can be restricted with the =-T NUM= 674option. The argument is the maximum number of seconds that each 675command is allowed to run. 676 677When a timeout occurs a warning is printed on stderr, and no automaton 678(or statistic) is output by =ltdo= for this specific pair of 679command/formula. The processing then continue with other formulas and 680tools. Timeouts are not considered as errors, so they have no effect 681on the exit status of =ltldo=. This behavior can be changed with 682option =--fail-on-timeout=, in which case timeouts are considered 683as errors. 684 685For each command (that does not terminate with a timeout) the runtime 686can be printed using the =%r= escape sequence. This makes =ltldo= an 687alternative to [[file:ltlcross.org][=ltlcross=]] for running benchmarks without any 688verification. 689