dstar2tgba.org 17.7 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
And now its conversion by =dstar2tgba= to a 1-state TGBA.
215

216
#+NAME: gfagfb2ba
217
#+BEGIN_SRC sh :results verbatim :exports code
218
dstar2tgba gfagfb -d
219
220
221
#+END_SRC
#+RESULTS: gfagfb2ba
#+begin_example
222
digraph "" {
223
  rankdir=LR
224
225
  label=<Inf(<font color="#1F78B4">⓿</font>)&amp;Inf(<font color="#FF4DA0">❶</font>)<br/>[gen. Büchi 2]>
  labelloc="t"
226
  node [shape="circle"]
227
  node [style="filled", fillcolor="#ffffa0"]
228
229
230
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
231
  node[fontsize=12] fontsize=12 stylesheet="spot.css" edge[arrowhead=vee, arrowsize=.7, fontsize=12]
232
233
  I [label="", style=invis, width=0]
  I -> 0
234
235
236
237
238
  0 [label=<0>]
  0 -> 0 [label=<!a &amp; !b>]
  0 -> 0 [label=<!a &amp; b<br/><font color="#FF4DA0">❶</font>>]
  0 -> 0 [label=<a &amp; !b<br/><font color="#1F78B4">⓿</font>>]
  0 -> 0 [label=<a &amp; b<br/><font color="#1F78B4">⓿</font><font color="#FF4DA0">❶</font>>]
239
240
241
}
#+end_example

242
#+BEGIN_SRC dot :file gfagfb2ba.svg :var txt=gfagfb2ba :exports results
243
244
245
$txt
#+END_SRC
#+RESULTS:
246
[[file:gfagfb2ba.svg]]
247
248
249
250
251

* Details

** General behavior

252
The =dstar2tgba= tool implements a 4-step process:
253

254
  1. read the automaton
255
256
257
258
  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

259
260
261
262
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.)
263

264
265
266
267
268
269
270
271
272
273
274
** 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:
275
:   -B, --ba                   Büchi Automaton (implies -S)
276
:   -C, --complete             output a complete automaton
277
:   -M, --monitor              Monitor (accepts all finite prefixes of the given
278
279
280
:                              property)
:   -S, --state-based-acceptance, --sbacc
:                              define the acceptance using states
281
:       --tgba                 Transition-based Generalized Büchi Automaton
282
283
:                              (default)

284
And these may be refined by a simplification goal, should the
285
286
post-processor routine had a choice to make:
#+BEGIN_SRC sh :results verbatim :exports results
287
dstar2tgba --help | sed -n '/Simplification goal:/,/^$/p' | sed '1d;$d'
288
289
#+END_SRC
#+RESULTS:
290
291
:   -a, --any                  no preference, do not bother making it small or
:                              deterministic
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
299
dstar2tgba --help | sed -n '/Simplification level:/,/^$/p' | sed '1d;$d'
300
301
302
303
304
305
306
307
308
#+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.

309
Finally, the output format can be changed with the following
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
310
[[file:oaut.org][common ouput options]]:
311
312
313
314
#+BEGIN_SRC sh :results verbatim :exports results
dstar2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d'
#+END_SRC
#+RESULTS:
315
316
317
#+begin_example
  -8, --utf8                 enable UTF-8 characters in output (ignored with
                             --lbtt or --spin)
318
319
320
      --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),
321
322
323
324
325
                             '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)
326
327
328
329
330
331
332
                             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)
333
334
335
336
337
338
339
340
341
342
                             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
343
344
345
      --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
346
347
348
349
  -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
350
351
352
  -s, --spin[=6|c]           Spin neverclaim (implies --ba).  Add letters to
                             select (6) Spin's 6.2.4 style, (c) comments on
                             states
353
354
      --stats=FORMAT         output statistics about the automaton
#+end_example
355
356
357
358
359
360
361
362
363
364

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
365
366
367
   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:
368
369
370
371
372
373
374
375
376
   - 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
377
378
output (Büchi) automaton, =%d=, whether the output automaton is
deterministic, and =%p= whether the automaton is complete.
379
380

#+BEGIN_SRC sh :results verbatim :exports both
381
randltl -n -1 --tree-size=10..14 a b c |
382
ltlfilt --remove-wm -r -u --size-min=3 -n 10 |
383
384
385
while read f; do
  echo "$f"
  ltlfilt -l -f "$f" |
386
  ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - |
387
  dstar2tgba -B --stats='  DRA: %Sst.; BA: %sst.; det.? %d; complete? %p'
388
389
390
391
392
done
#+END_SRC

#+RESULTS:
#+begin_example
393
(b | Fa) R Fc
394
  DRA: 9st.; BA: 9st.; det.? 1; complete? 1
395
396
Ga U (Gc R (!a | Gc))
  DRA: 7st.; BA: 7st.; det.? 0; complete? 0
397
398
GFc
  DRA: 3st.; BA: 3st.; det.? 1; complete? 1
399
400
401
402
403
!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))
404
  DRA: 4st.; BA: 3st.; det.? 1; complete? 0
405
406
407
408
409
410
411
412
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
413
414
415
416
417
#+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=
418
419
420
421
422
(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).
423

424
425
426
427
428
429
** 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
430

431
432
433
434
435
436
437
438
439
440
441
442
443
444
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.
445

446
447
448
449
450
451
452
453
454
455
456
457
458
459
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).

460
*** Rabin to BA
461

462
463
464
465
466
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.
467
468
469
470
471
472
473
474
475

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.

476
477
478
479
480
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
481
482
these SCCs will be nondeterministic.)  Our implementation also work on
automata with transition-based acceptance.
483
484
485

This specialized conversion is built in the =remove_fin()= procedure
described above.
486
487
488

*** Streett to TGBA

489
490
491
Streett acceptance have a specialized conversion into non-deterministic TGBA.
This improved conversion is automatically used by =to_generalized_buchi()=.

492
493
494
495
496
497
498
499
500
501
502
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
503
504
505
conversion happens to be deterministic.  This is pure luck: Spot does
not implement any algorithm to preserve the determinism of Streett
automata.