dstar2tgba.org 15.9 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
#+PROPERTY: header-args:sh :results verbatim :exports both
7

8
This tool converts automata into transition-based generalized Büchi
9
10
11
12
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.
13
14

In earlier version (before Spot 1.99.4) =dstar2tgba= was only able to
15
16
17
18
19
20
21
22
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...=.
23
24
25
26
27
28
29
30
31
32


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

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

By looking at the file =fagfb= you can see the =ltl2dsar= actually
44
produced a 4-state DRA:
45

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

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

90
#+BEGIN_SRC dot :file fagfb.svg :var txt=fagfb :exports results
91
92
93
94
$txt
#+END_SRC

#+RESULTS:
95
[[file:fagfb.svg]]
96
97
98
99
100

=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=):
101
102

#+NAME: fagfb2ba
103
#+BEGIN_SRC sh :exports code
104
dstar2tgba -B fagfb -d
105
106
#+END_SRC

107
#+BEGIN_SRC dot :file fagfb2ba.svg :var txt=fagfb2ba :exports results
108
109
110
$txt
#+END_SRC
#+RESULTS:
111
[[file:fagfb2ba.svg]]
112

113
114
115
116
117

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=):
118

119
#+BEGIN_SRC sh
120
121
122
123
124
125
126
dstar2tgba -s fagfb
#+END_SRC
#+RESULTS:
#+begin_example
never {
T0_init:
  if
127
  :: ((a) && (!(b))) -> goto T0_init
128
  :: (b) -> goto accept_S2
129
  fi;
130
T0_S1:
131
  if
132
133
  :: (!(b)) -> goto T0_S1
  :: (b) -> goto accept_S2
134
  fi;
135
accept_S2:
136
  if
137
138
  :: (!(b)) -> goto T0_S1
  :: (b) -> goto accept_S2
139
140
141
142
143
144
145
146
147
  fi;
}
#+end_example

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

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

150
#+NAME: gfafgb
151
#+BEGIN_SRC sh :exports code
152
ltlfilt -f 'GFa & GFb' -l | ltl2dstar --automata=streett --ltl2nba=spin:ltl2tgba@-Ds - gfagfb
153
autfilt --dot gfagfb
154
#+END_SRC
155

156
#+BEGIN_SRC dot :file gfafgb.svg :var txt=gfafgb :exports results
157
158
159
160
$txt
#+END_SRC

#+RESULTS:
161
[[file:gfafgb.svg]]
162
163
164



165
And now its conversion by =dstar2tgba= to a 1-state TGBA.
166

167
#+NAME: gfagfb2ba
168
#+BEGIN_SRC sh :exports code
169
dstar2tgba gfagfb -d
170
171
#+END_SRC

172
#+BEGIN_SRC dot :file gfagfb2ba.svg :var txt=gfagfb2ba :exports results
173
174
175
$txt
#+END_SRC
#+RESULTS:
176
[[file:gfagfb2ba.svg]]
177
178
179
180
181

* Details

** General behavior

182
The =dstar2tgba= tool implements a 4-step process:
183

184
  1. read the automaton
185
  2. convert it into TGBA
186
  3. post-process the resulting TGBA (simplifying the automaton, degeneralizing it into a BA or Monitor if requested)
187
188
  4. output the resulting automaton

189
190
191
192
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.)
193

194
195
196
197
198
199
** 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:
200
#+BEGIN_SRC sh :exports results
201
202
203
204
dstar2tgba --help | sed -n '/Output automaton type:/,/^$/p' | sed '1d;$d'
#+END_SRC

#+RESULTS:
205
:   -B, --ba                   Büchi Automaton (implies -S)
206
:   -C, --complete             output a complete automaton
207
:   -M, --monitor              Monitor (accepts all finite prefixes of the given
208
209
210
:                              property)
:   -S, --state-based-acceptance, --sbacc
:                              define the acceptance using states
211
:       --tgba                 Transition-based Generalized Büchi Automaton
212
213
:                              (default)

214
And these may be refined by a simplification goal, should the
215
post-processor routine had a choice to make:
216
#+BEGIN_SRC sh :exports results
217
dstar2tgba --help | sed -n '/Simplification goal:/,/^$/p' | sed '1d;$d'
218
219
#+END_SRC
#+RESULTS:
220
221
:   -a, --any                  no preference, do not bother making it small or
:                              deterministic
222
223
224
225
226
227
:   -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:

228
#+BEGIN_SRC sh :exports results
229
dstar2tgba --help | sed -n '/Simplification level:/,/^$/p' | sed '1d;$d'
230
231
232
233
234
235
236
237
238
#+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.

239
Finally, the output format can be changed with the following
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
240
[[file:oaut.org][common ouput options]]:
241
#+BEGIN_SRC sh :exports results
242
243
244
dstar2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d'
#+END_SRC
#+RESULTS:
245
246
247
#+begin_example
  -8, --utf8                 enable UTF-8 characters in output (ignored with
                             --lbtt or --spin)
248
249
250
      --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),
251
252
253
254
255
                             '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)
256
257
258
259
260
261
262
                             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)
263
264
265
266
267
268
269
270
271
272
                             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
273
274
275
      --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
276
277
278
279
  -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
280
281
282
  -s, --spin[=6|c]           Spin neverclaim (implies --ba).  Add letters to
                             select (6) Spin's 6.2.4 style, (c) comments on
                             states
283
284
      --stats=FORMAT         output statistics about the automaton
#+end_example
285
286
287
288
289
290
291
292
293
294

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
295
296
297
   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:
298
299
300
   - print it
   - then convert the formula into =ltl2dstar='s input format, process
     it with =ltl2dstar= (using =ltl2tgba= as the actual LTL->BA
301
     translator), and process the result with =dstar2tgba= to build a
302
303
304
305
306
     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
307
308
output (Büchi) automaton, =%d=, whether the output automaton is
deterministic, and =%p= whether the automaton is complete.
309

310
#+BEGIN_SRC sh
311
randltl -n -1 --tree-size=10..14 a b c |
312
ltlfilt --remove-wm -r -u --size-min=3 -n 10 |
313
314
315
while read f; do
  echo "$f"
  ltlfilt -l -f "$f" |
316
  ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - |
317
  dstar2tgba -B --stats='  DRA: %Sst.; BA: %sst.; det.? %d; complete? %p'
318
319
320
321
322
done
#+END_SRC

#+RESULTS:
#+begin_example
323
(b | Fa) R Fc
324
  DRA: 9st.; BA: 9st.; det.? 1; complete? 1
325
Ga U G(!a | Gc)
326
  DRA: 7st.; BA: 7st.; det.? 0; complete? 0
327
GFc
328
  DRA: 2st.; BA: 2st.; det.? 1; complete? 1
329
330
!a | (a R b)
  DRA: 3st.; BA: 2st.; det.? 1; complete? 0
331
332
Xc R G(b | G!c)
  DRA: 3st.; BA: 2st.; det.? 1; complete? 0
333
c & G(b | F(a & c))
334
  DRA: 4st.; BA: 3st.; det.? 1; complete? 0
335
336
337
XXFc
  DRA: 4st.; BA: 4st.; det.? 1; complete? 1
XFc | Gb
338
  DRA: 4st.; BA: 4st.; det.? 1; complete? 1
339
340
341
342
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
343
344
345
346
347
#+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=
348
349
350
351
352
(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).
353

354
355
356
357
358
359
** 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
360

361
362
363
364
365
366
367
368
369
370
371
372
373
374
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.
375

376
377
378
379
380
381
382
383
384
385
386
387
388
389
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).

390
*** Rabin to BA
391

392
393
394
395
396
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.
397
398
399
400
401
402
403
404
405

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.

406
407
408
409
410
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
411
412
these SCCs will be nondeterministic.)  Our implementation also work on
automata with transition-based acceptance.
413
414
415

This specialized conversion is built in the =remove_fin()= procedure
described above.
416
417
418

*** Streett to TGBA

419
420
421
Streett acceptance have a specialized conversion into non-deterministic TGBA.
This improved conversion is automatically used by =to_generalized_buchi()=.

422
423
424
425
426
427
428
429
430
431
432
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
433
434
435
conversion happens to be deterministic.  This is pure luck: Spot does
not implement any algorithm to preserve the determinism of Streett
automata.
436
437
438
439
440
441
442

#  LocalWords:  utf dstar tgba html args LBTT's dstar's Ds GFb DRA ba
#  LocalWords:  fagfb ltlfilt SRC nba dsar DBA Acc Sig svg txt init
#  LocalWords:  fi streett GFa gfafgb gfagfb degeneralizing sed sbacc
#  LocalWords:  ouput lbtt GraphViz's SCCs hoaf neverclaim randltl wm
#  LocalWords:  Sst sst det Fc Gc GFc Xc XXFc XFc Gb SCC CNF buchi et
#  LocalWords:  Krishnan al vis Löding's cdot