ltl2tgba.org 28 KB
 Alexandre Duret-Lutz committed Jan 25, 2015 1 # -*- coding: utf-8 -*-  Alexandre Duret-Lutz committed Apr 09, 2013 2 #+TITLE: =ltl2tgba=  Alexandre Duret-Lutz committed Jan 07, 2015 3 4 #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html  Alexandre Duret-Lutz committed Apr 09, 2013 5 6  This tool translates LTL or PSL formulas into two kinds of Büchi  Alexandre Duret-Lutz committed Apr 09, 2013 7 8 9 10 automata, or to monitors. The default is to output Transition-based Generalized Büchi Automata (hereinafter abbreviated TGBA), but more traditional Büchi automata (BA) may be requested using the =-B= option.  Alexandre Duret-Lutz committed Apr 09, 2013 11 12 13 14 15 16  * TGBA and BA Formulas to translate may be specified using [[file:ioltl.org][common input options for LTL/PSL formulas]].  Alexandre Duret-Lutz committed Jan 08, 2016 17 #+BEGIN_SRC sh :results verbatim :exports both  Alexandre Duret-Lutz committed Apr 09, 2013 18 19 ltl2tgba -f 'Fa & GFb' #+END_SRC  Alexandre Duret-Lutz committed Jan 08, 2016 20   Alexandre Duret-Lutz committed Apr 09, 2013 21 22 #+RESULTS: #+begin_example  Alexandre Duret-Lutz committed Jan 08, 2016 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 HOA: v1 name: "Fa & GFb" States: 2 Start: 1 AP: 2 "a" "b" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc complete properties: deterministic stutter-invariant --BODY-- State: 0 [1] 0 {0} [!1] 0 State: 1 [0] 0 [!0] 1 --END--  Alexandre Duret-Lutz committed Apr 09, 2013 40 41 42 43 44 45 46 47 #+end_example Actually, because =ltl2tgba= is often used with a single formula passed on the command line, the =-f= option can be omitted and any command-line parameter that is not the argument of some option will be assumed to be a formula to translate (this differs from [[file:ltlfilt.org][=ltlfilt=]], where such parameters are assumed to be filenames).  Alexandre Duret-Lutz committed Jul 16, 2015 48 =ltl2tgba= honors the [[file:oaut.org][common options for selecting the output format]].  Alexandre Duret-Lutz committed Jan 08, 2016 49 50 51 52 53 54 The default output format, as shown above, is the [[file:hoa.org][HOA]] format, as this can easily be piped to other tools. To convert the automaton into a picture, or into vectorial format, use =--dot= or =-d= to request [[http://www.graphviz.org/][GraphViz output]] and process the result with =dot= or =dotty=. Typically, you could get a =pdf= of this TGBA using  Alexandre Duret-Lutz committed Apr 09, 2013 55 #+BEGIN_SRC sh :results verbatim :exports code  Alexandre Duret-Lutz committed Jan 08, 2016 56 ltl2tgba "Fa & GFb" -d | dot -Tpdf > tgba.pdf  Alexandre Duret-Lutz committed Apr 09, 2013 57 58 59 #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Mar 17, 2015 60 The result would look like this (note that in this documentation  Alexandre Duret-Lutz committed Jul 17, 2015 61 we use some [[file:oaut.org][environment variables]] to produce a more colorful  Alexandre Duret-Lutz committed Mar 17, 2015 62 output by default)  Alexandre Duret-Lutz committed Apr 09, 2013 63 64 #+NAME: dotex #+BEGIN_SRC sh :results verbatim :exports none  Alexandre Duret-Lutz committed Jan 08, 2016 65 ltl2tgba "Fa & GFb" -d  Alexandre Duret-Lutz committed Apr 09, 2013 66 67 68 69 #+END_SRC #+RESULTS: dotex #+begin_example digraph G {  Alexandre Duret-Lutz committed Jan 06, 2015 70  rankdir=LR  Alexandre Duret-Lutz committed Jan 08, 2016 71  node [shape="circle"]  Alexandre Duret-Lutz committed Mar 17, 2015 72 73 74  fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"]  Alexandre Duret-Lutz committed Mar 26, 2015 75  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]  Alexandre Duret-Lutz committed Jan 06, 2015 76 77 78  I [label="", style=invis, width=0] I -> 1 0 [label="0"]  Alexandre Duret-Lutz committed Mar 17, 2015 79 80  0 -> 0 [label=>] 0 -> 0 [label=]  Alexandre Duret-Lutz committed Apr 09, 2013 81  1 [label="1"]  Alexandre Duret-Lutz committed Mar 17, 2015 82 83  1 -> 0 [label=] 1 -> 1 [label=]  Alexandre Duret-Lutz committed Apr 09, 2013 84 85 86 87 88 89 90 91 92 93 } #+end_example #+BEGIN_SRC dot :file dotex.png :cmdline -Tpng :var txt=dotex :exports results $txt #+END_SRC #+RESULTS: [[file:dotex.png]]  Alexandre Duret-Lutz committed Mar 17, 2015 94 95 96 97 98 99 100 101 102 103 Characters like ⓿, ❶, etc. denotes the acceptance sets a transition belongs to. In this case, there is only one acceptance set, called =0=, containing a single transition. You may have many transitions in the same acceptance set, and a transition may also belong to multiple acceptance sets. An infinite path through this automaton is accepting iff it visit each acceptance set infinitely often. Therefore, in the above example, any accepted path will /necessarily/ leave the initial state after a finite amount of steps, and then it will verify the property =b= infinitely often. It is also possible that an automaton do not use any acceptance set at all, in which any run is accepting.  Alexandre Duret-Lutz committed Apr 09, 2013 104 105 106 107 108  Here is a TGBA with multiple acceptance sets (we omit the call to =dot= to render the output of =ltl2tgba= from now on): #+NAME: dotex2  Alexandre Duret-Lutz committed Mar 17, 2015 109 #+BEGIN_SRC sh :results verbatim :exports code  Alexandre Duret-Lutz committed Jan 08, 2016 110 ltl2tgba "GFa & GFb" -d  Alexandre Duret-Lutz committed Apr 09, 2013 111 112 #+END_SRC #+RESULTS: dotex2  Alexandre Duret-Lutz committed Jan 06, 2015 113 114 115 #+begin_example digraph G { rankdir=LR  Alexandre Duret-Lutz committed Mar 17, 2015 116 117 118  fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"]  Alexandre Duret-Lutz committed Mar 26, 2015 119  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]  Alexandre Duret-Lutz committed Jan 06, 2015 120 121 122  I [label="", style=invis, width=0] I -> 0 0 [label="0"]  Alexandre Duret-Lutz committed Mar 17, 2015 123 124 125 126  0 -> 0 [label=>] 0 -> 0 [label=] 0 -> 0 [label=>] 0 -> 0 [label=>]  Alexandre Duret-Lutz committed Jan 06, 2015 127 128 } #+end_example  Alexandre Duret-Lutz committed Apr 09, 2013 129 130 131 132 133 134 135  #+BEGIN_SRC dot :file dotex2.png :cmdline -Tpng :var txt=dotex2 :exports results$txt #+END_SRC #+RESULTS: [[file:dotex2.png]]  Alexandre Duret-Lutz committed Mar 17, 2015 136 The above TGBA has two acceptance sets: ⓿ and ❶. The position of  Alexandre Duret-Lutz committed Jan 06, 2015 137 138 these acceptance sets ensures that atomic propositions =a= and =b= must be true infinitely often.  Alexandre Duret-Lutz committed Apr 09, 2013 139 140 141 142  A Büchi automaton for the previous formula can be obtained with the =-B= option:  Alexandre Duret-Lutz committed Mar 17, 2015 143 #+NAME: dotex2ba  Alexandre Duret-Lutz committed Apr 09, 2013 144 #+BEGIN_SRC sh :results verbatim :exports code  Alexandre Duret-Lutz committed Jan 08, 2016 145 ltl2tgba -B 'GFa & GFb' -d  Alexandre Duret-Lutz committed Apr 09, 2013 146 147 148 149 #+END_SRC #+RESULTS: dotex2ba #+begin_example digraph G {  Alexandre Duret-Lutz committed Jan 06, 2015 150  rankdir=LR  Alexandre Duret-Lutz committed May 13, 2015 151  node [shape="circle"]  Alexandre Duret-Lutz committed Mar 17, 2015 152 153 154  fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"]  Alexandre Duret-Lutz committed Mar 26, 2015 155  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]  Alexandre Duret-Lutz committed Jan 06, 2015 156 157  I [label="", style=invis, width=0] I -> 0  Alexandre Duret-Lutz committed May 13, 2015 158  0 [label="0", peripheries=2]  Alexandre Duret-Lutz committed Mar 17, 2015 159 160 161  0 -> 0 [label=] 0 -> 1 [label=] 0 -> 2 [label=]  Alexandre Duret-Lutz committed May 13, 2015 162  1 [label="1"]  Alexandre Duret-Lutz committed Mar 17, 2015 163 164 165  1 -> 0 [label=] 1 -> 1 [label=] 1 -> 2 [label=]  Alexandre Duret-Lutz committed May 13, 2015 166  2 [label="2"]  Alexandre Duret-Lutz committed Mar 17, 2015 167 168  2 -> 0 [label=] 2 -> 2 [label=]  Alexandre Duret-Lutz committed Apr 09, 2013 169 170 171 172 173 174 175 176 177 } #+end_example #+BEGIN_SRC dot :file dotex2ba.png :cmdline -Tpng :var txt=dotex2ba :exports results $txt #+END_SRC #+RESULTS: [[file:dotex2ba.png]]  Alexandre Duret-Lutz committed May 13, 2015 178 179 180 181 182 183 184 Although accepting states in the Büchi automaton are (traditionally) pictured with double-lines, internally this automaton is still handled as a TGBA with a single acceptance set such that the transitions leaving the state are either all accepting, or all non-accepting. You can see this underlying TGBA if you pass the =--dot=t= option (the =t= requests the use of transition-based acceptance as it is done internally):  Alexandre Duret-Lutz committed Apr 09, 2013 185   Alexandre Duret-Lutz committed Jan 06, 2015 186 187 188 189 190 191 #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba --dot=t -B 'GFa & GFb' #+END_SRC #+NAME: dotex2ba-t #+BEGIN_SRC sh :results verbatim :exports none  Alexandre Duret-Lutz committed Mar 17, 2015 192 ltl2tgba --dot=.t -B 'GFa & GFb'  Alexandre Duret-Lutz committed Jan 06, 2015 193 194 195 196 197 198 #+END_SRC #+RESULTS: dotex2ba-t #+begin_example digraph G { rankdir=LR  Alexandre Duret-Lutz committed Mar 17, 2015 199 200 201  fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"]  Alexandre Duret-Lutz committed Mar 26, 2015 202  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]  Alexandre Duret-Lutz committed Jan 06, 2015 203 204 205  I [label="", style=invis, width=0] I -> 0 0 [label="0"]  Alexandre Duret-Lutz committed Mar 17, 2015 206 207 208  0 -> 0 [label=>] 0 -> 1 [label=>] 0 -> 2 [label=>]  Alexandre Duret-Lutz committed Jan 06, 2015 209  1 [label="1"]  Alexandre Duret-Lutz committed Mar 17, 2015 210 211 212  1 -> 0 [label=] 1 -> 1 [label=] 1 -> 2 [label=]  Alexandre Duret-Lutz committed Jan 06, 2015 213  2 [label="2"]  Alexandre Duret-Lutz committed Mar 17, 2015 214 215  2 -> 0 [label=] 2 -> 2 [label=]  Alexandre Duret-Lutz committed Jan 06, 2015 216 217 218 219 220 221 222 223 224 } #+end_example #+BEGIN_SRC dot :file dotex2ba-t.png :cmdline -Tpng :var txt=dotex2ba-t :exports results$txt #+END_SRC #+RESULTS: [[file:dotex2ba-t.png]]  Alexandre Duret-Lutz committed May 14, 2015 225 226 227 228 229 230 Using option =-S= instead of option =-B= you can obtain generalized Büchi automata with state-based acceptance. Here is the same formula as above, for comparison. #+NAME: dotex2gba #+BEGIN_SRC sh :results verbatim :exports code  Alexandre Duret-Lutz committed Jan 08, 2016 231 ltl2tgba -S 'GFa & GFb' -d  Alexandre Duret-Lutz committed May 14, 2015 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 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 #+END_SRC #+RESULTS: dotex2gba #+begin_example digraph G { rankdir=LR node [shape="circle"] fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"] node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7] I [label="", style=invis, width=0] I -> 0 0 [label=<0
] 3 -> 1 [label=] 3 -> 2 [label=] 3 -> 3 [label=] } #+end_example #+BEGIN_SRC dot :file dotex2gba.png :cmdline -Tpng :var txt=dotex2gba :exports results $txt #+END_SRC #+RESULTS: [[file:dotex2gba.png]] Note that =ltl2tgba= is not very good at generating state-based generalized Büchi automata (GBA): all it does is generating a transition-based one internally, and then pushing acceptance sets onto states. On this example, the resulting GBA produced by =-S= is larger than the BA produced by =-B=.  Alexandre Duret-Lutz committed Jan 06, 2015 280 281 As already discussed on the page about [[file:oaut.org][common output options]], various options controls the output format of =ltl2tgba=:  Alexandre Duret-Lutz committed Apr 09, 2013 282 283 284 285 286  #+BEGIN_SRC sh :results verbatim :exports results ltl2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Jan 06, 2015 287 288 289 #+begin_example -8, --utf8 enable UTF-8 characters in output (ignored with --lbtt or --spin)  Alexandre Duret-Lutz committed May 13, 2015 290 291 292  --check[=PROP] test for the additional property PROP and output the result in the HOA format (implies -H). PROP may be any prefix of 'all' (default),  Alexandre Duret-Lutz committed Jan 08, 2016 293 294 295 296 297  'unambiguous', 'stutter-invariant', or 'strength'. -d, --dot[=1|a|b|B|c|e|f(FONT)|h|n|N|o|r|R|s|t|v|+INT] GraphViz's format. Add letters for (1) force numbered states, (a) acceptance display, (b)  Alexandre Duret-Lutz committed May 13, 2015 298  acceptance sets as bullets, (B) bullets except for  Alexandre Duret-Lutz committed Jan 08, 2016 299  Büchi/co-Büchi automata, (c) force circular  Alexandre Duret-Lutz committed May 13, 2015 300 301 302 303 304  nodes, (e) force elliptic nodes, (f(FONT)) use FONT, (h) horizontal layout, (v) vertical layout, (n) with name, (N) without name, (o) ordered transitions, (r) rainbow colors for acceptance sets, (R) color acceptance sets by Inf/Fin, (s)  Alexandre Duret-Lutz committed Jan 08, 2016 305 306 307 308 309 310 311 312 313 314  with SCCs, (t) force transition-based acceptance, (+INT) add INT to all set numbers -H, --hoaf[=i|l|m|s|t|v] Output the automaton in HOA format (default). Add letters to select (i) use implicit labels for complete deterministic automata, (s) prefer state-based acceptance when possible [default], (t) force transition-based acceptance, (m) mix state and transition-based acceptance, (k) use state labels when possible, (l) single-line output, (v) verbose properties  Alexandre Duret-Lutz committed Jan 06, 2015 315  --lbtt[=t] LBTT's format (add =t to force transition-based  Alexandre Duret-Lutz committed Jan 08, 2016 316  acceptance even on Büchi automata)  Alexandre Duret-Lutz committed Jan 06, 2015 317  --name=FORMAT set the name of the output automaton  Alexandre Duret-Lutz committed Mar 17, 2015 318 319 320  -o, --output=FORMAT send output to a file named FORMAT instead of standard output. The first automaton sent to a file truncates it unless FORMAT starts with '>>'.  Alexandre Duret-Lutz committed Jan 06, 2015 321  -q, --quiet suppress all normal output  Alexandre Duret-Lutz committed Jan 31, 2015 322 323 324  -s, --spin[=6|c] Spin neverclaim (implies --ba). Add letters to select (6) Spin's 6.2.4 style, (c) comments on states  Alexandre Duret-Lutz committed Jan 06, 2015 325 326  --stats=FORMAT output statistics about the automaton #+end_example  Alexandre Duret-Lutz committed Apr 09, 2013 327   Alexandre Duret-Lutz committed Apr 09, 2013 328 Option =-8= can be used to improve the readability of the output  Alexandre Duret-Lutz committed Apr 09, 2013 329 330 331 if your system can display UTF-8 correctly. #+NAME: dotex2ba8  Alexandre Duret-Lutz committed Mar 17, 2015 332 #+BEGIN_SRC sh :results verbatim :exports code  Alexandre Duret-Lutz committed Jan 08, 2016 333 ltl2tgba -B8 "GFa & GFb" -d  Alexandre Duret-Lutz committed Apr 09, 2013 334 335 336 337 #+END_SRC #+RESULTS: dotex2ba8 #+begin_example digraph G {  Alexandre Duret-Lutz committed Jan 06, 2015 338  rankdir=LR  Alexandre Duret-Lutz committed Mar 17, 2015 339 340 341  fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"]  Alexandre Duret-Lutz committed Mar 26, 2015 342  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]  Alexandre Duret-Lutz committed Jan 06, 2015 343 344  I [label="", style=invis, width=0] I -> 0  Alexandre Duret-Lutz committed Mar 26, 2015 345  0 [label=<0 >]  Alexandre Duret-Lutz committed Mar 17, 2015 346 347 348  0 -> 0 [label=] 0 -> 1 [label=] 0 -> 2 [label=]  Alexandre Duret-Lutz committed Mar 26, 2015 349  1 [label=<1>]  Alexandre Duret-Lutz committed Mar 17, 2015 350 351 352  1 -> 0 [label=] 1 -> 1 [label=] 1 -> 2 [label=]  Alexandre Duret-Lutz committed Mar 26, 2015 353  2 [label=<2>]  Alexandre Duret-Lutz committed Mar 17, 2015 354 355  2 -> 0 [label= ] 2 -> 2 [label=]  Alexandre Duret-Lutz committed Apr 09, 2013 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 } #+end_example #+BEGIN_SRC dot :file dotex2ba8.png :cmdline -Tpng :var txt=dotex2ba8 :exports results$txt #+END_SRC #+RESULTS: [[file:dotex2ba8.png]] * Spin output Using the =--spin= or =-s= option, =ltl2tgba= will produce a Büchi automaton (the =-B= option is implied) as a never claim that can be fed to Spin. =ltl2tgba -s= is therefore a drop-in replacement for =spin -f=. #+BEGIN_SRC sh :results verbatim :exports both ltl2tgba -s 'GFa & GFb' #+END_SRC #+RESULTS: #+begin_example never { /* G(Fa & Fb) */ accept_init: if :: ((a) && (b)) -> goto accept_init  Alexandre Duret-Lutz committed Jan 06, 2015 381 382  :: ((!(b))) -> goto T0_S2 :: ((!(a)) && (b)) -> goto T0_S3  Alexandre Duret-Lutz committed Apr 09, 2013 383 384 385  fi; T0_S2: if  Alexandre Duret-Lutz committed Jan 06, 2015 386 387 388  :: ((a) && (b)) -> goto accept_init :: ((!(b))) -> goto T0_S2 :: ((!(a)) && (b)) -> goto T0_S3  Alexandre Duret-Lutz committed Apr 09, 2013 389 390 391  fi; T0_S3: if  Alexandre Duret-Lutz committed Jan 06, 2015 392 393  :: ((a)) -> goto accept_init :: ((!(a))) -> goto T0_S3  Alexandre Duret-Lutz committed Apr 09, 2013 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418  fi; } #+end_example Since Spin 6 extended its syntax to support arbitrary atomic propositions, you may also need put the parser in =--lenient= mode to support these: #+BEGIN_SRC sh :results verbatim :exports both ltl2tgba -s --lenient '(a < b) U (process[2]@ok)' #+END_SRC #+RESULTS: : never { /* "a < b" U "process[2]@ok" */ : T0_init: : if : :: ((process[2]@ok)) -> goto accept_all : :: ((a < b) && (!(process[2]@ok))) -> goto T0_init : fi; : accept_all: : skip : } * Do you favor deterministic or small automata? The translation procedure can be controled by a few switches. A first  Alexandre Duret-Lutz committed Oct 26, 2015 419 420 set of options specifies the goal of the simplification routines: whenever possible, would you prefer a small automaton (=--small=) or a  Alexandre Duret-Lutz committed May 13, 2015 421 deterministic (=--deterministic=) automaton?  Alexandre Duret-Lutz committed Apr 09, 2013 422 423  #+BEGIN_SRC sh :results verbatim :exports results  Alexandre Duret-Lutz committed Oct 26, 2015 424 ltl2tgba --help | sed -n '/Simplification goal:/,/^$/p' | sed '1d;$d'  Alexandre Duret-Lutz committed Apr 09, 2013 425 426 #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed May 13, 2015 427 428 : -a, --any no preference, do not bother making it small or : deterministic  Alexandre Duret-Lutz committed Apr 09, 2013 429 430 431 : -D, --deterministic prefer deterministic automata : --small prefer small automata (default)  Alexandre Duret-Lutz committed May 13, 2015 432 433 434 435 The =--any= option tells the translator that it should attempt to reduce or produce a deterministic result result: any automaton denoting the given formula is OK. This effectively disables post-processings and speeds up the translation.  Alexandre Duret-Lutz committed Apr 09, 2013 436   Alexandre Duret-Lutz committed May 13, 2015 437 438 439 440 441 With the =-D= or =--deterministic= option, the translator will /attempt/ to produce a deterministic automaton, even if this requires a lot of states. =ltl2tgba= knows how to produce the minimal deterministic Büchi automaton for any obligation property (this includes safety properties).  Alexandre Duret-Lutz committed Apr 09, 2013 442 443 444 445 446  With the =--small= option (the default), the translator will not produce a deterministic automaton when it knows how to build smaller automaton.  Alexandre Duret-Lutz committed May 13, 2015 447 448 449 450 Note that options =--deterministic= and =--small= express /preferences/. They certainly do /not/ guarantee that the output will be deterministic, or will be the smallest automaton possible.  Alexandre Duret-Lutz committed Apr 09, 2013 451 452 453 454 An example formula where the difference between =-D= and =--small= is flagrant is =Ga|Gb|Gc=: #+NAME: gagbgc1  Alexandre Duret-Lutz committed Mar 17, 2015 455 #+BEGIN_SRC sh :results verbatim :exports code  Alexandre Duret-Lutz committed Jan 08, 2016 456 ltl2tgba 'Ga|Gb|Gc' -d  Alexandre Duret-Lutz committed Apr 09, 2013 457 458 459 460 #+END_SRC #+RESULTS: gagbgc1 #+begin_example digraph G {  Alexandre Duret-Lutz committed Jan 06, 2015 461  rankdir=LR  Alexandre Duret-Lutz committed May 13, 2015 462  node [shape="circle"]  Alexandre Duret-Lutz committed Mar 17, 2015 463 464 465  fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"]  Alexandre Duret-Lutz committed Mar 26, 2015 466  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]  Alexandre Duret-Lutz committed Jan 06, 2015 467 468  I [label="", style=invis, width=0] I -> 0  Alexandre Duret-Lutz committed Mar 26, 2015 469  0 [label=<0>]  Alexandre Duret-Lutz committed Mar 17, 2015 470 471 472  0 -> 1 [label=] 0 -> 2 [label=] 0 -> 3 [label=]  Alexandre Duret-Lutz committed Mar 26, 2015 473  1 [label=<1>]  Alexandre Duret-Lutz committed Mar 17, 2015 474  1 -> 1 [label=]  Alexandre Duret-Lutz committed Mar 26, 2015 475  2 [label=<2>]  Alexandre Duret-Lutz committed Mar 17, 2015 476  2 -> 2 [label=]  Alexandre Duret-Lutz committed Mar 26, 2015 477  3 [label=<3>]  Alexandre Duret-Lutz committed Mar 17, 2015 478  3 -> 3 [label=]  Alexandre Duret-Lutz committed Apr 09, 2013 479 480 481 482 483 484 485 486 487 } #+end_example #+BEGIN_SRC dot :file gagbgc1.png :cmdline -Tpng :var txt=gagbgc1 :exports results $txt #+END_SRC #+RESULTS: [[file:gagbgc1.png]]  Alexandre Duret-Lutz committed Mar 17, 2015 488 #+NAME: gagbgc2  Alexandre Duret-Lutz committed Apr 09, 2013 489 #+BEGIN_SRC sh :results verbatim :exports code  Alexandre Duret-Lutz committed Jan 08, 2016 490 ltl2tgba -D 'Ga|Gb|Gc' -d  Alexandre Duret-Lutz committed Apr 09, 2013 491 492 493 494 #+END_SRC #+RESULTS: gagbgc2 #+begin_example digraph G {  Alexandre Duret-Lutz committed Jan 06, 2015 495  rankdir=LR  Alexandre Duret-Lutz committed May 13, 2015 496  node [shape="circle"]  Alexandre Duret-Lutz committed Mar 17, 2015 497 498 499  fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"]  Alexandre Duret-Lutz committed Mar 26, 2015 500  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]  Alexandre Duret-Lutz committed Jan 06, 2015 501 502  I [label="", style=invis, width=0] I -> 6  Alexandre Duret-Lutz committed May 13, 2015 503  0 [label="0", peripheries=2]  Alexandre Duret-Lutz committed Mar 17, 2015 504  0 -> 0 [label=]  Alexandre Duret-Lutz committed May 13, 2015 505  1 [label="1", peripheries=2]  Alexandre Duret-Lutz committed Mar 17, 2015 506 507 508  1 -> 0 [label=] 1 -> 1 [label=] 1 -> 2 [label=]  Alexandre Duret-Lutz committed May 13, 2015 509  2 [label="2", peripheries=2]  Alexandre Duret-Lutz committed Mar 17, 2015 510  2 -> 2 [label=]  Alexandre Duret-Lutz committed May 13, 2015 511  3 [label="3", peripheries=2]  Alexandre Duret-Lutz committed Mar 17, 2015 512 513 514  3 -> 2 [label=] 3 -> 3 [label=] 3 -> 5 [label=]  Alexandre Duret-Lutz committed May 13, 2015 515  4 [label="4", peripheries=2]  Alexandre Duret-Lutz committed Mar 17, 2015 516 517 518  4 -> 0 [label=] 4 -> 4 [label=] 4 -> 5 [label=]  Alexandre Duret-Lutz committed May 13, 2015 519  5 [label="5", peripheries=2]  Alexandre Duret-Lutz committed Mar 17, 2015 520  5 -> 5 [label=]  Alexandre Duret-Lutz committed May 13, 2015 521  6 [label="6", peripheries=2]  Alexandre Duret-Lutz committed Mar 17, 2015 522 523 524 525 526 527 528  6 -> 0 [label=] 6 -> 1 [label=] 6 -> 2 [label=] 6 -> 3 [label=] 6 -> 4 [label=] 6 -> 5 [label=] 6 -> 6 [label=]  Alexandre Duret-Lutz committed Apr 09, 2013 529 530 531 532 533 534 535 536 537 538 539 540 541 } #+end_example #+BEGIN_SRC dot :file gagbgc2.png :cmdline -Tpng :var txt=gagbgc2 :exports results$txt #+END_SRC #+RESULTS: [[file:gagbgc2.png]] You can augment the number of terms in the disjunction to magnify the difference. For N terms, the =--small= automaton has N+1 states, while the =--deterministic= automaton needs 2^N-1 states.  Alexandre Duret-Lutz committed May 13, 2015 542 Add the =-C= or =--complete= option if you want to obtain a complete  Alexandre Duret-Lutz committed Sep 08, 2013 543 544 545 automaton, with a sink state capturing that rejected words that would not otherwise have a run in the output automaton.  Alexandre Duret-Lutz committed May 13, 2015 546 547 548 549 550 551 552 553 554 555 556 557 Add the =-U= or =--unambiguous= option if you want unambiguous automata to be produced. An automaton is unambiguous if any word is recognized by at most one accepting run of the automaton (however a word can be rejected by multiple runs, so unambiguous automata can be non-deterministic). The following example is an ambiguous Büchi automaton, because the are two ways to accept a run that repeats continuously the configuration $\bar ab$. #+NAME: ambig1 #+BEGIN_SRC sh :results verbatim :exports code  Alexandre Duret-Lutz committed Jan 08, 2016 558 ltl2tgba -B 'GFa -> GFb' -d  Alexandre Duret-Lutz committed May 13, 2015 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 #+END_SRC #+RESULTS: ambig1 #+begin_example digraph G { rankdir=LR node [shape="circle"] fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"] node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7] I [label="", style=invis, width=0] I -> 1 0 [label="0", peripheries=2] 0 -> 0 [label=] 1 [label="1"] 1 -> 0 [label=] 1 -> 1 [label=<1>] 1 -> 2 [label=] 2 [label="2", peripheries=2] 2 -> 2 [label=] 2 -> 3 [label=] 3 [label="3"] 3 -> 2 [label=] 3 -> 3 [label=] } #+end_example #+BEGIN_SRC dot :file ambig1.png :cmdline -Tpng :var txt=ambig1 :exports results $txt #+END_SRC #+RESULTS: [[file:ambig1.png]] Here is an unambiguous automaton for the same formula, in which there is only one run that recognizes this example word: #+NAME: ambig2 #+BEGIN_SRC sh :results verbatim :exports code  Alexandre Duret-Lutz committed Jan 08, 2016 597 ltl2tgba -B -U 'GFa -> GFb' -d  Alexandre Duret-Lutz committed May 13, 2015 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 #+END_SRC #+RESULTS: ambig2 #+begin_example digraph G { rankdir=LR node [shape="circle"] fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"] node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7] I [label="", style=invis, width=0] I -> 0 0 [label="0"] 0 -> 1 [label=] 0 -> 2 [label=<1>] 0 -> 3 [label=] 0 -> 4 [label=] 1 [label="1", peripheries=2] 1 -> 1 [label=] 2 [label="2", peripheries=2] 2 -> 2 [label=] 2 -> 5 [label=] 3 [label="3"] 3 -> 1 [label=] 3 -> 3 [label=] 3 -> 4 [label=] 4 [label="4"] 4 -> 3 [label=] 4 -> 4 [label=] 5 [label="5"] 5 -> 2 [label=] 5 -> 5 [label=] } #+end_example #+BEGIN_SRC dot :file ambig2.png :cmdline -Tpng :var txt=ambig2 :exports results$txt #+END_SRC #+RESULTS: [[file:ambig2.png]] Unlike =--small= and =--deterministic= that express preferences, options =--complete= and =--unambiguous= do guarantee that the output will be complete and unambiguous.  Alexandre Duret-Lutz committed Sep 08, 2013 646   Alexandre Duret-Lutz committed Apr 09, 2013 647 648 649 650 A last parameter that can be used to tune the translation is the amount of pre- and post-processing performed. These two steps can be adjusted via a common set of switches: #+BEGIN_SRC sh :results verbatim :exports results  Alexandre Duret-Lutz committed Oct 26, 2015 651 ltl2tgba --help | sed -n '/Simplification level:/,/^$/p' | sed '1d;$d'  Alexandre Duret-Lutz committed Apr 09, 2013 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 #+END_SRC #+RESULTS: : --high all available optimizations (slow, default) : --low minimal optimizations (fast) : --medium moderate optimizations Pre-processings are rewritings done on the LTL formulas, usually to reduce its size, but mainly to put it in a form that will help the translator (for instance =F(a|b)= is easier to translate than =F(a)|F(b)=). At =--low= level, only simple syntactic rewritings are performed. At =--medium= level, additional simplifications based on syntactic implications are performed. At =--high= level, language containment is used instead of syntactic implications. Post-processings are cleanups and simplifications of the automaton  Alexandre Duret-Lutz committed May 13, 2015 667 668 produced by the core translator. The algorithms used during post-processing are  Alexandre Duret-Lutz committed Apr 09, 2013 669 670 671 672 673 674 675 676 - SCC filtering: removing useless strongly connected components, and useless acceptance sets. - direct simulation: merge states based on suffix inclusion. - iterated simulations: merge states based on suffix inclusion, or prefix inclusion, in a loop. - WDBA minimization: determinize and minimize automata representing obligation properties. - degeneralization: convert a TGBA into a BA  Alexandre Duret-Lutz committed May 13, 2015 677 - BA simulation (again direct or iterated)  Alexandre Duret-Lutz committed Apr 09, 2013 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718  The chaining of these various algorithms depends on the selected combination of optimization level (=--low=, =--medium=, =--high=), translation intent (=--small=, =--deterministic=) and type of automaton desired (=--tgba=, =--ba=). A notable configuration is =--any --low=, which will produce a TGBA as fast as possible. In this case, post-processing is disabled, and only syntactic rewritings are performed. This can be used for satisfiability checking, although in this context even building an automaton is overkill (you only need an accepted run). Finally, it should be noted that the default optimization options (=--small --high=) are usually overkill. =--low= will produce good automata most of the time. Most of pattern formulas of [[file:genltl.org][=genltl=]] will be efficiently translated in this configuration (meaning that =--small --high= will not produce a better automaton). If you are planning to generate automata for large family of pattern formulas, it makes sense to experiment with the different settings on a small version of the pattern, and select the lowest setting that satisfies your expectations. * Translating multiple formulas for statistics If multiple formulas are given to =ltl2tgba=, the corresponding automata will be output one after the other. This is not very convenient, since most of these output formats are not designed to represent multiple automata, and tools like =dot= will only display the first one. One situation where passing many formulas to =ltl2tgba= is useful is in combination with the =--stats=FORMAT= option. This option will output statistics about the translated automata instead of the automata themselves. The =FORMAT= string should indicate which statistics should be output, and how they should be output using the following sequence of characters (other characters are output as-is): #+BEGIN_SRC sh :results verbatim :exports results ltl2tgba --help | sed -n '/^ *%/p' #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Dec 06, 2013 719 720 721 722 #+begin_example %% a single % %a number of acceptance sets %c number of SCCs  Alexandre Duret-Lutz committed Jan 06, 2015 723  %d 1 if the output is deterministic, 0 otherwise  Alexandre Duret-Lutz committed Dec 06, 2013 724 725  %e number of edges %f the formula, in Spot's syntax  Alexandre Duret-Lutz committed Jan 06, 2015 726  %F name of the input file  Alexandre Duret-Lutz committed Jan 08, 2016 727  %g acceptance condition (in HOA syntax)  Alexandre Duret-Lutz committed Jan 06, 2015 728 729 730 731 732  %L location in the input file %m name of the automaton %n number of nondeterministic states in output %p 1 if the output is complete, 0 otherwise %r processing time (excluding parsing) in seconds  Alexandre Duret-Lutz committed Dec 06, 2013 733 734  %s number of states %t number of transitions  Alexandre Duret-Lutz committed Jan 06, 2015 735  %w one word accepted by the output automaton  Alexandre Duret-Lutz committed Dec 06, 2013 736 #+end_example  Alexandre Duret-Lutz committed Apr 09, 2013 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768  For instance we can study the size of the automata generated for the right-nested =U= formulas as follows: #+BEGIN_SRC sh :results verbatim :exports both genltl --u-right=1..8 | ltl2tgba -F - --stats '%s states and %e edges for "%f"' #+END_SRC #+RESULTS: : 2 states and 2 edges for "p1" : 2 states and 3 edges for "p1 U p2" : 3 states and 6 edges for "p1 U (p2 U p3)" : 4 states and 10 edges for "p1 U (p2 U (p3 U p4))" : 5 states and 15 edges for "p1 U (p2 U (p3 U (p4 U p5)))" : 6 states and 21 edges for "p1 U (p2 U (p3 U (p4 U (p5 U p6))))" : 7 states and 28 edges for "p1 U (p2 U (p3 U (p4 U (p5 U (p6 U p7)))))" : 8 states and 36 edges for "p1 U (p2 U (p3 U (p4 U (p5 U (p6 U (p7 U p8))))))" Here =-F -= means that formulas should be read from the standard input. When computing the size of an automaton, we distinguish /transitions/ and /edges/. An edge between two states is labeled by a Boolean formula and may in fact represent several transitions labeled by compatible Boolean assignment. For instance if the atomic propositions are =x= and =y=, an edge labeled by the formula =!x= actually represents two transitions labeled respectively with =!x&y= and =!x&!y=. Two automata with the same structures (states and edges) but differing labels, may have a different count of transitions, e.g., if one has more restricted labels.  Alexandre Duret-Lutz committed Dec 06, 2013 769 770 771 [[file:csv.org][More examples of how to use =--stats= to create CSV files are on a separate page]].  Alexandre Duret-Lutz committed Apr 09, 2013 772 773 774 775 776 777 778 779 780 781 782 783 * Building Monitors In addition to TGBA and BA, =ltl2tgba= can output /monitor/ using the =-M= option. These are finite automata that accept all prefixes of a formula. The idea is that you can use these automata to monitor a system as it is running, and report a violation as soon as no compatible outgoing transition exist. =ltl2tgba -M= may output non-deterministic monitors while =ltl2tgba -MD= (short for =--monitor --deterministic=) will output the minimal deterministic monitor for the given formula.  Alexandre Duret-Lutz committed Mar 17, 2015 784 #+NAME: monitor1  Alexandre Duret-Lutz committed Apr 09, 2013 785 #+BEGIN_SRC sh :results verbatim :exports code  Alexandre Duret-Lutz committed Jan 08, 2016 786 ltl2tgba -M '(Xa & Fb) | Gc' -d  Alexandre Duret-Lutz committed Apr 09, 2013 787 788 789 790 791 #+END_SRC #+RESULTS: monitor1 #+begin_example digraph G {  Alexandre Duret-Lutz committed Jan 06, 2015 792  rankdir=LR  Alexandre Duret-Lutz committed Jan 08, 2016 793  node [shape="circle"]  Alexandre Duret-Lutz committed Mar 17, 2015 794 795 796  fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"]  Alexandre Duret-Lutz committed Mar 26, 2015 797  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]  Alexandre Duret-Lutz committed Jan 06, 2015 798 799  I [label="", style=invis, width=0] I -> 0  Alexandre Duret-Lutz committed Mar 26, 2015 800  0 [label=<0>]  Alexandre Duret-Lutz committed Mar 17, 2015 801 802  0 -> 1 [label=<1>] 0 -> 3 [label=]  Alexandre Duret-Lutz committed Mar 26, 2015 803  1 [label=<1>]  Alexandre Duret-Lutz committed Mar 17, 2015 804  1 -> 2 [label=]  Alexandre Duret-Lutz committed Mar 26, 2015 805  2 [label=<2>]  Alexandre Duret-Lutz committed Mar 17, 2015 806  2 -> 2 [label=<1>]  Alexandre Duret-Lutz committed Mar 26, 2015 807  3 [label=<3>]  Alexandre Duret-Lutz committed Mar 17, 2015 808  3 -> 3 [label=]  Alexandre Duret-Lutz committed Apr 09, 2013 809 810 811 812 813 814 815 816 817 818 } #+end_example #+BEGIN_SRC dot :file monitor1.png :cmdline -Tpng :var txt=monitor1 :exports results $txt #+END_SRC #+RESULTS: [[file:monitor1.png]]  Alexandre Duret-Lutz committed Mar 17, 2015 819 #+NAME: monitor2  Alexandre Duret-Lutz committed Apr 09, 2013 820 #+BEGIN_SRC sh :results verbatim :exports code  Alexandre Duret-Lutz committed Jan 08, 2016 821 ltl2tgba -MD '(Xa & Fb) | Gc' -d  Alexandre Duret-Lutz committed Apr 09, 2013 822 823 824 825 826 #+END_SRC #+RESULTS: monitor2 #+begin_example digraph G {  Alexandre Duret-Lutz committed Jan 06, 2015 827  rankdir=LR  Alexandre Duret-Lutz committed Jan 08, 2016 828  node [shape="circle"]  Alexandre Duret-Lutz committed Mar 17, 2015 829 830 831  fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"]  Alexandre Duret-Lutz committed Mar 26, 2015 832  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]  Alexandre Duret-Lutz committed Jan 06, 2015 833 834  I [label="", style=invis, width=0] I -> 3  Alexandre Duret-Lutz committed Mar 26, 2015 835  0 [label=<0>]  Alexandre Duret-Lutz committed Mar 17, 2015 836  0 -> 0 [label=<1>]  Alexandre Duret-Lutz committed Mar 26, 2015 837  1 [label=<1>]  Alexandre Duret-Lutz committed Mar 17, 2015 838  1 -> 0 [label=]  Alexandre Duret-Lutz committed Mar 26, 2015 839  2 [label=<2>]  Alexandre Duret-Lutz committed Mar 17, 2015 840  2 -> 2 [label=]  Alexandre Duret-Lutz committed Mar 26, 2015 841  3 [label=<3>]  Alexandre Duret-Lutz committed Mar 17, 2015 842 843  3 -> 1 [label=] 3 -> 4 [label=]  Alexandre Duret-Lutz committed Mar 26, 2015 844  4 [label=<4>]  Alexandre Duret-Lutz committed Mar 17, 2015 845 846  4 -> 0 [label=] 4 -> 2 [label=]  Alexandre Duret-Lutz committed Apr 09, 2013 847 848 849 850 851 852 853 854 855 856 857 858 } #+end_example #+BEGIN_SRC dot :file monitor2.png :cmdline -Tpng :var txt=monitor2 :exports results$txt #+END_SRC #+RESULTS: [[file:monitor2.png]] Because they accept all finite executions that could be extended to match the formula, monitor cannot be used to check for eventualities  Alexandre Duret-Lutz committed Mar 17, 2015 859 860 such as =F(a)=: indeed, any finite execution can be extended to match =F(a)=.  Alexandre Duret-Lutz committed Apr 09, 2013 861 862 863 864 865 866 867 868 869  # LocalWords: ltl tgba num toc PSL Büchi automata SRC GFb invis Acc # LocalWords: ltlfilt filenames GraphViz vectorial pdf Tpdf dotex # LocalWords: sed png cmdline Tpng txt iff GFa ba utf UTF lbtt Fb # LocalWords: GraphViz's LBTT's neverclaim SPOT's init goto fi Gb # LocalWords: controled Gc gagbgc disjunction pre rewritings SCC Xa # LocalWords: WDBA determinize degeneralization satisfiability SCCs # LocalWords: genltl nondeterministic eval setenv concat getenv # LocalWords: setq