ltl2tgba.org 35 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 May 10, 2016 3 #+DESCRIPTION: Spot command-line tool for translating LTL into Transition-based Generalized Büchi Automata. Alexandre Duret-Lutz committed Jan 07, 2015 4 5 #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html Alexandre Duret-Lutz committed Apr 09, 2013 6 Alexandre Duret-Lutz committed Feb 12, 2016 7 8 9 10 11 12 13 14 15 This tool translates LTL or PSL formulas into different types of automata. The inner algorithm produces Transition-based Generalized Büchi Automata, hence the name of the tools, but =ltl2tgba= has grown and now offers several options to adjust the type of automaton output. Those options will be covered in more detail below, but here is a quick summary: Alexandre Duret-Lutz committed Aug 06, 2016 16 17 - =--tgba= (the default) outputs Transition-based Generalized Büchi Automata Alexandre Duret-Lutz committed Feb 12, 2016 18 - =--ba= (or =-B=) outputs state-based Büchi automata Alexandre Duret-Lutz committed Jan 08, 2018 19 20 - =--monitor= (or =-M=) outputs monitors - =--generic --deterministic= (or =-DG=) will do whatever it takes to Alexandre Duret-Lutz committed Feb 12, 2016 21 22 produce a deterministic automaton, and may output generalized Büchi, or parity acceptance. Alexandre Duret-Lutz committed Jan 08, 2018 23 24 - =--parity --deterministic= (or =-DP=) will produce a deterministic automaton with parity acceptance. Alexandre Duret-Lutz committed Apr 09, 2013 25 26 27 28 29 30 * 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 31 #+BEGIN_SRC sh :results verbatim :exports both Alexandre Duret-Lutz committed Apr 09, 2013 32 33 ltl2tgba -f 'Fa & GFb' #+END_SRC Alexandre Duret-Lutz committed Jan 08, 2016 34 Alexandre Duret-Lutz committed Apr 09, 2013 35 36 #+RESULTS: #+begin_example Alexandre Duret-Lutz committed Jan 08, 2016 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 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 54 55 56 57 58 59 60 61 #+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 62 =ltl2tgba= honors the [[file:oaut.org][common options for selecting the output format]]. Alexandre Duret-Lutz committed Jan 08, 2016 63 64 65 66 67 68 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 69 #+BEGIN_SRC sh :results verbatim :exports code Alexandre Duret-Lutz committed Jan 08, 2016 70 ltl2tgba "Fa & GFb" -d | dot -Tpdf > tgba.pdf Alexandre Duret-Lutz committed Apr 09, 2013 71 72 73 #+END_SRC #+RESULTS: Alexandre Duret-Lutz committed Mar 17, 2015 74 The result would look like this (note that in this documentation Alexandre Duret-Lutz committed Aug 06, 2016 75 we use some [[file:oaut.org::#default-dot][environment variables]] to produce a more colorful Alexandre Duret-Lutz committed Mar 17, 2015 76 output by default) Alexandre Duret-Lutz committed Apr 09, 2013 77 78 #+NAME: dotex #+BEGIN_SRC sh :results verbatim :exports none Alexandre Duret-Lutz committed Jan 08, 2016 79 ltl2tgba "Fa & GFb" -d Alexandre Duret-Lutz committed Apr 09, 2013 80 81 82 83 #+END_SRC #+RESULTS: dotex #+begin_example digraph G { Alexandre Duret-Lutz committed Jan 06, 2015 84 rankdir=LR Alexandre Duret-Lutz committed Jan 08, 2016 85 node [shape="circle"] Alexandre Duret-Lutz committed Mar 17, 2015 86 87 88 fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"] Alexandre Duret-Lutz committed Mar 26, 2015 89 node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7] Alexandre Duret-Lutz committed Jan 06, 2015 90 91 92 I [label="", style=invis, width=0] I -> 1 0 [label="0"] Alexandre Duret-Lutz committed Mar 17, 2015 93 94 0 -> 0 [label=>] 0 -> 0 [label=] Alexandre Duret-Lutz committed Apr 09, 2013 95 1 [label="1"] Alexandre Duret-Lutz committed Mar 17, 2015 96 97 1 -> 0 [label=] 1 -> 1 [label=] Alexandre Duret-Lutz committed Apr 09, 2013 98 99 100 } #+end_example Alexandre Duret-Lutz committed Nov 22, 2017 101 #+BEGIN_SRC dot :file dotex.svg :var txt=dotex :exports results Alexandre Duret-Lutz committed Apr 09, 2013 102 103 104 105 $txt #+END_SRC #+RESULTS: Alexandre Duret-Lutz committed Nov 22, 2017 106 [[file:dotex.svg]] Alexandre Duret-Lutz committed Apr 09, 2013 107 Alexandre Duret-Lutz committed Mar 17, 2015 108 109 110 111 112 113 114 115 116 117 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 118 119 120 121 122 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 123 #+BEGIN_SRC sh :results verbatim :exports code Alexandre Duret-Lutz committed Jan 08, 2016 124 ltl2tgba "GFa & GFb" -d Alexandre Duret-Lutz committed Apr 09, 2013 125 126 #+END_SRC #+RESULTS: dotex2 Alexandre Duret-Lutz committed Jan 06, 2015 127 128 129 #+begin_example digraph G { rankdir=LR Alexandre Duret-Lutz committed Mar 17, 2015 130 131 132 fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"] Alexandre Duret-Lutz committed Mar 26, 2015 133 node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7] Alexandre Duret-Lutz committed Jan 06, 2015 134 135 136 I [label="", style=invis, width=0] I -> 0 0 [label="0"] Alexandre Duret-Lutz committed Mar 17, 2015 137 138 139 140 0 -> 0 [label=>] 0 -> 0 [label=] 0 -> 0 [label=>] 0 -> 0 [label=>] Alexandre Duret-Lutz committed Jan 06, 2015 141 142 } #+end_example Alexandre Duret-Lutz committed Apr 09, 2013 143 Alexandre Duret-Lutz committed Nov 22, 2017 144 #+BEGIN_SRC dot :file dotex2.svg :var txt=dotex2 :exports results Alexandre Duret-Lutz committed Apr 09, 2013 145 146 147$txt #+END_SRC #+RESULTS: Alexandre Duret-Lutz committed Nov 22, 2017 148 [[file:dotex2.svg]] Alexandre Duret-Lutz committed Apr 09, 2013 149 Alexandre Duret-Lutz committed Mar 10, 2018 150 The above TGBA has two acceptance sets: ⓿ and ❶. The definition of Alexandre Duret-Lutz committed Jan 06, 2015 151 152 these acceptance sets ensures that atomic propositions =a= and =b= must be true infinitely often. Alexandre Duret-Lutz committed Apr 09, 2013 153 154 155 156 A Büchi automaton for the previous formula can be obtained with the =-B= option: Alexandre Duret-Lutz committed Mar 17, 2015 157 #+NAME: dotex2ba Alexandre Duret-Lutz committed Apr 09, 2013 158 #+BEGIN_SRC sh :results verbatim :exports code Alexandre Duret-Lutz committed Jan 08, 2016 159 ltl2tgba -B 'GFa & GFb' -d Alexandre Duret-Lutz committed Apr 09, 2013 160 161 162 163 #+END_SRC #+RESULTS: dotex2ba #+begin_example digraph G { Alexandre Duret-Lutz committed Jan 06, 2015 164 rankdir=LR Alexandre Duret-Lutz committed May 13, 2015 165 node [shape="circle"] Alexandre Duret-Lutz committed Mar 17, 2015 166 167 168 fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"] Alexandre Duret-Lutz committed Mar 26, 2015 169 node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7] Alexandre Duret-Lutz committed Jan 06, 2015 170 171 I [label="", style=invis, width=0] I -> 0 Alexandre Duret-Lutz committed May 13, 2015 172 0 [label="0", peripheries=2] Alexandre Duret-Lutz committed Mar 17, 2015 173 174 175 0 -> 0 [label=] 0 -> 1 [label=] 0 -> 2 [label=] Alexandre Duret-Lutz committed May 13, 2015 176 1 [label="1"] Alexandre Duret-Lutz committed Mar 17, 2015 177 178 179 1 -> 0 [label=] 1 -> 1 [label=] 1 -> 2 [label=] Alexandre Duret-Lutz committed May 13, 2015 180 2 [label="2"] Alexandre Duret-Lutz committed Mar 17, 2015 181 182 2 -> 0 [label=] 2 -> 2 [label=] Alexandre Duret-Lutz committed Apr 09, 2013 183 184 185 } #+end_example Alexandre Duret-Lutz committed Nov 22, 2017 186 #+BEGIN_SRC dot :file dotex2ba.svg :var txt=dotex2ba :exports results Alexandre Duret-Lutz committed Apr 09, 2013 187 188 189 $txt #+END_SRC #+RESULTS: Alexandre Duret-Lutz committed Nov 22, 2017 190 [[file:dotex2ba.svg]] Alexandre Duret-Lutz committed Apr 09, 2013 191 Alexandre Duret-Lutz committed May 13, 2015 192 193 194 195 196 197 198 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 199 Alexandre Duret-Lutz committed Jan 06, 2015 200 201 202 203 204 205 #+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 206 ltl2tgba --dot=.t -B 'GFa & GFb' Alexandre Duret-Lutz committed Jan 06, 2015 207 208 209 210 211 212 #+END_SRC #+RESULTS: dotex2ba-t #+begin_example digraph G { rankdir=LR Alexandre Duret-Lutz committed Mar 17, 2015 213 214 215 fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"] Alexandre Duret-Lutz committed Mar 26, 2015 216 node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7] Alexandre Duret-Lutz committed Jan 06, 2015 217 218 219 I [label="", style=invis, width=0] I -> 0 0 [label="0"] Alexandre Duret-Lutz committed Mar 17, 2015 220 221 222 0 -> 0 [label=>] 0 -> 1 [label=>] 0 -> 2 [label=>] Alexandre Duret-Lutz committed Jan 06, 2015 223 1 [label="1"] Alexandre Duret-Lutz committed Mar 17, 2015 224 225 226 1 -> 0 [label=] 1 -> 1 [label=] 1 -> 2 [label=] Alexandre Duret-Lutz committed Jan 06, 2015 227 2 [label="2"] Alexandre Duret-Lutz committed Mar 17, 2015 228 229 2 -> 0 [label=] 2 -> 2 [label=] Alexandre Duret-Lutz committed Jan 06, 2015 230 231 232 } #+end_example Alexandre Duret-Lutz committed Nov 22, 2017 233 #+BEGIN_SRC dot :file dotex2ba-t.svg :var txt=dotex2ba-t :exports results Alexandre Duret-Lutz committed Jan 06, 2015 234 235 236$txt #+END_SRC #+RESULTS: Alexandre Duret-Lutz committed Nov 22, 2017 237 [[file:dotex2ba-t.svg]] Alexandre Duret-Lutz committed Jan 06, 2015 238 Alexandre Duret-Lutz committed May 14, 2015 239 240 241 242 243 244 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 245 ltl2tgba -S 'GFa & GFb' -d Alexandre Duret-Lutz committed May 14, 2015 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 280 281 #+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 Alexandre Duret-Lutz committed Nov 22, 2017 282 #+BEGIN_SRC dot :file dotex2gba.svg :var txt=dotex2gba :exports results Alexandre Duret-Lutz committed May 14, 2015 283 284 285 $txt #+END_SRC #+RESULTS: Alexandre Duret-Lutz committed Nov 22, 2017 286 [[file:dotex2gba.svg]] Alexandre Duret-Lutz committed May 14, 2015 287 288 289 290 291 292 293 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 294 295 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 296 297 298 299 300 #+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 301 302 303 #+begin_example -8, --utf8 enable UTF-8 characters in output (ignored with --lbtt or --spin) Alexandre Duret-Lutz committed May 13, 2015 304 305 306 --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 307 308 309 310 311 '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 312 acceptance sets as bullets, (B) bullets except for Alexandre Duret-Lutz committed Jan 08, 2016 313 Büchi/co-Büchi automata, (c) force circular Alexandre Duret-Lutz committed May 13, 2015 314 315 316 317 318 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 319 320 321 322 323 324 325 326 327 328 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 329 --lbtt[=t] LBTT's format (add =t to force transition-based Alexandre Duret-Lutz committed Jan 08, 2016 330 acceptance even on Büchi automata) Alexandre Duret-Lutz committed Jan 06, 2015 331 --name=FORMAT set the name of the output automaton Alexandre Duret-Lutz committed Mar 17, 2015 332 333 334 -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 335 -q, --quiet suppress all normal output Alexandre Duret-Lutz committed Jan 31, 2015 336 337 338 -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 339 340 --stats=FORMAT output statistics about the automaton #+end_example Alexandre Duret-Lutz committed Apr 09, 2013 341 Alexandre Duret-Lutz committed Apr 09, 2013 342 Option =-8= can be used to improve the readability of the output Alexandre Duret-Lutz committed Apr 09, 2013 343 344 345 if your system can display UTF-8 correctly. #+NAME: dotex2ba8 Alexandre Duret-Lutz committed Mar 17, 2015 346 #+BEGIN_SRC sh :results verbatim :exports code Alexandre Duret-Lutz committed Jan 08, 2016 347 ltl2tgba -B8 "GFa & GFb" -d Alexandre Duret-Lutz committed Apr 09, 2013 348 349 350 351 #+END_SRC #+RESULTS: dotex2ba8 #+begin_example digraph G { Alexandre Duret-Lutz committed Jan 06, 2015 352 rankdir=LR Alexandre Duret-Lutz committed Mar 17, 2015 353 354 355 fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"] Alexandre Duret-Lutz committed Mar 26, 2015 356 node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7] Alexandre Duret-Lutz committed Jan 06, 2015 357 358 I [label="", style=invis, width=0] I -> 0 Alexandre Duret-Lutz committed Mar 26, 2015 359 0 [label=<0 >] Alexandre Duret-Lutz committed Mar 17, 2015 360 361 362 0 -> 0 [label=] 0 -> 1 [label=] 0 -> 2 [label=] Alexandre Duret-Lutz committed Mar 26, 2015 363 1 [label=<1>] Alexandre Duret-Lutz committed Mar 17, 2015 364 365 366 1 -> 0 [label=] 1 -> 1 [label=] 1 -> 2 [label=] Alexandre Duret-Lutz committed Mar 26, 2015 367 2 [label=<2>] Alexandre Duret-Lutz committed Mar 17, 2015 368 369 2 -> 0 [label= ] 2 -> 2 [label=] Alexandre Duret-Lutz committed Apr 09, 2013 370 371 372 } #+end_example Alexandre Duret-Lutz committed Nov 22, 2017 373 #+BEGIN_SRC dot :file dotex2ba8.svg :var txt=dotex2ba8 :exports results Alexandre Duret-Lutz committed Apr 09, 2013 374 375 376$txt #+END_SRC #+RESULTS: Alexandre Duret-Lutz committed Nov 22, 2017 377 [[file:dotex2ba8.svg]] Alexandre Duret-Lutz committed Apr 09, 2013 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 * 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 395 396 :: ((!(b))) -> goto T0_S2 :: ((!(a)) && (b)) -> goto T0_S3 Alexandre Duret-Lutz committed Apr 09, 2013 397 398 399 fi; T0_S2: if Alexandre Duret-Lutz committed Jan 06, 2015 400 401 402 :: ((a) && (b)) -> goto accept_init :: ((!(b))) -> goto T0_S2 :: ((!(a)) && (b)) -> goto T0_S3 Alexandre Duret-Lutz committed Apr 09, 2013 403 404 405 fi; T0_S3: if Alexandre Duret-Lutz committed Jan 06, 2015 406 407 :: ((a)) -> goto accept_init :: ((!(a))) -> goto T0_S3 Alexandre Duret-Lutz committed Apr 09, 2013 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 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 433 434 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 435 deterministic (=--deterministic=) automaton? Alexandre Duret-Lutz committed Apr 09, 2013 436 437 #+BEGIN_SRC sh :results verbatim :exports results Alexandre Duret-Lutz committed Oct 26, 2015 438 ltl2tgba --help | sed -n '/Simplification goal:/,/^$/p' | sed '1d;$d' Alexandre Duret-Lutz committed Apr 09, 2013 439 440 #+END_SRC #+RESULTS: Alexandre Duret-Lutz committed May 13, 2015 441 442 : -a, --any no preference, do not bother making it small or : deterministic Alexandre Duret-Lutz committed Apr 09, 2013 443 444 445 : -D, --deterministic prefer deterministic automata : --small prefer small automata (default) Alexandre Duret-Lutz committed May 13, 2015 446 447 448 449 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 450 Alexandre Duret-Lutz committed May 13, 2015 451 452 453 454 455 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 456 457 458 459 460 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 461 462 463 464 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 Feb 12, 2016 465 466 467 468 469 470 471 In particular, for properties more complex than obligations, it is possible that no deterministic TGBA exist, and even if it exists, =ltl2tgba= might not find it: so a non-deterministic automaton can be returned in this case. If you absolutely want a deterministic automaton, [[#generic][read on about the =--generic= option below]]. Alexandre Duret-Lutz committed Apr 09, 2013 472 473 474 475 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 476 #+BEGIN_SRC sh :results verbatim :exports code Alexandre Duret-Lutz committed Jan 08, 2016 477 ltl2tgba 'Ga|Gb|Gc' -d Alexandre Duret-Lutz committed Apr 09, 2013 478 479 480 481 #+END_SRC #+RESULTS: gagbgc1 #+begin_example digraph G { Alexandre Duret-Lutz committed Jan 06, 2015 482 rankdir=LR Alexandre Duret-Lutz committed May 13, 2015 483 node [shape="circle"] Alexandre Duret-Lutz committed Mar 17, 2015 484 485 486 fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"] Alexandre Duret-Lutz committed Mar 26, 2015 487 node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7] Alexandre Duret-Lutz committed Jan 06, 2015 488 489 I [label="", style=invis, width=0] I -> 0 Alexandre Duret-Lutz committed Mar 26, 2015 490 0 [label=<0>] Alexandre Duret-Lutz committed Mar 17, 2015 491 492 493 0 -> 1 [label=] 0 -> 2 [label=] 0 -> 3 [label=] Alexandre Duret-Lutz committed Mar 26, 2015 494 1 [label=<1>] Alexandre Duret-Lutz committed Mar 17, 2015 495 1 -> 1 [label=] Alexandre Duret-Lutz committed Mar 26, 2015 496 2 [label=<2>] Alexandre Duret-Lutz committed Mar 17, 2015 497 2 -> 2 [label=] Alexandre Duret-Lutz committed Mar 26, 2015 498 3 [label=<3>] Alexandre Duret-Lutz committed Mar 17, 2015 499 3 -> 3 [label=] Alexandre Duret-Lutz committed Apr 09, 2013 500 501 502 } #+end_example Alexandre Duret-Lutz committed Nov 22, 2017 503 #+BEGIN_SRC dot :file gagbgc1.svg :var txt=gagbgc1 :exports results Alexandre Duret-Lutz committed Apr 09, 2013 504 505 506 $txt #+END_SRC #+RESULTS: Alexandre Duret-Lutz committed Nov 22, 2017 507 [[file:gagbgc1.svg]] Alexandre Duret-Lutz committed Apr 09, 2013 508 Alexandre Duret-Lutz committed Mar 17, 2015 509 #+NAME: gagbgc2 Alexandre Duret-Lutz committed Apr 09, 2013 510 #+BEGIN_SRC sh :results verbatim :exports code Alexandre Duret-Lutz committed Jan 08, 2016 511 ltl2tgba -D 'Ga|Gb|Gc' -d Alexandre Duret-Lutz committed Apr 09, 2013 512 513 514 515 #+END_SRC #+RESULTS: gagbgc2 #+begin_example digraph G { Alexandre Duret-Lutz committed Jan 06, 2015 516 rankdir=LR Alexandre Duret-Lutz committed May 13, 2015 517 node [shape="circle"] Alexandre Duret-Lutz committed Mar 17, 2015 518 519 520 fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"] Alexandre Duret-Lutz committed Mar 26, 2015 521 node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7] Alexandre Duret-Lutz committed Jan 06, 2015 522 523 I [label="", style=invis, width=0] I -> 6 Alexandre Duret-Lutz committed May 13, 2015 524 0 [label="0", peripheries=2] Alexandre Duret-Lutz committed Mar 17, 2015 525 0 -> 0 [label=] Alexandre Duret-Lutz committed May 13, 2015 526 1 [label="1", peripheries=2] Alexandre Duret-Lutz committed Mar 17, 2015 527 528 529 1 -> 0 [label=] 1 -> 1 [label=] 1 -> 2 [label=] Alexandre Duret-Lutz committed May 13, 2015 530 2 [label="2", peripheries=2] Alexandre Duret-Lutz committed Mar 17, 2015 531 2 -> 2 [label=] Alexandre Duret-Lutz committed May 13, 2015 532 3 [label="3", peripheries=2] Alexandre Duret-Lutz committed Mar 17, 2015 533 534 535 3 -> 2 [label=] 3 -> 3 [label=] 3 -> 5 [label=] Alexandre Duret-Lutz committed May 13, 2015 536 4 [label="4", peripheries=2] Alexandre Duret-Lutz committed Mar 17, 2015 537 538 539 4 -> 0 [label=] 4 -> 4 [label=] 4 -> 5 [label=] Alexandre Duret-Lutz committed May 13, 2015 540 5 [label="5", peripheries=2] Alexandre Duret-Lutz committed Mar 17, 2015 541 5 -> 5 [label=] Alexandre Duret-Lutz committed May 13, 2015 542 6 [label="6", peripheries=2] Alexandre Duret-Lutz committed Mar 17, 2015 543 544 545 546 547 548 549 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 550 551 552 } #+end_example Alexandre Duret-Lutz committed Nov 22, 2017 553 #+BEGIN_SRC dot :file gagbgc2.svg :var txt=gagbgc2 :exports results Alexandre Duret-Lutz committed Apr 09, 2013 554 555 556$txt #+END_SRC #+RESULTS: Alexandre Duret-Lutz committed Nov 22, 2017 557 [[file:gagbgc2.svg]] Alexandre Duret-Lutz committed Apr 09, 2013 558 559 560 561 562 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 563 Add the =-C= or =--complete= option if you want to obtain a complete Alexandre Duret-Lutz committed Sep 08, 2013 564 565 566 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 567 568 569 570 571 572 573 574 575 576 577 578 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 579 ltl2tgba -B 'GFa -> GFb' -d Alexandre Duret-Lutz committed May 13, 2015 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 #+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 Alexandre Duret-Lutz committed Nov 22, 2017 607 #+BEGIN_SRC dot :file ambig1.svg :var txt=ambig1 :exports results Alexandre Duret-Lutz committed May 13, 2015 608 609 610 $txt #+END_SRC #+RESULTS: Alexandre Duret-Lutz committed Nov 22, 2017 611 [[file:ambig1.svg]] Alexandre Duret-Lutz committed May 13, 2015 612 613 614 615 616 617 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 618 ltl2tgba -B -U 'GFa -> GFb' -d Alexandre Duret-Lutz committed May 13, 2015 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 646 647 648 649 650 651 652 653 654 #+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 Alexandre Duret-Lutz committed Nov 22, 2017 655 #+BEGIN_SRC dot :file ambig2.svg :var txt=ambig2 :exports results Alexandre Duret-Lutz committed May 13, 2015 656 657 658 659$txt #+END_SRC #+RESULTS: Alexandre Duret-Lutz committed Nov 22, 2017 660 [[file:ambig2.svg]] Alexandre Duret-Lutz committed May 13, 2015 661 662 663 664 665 666 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 667 Alexandre Duret-Lutz committed Apr 09, 2013 668 669 670 671 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 672 ltl2tgba --help | sed -n '/Simplification level:/,/^$/p' | sed '1d;$d' Alexandre Duret-Lutz committed Apr 09, 2013 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 #+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 688 689 produced by the core translator. The algorithms used during post-processing are Alexandre Duret-Lutz committed Apr 09, 2013 690 691 692 693 694 695 696 697 - 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 698 - BA simulation (again direct or iterated) Alexandre Duret-Lutz committed Apr 09, 2013 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 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. Alexandre Duret-Lutz committed Jan 08, 2018 721 * Deterministic automata with =--generic --deterministic= Alexandre Duret-Lutz committed Feb 12, 2016 722 723 724 725 726 727 :PROPERTIES: :CUSTOM_ID: generic :END: The =--generic= (or =-G=) option allows =ltl2tgba= to use more complex acceptance. Combined with =--deterministic= (or =-D=) this Alexandre Duret-Lutz committed Aug 06, 2016 728 729 allows the use of a determinization algorithm that produces automata with parity acceptance. Alexandre Duret-Lutz committed Feb 12, 2016 730 731 732 733 734 For instance =FGa= is the typical formula for which not deterministic TGBA exists. #+NAME: ltl2tgba-fga Alexandre Duret-Lutz committed Feb 12, 2016 735 #+BEGIN_SRC sh :results verbatim :exports code Alexandre Duret-Lutz committed Mar 10, 2018 736 ltl2tgba "FGa" -D -d Alexandre Duret-Lutz committed Feb 12, 2016 737 738 #+END_SRC Alexandre Duret-Lutz committed Nov 22, 2017 739 #+BEGIN_SRC dot :file ltl2tgba-fga.svg :var txt=ltl2tgba-fga :exports results Alexandre Duret-Lutz committed Feb 12, 2016 740 741 742 743 $txt #+END_SRC #+RESULTS: Alexandre Duret-Lutz committed Nov 22, 2017 744 [[file:ltl2tgba-fga.svg]] Alexandre Duret-Lutz committed Feb 12, 2016 745 746 747 748 But with =--generic=, =ltl2tgba= will output the following Rabin automaton: #+NAME: ltl2tgba-fga-D Alexandre Duret-Lutz committed Feb 12, 2016 749 #+BEGIN_SRC sh :results verbatim :exports code Alexandre Duret-Lutz committed Mar 10, 2018 750 ltl2tgba "FGa" -G -D -d Alexandre Duret-Lutz committed Feb 12, 2016 751 752 #+END_SRC Alexandre Duret-Lutz committed Nov 22, 2017 753 #+BEGIN_SRC dot :file ltl2tgba-fga-D.svg :var txt=ltl2tgba-fga-D :exports results Alexandre Duret-Lutz committed Feb 12, 2016 754 755 756 757$txt #+END_SRC #+RESULTS: Alexandre Duret-Lutz committed Nov 22, 2017 758 [[file:ltl2tgba-fga-D.svg]] Alexandre Duret-Lutz committed Feb 12, 2016 759 760 761 762 763 Note that determinization algorithm implemented actually outputs parity acceptance, but =Fin(0)&Inf(1)= can be interpreted either as =Rabin 1= or =parity min odd 2=. Alexandre Duret-Lutz committed Feb 12, 2016 764 765 766 The [[./man/spot-x.7.html][=spot-x=]](7) man page lists a few =-x= options (=det-scc=, =det-simul=, =det-stutter=) of the determinization algorithm that are Alexandre Duret-Lutz committed Aug 06, 2016 767 enabled by default, but that you may want to disable for experimental Alexandre Duret-Lutz committed Feb 12, 2016 768 769 770 771 772 773 purpose. For instance the following deterministic automaton #+NAME: ltl2tgba-det1 #+BEGIN_SRC sh :results verbatim :exports code Alexandre Duret-Lutz committed Mar 10, 2018 774 ltl2tgba "F(a W FGb)" -G -D -d Alexandre Duret-Lutz committed Feb 12, 2016 775 776 #+END_SRC Alexandre Duret-Lutz committed Nov 22, 2017 777 #+BEGIN_SRC dot :file ltl2tgba-det1.svg :var txt=ltl2tgba-det1 :exports results Alexandre Duret-Lutz committed Feb 12, 2016 778 779 780 781 $txt #+END_SRC #+RESULTS: Alexandre Duret-Lutz committed Nov 22, 2017 782 [[file:ltl2tgba-det1.svg]] Alexandre Duret-Lutz committed Feb 12, 2016 783 784 785 786 787 would be larger if SCC-based optimizations were disabled: #+NAME: ltl2tgba-det2 #+BEGIN_SRC sh :results verbatim :exports code Alexandre Duret-Lutz committed Mar 10, 2018 788 ltl2tgba "F(a W FGb)" -x '!det-scc' -G -D -d Alexandre Duret-Lutz committed Feb 12, 2016 789 790 #+END_SRC Alexandre Duret-Lutz committed Nov 22, 2017 791 #+BEGIN_SRC dot :file ltl2tgba-det2.svg :var txt=ltl2tgba-det2 :exports results Alexandre Duret-Lutz committed Feb 12, 2016 792 793 794 795$txt #+END_SRC #+RESULTS: Alexandre Duret-Lutz committed Nov 22, 2017 796 [[file:ltl2tgba-det2.svg]] Alexandre Duret-Lutz committed Feb 12, 2016 797 Alexandre Duret-Lutz committed Jan 08, 2018 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 While the =--generic= option currently only builds automata with generalized-Büchi or parity acceptance, this is very likely to change in the future. * Deterministic automata with =--parity --deterministic= Using the =--parity= (or upper-case =-P=) option will force the acceptance condition to be of a parity type. This has to be understood in the sense of the HOA format, where: - multiple parity types are defined (=min odd n=, =min even n=, =max odd n=, and =max even n= where =n= is the number of acceptance sets), and - the parity acceptance is only a type of acceptance condition, i.e., a formula expressed in terms of acceptance sets, and does not have additional constraints on these sets. In particular it is not necessary the case that each transition or state belongs to exactly one acceptance set (this is the "colored" property, see below). Under these assumptions, Büchi acceptance is just one kind of parity (in HOA =Buchi= is equivalent to =parity max even 1= or =parity min even 1=), Rabin with one pair is also a parity acceptance (=Rabin 1= is equivalent to =parity min odd 2=), and Streett with one pair as well (=Streett 1= is equivalent to =parity max odd 2=). In the current implementation, using =ltl2tgba --parity= (without =--deterministic=) will always produce a Büchi automaton, and when =--deterministic= (or =-D=) is added, it will produce an deterministic automaton with Büchi acceptance (=parity min even 1=) or with =parity min odd n= acceptance, because the latter is the type of parity acceptance that our determinization procedure outputs. For instance, =FGa= gets translated into an automaton with =Rabin 1= acceptance (another name for =parity min odd 2=): #+NAME: ltl2tgba-dp1 #+BEGIN_SRC sh :results verbatim :exports code Alexandre Duret-Lutz committed Mar 10, 2018 834 ltl2tgba "FGa" -D -P -d Alexandre Duret-Lutz committed Jan 08, 2018 835 836 837 838 839 840 841 842 843 844 845 846 847 848 #+END_SRC #+BEGIN_SRC dot :file ltl2tgba-dp1.svg :var txt=ltl2tgba-dp1 :exports results $txt #+END_SRC #+RESULTS: [[file:ltl2tgba-dp1.svg]] And =GFa & GFb= gets translated into a =Büchi= automaton (another name for =parity min even 1=): #+NAME: ltl2tgba-dp2 #+BEGIN_SRC sh :results verbatim :exports code Alexandre Duret-Lutz committed Mar 10, 2018 849 ltl2tgba "GFa & GFb" -D -P -d Alexandre Duret-Lutz committed Jan 08, 2018 850 851 852 853 854 855 856 857 858 859 860 861 862 863 #+END_SRC #+BEGIN_SRC dot :file ltl2tgba-dp2.svg :var txt=ltl2tgba-dp2 :exports results$txt #+END_SRC #+RESULTS: [[file:ltl2tgba-dp2.svg]] If we really want to use the same style of parity acceptance for all outputs, we can specify it as an argument to the =--parity= option. For instance #+NAME: ltl2tgba-dp3 #+BEGIN_SRC sh :results verbatim :exports code Alexandre Duret-Lutz committed Mar 10, 2018 864 ltl2tgba "GFa & GFb" -D -P'min odd' -d Alexandre Duret-Lutz committed Jan 08, 2018 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 #+END_SRC #+BEGIN_SRC dot :file ltl2tgba-dp3.svg :var txt=ltl2tgba-dp3 :exports results $txt #+END_SRC #+RESULTS: [[file:ltl2tgba-dp3.svg]] The =--colored-parity= (or lower-case =-p=) option works similarly to =--parity=, but additionally requests that the automaton be colored. I.e., each transition (or state if state-based acceptance is requested) should belong to exactly one acceptance set. #+NAME: ltl2tgba-dp4 #+BEGIN_SRC sh :results verbatim :exports code Alexandre Duret-Lutz committed Mar 10, 2018 882 ltl2tgba "GFa & GFb" -D -p -d Alexandre Duret-Lutz committed Jan 08, 2018 883 884 885 886 887 888 889 890 891 892 893 #+END_SRC #+BEGIN_SRC dot :file ltl2tgba-dp4.svg :var txt=ltl2tgba-dp4 :exports results$txt #+END_SRC #+RESULTS: [[file:ltl2tgba-dp4.svg]] #+NAME: ltl2tgba-dp5 #+BEGIN_SRC sh :results verbatim :exports code Alexandre Duret-Lutz committed Mar 10, 2018 894 ltl2tgba "GFa & GFb" -D -p'min odd' -d Alexandre Duret-Lutz committed Jan 08, 2018 895 896 897 898 899 900 901 902 903 904 905 906 907 908 #+END_SRC #+BEGIN_SRC dot :file ltl2tgba-dp5.svg :var txt=ltl2tgba-dp5 :exports results $txt #+END_SRC #+RESULTS: [[file:ltl2tgba-dp5.svg]] Note that all these options can be combined with state-based acceptance if needed: #+NAME: ltl2tgba-dp6 #+BEGIN_SRC sh :results verbatim :exports code Alexandre Duret-Lutz committed Mar 10, 2018 909 ltl2tgba "GFa & GFb" -D -S -p'max even' -d Alexandre Duret-Lutz committed Jan 08, 2018 910 911 912 913 914 915 916 917 918 #+END_SRC #+BEGIN_SRC dot :file ltl2tgba-dp6.svg :var txt=ltl2tgba-dp6 :exports results$txt #+END_SRC #+RESULTS: [[file:ltl2tgba-dp6.svg]] Alexandre Duret-Lutz committed Apr 09, 2013 919 920 921 * Translating multiple formulas for statistics If multiple formulas are given to =ltl2tgba=, the corresponding Alexandre Duret-Lutz committed Aug 06, 2016 922 923 924 925 automata will be output one after the other. The default output format HOA is designed to allow streaming automata this way to build processing pipelines, but Spot's automaton parser can also read a stream of automata in other formats. Alexandre Duret-Lutz committed Apr 09, 2013 926 Alexandre Duret-Lutz committed Aug 06, 2016 927 928 Another situation where passing many formulas to =ltl2tgba= is useful is in combination with the =--stats=FORMAT= option. This option will Alexandre Duret-Lutz committed Apr 09, 2013 929 930 931 932 933 934 935 936 937 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 938 939 940 941 #+begin_example %% a single % %a number of acceptance sets %c number of SCCs Alexandre Duret-Lutz committed Jan 06, 2015 942 %d 1 if the output is deterministic, 0 otherwise Alexandre Duret-Lutz committed Dec 06, 2013 943 944 %e number of edges %f the formula, in Spot's syntax Alexandre Duret-Lutz committed Jan 06, 2015 945 %F name of the input file Alexandre Duret-Lutz committed Jan 08, 2016 946 %g acceptance condition (in HOA syntax) Alexandre Duret-Lutz committed Jan 06, 2015 947 948 949 950 951 %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 952 953 %s number of states %t number of transitions Alexandre Duret-Lutz committed Jan 06, 2015 954 %w one word accepted by the output automaton Alexandre Duret-Lutz committed Dec 06, 2013 955 #+end_example Alexandre Duret-Lutz committed Apr 09, 2013 956 957 958 959 960 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 Alexandre Duret-Lutz committed Jul 19, 2016 961 genltl --u-right=1..8 | ltl2tgba --stats '%s states and %e edges for "%f"' Alexandre Duret-Lutz committed Apr 09, 2013 962 963 964 965 966 967 968 969 970 971 972 #+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))))))" Alexandre Duret-Lutz committed Jul 19, 2016 973 974 975 976 977 Note that because no formula have been passed as argument to =ltl2tgba=, it defaulted to reading them from standard input. Such a behaviour can be requested explicitly with =-F -= if needed (e.g., to read from standard input in addition to processing other formula supplied with =-f=). Alexandre Duret-Lutz committed Apr 09, 2013 978 979 980 981 982 983 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. Alexandre Duret-Lutz committed Aug 06, 2016 984 985 986 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=. Alexandre Duret-Lutz committed Apr 09, 2013 987 988 989 990 991 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 992 993 994 [[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 995 * Building Monitors Alexandre Duret-Lutz committed Mar 03, 2017 996 997 998 :PROPERTIES: :CUSTOM_ID: monitors :END: Alexandre Duret-Lutz committed Apr 09, 2013 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 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 1010 #+NAME: monitor1 Alexandre Duret-Lutz committed Apr 09, 2013 1011 #+BEGIN_SRC sh :results verbatim :exports code Alexandre Duret-Lutz committed Jan 08, 2016 1012 ltl2tgba -M '(Xa & Fb) | Gc' -d Alexandre Duret-Lutz committed Apr 09, 2013 1013 1014 1015 1016 1017 #+END_SRC #+RESULTS: monitor1 #+begin_example digraph G { Alexandre Duret-Lutz committed Jan 06, 2015 1018 rankdir=LR Alexandre Duret-Lutz committed Jan 08, 2016 1019 node [shape="circle"] Alexandre Duret-Lutz committed Mar 17, 2015 1020 1021 1022 fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"] Alexandre Duret-Lutz committed Mar 26, 2015 1023 node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7] Alexandre Duret-Lutz committed Jan 06, 2015 1024 1025 I [label="", style=invis, width=0] I -> 0 Alexandre Duret-Lutz committed Mar 26, 2015 1026 0 [label=<0>] Alexandre Duret-Lutz committed Mar 17, 2015 1027 1028 0 -> 1 [label=<1>] 0 -> 3 [label=] Alexandre Duret-Lutz committed Mar 26, 2015 1029 1 [label=<1>] Alexandre Duret-Lutz committed Mar 17, 2015 1030 1 -> 2 [label=] Alexandre Duret-Lutz committed Mar 26, 2015 1031 2 [label=<2>] Alexandre Duret-Lutz committed Mar 17, 2015 1032 2 -> 2 [label=<1>] Alexandre Duret-Lutz committed Mar 26, 2015 1033 3 [label=<3>] Alexandre Duret-Lutz committed Mar 17, 2015 1034 3 -> 3 [label=] Alexandre Duret-Lutz committed Apr 09, 2013 1035 1036 1037 } #+end_example Alexandre Duret-Lutz committed Nov 22, 2017 1038 #+BEGIN_SRC dot :file monitor1.svg :var txt=monitor1 :exports results Alexandre Duret-Lutz committed Apr 09, 2013 1039 1040 1041 1042 $txt #+END_SRC #+RESULTS: Alexandre Duret-Lutz committed Nov 22, 2017 1043 [[file:monitor1.svg]] Alexandre Duret-Lutz committed Apr 09, 2013 1044 Alexandre Duret-Lutz committed Mar 17, 2015 1045 #+NAME: monitor2 Alexandre Duret-Lutz committed Apr 09, 2013 1046 #+BEGIN_SRC sh :results verbatim :exports code Alexandre Duret-Lutz committed Jan 08, 2016 1047 ltl2tgba -MD '(Xa & Fb) | Gc' -d Alexandre Duret-Lutz committed Apr 09, 2013 1048 1049 #+END_SRC Alexandre Duret-Lutz committed Nov 22, 2017 1050 #+BEGIN_SRC dot :file monitor2.svg :var txt=monitor2 :exports results Alexandre Duret-Lutz committed Apr 09, 2013 1051 1052 1053 1054$txt #+END_SRC #+RESULTS: Alexandre Duret-Lutz committed Nov 22, 2017 1055 [[file:monitor2.svg]] Alexandre Duret-Lutz committed Apr 09, 2013 1056 1057 1058 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 1059 1060 such as =F(a)=: indeed, any finite execution can be extended to match =F(a)=. Alexandre Duret-Lutz committed Apr 09, 2013 1061 Alexandre Duret-Lutz committed Mar 03, 2017 1062 1063 For more discussion and examples about monitor, see also our [[file:tut11.org][separate page showing how to build them in Python and C++]]. Alexandre Duret-Lutz committed Mar 03, 2017 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 Because Monitors accept every recognized run (in other words, they only reject words that are not recognized), it makes little sense to use option =-C= to request /complete/ monitors. If uou combine =-C= with =-M=, the result will output as a Büchi automaton if (and only if) a sink state had to be added. For instance, here is the "complete" version of the previous monitor. #+NAME: monitor3 #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba -C -M -D '(Xa & Fb) | Gc' -d #+END_SRC Alexandre Duret-Lutz committed Nov 22, 2017 1077 #+BEGIN_SRC dot :file monitor3.svg :var txt=monitor3 :exports results Alexandre Duret-Lutz committed Mar 03, 2017 1078 1079 1080 1081 \$txt #+END_SRC #+RESULTS: Alexandre Duret-Lutz committed Nov 22, 2017 1082 [[file:monitor3.svg]] Alexandre Duret-Lutz committed Mar 03, 2017 1083 1084 1085 1086 Alexandre Duret-Lutz committed Apr 09, 2013 1087 1088 1089 1090 1091 1092 1093 1094 # 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