ltl2tgba.org 37.2 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 Jun 27, 2018 4 #+INCLUDE: setup.org  Alexandre Duret-Lutz committed Jan 07, 2015 5 #+HTML_LINK_UP: tools.html  Alexandre Duret-Lutz committed Apr 17, 2019 6 #+PROPERTY: header-args:sh :results verbatim :exports both  Alexandre Duret-Lutz committed Apr 09, 2013 7   Alexandre Duret-Lutz committed Feb 12, 2016 8 9 10 11 This tool translates LTL or PSL formulas into different types of automata. The inner algorithm produces Transition-based Generalized Büchi  Alexandre Duret-Lutz committed Jun 27, 2018 12 Automata, hence the name of the tool, but =ltl2tgba= has grown and  Alexandre Duret-Lutz committed Feb 12, 2016 13 14 15 16 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 17 18 - =--tgba= (the default) outputs Transition-based Generalized Büchi Automata  Alexandre Duret-Lutz committed Feb 12, 2016 19 - =--ba= (or =-B=) outputs state-based Büchi automata  Alexandre Duret-Lutz committed Jan 08, 2018 20 21 - =--monitor= (or =-M=) outputs monitors - =--generic --deterministic= (or =-DG=) will do whatever it takes to  Alexandre Duret-Lutz committed Jun 20, 2018 22 23  produce a deterministic automaton, and may use any acceptance condition  Alexandre Duret-Lutz committed Jan 08, 2018 24 25 - =--parity --deterministic= (or =-DP=) will produce a deterministic automaton with parity acceptance.  Alexandre Duret-Lutz committed Apr 09, 2013 26   Alexandre Duret-Lutz committed Jun 27, 2018 27 28 29 (The latter two can also be used with =--deterministic=, but that is less frequent.)  Alexandre Duret-Lutz committed Apr 09, 2013 30 31 32 33 34 * TGBA and BA Formulas to translate may be specified using [[file:ioltl.org][common input options for LTL/PSL formulas]].  Alexandre Duret-Lutz committed Jul 30, 2019 35 #+BEGIN_SRC sh :wrap SRC hoa  Alexandre Duret-Lutz committed Apr 09, 2013 36 37 ltl2tgba -f 'Fa & GFb' #+END_SRC  Alexandre Duret-Lutz committed Jan 08, 2016 38   Alexandre Duret-Lutz committed Apr 09, 2013 39 #+RESULTS:  Alexandre Duret-Lutz committed Jul 30, 2019 40 #+begin_SRC hoa  Alexandre Duret-Lutz committed Jan 08, 2016 41 42 43 HOA: v1 name: "Fa & GFb" States: 2  Alexandre Duret-Lutz committed Jul 30, 2019 44 Start: 0  Alexandre Duret-Lutz committed Jan 08, 2016 45 46 47 48 49 50 51 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  Alexandre Duret-Lutz committed Jul 30, 2019 52 53 [!0] 0 [0] 1  Alexandre Duret-Lutz committed Jan 08, 2016 54 State: 1  Alexandre Duret-Lutz committed Jul 30, 2019 55 56 [!1] 1 [1] 1 {0}  Alexandre Duret-Lutz committed Jan 08, 2016 57 --END--  Alexandre Duret-Lutz committed Jul 30, 2019 58 #+end_SRC  Alexandre Duret-Lutz committed Apr 09, 2013 59 60 61 62 63 64 65  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 66 =ltl2tgba= honors the [[file:oaut.org][common options for selecting the output format]].  Alexandre Duret-Lutz committed Jan 08, 2016 67 68 69 70 71 72 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 17, 2019 73 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Jan 08, 2016 74 ltl2tgba "Fa & GFb" -d | dot -Tpdf > tgba.pdf  Alexandre Duret-Lutz committed Apr 09, 2013 75 76 77 #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Mar 17, 2015 78 The result would look like this (note that in this documentation  Alexandre Duret-Lutz committed Aug 06, 2016 79 we use some [[file:oaut.org::#default-dot][environment variables]] to produce a more colorful  Alexandre Duret-Lutz committed Mar 17, 2015 80 output by default)  Alexandre Duret-Lutz committed Apr 09, 2013 81 #+NAME: dotex  Alexandre Duret-Lutz committed Apr 17, 2019 82 #+BEGIN_SRC sh :exports none  Alexandre Duret-Lutz committed Jan 08, 2016 83 ltl2tgba "Fa & GFb" -d  Alexandre Duret-Lutz committed Apr 09, 2013 84 85 #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 86 #+BEGIN_SRC dot :file dotex.svg :var txt=dotex :exports results  Alexandre Duret-Lutz committed Apr 09, 2013 87 88 89 90 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 91 [[file:dotex.svg]]  Alexandre Duret-Lutz committed Apr 09, 2013 92   Alexandre Duret-Lutz committed Mar 17, 2015 93 94 95 96 97 98 99 100 101 102 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 103 104 105 106 107  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 Apr 17, 2019 108 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Jan 08, 2016 109 ltl2tgba "GFa & GFb" -d  Alexandre Duret-Lutz committed Apr 09, 2013 110 111 #+END_SRC #+RESULTS: dotex2  Alexandre Duret-Lutz committed Jan 06, 2015 112 113 114 #+begin_example digraph G { rankdir=LR  Alexandre Duret-Lutz committed Mar 17, 2015 115 116 117  fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"]  Alexandre Duret-Lutz committed Mar 26, 2015 118  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]  Alexandre Duret-Lutz committed Jan 06, 2015 119 120 121  I [label="", style=invis, width=0] I -> 0 0 [label="0"]  Alexandre Duret-Lutz committed Mar 17, 2015 122 123 124 125  0 -> 0 [label=>] 0 -> 0 [label=] 0 -> 0 [label=>] 0 -> 0 [label=>]  Alexandre Duret-Lutz committed Jan 06, 2015 126 127 } #+end_example  Alexandre Duret-Lutz committed Apr 09, 2013 128   Alexandre Duret-Lutz committed Nov 22, 2017 129 #+BEGIN_SRC dot :file dotex2.svg :var txt=dotex2 :exports results  Alexandre Duret-Lutz committed Apr 09, 2013 130 131 132 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 133 [[file:dotex2.svg]]  Alexandre Duret-Lutz committed Apr 09, 2013 134   Alexandre Duret-Lutz committed Mar 10, 2018 135 The above TGBA has two acceptance sets: ⓿ and ❶. The definition of  Alexandre Duret-Lutz committed Jan 06, 2015 136 137 these acceptance sets ensures that atomic propositions =a= and =b= must be true infinitely often.  Alexandre Duret-Lutz committed Apr 09, 2013 138 139 140 141  A Büchi automaton for the previous formula can be obtained with the =-B= option:  Alexandre Duret-Lutz committed Mar 17, 2015 142 #+NAME: dotex2ba  Alexandre Duret-Lutz committed Apr 17, 2019 143 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Jan 08, 2016 144 ltl2tgba -B 'GFa & GFb' -d  Alexandre Duret-Lutz committed Apr 09, 2013 145 146 147 148 #+END_SRC #+RESULTS: dotex2ba #+begin_example digraph G {  Alexandre Duret-Lutz committed Jan 06, 2015 149  rankdir=LR  Alexandre Duret-Lutz committed May 13, 2015 150  node [shape="circle"]  Alexandre Duret-Lutz committed Mar 17, 2015 151 152 153  fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"]  Alexandre Duret-Lutz committed Mar 26, 2015 154  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]  Alexandre Duret-Lutz committed Jan 06, 2015 155 156  I [label="", style=invis, width=0] I -> 0  Alexandre Duret-Lutz committed May 13, 2015 157  0 [label="0", peripheries=2]  Alexandre Duret-Lutz committed Mar 17, 2015 158 159 160  0 -> 0 [label=] 0 -> 1 [label=] 0 -> 2 [label=]  Alexandre Duret-Lutz committed May 13, 2015 161  1 [label="1"]  Alexandre Duret-Lutz committed Mar 17, 2015 162 163 164  1 -> 0 [label=] 1 -> 1 [label=] 1 -> 2 [label=]  Alexandre Duret-Lutz committed May 13, 2015 165  2 [label="2"]  Alexandre Duret-Lutz committed Mar 17, 2015 166 167  2 -> 0 [label=] 2 -> 2 [label=]  Alexandre Duret-Lutz committed Apr 09, 2013 168 169 170 } #+end_example  Alexandre Duret-Lutz committed Nov 22, 2017 171 #+BEGIN_SRC dot :file dotex2ba.svg :var txt=dotex2ba :exports results  Alexandre Duret-Lutz committed Apr 09, 2013 172 173 174 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 175 [[file:dotex2ba.svg]]  Alexandre Duret-Lutz committed Apr 09, 2013 176   Alexandre Duret-Lutz committed May 13, 2015 177 178 179 180 181 182 183 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 184   Alexandre Duret-Lutz committed Apr 17, 2019 185 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Jan 06, 2015 186 187 188 189 ltl2tgba --dot=t -B 'GFa & GFb' #+END_SRC #+NAME: dotex2ba-t  Alexandre Duret-Lutz committed Apr 17, 2019 190 #+BEGIN_SRC sh :exports none  Alexandre Duret-Lutz committed Mar 17, 2015 191 ltl2tgba --dot=.t -B 'GFa & GFb'  Alexandre Duret-Lutz committed Jan 06, 2015 192 193 194 195 196 197 #+END_SRC #+RESULTS: dotex2ba-t #+begin_example digraph G { rankdir=LR  Alexandre Duret-Lutz committed Mar 17, 2015 198 199 200  fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"]  Alexandre Duret-Lutz committed Mar 26, 2015 201  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]  Alexandre Duret-Lutz committed Jan 06, 2015 202 203 204  I [label="", style=invis, width=0] I -> 0 0 [label="0"]  Alexandre Duret-Lutz committed Mar 17, 2015 205 206 207  0 -> 0 [label=>] 0 -> 1 [label=>] 0 -> 2 [label=>]  Alexandre Duret-Lutz committed Jan 06, 2015 208  1 [label="1"]  Alexandre Duret-Lutz committed Mar 17, 2015 209 210 211  1 -> 0 [label=] 1 -> 1 [label=] 1 -> 2 [label=]  Alexandre Duret-Lutz committed Jan 06, 2015 212  2 [label="2"]  Alexandre Duret-Lutz committed Mar 17, 2015 213 214  2 -> 0 [label=] 2 -> 2 [label=]  Alexandre Duret-Lutz committed Jan 06, 2015 215 216 217 } #+end_example  Alexandre Duret-Lutz committed Nov 22, 2017 218 #+BEGIN_SRC dot :file dotex2ba-t.svg :var txt=dotex2ba-t :exports results  Alexandre Duret-Lutz committed Jan 06, 2015 219 220 221 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 222 [[file:dotex2ba-t.svg]]  Alexandre Duret-Lutz committed Jan 06, 2015 223   Alexandre Duret-Lutz committed May 14, 2015 224 225 226 227 228 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  Alexandre Duret-Lutz committed Apr 17, 2019 229 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Jan 08, 2016 230 ltl2tgba -S 'GFa & GFb' -d  Alexandre Duret-Lutz committed May 14, 2015 231 232 #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 233 #+BEGIN_SRC dot :file dotex2gba.svg :var txt=dotex2gba :exports results  Alexandre Duret-Lutz committed May 14, 2015 234 235 236 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 237 [[file:dotex2gba.svg]]  Alexandre Duret-Lutz committed May 14, 2015 238 239 240 241 242 243 244  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 245 246 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 247   Alexandre Duret-Lutz committed Apr 17, 2019 248 #+BEGIN_SRC sh :exports results  Alexandre Duret-Lutz committed Apr 09, 2013 249 250 251 ltl2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Jan 06, 2015 252 253 254 #+begin_example -8, --utf8 enable UTF-8 characters in output (ignored with --lbtt or --spin)  Alexandre Duret-Lutz committed May 13, 2015 255 256 257  --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 258 259 260 261 262  '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 263  acceptance sets as bullets, (B) bullets except for  Alexandre Duret-Lutz committed Jan 08, 2016 264  Büchi/co-Büchi automata, (c) force circular  Alexandre Duret-Lutz committed May 13, 2015 265 266 267 268 269  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 270 271 272 273 274 275 276 277 278 279  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 280  --lbtt[=t] LBTT's format (add =t to force transition-based  Alexandre Duret-Lutz committed Jan 08, 2016 281  acceptance even on Büchi automata)  Alexandre Duret-Lutz committed Jan 06, 2015 282  --name=FORMAT set the name of the output automaton  Alexandre Duret-Lutz committed Mar 17, 2015 283 284 285  -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 286  -q, --quiet suppress all normal output  Alexandre Duret-Lutz committed Jan 31, 2015 287 288 289  -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 290 291  --stats=FORMAT output statistics about the automaton #+end_example  Alexandre Duret-Lutz committed Apr 09, 2013 292   Alexandre Duret-Lutz committed Apr 09, 2013 293 Option =-8= can be used to improve the readability of the output  Alexandre Duret-Lutz committed Apr 09, 2013 294 295 296 if your system can display UTF-8 correctly. #+NAME: dotex2ba8  Alexandre Duret-Lutz committed Apr 17, 2019 297 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Jan 08, 2016 298 ltl2tgba -B8 "GFa & GFb" -d  Alexandre Duret-Lutz committed Apr 09, 2013 299 300 301 302 #+END_SRC #+RESULTS: dotex2ba8 #+begin_example digraph G {  Alexandre Duret-Lutz committed Jan 06, 2015 303  rankdir=LR  Alexandre Duret-Lutz committed Mar 17, 2015 304 305 306  fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"]  Alexandre Duret-Lutz committed Mar 26, 2015 307  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]  Alexandre Duret-Lutz committed Jan 06, 2015 308 309  I [label="", style=invis, width=0] I -> 0  Alexandre Duret-Lutz committed Mar 26, 2015 310  0 [label=<0 >]  Alexandre Duret-Lutz committed Mar 17, 2015 311 312 313  0 -> 0 [label=] 0 -> 1 [label=] 0 -> 2 [label=]  Alexandre Duret-Lutz committed Mar 26, 2015 314  1 [label=<1>]  Alexandre Duret-Lutz committed Mar 17, 2015 315 316 317  1 -> 0 [label=] 1 -> 1 [label=] 1 -> 2 [label=]  Alexandre Duret-Lutz committed Mar 26, 2015 318  2 [label=<2>]  Alexandre Duret-Lutz committed Mar 17, 2015 319 320  2 -> 0 [label= ] 2 -> 2 [label=]  Alexandre Duret-Lutz committed Apr 09, 2013 321 322 323 } #+end_example  Alexandre Duret-Lutz committed Nov 22, 2017 324 #+BEGIN_SRC dot :file dotex2ba8.svg :var txt=dotex2ba8 :exports results  Alexandre Duret-Lutz committed Apr 09, 2013 325 326 327 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 328 [[file:dotex2ba8.svg]]  Alexandre Duret-Lutz committed Apr 09, 2013 329 330 331 332 333 334 335 336  * 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=.  Alexandre Duret-Lutz committed Apr 17, 2019 337 #+BEGIN_SRC sh  Alexandre Duret-Lutz committed Apr 09, 2013 338 339 340 341 342 343 344 345 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 346 347  :: ((!(b))) -> goto T0_S2 :: ((!(a)) && (b)) -> goto T0_S3  Alexandre Duret-Lutz committed Apr 09, 2013 348 349 350  fi; T0_S2: if  Alexandre Duret-Lutz committed Jan 06, 2015 351 352 353  :: ((a) && (b)) -> goto accept_init :: ((!(b))) -> goto T0_S2 :: ((!(a)) && (b)) -> goto T0_S3  Alexandre Duret-Lutz committed Apr 09, 2013 354 355 356  fi; T0_S3: if  Alexandre Duret-Lutz committed Jan 06, 2015 357 358  :: ((a)) -> goto accept_init :: ((!(a))) -> goto T0_S3  Alexandre Duret-Lutz committed Apr 09, 2013 359 360 361 362 363 364 365 366  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:  Alexandre Duret-Lutz committed Apr 17, 2019 367 #+BEGIN_SRC sh  Alexandre Duret-Lutz committed Apr 09, 2013 368 369 370 371 372 373 ltl2tgba -s --lenient '(a < b) U (process[2]@ok)' #+END_SRC #+RESULTS: : never { /* "a < b" U "process[2]@ok" */ : T0_init: : if  Alexandre Duret-Lutz committed Apr 17, 2019 374 : :: (process[2]@ok) -> goto accept_all  Alexandre Duret-Lutz committed Apr 09, 2013 375 376 377 378 379 380 381 382 383 : :: ((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 384 385 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 386 deterministic (=--deterministic=) automaton?  Alexandre Duret-Lutz committed Apr 09, 2013 387   Alexandre Duret-Lutz committed Apr 17, 2019 388 #+BEGIN_SRC sh :exports results  Alexandre Duret-Lutz committed Oct 26, 2015 389 ltl2tgba --help | sed -n '/Simplification goal:/,/^$/p' | sed '1d;$d'  Alexandre Duret-Lutz committed Apr 09, 2013 390 391 #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed May 13, 2015 392 393 : -a, --any no preference, do not bother making it small or : deterministic  Alexandre Duret-Lutz committed Apr 17, 2019 394 395 396 : -D, --deterministic prefer deterministic automata (combine with : --generic to be sure to obtain a deterministic : automaton)  Alexandre Duret-Lutz committed Apr 09, 2013 397 398 : --small prefer small automata (default)  Alexandre Duret-Lutz committed May 13, 2015 399 400 401 402 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 403   Alexandre Duret-Lutz committed May 13, 2015 404 405 406 407 408 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 409 410 411 412 413  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 414 415 416 417 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 418 419 420 421 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  Alexandre Duret-Lutz committed Jun 20, 2018 422 automaton, see [[#generic][the =--generic= option]] or [[#parity][the =--parity= option]].  Alexandre Duret-Lutz committed Feb 12, 2016 423   Alexandre Duret-Lutz committed Apr 09, 2013 424 425 426 427 An example formula where the difference between =-D= and =--small= is flagrant is =Ga|Gb|Gc=: #+NAME: gagbgc1  Alexandre Duret-Lutz committed Apr 17, 2019 428 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Jan 08, 2016 429 ltl2tgba 'Ga|Gb|Gc' -d  Alexandre Duret-Lutz committed Apr 09, 2013 430 431 432 433 #+END_SRC #+RESULTS: gagbgc1 #+begin_example digraph G {  Alexandre Duret-Lutz committed Jan 06, 2015 434  rankdir=LR  Alexandre Duret-Lutz committed May 13, 2015 435  node [shape="circle"]  Alexandre Duret-Lutz committed Mar 17, 2015 436 437 438  fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"]  Alexandre Duret-Lutz committed Mar 26, 2015 439  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]  Alexandre Duret-Lutz committed Jan 06, 2015 440 441  I [label="", style=invis, width=0] I -> 0  Alexandre Duret-Lutz committed Mar 26, 2015 442  0 [label=<0>]  Alexandre Duret-Lutz committed Mar 17, 2015 443 444 445  0 -> 1 [label=] 0 -> 2 [label=] 0 -> 3 [label=]  Alexandre Duret-Lutz committed Mar 26, 2015 446  1 [label=<1>]  Alexandre Duret-Lutz committed Mar 17, 2015 447  1 -> 1 [label=]  Alexandre Duret-Lutz committed Mar 26, 2015 448  2 [label=<2>]  Alexandre Duret-Lutz committed Mar 17, 2015 449  2 -> 2 [label=]  Alexandre Duret-Lutz committed Mar 26, 2015 450  3 [label=<3>]  Alexandre Duret-Lutz committed Mar 17, 2015 451  3 -> 3 [label=]  Alexandre Duret-Lutz committed Apr 09, 2013 452 453 454 } #+end_example  Alexandre Duret-Lutz committed Nov 22, 2017 455 #+BEGIN_SRC dot :file gagbgc1.svg :var txt=gagbgc1 :exports results  Alexandre Duret-Lutz committed Apr 09, 2013 456 457 458 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 459 [[file:gagbgc1.svg]]  Alexandre Duret-Lutz committed Apr 09, 2013 460   Alexandre Duret-Lutz committed Mar 17, 2015 461 #+NAME: gagbgc2  Alexandre Duret-Lutz committed Apr 17, 2019 462 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Jan 08, 2016 463 ltl2tgba -D 'Ga|Gb|Gc' -d  Alexandre Duret-Lutz committed Apr 09, 2013 464 465 466 467 #+END_SRC #+RESULTS: gagbgc2 #+begin_example digraph G {  Alexandre Duret-Lutz committed Jan 06, 2015 468  rankdir=LR  Alexandre Duret-Lutz committed May 13, 2015 469  node [shape="circle"]  Alexandre Duret-Lutz committed Mar 17, 2015 470 471 472  fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"]  Alexandre Duret-Lutz committed Mar 26, 2015 473  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]  Alexandre Duret-Lutz committed Jan 06, 2015 474 475  I [label="", style=invis, width=0] I -> 6  Alexandre Duret-Lutz committed May 13, 2015 476  0 [label="0", peripheries=2]  Alexandre Duret-Lutz committed Mar 17, 2015 477  0 -> 0 [label=]  Alexandre Duret-Lutz committed May 13, 2015 478  1 [label="1", peripheries=2]  Alexandre Duret-Lutz committed Mar 17, 2015 479 480 481  1 -> 0 [label=] 1 -> 1 [label=] 1 -> 2 [label=]  Alexandre Duret-Lutz committed May 13, 2015 482  2 [label="2", peripheries=2]  Alexandre Duret-Lutz committed Mar 17, 2015 483  2 -> 2 [label=]  Alexandre Duret-Lutz committed May 13, 2015 484  3 [label="3", peripheries=2]  Alexandre Duret-Lutz committed Mar 17, 2015 485 486 487  3 -> 2 [label=] 3 -> 3 [label=] 3 -> 5 [label=]  Alexandre Duret-Lutz committed May 13, 2015 488  4 [label="4", peripheries=2]  Alexandre Duret-Lutz committed Mar 17, 2015 489 490 491  4 -> 0 [label=] 4 -> 4 [label=] 4 -> 5 [label=]  Alexandre Duret-Lutz committed May 13, 2015 492  5 [label="5", peripheries=2]  Alexandre Duret-Lutz committed Mar 17, 2015 493  5 -> 5 [label=]  Alexandre Duret-Lutz committed May 13, 2015 494  6 [label="6", peripheries=2]  Alexandre Duret-Lutz committed Mar 17, 2015 495 496 497 498 499 500 501  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 502 503 504 } #+end_example  Alexandre Duret-Lutz committed Nov 22, 2017 505 #+BEGIN_SRC dot :file gagbgc2.svg :var txt=gagbgc2 :exports results  Alexandre Duret-Lutz committed Apr 09, 2013 506 507 508 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 509 [[file:gagbgc2.svg]]  Alexandre Duret-Lutz committed Apr 09, 2013 510 511 512 513 514  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 515 Add the =-C= or =--complete= option if you want to obtain a complete  Alexandre Duret-Lutz committed Sep 08, 2013 516 517 518 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 519 520 521 522 523 524 525 526 527 528 529 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  Alexandre Duret-Lutz committed Apr 17, 2019 530 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Jan 08, 2016 531 ltl2tgba -B 'GFa -> GFb' -d  Alexandre Duret-Lutz committed May 13, 2015 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 #+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 559 #+BEGIN_SRC dot :file ambig1.svg :var txt=ambig1 :exports results  Alexandre Duret-Lutz committed May 13, 2015 560 561 562 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 563 [[file:ambig1.svg]]  Alexandre Duret-Lutz committed May 13, 2015 564 565 566 567 568  Here is an unambiguous automaton for the same formula, in which there is only one run that recognizes this example word: #+NAME: ambig2  Alexandre Duret-Lutz committed Apr 17, 2019 569 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Jan 08, 2016 570 ltl2tgba -B -U 'GFa -> GFb' -d  Alexandre Duret-Lutz committed May 13, 2015 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 #+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 607 #+BEGIN_SRC dot :file ambig2.svg :var txt=ambig2 :exports results  Alexandre Duret-Lutz committed May 13, 2015 608 609 610 611 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 612 [[file:ambig2.svg]]  Alexandre Duret-Lutz committed May 13, 2015 613 614 615 616 617 618  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 619   Alexandre Duret-Lutz committed Apr 09, 2013 620 621 622 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:  Alexandre Duret-Lutz committed Apr 17, 2019 623 #+BEGIN_SRC sh :exports results  Alexandre Duret-Lutz committed Oct 26, 2015 624 ltl2tgba --help | sed -n '/Simplification level:/,/^$/p' | sed '1d;$d'  Alexandre Duret-Lutz committed Apr 09, 2013 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 #+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 640 641 produced by the core translator. The algorithms used during post-processing are  Alexandre Duret-Lutz committed Apr 09, 2013 642 643 644 645 646 647 648 649 - 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 650 - BA simulation (again direct or iterated)  Alexandre Duret-Lutz committed Apr 09, 2013 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672  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 673 * Deterministic automata with =--generic --deterministic=  Alexandre Duret-Lutz committed Feb 12, 2016 674 675 676 677 678  :PROPERTIES: :CUSTOM_ID: generic :END: The =--generic= (or =-G=) option allows =ltl2tgba= to use more  Alexandre Duret-Lutz committed Jun 20, 2018 679 680 681 682 683 684 685 686 687  complex acceptance conditions. This is done by splitting the LTL formulas on Boolean connectives to recognize some subformulas that are either to translate with different types of acceptance conditions, and then combining everything back together. Combined with =--deterministic= (or =-D=) this allows the use of a determinization algorithm that produces automata with parity acceptance. This is only used for subformulas for which we do not know a better way to get a deterministic automaton.  Alexandre Duret-Lutz committed Feb 12, 2016 688 689 690 691 692  For instance =FGa= is the typical formula for which not deterministic TGBA exists. #+NAME: ltl2tgba-fga  Alexandre Duret-Lutz committed Apr 17, 2019 693 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Mar 10, 2018 694 ltl2tgba "FGa" -D -d  Alexandre Duret-Lutz committed Feb 12, 2016 695 696 #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 697 #+BEGIN_SRC dot :file ltl2tgba-fga.svg :var txt=ltl2tgba-fga :exports results  Alexandre Duret-Lutz committed Feb 12, 2016 698 699 700 701  $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 702 [[file:ltl2tgba-fga.svg]]  Alexandre Duret-Lutz committed Feb 12, 2016 703   Alexandre Duret-Lutz committed Jun 20, 2018 704  But with =--generic=, =ltl2tgba= will output the following co-Büchi automaton:  Alexandre Duret-Lutz committed Feb 12, 2016 705 706  #+NAME: ltl2tgba-fga-D  Alexandre Duret-Lutz committed Apr 17, 2019 707 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Mar 10, 2018 708 ltl2tgba "FGa" -G -D -d  Alexandre Duret-Lutz committed Feb 12, 2016 709 710 #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 711 #+BEGIN_SRC dot :file ltl2tgba-fga-D.svg :var txt=ltl2tgba-fga-D :exports results  Alexandre Duret-Lutz committed Feb 12, 2016 712 713 714 715 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 716 [[file:ltl2tgba-fga-D.svg]]  Alexandre Duret-Lutz committed Feb 12, 2016 717   Alexandre Duret-Lutz committed Jun 20, 2018 718 719 720 721 722  If we translate =Fb|Gc= as a deterministic automaton with any acceptance condition, we get a weak and deterministic Büchi automaton: #+NAME: ltl2tgba-fbgc-D  Alexandre Duret-Lutz committed Apr 17, 2019 723 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Jun 20, 2018 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 ltl2tgba "Fb|Gc" -G -D -d #+END_SRC #+BEGIN_SRC dot :file ltl2tgba-fbgc-D.svg :var txt=ltl2tgba-fbgc-D :exports results $txt #+END_SRC #+RESULTS: [[file:ltl2tgba-fbgc-D.svg]] Finally if we translate the conjunction of these two subformulas, a product of these two automata will be made, producing: #+NAME: ltl2tgba-fbgcfga-D  Alexandre Duret-Lutz committed Apr 17, 2019 739 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Jun 20, 2018 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 ltl2tgba "(Fb|Gc)&FGa" -G -D -d #+END_SRC #+BEGIN_SRC dot :file ltl2tgba-fbgcfga-D.svg :var txt=ltl2tgba-fbgcfga-D :exports results$txt #+END_SRC #+RESULTS: [[file:ltl2tgba-fbgcfga-D.svg]] Disabling the splitting of the original formula LTL formulas can be done using option =-x ltl-split=0=. In that case the formula =(Fb|Gc)&FGa= will be translated into a single TGBA, and because this TGBA is non-deterministic, it will then be determinized into an automaton with parity acceptance: #+NAME: ltl2tgba-fbgcfga-nosplit-D  Alexandre Duret-Lutz committed Apr 17, 2019 757 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Jun 20, 2018 758 759 760 761 762 763 764 765 ltl2tgba "(Fb|Gc)&FGa" -G -D -xltl-split=0 -d #+END_SRC #+BEGIN_SRC dot :file ltl2tgba-fbgcfga-nosplit-D.svg :var txt=ltl2tgba-fbgcfga-nosplit-D :exports results $txt #+END_SRC #+RESULTS: [[file:ltl2tgba-fbgcfga-nosplit-D.svg]]  Alexandre Duret-Lutz committed Feb 12, 2016 766   Alexandre Duret-Lutz committed Feb 12, 2016 767 768 769  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 770 enabled by default, but that you may want to disable for experimental  Alexandre Duret-Lutz committed Feb 12, 2016 771 772 773 774 775 purpose. For instance the following deterministic automaton #+NAME: ltl2tgba-det1  Alexandre Duret-Lutz committed Apr 17, 2019 776 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Mar 10, 2018 777 ltl2tgba "F(a W FGb)" -G -D -d  Alexandre Duret-Lutz committed Feb 12, 2016 778 779 #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 780 #+BEGIN_SRC dot :file ltl2tgba-det1.svg :var txt=ltl2tgba-det1 :exports results  Alexandre Duret-Lutz committed Feb 12, 2016 781 782 783 784 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 785 [[file:ltl2tgba-det1.svg]]  Alexandre Duret-Lutz committed Feb 12, 2016 786 787 788 789  would be larger if SCC-based optimizations were disabled: #+NAME: ltl2tgba-det2  Alexandre Duret-Lutz committed Apr 17, 2019 790 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Jun 20, 2018 791 ltl2tgba "F(a W FGb)" -xdet-scc=0 -G -D -d  Alexandre Duret-Lutz committed Feb 12, 2016 792 793 #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 794 #+BEGIN_SRC dot :file ltl2tgba-det2.svg :var txt=ltl2tgba-det2 :exports results  Alexandre Duret-Lutz committed Feb 12, 2016 795 796 797 798  $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 799 [[file:ltl2tgba-det2.svg]]  Alexandre Duret-Lutz committed Feb 12, 2016 800   Alexandre Duret-Lutz committed Jan 08, 2018 801 * Deterministic automata with =--parity --deterministic=  Alexandre Duret-Lutz committed Jun 20, 2018 802 803 804  :PROPERTIES: :CUSTOM_ID: parity :END:  Alexandre Duret-Lutz committed Jan 08, 2018 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 834  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  Alexandre Duret-Lutz committed Apr 17, 2019 835 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Mar 10, 2018 836 ltl2tgba "FGa" -D -P -d  Alexandre Duret-Lutz committed Jan 08, 2018 837 838 839 840 841 842 843 844 845 846 847 848 849 #+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  Alexandre Duret-Lutz committed Apr 17, 2019 850 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Mar 10, 2018 851 ltl2tgba "GFa & GFb" -D -P -d  Alexandre Duret-Lutz committed Jan 08, 2018 852 853 854 855 856 857 858 859 860 861 862 863 864 #+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  Alexandre Duret-Lutz committed Apr 17, 2019 865 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Mar 10, 2018 866 ltl2tgba "GFa & GFb" -D -P'min odd' -d  Alexandre Duret-Lutz committed Jan 08, 2018 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 #+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  Alexandre Duret-Lutz committed Apr 17, 2019 883 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Mar 10, 2018 884 ltl2tgba "GFa & GFb" -D -p -d  Alexandre Duret-Lutz committed Jan 08, 2018 885 886 887 888 889 890 891 892 893 894 #+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  Alexandre Duret-Lutz committed Apr 17, 2019 895 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Mar 10, 2018 896 ltl2tgba "GFa & GFb" -D -p'min odd' -d  Alexandre Duret-Lutz committed Jan 08, 2018 897 898 899 900 901 902 903 904 905 906 907 908 909 #+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  Alexandre Duret-Lutz committed Apr 17, 2019 910 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Mar 10, 2018 911 ltl2tgba "GFa & GFb" -D -S -p'max even' -d  Alexandre Duret-Lutz committed Jan 08, 2018 912 913 914 915 916 917 918 919 920 #+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 921 922 923 * Translating multiple formulas for statistics If multiple formulas are given to =ltl2tgba=, the corresponding  Alexandre Duret-Lutz committed Aug 06, 2016 924 925 926 927 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 928   Alexandre Duret-Lutz committed Aug 06, 2016 929 930 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 931 932 933 934 935 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):  Alexandre Duret-Lutz committed Apr 17, 2019 936 #+BEGIN_SRC sh :exports results  Alexandre Duret-Lutz committed Jun 20, 2018 937 ltl2tgba --help | sed -n '/ sequences:/,/^$/p' | sed '1d;$d'  Alexandre Duret-Lutz committed Apr 09, 2013 938 939 #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Dec 06, 2013 940 #+begin_example  Alexandre Duret-Lutz committed Jun 20, 2018 941 942 943 944  %< the part of the line before the formula if it comes from a column extracted from a CSV file %> the part of the line after the formula if it comes from a column extracted from a CSV file  Alexandre Duret-Lutz committed Dec 06, 2013 945 946  %% a single % %a number of acceptance sets  Alexandre Duret-Lutz committed Jun 20, 2018 947 948 949 950 951 952  %c, %[LETTERS]c number of SCCs; you may filter the SCCs to count using the following LETTERS, possibly concatenated: (a) accepting, (r) rejecting, (c) complete, (v) trivial, (t) terminal, (w) weak, (iw) inherently weak. Use uppercase letters to negate them.  Alexandre Duret-Lutz committed Jan 06, 2015 953  %d 1 if the output is deterministic, 0 otherwise  Alexandre Duret-Lutz committed Jun 20, 2018 954  %e number of reachable edges  Alexandre Duret-Lutz committed Dec 06, 2013 955  %f the formula, in Spot's syntax  Alexandre Duret-Lutz committed Jan 06, 2015 956  %F name of the input file  Alexandre Duret-Lutz committed Jun 20, 2018 957 958 959 960 961 962 963 964 965 966 967 968  %g, %[LETTERS]g acceptance condition (in HOA syntax); add brackets to print an acceptance name instead and LETTERS to tweak the format: (0) no parameters, (a) accentuated, (b) abbreviated, (d) style used in dot output, (g) no generalized parameter, (l) recognize Street-like and Rabin-like, (m) no main parameter, (p) no parity parameter, (o) name unknown acceptance as 'other', (s) shorthand for 'lo0'. %h the automaton in HOA format on a single line (use %[opt]h to specify additional options as in --hoa=opt)  Alexandre Duret-Lutz committed Jan 06, 2015 969 970 971 972  %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  Alexandre Duret-Lutz committed Jun 20, 2018 973 974 975 976 977 978 979 980  %r wall-clock time elapsed in seconds (excluding parsing) %R, %[LETTERS]R CPU time (excluding parsing), in seconds; Add LETTERS to restrict to(u) user time, (s) system time, (p) parent process, or (c) children processes. %s number of reachable states %t number of reachable transitions  Alexandre Duret-Lutz committed Jan 06, 2015 981  %w one word accepted by the output automaton  Alexandre Duret-Lutz committed Jun 20, 2018 982 983 984 985 986 987 988 989  %x, %[LETTERS]x number of atomic propositions declared in the automaton; add LETTERS to list atomic propositions with (n) no quoting, (s) occasional double-quotes with C-style escape, (d) double-quotes with C-style escape, (c) double-quotes with CSV-style escape, (p) between parentheses, any extra non-alphanumeric character will be used to separate propositions  Alexandre Duret-Lutz committed Dec 06, 2013 990 #+end_example  Alexandre Duret-Lutz committed Apr 09, 2013 991 992 993 994  For instance we can study the size of the automata generated for the right-nested =U= formulas as follows:  Alexandre Duret-Lutz committed Apr 17, 2019 995 #+BEGIN_SRC sh  Alexandre Duret-Lutz committed Jul 19, 2016 996 genltl --u-right=1..8 | ltl2tgba --stats '%s states and %e edges for "%f"'  Alexandre Duret-Lutz committed Apr 09, 2013 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 #+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 1008 1009 Note that because no formula have been passed as argument to =ltl2tgba=, it defaulted to reading them from standard input. Such a  Alexandre Duret-Lutz committed Jul 21, 2020 1010 behavior can be requested explicitly with =-F -= if needed (e.g., to  Alexandre Duret-Lutz committed Jul 19, 2016 1011 1012 read from standard input in addition to processing other formula supplied with =-f=).  Alexandre Duret-Lutz committed Apr 09, 2013 1013 1014 1015 1016 1017 1018  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 1019 1020 1021 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 1022 1023 1024 1025 1026  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 1027 1028 1029 [[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 1030 * Building Monitors  Alexandre Duret-Lutz committed Mar 03, 2017 1031 1032 1033  :PROPERTIES: :CUSTOM_ID: monitors :END:  Alexandre Duret-Lutz committed Apr 09, 2013 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044  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 1045 #+NAME: monitor1  Alexandre Duret-Lutz committed Apr 17, 2019 1046 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Jan 08, 2016 1047 ltl2tgba -M '(Xa & Fb) | Gc' -d  Alexandre Duret-Lutz committed Apr 09, 2013 1048 1049 1050 1051 1052 #+END_SRC #+RESULTS: monitor1 #+begin_example digraph G {  Alexandre Duret-Lutz committed Jan 06, 2015 1053  rankdir=LR  Alexandre Duret-Lutz committed Jan 08, 2016 1054  node [shape="circle"]  Alexandre Duret-Lutz committed Mar 17, 2015 1055 1056 1057  fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"]  Alexandre Duret-Lutz committed Mar 26, 2015 1058  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]  Alexandre Duret-Lutz committed Jan 06, 2015 1059 1060  I [label="", style=invis, width=0] I -> 0  Alexandre Duret-Lutz committed Mar 26, 2015 1061  0 [label=<0>]  Alexandre Duret-Lutz committed Mar 17, 2015 1062 1063  0 -> 1 [label=<1>] 0 -> 3 [label=]  Alexandre Duret-Lutz committed Mar 26, 2015 1064  1 [label=<1>]  Alexandre Duret-Lutz committed Mar 17, 2015 1065  1 -> 2 [label=]  Alexandre Duret-Lutz committed Mar 26, 2015 1066  2 [label=<2>]  Alexandre Duret-Lutz committed Mar 17, 2015 1067  2 -> 2 [label=<1>]  Alexandre Duret-Lutz committed Mar 26, 2015 1068  3 [label=<3>]  Alexandre Duret-Lutz committed Mar 17, 2015 1069  3 -> 3 [label=]  Alexandre Duret-Lutz committed Apr 09, 2013 1070 1071 1072 } #+end_example  Alexandre Duret-Lutz committed Nov 22, 2017 1073 #+BEGIN_SRC dot :file monitor1.svg :var txt=monitor1 :exports results  Alexandre Duret-Lutz committed Apr 09, 2013 1074 1075 1076 1077 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 1078 [[file:monitor1.svg]]  Alexandre Duret-Lutz committed Apr 09, 2013 1079   Alexandre Duret-Lutz committed Mar 17, 2015 1080 #+NAME: monitor2  Alexandre Duret-Lutz committed Apr 17, 2019 1081 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Jan 08, 2016 1082 ltl2tgba -MD '(Xa & Fb) | Gc' -d  Alexandre Duret-Lutz committed Apr 09, 2013 1083 1084 #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 1085 #+BEGIN_SRC dot :file monitor2.svg :var txt=monitor2 :exports results  Alexandre Duret-Lutz committed Apr 09, 2013 1086 1087 1088 1089 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 1090 [[file:monitor2.svg]]  Alexandre Duret-Lutz committed Apr 09, 2013 1091 1092 1093  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 1094 1095 such as =F(a)=: indeed, any finite execution can be extended to match =F(a)=.  Alexandre Duret-Lutz committed Apr 09, 2013 1096   Alexandre Duret-Lutz committed Mar 03, 2017 1097 1098 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 1099 1100 1101  Because Monitors accept every recognized run (in other words, they only reject words that are not recognized), it makes little sense to  Alexandre Duret-Lutz committed Jul 21, 2020 1102 use option =-C= to request /complete/ monitors. If you combine =-C=  Alexandre Duret-Lutz committed Mar 03, 2017 1103 1104 1105 1106 1107 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  Alexandre Duret-Lutz committed Apr 17, 2019 1108 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Mar 03, 2017 1109 1110 1111 ltl2tgba -C -M -D '(Xa & Fb) | Gc' -d #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 1112 #+BEGIN_SRC dot :file monitor3.svg :var txt=monitor3 :exports results  Alexandre Duret-Lutz committed Mar 03, 2017 1113 1114 1115 1116 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 1117 [[file:monitor3.svg]]  Alexandre Duret-Lutz committed Mar 03, 2017 1118 1119 1120 1121   Alexandre Duret-Lutz committed Apr 09, 2013 1122 1123 1124 1125 1126 1127 # 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  Alexandre Duret-Lutz committed Jul 21, 2020 1128 1129 1130 1131 1132 # LocalWords: genltl nondeterministic eval setenv concat getenv DG # LocalWords: setq html args acc Buchi rankdir fontname Lato svg br # LocalWords: fillcolor ffffa vee arrowsize gba hoaf processings dp # LocalWords: ambig FGa fga fbgc fbgcfga determinized nosplit xltl # LocalWords: det scc simul FGb xdet P'min p'min p'max CSV iw