dstar2tgba.org 18.5 KB
Newer Older
1
# -*- coding: utf-8 -*-
2
#+TITLE: =dstar2tgba=
3
#+DESCRIPTION: Spot command-line tool for converting automata into Transition-based Generalized Büchi Automata.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
4
#+INCLUDE: setup.org
5
#+HTML_LINK_UP: tools.html
6

7
This tool converts automata into transition-based generalized Büchi
8
9
10
11
automata, a.k.a., TGBA.  It can also produce Büchi automata on request
(=-B=).  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 automaton to convert.
12
13

In earlier version (before Spot 1.99.4) =dstar2tgba= was only able to
14
15
16
17
18
19
20
21
read automata written in [[http://www.ltl2dstar.de/docs/ltl2dstar.html][the format output by =ltl2dstar=]].  However
nowadays it can read automata in any of the supported formats ([[file:hoa.org][HOA]],
LBTT's format, ltl2dstar's format, and never claims).  Also
=dstar2tgba= used to be the only tool being able to read ltl2dstar's
format, but today this format can also be read by any of the tool that
read automata.  So in practice, running =dstar2tgba some files...=
produces the same result as running =autfilt --tgba --high --small
some files...=.
22
23
24
25
26
27
28
29
30
31


* 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:
32
1. run =ltl2tgba -Ds= to build a Büchi automaton for =(a U b) & GFb=, and then
33
34
35
36
37
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=.

38
#+BEGIN_SRC sh :results silent :exports both
39
ltlfilt -f '(a U b) & GFb' -l | ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - fagfb
40
41
42
#+END_SRC

By looking at the file =fagfb= you can see the =ltl2dsar= actually
43
produced a 4-state DRA:
44
45
46
47
48
49
50
51

#+BEGIN_SRC sh :results verbatim :exports both
cat fagfb
#+END_SRC
#+RESULTS:
#+begin_example
DRA v2 explicit
Comment: "Safra[NBA=3]"
52
States: 4
53
Acceptance-Pairs: 1
54
Start: 2
55
56
57
58
AP: 2 "a" "b"
---
State: 0
Acc-Sig: +0
59
60
3
3
61
62
63
0
0
State: 1
64
65
66
Acc-Sig: -0
1
1
67
68
69
70
1
1
State: 2
Acc-Sig:
71
1
72
73
74
2
0
0
75
76
77
78
79
80
State: 3
Acc-Sig:
3
3
0
0
81
82
#+end_example

83
84
Let's display this automaton with =autfilt=:
#+NAME: fagfb
85
#+BEGIN_SRC sh :results verbatim :exports code
86
autfilt fagfb --dot
87
#+END_SRC
88

89
#+RESULTS: fagfb
90
91
#+begin_example
digraph G {
92
  rankdir=LR
93
94
95
96
97
98
99
  label=<Fin(<font color="#5DA5DA">⓿</font>) &amp; Inf(<font color="#F17CB0">❶</font>)>
  labelloc="t"
  node [shape="circle"]
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
100
  I [label="", style=invis, width=0]
101
102
103
104
105
106
107
108
109
110
111
112
113
  I -> 2
  0 [label=<0<br/><font color="#F17CB0">❶</font>>]
  0 -> 0 [label=<b>]
  0 -> 3 [label=<!b>]
  1 [label=<1<br/><font color="#5DA5DA">⓿</font>>]
  1 -> 1 [label=<1>]
  2 [label=<2>]
  2 -> 0 [label=<b>]
  2 -> 1 [label=<!a &amp; !b>]
  2 -> 2 [label=<a &amp; !b>]
  3 [label=<3>]
  3 -> 0 [label=<b>]
  3 -> 3 [label=<!b>]
114
115
116
}
#+end_example

117
#+BEGIN_SRC dot :file fagfb.svg :var txt=fagfb :exports results
118
119
120
121
$txt
#+END_SRC

#+RESULTS:
122
[[file:fagfb.svg]]
123
124
125
126
127

=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=):
128
129

#+NAME: fagfb2ba
130
#+BEGIN_SRC sh :results verbatim :exports code
131
dstar2tgba -B fagfb -d
132
133
134
135
#+END_SRC
#+RESULTS: fagfb2ba
#+begin_example
digraph G {
136
  rankdir=LR
137
  node [shape="circle"]
138
139
140
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
141
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
142
  I [label="", style=invis, width=0]
143
  I -> 1
144
  0 [label="0", peripheries=2]
145
146
  0 -> 0 [label=<b>]
  0 -> 2 [label=<!b>]
147
148
149
150
  1 [label="1"]
  1 -> 0 [label=<b>]
  1 -> 1 [label=<a &amp; !b>]
  2 [label="2"]
151
152
  2 -> 0 [label=<b>]
  2 -> 2 [label=<!b>]
153
154
155
}
#+end_example

156
#+BEGIN_SRC dot :file fagfb2ba.svg :var txt=fagfb2ba :exports results
157
158
159
$txt
#+END_SRC
#+RESULTS:
160
[[file:fagfb2ba.svg]]
161

162
163
164
165
166

Note that by default the output is not complete.  Use =-C= if you want
a complete automaton.

But we could as well require the output as a never claim for Spin (option =-s=):
167
168
169
170
171
172
173
174
175

#+BEGIN_SRC sh :results verbatim :exports both
dstar2tgba -s fagfb
#+END_SRC
#+RESULTS:
#+begin_example
never {
T0_init:
  if
176
  :: (b) -> goto accept_S0
177
  :: ((a) && (!(b))) -> goto T0_init
178
  fi;
179
accept_S0:
180
  if
181
182
  :: (b) -> goto accept_S0
  :: (!(b)) -> goto T0_S2
183
  fi;
184
T0_S2:
185
  if
186
187
  :: (b) -> goto accept_S0
  :: (!(b)) -> goto T0_S2
188
189
190
191
192
193
194
195
196
  fi;
}
#+end_example

** Streett to TGBA
:PROPERTIES:
  :CUSTOM_ID: streett_to_tgba_example
:END:

197
Here is the translation of =GFa | GFb= to a 4-state Streett automaton:
198

199
200
#+NAME: gfafgb
#+BEGIN_SRC sh :results verbatim :exports code
201
ltlfilt -f 'GFa & GFb' -l | ltl2dstar --automata=streett --ltl2nba=spin:ltl2tgba@-Ds - gfagfb
202
autfilt --dot gfagfb
203
#+END_SRC
204

205
#+BEGIN_SRC dot :file gfafgb.svg :var txt=gfafgb :exports results
206
207
208
209
$txt
#+END_SRC

#+RESULTS:
210
[[file:gfafgb.svg]]
211
212
213
214
215
216



And now its conversion by =dstar2tgba= to a 4-state TGBA.
We don't pass any option to =dstar2tgba= because converting to TGBA is
the default:
217

218
#+NAME: gfagfb2ba
219
#+BEGIN_SRC sh :results verbatim :exports code
220
dstar2tgba gfagfb -d
221
222
223
224
#+END_SRC
#+RESULTS: gfagfb2ba
#+begin_example
digraph G {
225
  rankdir=LR
226
  node [shape="circle"]
227
228
229
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
230
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
231
232
233
  I [label="", style=invis, width=0]
  I -> 0
  0 [label="0"]
234
235
236
237
  0 -> 0 [label=<a &amp; b<br/><font color="#5DA5DA">⓿</font><font color="#F17CB0">❶</font>>]
  0 -> 1 [label=<!a &amp; b<br/><font color="#5DA5DA">⓿</font><font color="#F17CB0">❶</font>>]
  0 -> 2 [label=<a &amp; !b<br/><font color="#5DA5DA">⓿</font><font color="#F17CB0">❶</font>>]
  0 -> 3 [label=<!a &amp; !b<br/><font color="#5DA5DA">⓿</font><font color="#F17CB0">❶</font>>]
238
  1 [label="1"]
239
  1 -> 0 [label=<a &amp; b<br/><font color="#F17CB0">❶</font>>]
240
  1 -> 1 [label=<!a &amp; b<br/><font color="#F17CB0">❶</font>>]
241
242
243
244
245
246
247
248
249
250
251
252
  1 -> 2 [label=<a &amp; !b<br/><font color="#F17CB0">❶</font>>]
  1 -> 3 [label=<!a &amp; !b<br/><font color="#F17CB0">❶</font>>]
  2 [label="2"]
  2 -> 0 [label=<a &amp; b<br/><font color="#5DA5DA">⓿</font>>]
  2 -> 1 [label=<!a &amp; b<br/><font color="#5DA5DA">⓿</font>>]
  2 -> 2 [label=<a &amp; !b<br/><font color="#5DA5DA">⓿</font>>]
  2 -> 3 [label=<!a &amp; !b<br/><font color="#5DA5DA">⓿</font>>]
  3 [label="3"]
  3 -> 0 [label=<a &amp; b>]
  3 -> 1 [label=<!a &amp; b>]
  3 -> 2 [label=<a &amp; !b>]
  3 -> 3 [label=<!a &amp; !b>]
253
254
255
}
#+end_example

256
#+BEGIN_SRC dot :file gfagfb2ba.svg :var txt=gfagfb2ba :exports results
257
258
259
$txt
#+END_SRC
#+RESULTS:
260
[[file:gfagfb2ba.svg]]
261

262
263
264
Obviously the resulting automaton could be simplified further, as the
minimal TGBA for this formula has a single state.  (Patches
welcome...)
265
266
267
268
269

* Details

** General behavior

270
The =dstar2tgba= tool implements a 4-step process:
271

272
  1. read the automaton
273
274
275
276
  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

277
278
279
280
BTW, the above scenario is also exactly what you get with [[file:autfilt.org][=autfilt=]] if
you run it as =autfilt --tgba --high --small=.  (This is true only
since version 1.99.4, since both tools can now read the same file
formats.)
281

282
283
284
285
286
287
288
289
290
291
292
** 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:
293
:   -B, --ba                   Büchi Automaton (implies -S)
294
:   -C, --complete             output a complete automaton
295
:   -M, --monitor              Monitor (accepts all finite prefixes of the given
296
297
298
:                              property)
:   -S, --state-based-acceptance, --sbacc
:                              define the acceptance using states
299
:       --tgba                 Transition-based Generalized Büchi Automaton
300
301
:                              (default)

302
And these may be refined by a simplification goal, should the
303
304
post-processor routine had a choice to make:
#+BEGIN_SRC sh :results verbatim :exports results
305
dstar2tgba --help | sed -n '/Simplification goal:/,/^$/p' | sed '1d;$d'
306
307
#+END_SRC
#+RESULTS:
308
309
:   -a, --any                  no preference, do not bother making it small or
:                              deterministic
310
311
312
313
314
315
316
:   -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
317
dstar2tgba --help | sed -n '/Simplification level:/,/^$/p' | sed '1d;$d'
318
319
320
321
322
323
324
325
326
#+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.

327
Finally, the output format can be changed with the following
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
328
[[file:oaut.org][common ouput options]]:
329
330
331
332
#+BEGIN_SRC sh :results verbatim :exports results
dstar2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d'
#+END_SRC
#+RESULTS:
333
334
335
#+begin_example
  -8, --utf8                 enable UTF-8 characters in output (ignored with
                             --lbtt or --spin)
336
337
338
      --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),
339
340
341
342
343
                             '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)
344
345
346
347
348
349
350
                             acceptance sets as bullets, (B) bullets except for
                             Büchi/co-Büchi automata, (c) force circular
                             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)
351
352
353
354
355
356
357
358
359
360
                             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
361
362
363
      --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
364
365
366
367
  -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 '>>'.
  -q, --quiet                suppress all normal output
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
368
369
370
  -s, --spin[=6|c]           Spin neverclaim (implies --ba).  Add letters to
                             select (6) Spin's 6.2.4 style, (c) comments on
                             states
371
372
      --stats=FORMAT         output statistics about the automaton
#+end_example
373
374
375
376
377
378
379
380
381
382

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
383
384
385
   formulas that have a size less then 3 (=--size-min=3=), and
   keep only the 10 first formulas (=-n 10=)
3. loop to process each of these formula:
386
387
388
389
390
391
392
393
394
   - 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
395
396
output (Büchi) automaton, =%d=, whether the output automaton is
deterministic, and =%p= whether the automaton is complete.
397
398

#+BEGIN_SRC sh :results verbatim :exports both
399
randltl -n -1 --tree-size=10..14 a b c |
400
ltlfilt --remove-wm -r -u --size-min=3 -n 10 |
401
402
403
while read f; do
  echo "$f"
  ltlfilt -l -f "$f" |
404
  ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - |
405
  dstar2tgba -B --stats='  DRA: %Sst.; BA: %sst.; det.? %d; complete? %p'
406
407
408
409
410
done
#+END_SRC

#+RESULTS:
#+begin_example
411
(b | Fa) R Fc
412
  DRA: 9st.; BA: 9st.; det.? 1; complete? 1
413
414
Ga U (Gc R (!a | Gc))
  DRA: 7st.; BA: 7st.; det.? 0; complete? 0
415
416
GFc
  DRA: 3st.; BA: 3st.; det.? 1; complete? 1
417
418
419
420
421
!a | (a R b)
  DRA: 3st.; BA: 2st.; det.? 1; complete? 0
Xc R (G!c R (b | G!c))
  DRA: 4st.; BA: 2st.; det.? 1; complete? 0
c & G(b | F(a & c))
422
  DRA: 4st.; BA: 3st.; det.? 1; complete? 0
423
424
425
426
427
428
429
430
XXFc
  DRA: 4st.; BA: 4st.; det.? 1; complete? 1
XFc | Gb
  DRA: 5st.; BA: 4st.; det.? 1; complete? 1
G(((!a & Gc) | (a & F!c)) U (!a | Ga))
  DRA: 6st.; BA: 5st.; det.? 1; complete? 1
a & !b
  DRA: 3st.; BA: 2st.; det.? 1; complete? 0
431
432
433
434
435
#+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=
436
437
438
439
440
(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).
441

442
443
444
445
446
447
** Conversion of various acceptance conditions to TGBA and BA

Spot implements several acceptance conversion algorithms.
There is one generic cases, with some specialized variants.

*** Generic case
448

449
450
451
452
453
454
455
456
457
458
459
460
461
462
The most generic one, called =remove_fin()= in Spot, takes an
automaton with any acceptance condition, and as its name suggests, it
removes all the =Fin(x)= from the acceptance condition: the output is
an automaton whose acceptance conditions is a Boolean combination of
=Inf(x)= acceptance primitive.  (Such automata with Fin-less
acceptance can be easily tested for emptiness using SCC-based
emptiness checks.)  This algorithm works by fist converting the
acceptance conditions into disjunctive normal form, and then removing
any =Fin(x)= acceptance by adding non-deterministic jumps into clones
of the SCCs that intersect set =x=.  This is done with a few tricks
that limits the numbers of clones, and that ensure that the resulting
automaton uses /at most/ one extra acceptance sets.  This algorithm is
not readily available from =dstar2tgba=, but [[file:autfilt.org][=autfilt=]] has an option
=--remove-fin= if you need it.
463

464
465
466
467
468
469
470
471
472
473
474
475
476
477
From an automaton with Fin-less acceptance, one can obtain a TGBA
without changing the transitions structure: take the Fin-less
acceptance, transform it into conjunctive normal form (CNF), and
create one new Fin-accepting set for each conjunct of the CNF.  The
combination of these two algorithms is implemented by the
=to_generalized_buchi()= function in Spot.

Finally a TGBA can easily be converted into a BA with classical
degeneralization algorithms (our version of that includes several
SCC-based optimizations described in our [[https://www.lrde.epita.fr/~adl/dl/adl/babiak.13.spin.pdf][SPIN'13 paper]]).

This generalized case is specialized for two types of acceptances that
are common (Rabin and Streett).

478
*** Rabin to BA
479

480
481
482
483
484
When the input is a Rabin automaton, a dedicated conversion to BA is
used.  This procedure actually works for input that is called
Rabin-like, i.e., any acceptance formula that can easily be converted
to Rabin by adding some extra Fin or Inf terms to the acceptance
conditions and ensuring that those terms are always true.
485
486
487
488
489
490
491
492
493

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.

494
495
496
497
498
Spot implements a slight refinement to the above technique by doing it
SCC-wise: any DRA will be converted into a BA, and the determinism
will be conserved only for strongly connected components where
determinism can be conserved.  (If some SCC is not DBA-realizable, it
will be cloned into several deterministic SCC, but the jumps between
499
500
these SCCs will be nondeterministic.)  Our implementation also work on
automata with transition-based acceptance.
501
502
503

This specialized conversion is built in the =remove_fin()= procedure
described above.
504
505
506

*** Streett to TGBA

507
508
509
Streett acceptance have a specialized conversion into non-deterministic TGBA.
This improved conversion is automatically used by =to_generalized_buchi()=.

510
511
512
513
514
515
516
517
518
519
520
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
521
522
523
conversion happens to be deterministic.  This is pure luck: Spot does
not implement any algorithm to preserve the determinism of Streett
automata.