dstar2tgba.org 12.7 KB
Newer Older
1
# -*- coding: utf-8 -*-
2
#+TITLE: =dstar2tgba=
3
4
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html
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

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=]].

69
For instance here is the conversion to a Büchi automaton (=-B=) in [[http://www.graphviz.org/][GraphViz]]'s format:
70

71
#+BEGIN_SRC sh :results verbatim :exports code
72
73
dstar2tgba -B fagfb
#+END_SRC
74
75
76
77

#+BEGIN_SRC sh :results verbatim :exports results
SPOT_DOTEXTRA= dstar2tgba -B fagfb --dot=
#+END_SRC
78
79
80
#+RESULTS:
#+begin_example
digraph G {
81
82
  rankdir=LR
  I [label="", style=invis, width=0]
83
84
85
86
87
88
89
  I -> 1
  0 [label="0", peripheries=2]
  0 -> 0 [label="b"]
  0 -> 2 [label="!b"]
  1 [label="1"]
  1 -> 0 [label="a"]
  1 -> 1 [label="!a"]
90
  2 [label="2"]
91
  2 -> 0 [label="b"]
92
  2 -> 2 [label="!b"]
93
94
95
}
#+end_example

96
97
98
Which can be rendered as (note that in this documentation
we use some [[file:aout.org][environement variables]] to produce a more colorful
output by default):
99
100

#+NAME: fagfb2ba
101
102
#+BEGIN_SRC sh :results verbatim :exports code
dstar2tgba -B fagfb
103
104
105
106
#+END_SRC
#+RESULTS: fagfb2ba
#+begin_example
digraph G {
107
  rankdir=LR
108
109
110
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
111
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
112
  I [label="", style=invis, width=0]
113
  I -> 1
114
  0 [label=<0<br/><font color="#5DA5DA">⓿</font>>]
115
116
  0 -> 0 [label=<b>]
  0 -> 2 [label=<!b>]
117
  1 [label=<1>]
118
119
  1 -> 0 [label=<a>]
  1 -> 1 [label=<!a>]
120
  2 [label=<2>]
121
122
  2 -> 0 [label=<b>]
  2 -> 2 [label=<!b>]
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
}
#+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
143
  :: ((a)) -> goto accept_S2
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
  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
166
ltlfilt -f 'GFa & GFb' -l | ltl2dstar --automata=streett --ltl2nba=spin:ltl2tgba@-Ds - gfagfb
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
203
204
205
206
207
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:

208
#+NAME: gfagfb2ba
209
210
211
212
213
214
#+BEGIN_SRC sh :results verbatim :exports code
dstar2tgba gfagfb
#+END_SRC
#+RESULTS: gfagfb2ba
#+begin_example
digraph G {
215
  rankdir=LR
216
217
218
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
219
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
220
221
222
  I [label="", style=invis, width=0]
  I -> 0
  0 [label="0"]
223
  0 -> 1 [label=<1>]
224
  1 [label="1"]
225
226
227
228
  1 -> 1 [label=<!a &amp; !b>]
  1 -> 1 [label=<a &amp; !b<br/><font color="#5DA5DA">⓿</font>>]
  1 -> 1 [label=<!a &amp; b<br/><font color="#F17CB0">❶</font>>]
  1 -> 1 [label=<a &amp; b<br/><font color="#5DA5DA">⓿</font><font color="#F17CB0">❶</font>>]
229
230
231
232
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
}
#+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
276
277
:   -C, --complete             output a complete automaton (combine with other
:                              intents)
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
:   -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.

295
296
Finally, the output format can be changed with the following
[[file:oaout.org][common ouput options]]:
297
298
299
300
#+BEGIN_SRC sh :results verbatim :exports results
dstar2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d'
#+END_SRC
#+RESULTS:
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
#+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
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
316
317
318
  -s, --spin[=6|c]           Spin neverclaim (implies --ba).  Add letters to
                             select (6) Spin's 6.2.4 style, (c) comments on
                             states
319
320
      --stats=FORMAT         output statistics about the automaton
#+end_example
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342

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
343
344
output (Büchi) automaton, =%d=, whether the output automaton is
deterministic, and =%p= whether the automaton is complete.
345
346

#+BEGIN_SRC sh :results verbatim :exports both
347
randltl -n -1 --tree-size=10..14 a b c |
348
349
350
351
352
ltlfilt --remove-wm -r -u --size-min=3 |
head -n 10 |
while read f; do
  echo "$f"
  ltlfilt -l -f "$f" |
353
  ltl2dstar --ltl2nba=spin:../../src/bin/ltl2tgba@-Ds - - |
354
  dstar2tgba -B --stats='  DRA: %Sst.; BA: %sst.; det.? %d; complete? %p'
355
356
357
358
359
done
#+END_SRC

#+RESULTS:
#+begin_example
360
361
362
363
(b | Fa) R Fc
  DRA: 9st.; BA: 6st.; det.? 1; complete? 1
Ga U (Gc R (!a | Gc))
  DRA: 7st.; BA: 7st.; det.? 0; complete? 0
364
365
GFc
  DRA: 3st.; BA: 3st.; det.? 1; complete? 1
366
367
368
369
370
371
372
373
374
375
376
377
378
379
!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))
  DRA: 5st.; BA: 3st.; det.? 1; complete? 0
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
380
381
382
383
384
#+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=
385
386
387
388
389
(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).
390
391
392
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

** 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
424
425
426
conversion happens to be deterministic.  This is pure luck: Spot does
not implement any algorithm to preserve the determinism of Streett
automata.