dstar2tgba.org 12.3 KB
 Alexandre Duret-Lutz committed Aug 26, 2013 1 #+TITLE: =dstar2tgba=  Alexandre Duret-Lutz committed Jan 07, 2015 2 3 #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html  Alexandre Duret-Lutz committed Aug 26, 2013 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75  This tool converts deterministic Rabin and Streett automata, presented in [[http://www.ltl2dstar.de/docs/ltl2dstar.html][the format output by =ltl2dstar=]], into Büchi automata. It's usage is almost similar to [[file:ltl2tgba.org][=ltl2tgba=]] except that instead of supplying a formula to translate, you should specify a filename containing the deterministic Rabin or Streett automaton to convert. * Two quick examples Here are some brief examples before we discuss the behavior of =dstar2tgba= in more detail. ** From Rabin to Büchi The following command instructs =ltl2dstar= to: 1. run =ltl2tgba -sD= to build a Büchi automaton for =Fa & GFb=, and then 2. convert that Büchi automaton into a deterministic Rabin automaton (DRA) stored in =fagfb=. Additionally we use =ltlfilt= to convert our formula to the prefix format used by =ltl2dstar=. #+BEGIN_SRC sh :results verbatim :exports node ltlfilt -f 'Fa & GFb' -l | ltl2dstar --ltl2nba=spin:../../src/bin/ltl2tgba@-sD - fagfb #+END_SRC By looking at the file =fagfb= you can see the =ltl2dsar= actually produced a 3-state DRA: #+BEGIN_SRC sh :results verbatim :exports both cat fagfb #+END_SRC #+RESULTS: #+begin_example DRA v2 explicit Comment: "Safra[NBA=3]" States: 3 Acceptance-Pairs: 1 Start: 1 AP: 2 "a" "b" --- State: 0 Acc-Sig: +0 2 2 0 0 State: 1 Acc-Sig: 1 0 1 0 State: 2 Acc-Sig: 2 2 0 0 #+end_example =dstar2tgba= can now be used to convert this DRA into a TGBA, a BA, or a Monitor, using the same options as [[file:ltl2tgba.org][=ltl2tgba=]]. For instance here is the conversion to a Büchi automaton (=-B=) in [[http://http://www.graphviz.org/][GraphViz]]'s format: #+BEGIN_SRC sh :results verbatim :exports both dstar2tgba -B fagfb #+END_SRC #+RESULTS: #+begin_example digraph G {  Alexandre Duret-Lutz committed Jan 06, 2015 76 77 78 79 80 81 82 83 84 85 86 87  rankdir=LR I [label="", style=invis, width=0] I -> 0 0 [label="0"] 0 -> 0 [label="!a"] 0 -> 1 [label="a"] 1 [label="1", peripheries=2] 1 -> 1 [label="b"] 1 -> 2 [label="!b"] 2 [label="2"] 2 -> 1 [label="b"] 2 -> 2 [label="!b"]  Alexandre Duret-Lutz committed Aug 26, 2013 88 89 90 91 92 93 94 95 96 97 98 99 } #+end_example Which can be rendered as: #+NAME: fagfb2ba #+BEGIN_SRC sh :results verbatim :exports none dstar2tgba -B fagfb | sed 's/\\/\\\\/' #+END_SRC #+RESULTS: fagfb2ba #+begin_example digraph G {  Alexandre Duret-Lutz committed Jan 06, 2015 100 101 102 103 104 105 106 107 108 109 110 111  rankdir=LR I [label="", style=invis, width=0] I -> 0 0 [label="0"] 0 -> 0 [label="!a"] 0 -> 1 [label="a"] 1 [label="1", peripheries=2] 1 -> 1 [label="b"] 1 -> 2 [label="!b"] 2 [label="2"] 2 -> 1 [label="b"] 2 -> 2 [label="!b"]  Alexandre Duret-Lutz committed Aug 26, 2013 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 } #+end_example #+BEGIN_SRC dot :file fagfb2ba.png :cmdline -Tpng :var txt=fagfb2ba :exports results $txt #+END_SRC #+RESULTS: [[file:fagfb2ba.png]] But we could as well require the output to be output as a never claim for Spin (option =-s=): #+BEGIN_SRC sh :results verbatim :exports both dstar2tgba -s fagfb #+END_SRC #+RESULTS: #+begin_example never { T0_init: if :: ((!(a))) -> goto T0_init  Alexandre Duret-Lutz committed Jan 06, 2015 132  :: ((a)) -> goto accept_S2  Alexandre Duret-Lutz committed Aug 26, 2013 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202  fi; accept_S2: if :: ((b)) -> goto accept_S2 :: ((!(b))) -> goto T0_S3 fi; T0_S3: if :: ((b)) -> goto accept_S2 :: ((!(b))) -> goto T0_S3 fi; } #+end_example ** Streett to TGBA :PROPERTIES: :CUSTOM_ID: streett_to_tgba_example :END: Here is the translation of =GFa & GFb= to a 4-state Streett automaton: #+BEGIN_SRC sh :results verbatim :exports both ltlfilt -f 'GFa & GFb' -l | ltl2dstar --automata=streett --ltl2nba=spin:../../src/bin/ltl2tgba@-sD - gfagfb cat gfagfb #+END_SRC #+RESULTS: #+begin_example DSA v2 explicit Comment: "Streett{Union{Safra[NBA=2],Safra[NBA=2]}}" States: 4 Acceptance-Pairs: 2 Start: 0 AP: 2 "a" "b" --- State: 0 Acc-Sig: -0 -1 3 2 1 0 State: 1 Acc-Sig: +0 -1 3 2 1 0 State: 2 Acc-Sig: -0 +1 3 2 1 0 State: 3 Acc-Sig: +0 +1 3 2 1 0 #+end_example And now its conversion by =dstar2tgba= to a 2-state Büchi automaton. We don't pass any option to =dstar2tgba= because converting to TGBA in GraphViz's format is the default: #+BEGIN_SRC sh :results verbatim :exports code dstar2tgba gfagfb #+END_SRC #+RESULTS: #+begin_example digraph G {  Alexandre Duret-Lutz committed Jan 06, 2015 203 204 205 206 207  rankdir=LR I [label="", style=invis, width=0] I -> 0 0 [label="0"] 0 -> 1 [label="1"]  Alexandre Duret-Lutz committed Aug 26, 2013 208  1 [label="1"]  Alexandre Duret-Lutz committed Jan 06, 2015 209 210 211 212  1 -> 1 [label="!a & !b"] 1 -> 1 [label="a & !b\n{0}"] 1 -> 1 [label="!a & b\n{1}"] 1 -> 1 [label="a & b\n{0,1}"]  Alexandre Duret-Lutz committed Aug 26, 2013 213 214 215 216 217 218 219 220 221 222 } #+end_example #+NAME: gfagfb2ba #+BEGIN_SRC sh :results verbatim :exports none dstar2tgba gfagfb | sed 's/\\/\\\\/g' #+END_SRC #+RESULTS: gfagfb2ba #+begin_example digraph G {  Alexandre Duret-Lutz committed Jan 06, 2015 223 224 225 226 227  rankdir=LR I [label="", style=invis, width=0] I -> 0 0 [label="0"] 0 -> 1 [label="1"]  Alexandre Duret-Lutz committed Aug 26, 2013 228  1 [label="1"]  Alexandre Duret-Lutz committed Jan 06, 2015 229 230 231 232  1 -> 1 [label="!a & !b"] 1 -> 1 [label="a & !b\\n{0}"] 1 -> 1 [label="!a & b\\n{1}"] 1 -> 1 [label="a & b\\n{0,1}"]  Alexandre Duret-Lutz committed Aug 26, 2013 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 } #+end_example #+BEGIN_SRC dot :file gfagfb2ba.png :cmdline -Tpng :var txt=gfagfb2ba :exports results$txt #+END_SRC #+RESULTS: [[file:gfagfb2ba.png]] (Obviously the resulting automaton could be simplified further, by starting with the second state right away.) * Details ** General behavior The =dstar2tgba= tool implement a 4-step process: 1. read the DRA/DSA 2. convert it into TGBA 3. postprocess the resulting TGBA (simplifying the automaton, a degeneralizing it into a BA or Monitor if requested) 4. output the resulting automaton ** Controlling output The last two steps are shared with =ltl2tgba= and use the same options. The type of automaton to produce can be selected using the =-B= or =-M= switches: #+BEGIN_SRC sh :results verbatim :exports results dstar2tgba --help | sed -n '/Output automaton type:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: : -B, --ba Büchi Automaton : -M, --monitor Monitor (accepts all finite prefixes of the given : formula) : --tgba Transition-based Generalized Büchi Automaton : (default) And these may be refined by a translation intent, should the post-processor routine had a choice to make: #+BEGIN_SRC sh :results verbatim :exports results dstar2tgba --help | sed -n '/Translation intent:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: : -a, --any no preference  Alexandre Duret-Lutz committed Sep 08, 2013 280 281 : -C, --complete output a complete automaton (combine with other : intents)  Alexandre Duret-Lutz committed Aug 26, 2013 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 : -D, --deterministic prefer deterministic automata : --small prefer small automata (default) The effort put into post-processing can be limited with the =--low= or =--medium= options: #+BEGIN_SRC sh :results verbatim :exports results dstar2tgba --help | sed -n '/Optimization level:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: : --high all available optimizations (slow, default) : --low minimal optimizations (fast) : --medium moderate optimizations For instance using =-a --low= will skip any optional post-processing, should you find =dstar2tgba= too slow.  Alexandre Duret-Lutz committed Jan 06, 2015 299 300 Finally, the output format can be changed with the following [[file:oaout.org][common ouput options]]:  Alexandre Duret-Lutz committed Aug 26, 2013 301 302 303 304 #+BEGIN_SRC sh :results verbatim :exports results dstar2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Jan 06, 2015 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 #+begin_example -8, --utf8 enable UTF-8 characters in output (ignored with --lbtt or --spin) --dot[=c|h|n|N|s|t|v] GraphViz's format (default). Add letters to chose (c) circular nodes, (h) horizontal layout, (v) vertical layout, (n) with name, (N) without name, (s) with SCCs, (t) always transition-based acceptance. -H, --hoaf[=s|t|m|l] Output the automaton in HOA format. Add letters to select (s) state-based acceptance, (t) transition-based acceptance, (m) mixed acceptance, (l) single-line output --lbtt[=t] LBTT's format (add =t to force transition-based acceptance even on Büchi automata) --name=FORMAT set the name of the output automaton -s, --spin Spin neverclaim (implies --ba) --spot SPOT's format --stats=FORMAT output statistics about the automaton #+end_example  Alexandre Duret-Lutz committed Aug 26, 2013 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345  The =--stats= options can output statistics about the input and the output automaton, so it can be useful to search for particular pattern. For instance here is a complex command that will 1. generate an infinite stream of random LTL formulas with [[file:randltl.org][=randltl=]], 2. use [[file:ltlfilt.org][=ltlfilt=]] to rewrite the W and M operators away (=--remove-wm=), simplify the formulas (=-r=), remove duplicates (=u=) as well as formulas that have a size less then 3 (=--size-min=3=), 3. use =head= to keep only 10 of such formula 4. loop to process each of these formula: - print it - then convert the formula into =ltl2dstar='s input format, process it with =ltl2dstar= (using =ltl2tgba= as the actual LTL->BA transltor), and process the result with =dstar2tgba= to build a Büchi automaton (=-B=), favoring determinism if we can (=-D=), and finally displaying some statistics about this conversion. The statistics displayed in this case are: =%S=, the number of states of the input (Rabin) automaton, =%s=, the number of states of the  Alexandre Duret-Lutz committed Sep 08, 2013 346 347 output (Büchi) automaton, =%d=, whether the output automaton is deterministic, and =%p= whether the automaton is complete.  Alexandre Duret-Lutz committed Aug 26, 2013 348 349  #+BEGIN_SRC sh :results verbatim :exports both  Alexandre Duret-Lutz committed Jan 06, 2015 350 randltl -n -1 --tree-size=10..14 a b c |  Alexandre Duret-Lutz committed Aug 26, 2013 351 352 353 354 355 356 ltlfilt --remove-wm -r -u --size-min=3 | head -n 10 | while read f; do echo "$f" ltlfilt -l -f "$f" | ltl2dstar --ltl2nba=spin:../../src/bin/ltl2tgba@-sD - - |  Alexandre Duret-Lutz committed Sep 08, 2013 357  dstar2tgba -B --stats=' DRA: %Sst.; BA: %sst.; det.? %d; complete? %p'  Alexandre Duret-Lutz committed Aug 26, 2013 358 359 360 361 362 done #+END_SRC #+RESULTS: #+begin_example  Alexandre Duret-Lutz committed Jan 06, 2015 363 c U (c & (a | b | (Xc U (a & Xc))))  Alexandre Duret-Lutz committed Sep 08, 2013 364  DRA: 3st.; BA: 2st.; det.? 1; complete? 0  Alexandre Duret-Lutz committed Jan 06, 2015 365 366 367 368 369 !b | F!c DRA: 3st.; BA: 3st.; det.? 1; complete? 1 (!a R F!b) R !b DRA: 6st.; BA: 5st.; det.? 1; complete? 0 b U !c  Alexandre Duret-Lutz committed Sep 08, 2013 370  DRA: 3st.; BA: 2st.; det.? 1; complete? 0  Alexandre Duret-Lutz committed Jan 06, 2015 371 372 373 374 375 GFc DRA: 3st.; BA: 3st.; det.? 1; complete? 1 (F!c U a) R !a DRA: 6st.; BA: 5st.; det.? 1; complete? 0 b | G!b  Alexandre Duret-Lutz committed Sep 08, 2013 376  DRA: 4st.; BA: 3st.; det.? 1; complete? 0  Alexandre Duret-Lutz committed Jan 06, 2015 377 378 379 380 381 382 !a R (!c & (!a | (F!b U (!a & F!b)))) DRA: 5st.; BA: 4st.; det.? 1; complete? 0 F(a & !b & G!c) DRA: 2st.; BA: 3st.; det.? 0; complete? 0 GF!c DRA: 3st.; BA: 3st.; det.? 1; complete? 1  Alexandre Duret-Lutz committed Aug 26, 2013 383 384 385 386 387 #+end_example An important point you should be aware of when comparing these numbers of states is that the deterministic automata produced by =ltl2dstar= are complete, while the automata produced by =dstar2tgba=  Alexandre Duret-Lutz committed Sep 08, 2013 388 389 390 391 392 (deterministic or not) are not complete by default. This can explain a difference of one state (the so called "sink" state). You can instruct =dstar2tgba= to output a complete automaton using the =--complete= option (or =-C= for short).  Alexandre Duret-Lutz committed Aug 26, 2013 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429  ** Conversion from Rabin and Streett to TGBA The algorithms used to convert Rabin and Streett into TGBA/BA are different. *** Rabin to BA The conversion implemented is a variation of Krishnan et al.'s "Deterministic ω-Automata vis-a-vis Deterministic Büchi Automata" (ISAAC'94) paper. They explain how to convert a deterministic Rabin automaton (DRA) into a deterministic Büchi automaton (DBA) when such an automaton exist. The surprising result is that when a DRA is DBA-realizable, a DBA can be obtained from the DRA without changing its transition structure. Spot implements a slight refinement to the above technique: any DRA will be converted into a BA, and the determinism will be conserved only in strongly connected components where determinism can be conserved. *** Streett to TGBA Streett automata are converted into non-deterministic TGBA. When a Streett automaton uses multiple acceptance pairs, we use generalized acceptance conditions in the TGBA to limit the combinatorial explosion. A straightforward translation from Streett to BA, as described for instance by [[http://www.automata.rwth-aachen.de/~loeding/diploma_loeding.pdf][Löding's diploma thesis]], will create a BA with $|Q|\cdot(4^n-3^n+2)$ states if the input Streett automaton has $|Q|$ states and $n$ acceptance pairs. Our translation to TGBA limits this to $|Q|\cdot(2^n+1)$ states. Sometimes, as in the [[#streett_to_tgba_example][example for =GFa & GFb=]] the output of this conversion will happen to be deterministic. Let's say that this is luck: Spot does not implement any algorithm to preserve the determinism of Streett automata.