satmin.org 30 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
# -*- coding: utf-8 -*-
2
#+TITLE: SAT-based Minimization of Deterministic ω-Automata
3
4
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html
5

6
7
This page explains how to use [[file:ltl2tgba.org][=ltl2tgba=]], [[file:dstar2tgba.org][=dstar2tgba=]], or [[file:autfilt.org][=autfilt=]]
to minimize deterministic automata using a SAT solver.
8
9
10
11
12
13

Let us first state a few facts about this minimization procedure.

1) The procedure works only on *deterministic* Büchi automata: any
   recurrence property can be converted into a deterministic Büchi
   automaton, and sometimes there are several ways of doing so.
14
2) Spot actually implements two SAT-based minimization procedures: one
15
   that builds a deterministic transition-based Büchi automaton
16
17
18
19
20
21
   (DTBA), and one that builds a deterministic transition-based
   ω-automaton with arbitrary acceptance condition (DTωA).  In
   [[file:ltl2tgba.org][=ltl2tgba=]] and [[file:dstar2tgba.org][=dstar2tgba=]], the latter procedure is restricted to
   TGBA.  In [[file:autfilt.org][=autfilt=]] it can use different and acceptance conditions
   for input and output, so you could for instance input a Rabin
   automaton, and produce a Streett automaton.
22
23
24
25
26
3) These two procedures can optionally constrain their output to
   use state-based acceptance. (They simply restrict all the outgoing
   transitions of a state to belong to the same acceptance sets.)
4) A SAT solver should be installed for this to work. (Spot does not
   distribute any SAT solver.)
27
5) [[file:ltl2tgba.org][=ltl2tgba=]] and [[file:dstar2tgba.org][=dstar2tgba=]] will always try to output an automaton.
28
29
30
31
32
33
34
35
   If they fail to determinize the property, they will simply output a
   nondeterministic automaton, if they managed to obtain a
   deterministic automaton but failed to minimize it (e.g., the
   requested number of states in the final automaton is too low), they
   will return that "unminimized" deterministic automaton.  There are
   only two cases where these tool will abort without returning an
   automaton: when the number of clauses output by Spot (and to be fed
   to the SAT solver) exceeds $2^{31}$, or when the SAT-solver was
36
37
   killed by a signal. [[file:autfilt.org][=autfilt --sat-minimize=]] will only output an
   automaton if the SAT-based minimization was successful.
38
39
40
41
6) Our [[https://www.lrde.epita.fr/~adl/dl/adl/baarir.14.forte.pdf][FORTE'14 paper]] describes the SAT encoding for the minimization
   of deterministic BA and TGBA.  Our [[https://www.lrde.epita.fr/~adl/dl/adl/baarir.15.lpar.pdf][LPAR'15 paper]] describes the
   generalization of the SAT encoding to deal with deterministic TωA
   with any acceptance condition.
42

43
* How to change the SAT solver used
44
45

The environment variable =SPOT_SATSOLVER= can be used to change the
46
47
48
49
50
51
52
53
54
SAT solver used by Spot.  The default is "=glucose -verb=0 -model %I
>%O=", therefore if you have installed [[http://www.labri.fr/perso/lsimon/glucose/][=glucose= 3.0]] in your =$PATH=,
it should work right away.  Otherwise you may redefine this variable
to point the correct location or to another SAT solver (for older
versions of glucose, remove the =-model= option).  The =%I= and =%O=
sequences will be replaced by the names of temporary files containing
the input for the SAT solver and receiving its output.  We assume that
the SAT solver should follow the conventions of the [[http://www.satcompetition.org/][SAT competition]]
for input and output.
55

56
* Enabling SAT-based minimization in =ltl2tgba= or =dstar2tgba=
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105

Both tools follow the same interface, because they use the same
post-processing steps internally (i.e., the =spot::postprocessor=
class).

First, option =-D= should be used to declare that you are looking for
more determinism.  This will tweak the translation algorithm used by
=ltl2tgba= to improve determinism, and will also instruct the
post-processing routine used by both tools to prefer a
deterministic automaton over a smaller equivalent nondeterministic
automaton.

However =-D= is not a guarantee to obtain a deterministic automaton,
even if one exists.  For instance, =-D= fails to produce a
deterministic automaton for =GF(a <-> XXb)=.  Instead we get a 9-state
non-deterministic automaton.

#+BEGIN_SRC sh :results verbatim :exports both
ltl2tgba -D "GF(a <-> XXb)" --stats='states=%s, det=%d'
#+END_SRC
#+RESULTS:
: states=9, det=0

Option =-x tba-det= enables an additional
determinization procedure, that would otherwise not be used by =-D=
alone.  This procedure will work on any automaton that can be
represented by a DTBA; if the automaton to process use multiple
acceptance conditions, it will be degeneralized first.

On our example, =-x tba-det= successfully produces a deterministic
TBA, but a non-minimal one:

#+BEGIN_SRC sh :results verbatim :exports both
ltl2tgba -D -x tba-det "GF(a <-> XXb)" --stats='states=%s, det=%d'
#+END_SRC
#+RESULTS:
: states=7, det=1

Option =-x sat-minimize= will turn-on SAT-based minimization.  It also
implies =-x tba-det=, so there is no need to supply both options.

#+BEGIN_SRC sh :results verbatim :exports both
ltl2tgba -D -x sat-minimize "GF(a <-> XXb)" --stats='states=%s, det=%d'
#+END_SRC
#+RESULTS:
: states=4, det=1

We can draw it:

106
#+NAME: gfaexxb3
107
108
109
#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba -D -x sat-minimize "GF(a <-> XXb)"
#+END_SRC
110
#+RESULTS: gfaexxb3
111
112
#+begin_example
digraph G {
113
  rankdir=LR
114
  node [shape="circle"]
115
116
117
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
118
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
119
120
121
  I [label="", style=invis, width=0]
  I -> 0
  0 [label="0"]
122
123
124
125
  0 -> 1 [label=<!a &amp; !b<br/><font color="#5DA5DA">⓿</font>>]
  0 -> 2 [label=<!a &amp; b>]
  0 -> 3 [label=<a &amp; b>]
  0 -> 3 [label=<a &amp; !b<br/><font color="#5DA5DA">⓿</font>>]
126
  1 [label="1"]
127
128
129
130
  1 -> 0 [label=<a &amp; b>]
  1 -> 0 [label=<a &amp; !b<br/><font color="#5DA5DA">⓿</font>>]
  1 -> 1 [label=<!a &amp; b>]
  1 -> 1 [label=<!a &amp; !b<br/><font color="#5DA5DA">⓿</font>>]
131
  2 [label="2"]
132
133
134
135
  2 -> 0 [label=<a &amp; !b>]
  2 -> 1 [label=<!a &amp; b<br/><font color="#5DA5DA">⓿</font>>]
  2 -> 1 [label=<!a &amp; !b>]
  2 -> 3 [label=<a &amp; b<br/><font color="#5DA5DA">⓿</font>>]
136
  3 [label="3"]
137
138
139
140
  3 -> 2 [label=<!a &amp; b<br/><font color="#5DA5DA">⓿</font>>]
  3 -> 2 [label=<!a &amp; !b>]
  3 -> 3 [label=<a &amp; b<br/><font color="#5DA5DA">⓿</font>>]
  3 -> 3 [label=<a &amp; !b>]
141
142
143
144
145
146
147
148
149
}
#+end_example

#+BEGIN_SRC dot :file gfaexxb3.png :cmdline -Tpng :var txt=gfaexxb3 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:gfaexxb3.png]]

150
Clearly this is automaton benefits from the transition-based
151
152
153
154
acceptance.  If we want a traditional Büchi automaton, with
state-based acceptance, we only need to add the =-B= option.  The
result will of course be slightly bigger.

155
#+NAME: gfaexxb4
156
157
158
159
160
161
#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba -BD -x sat-minimize "GF(a <-> XXb)"
#+END_SRC
#+RESULTS: gfaexxb4
#+begin_example
digraph G {
162
  rankdir=LR
163
164
165
166
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
  node[style=filled, fillcolor="#ffffa0"]
167
168
169
  I [label="", style=invis, width=0]
  I -> 0
  0 [label="0"]
170
171
172
  0 -> 0 [label=<!a &amp; b>]
  0 -> 1 [label=<!b>]
  0 -> 2 [label=<a &amp; b>]
173
174
175
  1 [label="1", peripheries=2]
  1 -> 4 [label=<!a>]
  1 -> 5 [label=<a>]
176
  2 [label="2"]
177
178
179
  2 -> 1 [label=<!b>]
  2 -> 4 [label=<!a &amp; b>]
  2 -> 5 [label=<a &amp; b>]
180
181
182
183
  3 [label="3", peripheries=2]
  3 -> 0 [label=<!a>]
  3 -> 1 [label=<a &amp; !b>]
  3 -> 2 [label=<a &amp; b>]
184
  4 [label="4"]
185
186
187
188
  4 -> 0 [label=<!a &amp; !b>]
  4 -> 1 [label=<a &amp; b>]
  4 -> 2 [label=<a &amp; !b>]
  4 -> 3 [label=<!a &amp; b>]
189
  5 [label="5"]
190
191
192
193
  5 -> 1 [label=<a &amp; b>]
  5 -> 3 [label=<!a &amp; b>]
  5 -> 4 [label=<!a &amp; !b>]
  5 -> 5 [label=<a &amp; !b>]
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
}
#+end_example

#+BEGIN_SRC dot :file gfaexxb4.png :cmdline -Tpng :var txt=gfaexxb4 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:gfaexxb4.png]]


There are cases where =ltl2tgba='s =tba-det= algorithm fails to produce a deterministic automaton.
In that case, SAT-based minimization is simply skipped.  For instance:

#+BEGIN_SRC sh :results verbatim :exports both
ltl2tgba -D -x sat-minimize "Ga R (F!b & (c U b))" --stats='states=%s, det=%d'
#+END_SRC
#+RESULTS:
: states=4, det=0

The question, of course, is whether there exist a deterministic
automaton for this formula, in other words: is this a recurrence
215
216
property?  There are two ways to answer this question using Spot and
some help from [[http://www.ltl2dstar.de/][=ltl2dstar=]].
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238

The first is purely syntactic.  If a formula belongs to the class of
"syntactic recurrence formulas", it expresses a syntactic property.
(Of course there are formulas that expresses a syntactic properties
without being syntactic recurrences.)  [[file:ltlfilt.org][=ltlfilt=]] can be instructed to
print only formulas that are syntactic recurrences:

#+BEGIN_SRC sh :results verbatim :exports both
ltlfilt --syntactic-recurrence -f "Ga R (F!b & (c U b))"
#+END_SRC
#+RESULTS:
: Ga R (F!b & (c U b))

Since our input formula was output, it expresses a recurrence property.

The second way to check whether a formula is a recurrence is by
converting a deterministic Rabin automaton using [[file:dstar2tgba.org][=dstar2tgba=]].  The
output is guaranteed to be deterministic if and only if the input DRA
expresses a recurrence property.

#+BEGIN_SRC sh :results verbatim :exports both
ltlfilt -f "Ga R (F!b & (c U b))" -l |
239
ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - |
240
241
242
243
244
245
246
247
248
249
250
251
252
dstar2tgba -D --stats='input(states=%S) output(states=%s, acc-sets=%a, det=%d)'
#+END_SRC
#+RESULTS:
: input(states=11) output(states=9, acc-sets=1, det=1)

In the above command, =ltlfilt= is used to convert the LTL formula
into =ltl2dstar='s syntax.  Then =ltl2dstar= creates a deterministic
Rabin automaton (using =ltl2tgba= as an LTL to BA translator), and the
resulting 11-state DRA is converted into a 9-state DTBA by
=dstar2tgba=.  Since that result is deterministic, we can conclude
that the formula was a recurrence.

As far as SAT-based minimization goes, =dstar2tgba= will take the same
253
options as =ltl2tgba=.  For instance we can see that the smallest DTBA
254
255
256
257
has 6 states:

#+BEGIN_SRC sh :results verbatim :exports both
ltlfilt -f "Ga R (F!b & (c U b))" -l |
258
ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - |
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
dstar2tgba -D -x sat-minimize --stats='input(states=%S) output(states=%s, acc-sets=%a, det=%d)'
#+END_SRC
#+RESULTS:
: input(states=11) output(states=6, acc-sets=1, det=1)

* More acceptance sets

The formula "=Ga R (F!b & (c U b))=" can in fact be minimized into an
even smaller automaton if we use multiple acceptance sets.

Unfortunately because =dstar2tgba= does not know the formula being
translated, and it always convert a DRA into a DBA (with a single
acceptance set) before further processing, it does not know if using
more acceptance sets could be useful to further minimize it.   This
number of acceptance sets can however be specified on the command-line
with option =-x sat-acc=M=.  For instance:

#+BEGIN_SRC sh :results verbatim :exports both
ltlfilt -f "Ga R (F!b & (c U b))" -l |
278
ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - |
279
280
281
282
283
dstar2tgba -D -x sat-minimize,sat-acc=2 --stats='input(states=%S) output(states=%s, acc-sets=%a, det=%d)'
#+END_SRC
#+RESULTS:
: input(states=11) output(states=5, acc-sets=2, det=1)

284
285
286
Beware that the size of the SAT problem is exponential in the number
of acceptance sets (adding one acceptance set, in the input automaton
or in the output automaton, will double the size of the problem).
287
288
289
290
291
292
293
294

The case of =ltl2tgba= is slightly different because it can remember
the number of acceptance sets used by the translation algorithm, and
reuse that for SAT-minimization even if the automaton had to be
degeneralized in the meantime for the purpose of determinization.

* Low-level details

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
295
The following figure (from our [[https://www.lrde.epita.fr/~adl/dl/adl/baarir.14.forte.pdf][FORTE'14 paper]]) gives an overview of
296
297
298
299
the processing chains that can be used to turn an LTL formula into a
minimal DBA/DTBA/DTGBA.  The blue area at the top describes =ltl2tgba
-D -x sat-minimize=, while the purple area at the bottom corresponds
to =dstar2tgba -D -x stat-minimize=.
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345

[[file:satmin.png]]

The picture is slightly inaccurate in the sense that both =ltl2tgba=
and =dstar2tgba= are actually using the same post-processing chain:
only the initial translation to TGBA or conversion to DBA differs, the
rest is the same.  However in the case of =dstar2tgba=, no
degeneration or determinization are needed.

Also the picture does not show what happens when =-B= is used: any
DTBA is degeneralized into a DBA, before being sent to "DTBA SAT
minimization", with a special option to request state-based output.

The WDBA-minimization boxes are able to produce minimal Weak DBA from
any TGBA representing an obligation property.  In that case using
transition-based or generalized acceptance will not allow further
reduction.  This minimal WDBA is always used when =-D= is given
(otherwise, for the default =--small= option, the minimal WDBA is only
used if it is smaller than the nondeterministic automaton it has been
built from).

The "simplify" boxes are actually simulation-based reductions, and
SCC-based simplifications.

The red boxes "not in TCONG" or "not a recurrence" correspond to
situations where the tools will produce non-deterministic automata.

The following options can be used to fine-tune this procedure:

- =-x tba-det= :: attempt a powerset construction and check if
                  there exists a acceptance set such that the
                  resulting DTBA is equivalent to the input
- =-x sat-minimize= :: enable SAT-based minimization.  By default it
     tries to reduce the size of the automaton one state at a time.
     This option implies =-x tba-det=.
- =-x sat-minimize=2= :: enabled SAT-based minimization, but perform a
     dichotomy to locate the correct automaton size.  Use this only if
     you suspect that the optimal size is far away from the input
     size.  This option implies =-x tba-det=.
- =-x sat-acc=$m$= :: attempt to build a minimal DTGBA with $m$ acceptance sets.
     This options implies =-x sat-minimize=.
- =-x sat-states=$n$= :: attempt to build an equivalent DTGBA with $n$
     states.  This also implies =-x sat-minimize= but won't perform
     any loop to lower the number of states.  Note that $n$ should be
     the number of states in a complete automaton, while =ltl2tgba=
     and =dstar2tgba= both remove sink states in their output by
346
     default (use option =--complete= to output a complete automaton).
347
348
349
350
351
352
353
     Also note that even with the =--complete= option, the output
     automaton may have appear to have less states because the other
     are unreachable.
- =-x state-based= :: for all outgoing transition of each state
     to belong to the same acceptance sets.
- =-x !wdba-minimize= :: disable WDBA minimization.

354
When options =-B= and =-x sat-minimize= are both used, =-x
355
356
357
state-based= and =-x sat-acc=1= are implied.  Similarly, when option
=-S= and =-x sat-minimize= are both used, then option =-x state-based=
is implied.
358

359
360
361
362
363
364
365
366
* Using =autfilt --sat-minimize= to minimize any deterministic ω-automaton

This interface is new in Spot 1.99 and allows to minimize any
deterministic ω-automaton, regardless of the acceptance condition
used.  By default, the procedure will try to use the same acceptance
condition (or any inferior one) and produce transition-based
acceptance.

367
For our example, let us first generate a deterministic Rabin
368
369
automaton with [[http://www.ltl2dstar.de/][=ltl2dstar=]].

370
#+BEGIN_SRC sh :results silent :exports both
371
ltlfilt -f "FGa | FGb" -l |
372
ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds --output-format=hoa - - > output.hoa
373
374
375
376
377
378
379
380
381
382
383
#+END_SRC

Let's draw it:
#+NAME: autfiltsm1
#+BEGIN_SRC sh :results verbatim :exports code
autfilt output.hoa --dot=.a
#+END_SRC
#+RESULTS: autfiltsm1
#+begin_example
digraph G {
  rankdir=LR
384
  label=<(Fin(<font color="#5DA5DA">⓿</font>) &amp; Inf(<font color="#F17CB0">❶</font>)) | (Fin(<font color="#FAA43A">❷</font>) &amp; Inf(<font color="#B276B2">❸</font>))>
385
386
387
388
389
390
391
392
  labelloc="t"
  node [shape="circle"]
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
  I [label="", style=invis, width=0]
  I -> 0
393
  0 [label=<0<br/><font color="#5DA5DA">⓿</font><font color="#FAA43A">❷</font>>]
394
395
396
397
  0 -> 0 [label=<!a &amp; !b>]
  0 -> 1 [label=<a &amp; !b>]
  0 -> 2 [label=<!a &amp; b>]
  0 -> 3 [label=<a &amp; b>]
398
  1 [label=<1<br/><font color="#F17CB0">❶</font><font color="#FAA43A">❷</font>>]
399
400
401
402
  1 -> 0 [label=<!a &amp; !b>]
  1 -> 1 [label=<a &amp; !b>]
  1 -> 2 [label=<!a &amp; b>]
  1 -> 3 [label=<a &amp; b>]
403
  2 [label=<2<br/><font color="#5DA5DA">⓿</font><font color="#B276B2">❸</font>>]
404
405
406
407
  2 -> 0 [label=<!a &amp; !b>]
  2 -> 1 [label=<a &amp; !b>]
  2 -> 2 [label=<!a &amp; b>]
  2 -> 3 [label=<a &amp; b>]
408
  3 [label=<3<br/><font color="#F17CB0">❶</font><font color="#B276B2">❸</font>>]
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
  3 -> 0 [label=<!a &amp; !b>]
  3 -> 1 [label=<a &amp; !b>]
  3 -> 2 [label=<!a &amp; b>]
  3 -> 3 [label=<a &amp; b>]
}
#+end_example

#+BEGIN_SRC dot :file autfiltsm1.png :cmdline -Tpng :var txt=autfiltsm1 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:autfiltsm1.png]]

So this is a state-based Rabin automaton with two pairs.  If we call
=autfilt= with the =--sat-minimize= option, we can get the following
transition-based version (the output may change depending on the SAT
solver used):

#+NAME: autfiltsm2
#+BEGIN_SRC sh :results verbatim :exports code
autfilt --sat-minimize output.hoa --dot=.a
#+END_SRC
#+RESULTS: autfiltsm2
#+begin_example
digraph G {
  rankdir=LR
435
  label=<(Fin(<font color="#5DA5DA">⓿</font>) &amp; Inf(<font color="#F17CB0">❶</font>)) | (Fin(<font color="#FAA43A">❷</font>) &amp; Inf(<font color="#B276B2">❸</font>))>
436
437
438
439
440
441
442
443
444
  labelloc="t"
  node [shape="circle"]
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
  I [label="", style=invis, width=0]
  I -> 0
  0 [label="0"]
445
446
447
448
  0 -> 0 [label=<a &amp; b<br/><font color="#F17CB0">❶</font>>]
  0 -> 0 [label=<!a &amp; !b<br/><font color="#5DA5DA">⓿</font><font color="#FAA43A">❷</font>>]
  0 -> 0 [label=<a &amp; !b<br/><font color="#F17CB0">❶</font><font color="#FAA43A">❷</font>>]
  0 -> 0 [label=<!a &amp; b<br/><font color="#5DA5DA">⓿</font><font color="#B276B2">❸</font>>]
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
}
#+end_example

#+BEGIN_SRC dot :file autfiltsm2.png :cmdline -Tpng :var txt=autfiltsm2 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:autfiltsm2.png]]

We can also attempt to build a state-based version with

#+NAME: autfiltsm3
#+BEGIN_SRC sh :results verbatim :exports code
autfilt -S --sat-minimize output.hoa --dot=.a
#+END_SRC

#+RESULTS: autfiltsm3
#+begin_example
digraph G {
  rankdir=LR
469
  label=<(Fin(<font color="#5DA5DA">⓿</font>) &amp; Inf(<font color="#F17CB0">❶</font>)) | (Fin(<font color="#FAA43A">❷</font>) &amp; Inf(<font color="#B276B2">❸</font>))>
470
471
472
473
474
475
476
477
  labelloc="t"
  node [shape="circle"]
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
  I [label="", style=invis, width=0]
  I -> 0
478
  0 [label=<0<br/><font color="#F17CB0">❶</font><font color="#FAA43A">❷</font>>]
479
480
  0 -> 0 [label=<b>]
  0 -> 1 [label=<!b>]
481
  1 [label=<1<br/><font color="#5DA5DA">⓿</font><font color="#B276B2">❸</font>>]
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
  1 -> 0 [label=<!a>]
  1 -> 1 [label=<a>]
}
#+end_example

#+BEGIN_SRC dot :file autfiltsm3.png :cmdline -Tpng :var txt=autfiltsm3 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:autfiltsm3.png]]

This is clearly smaller than the input automaton.  In this example the
acceptance condition did not change.  The SAT-based minimization only
tries to minimize the number of states, but sometime the
simplifications algorithms that are run before we attempt SAT-solving
will simplify the acceptance, because even removing a single
acceptance set can halve the run time.

You can however force a specific acceptance to be used as output.
Let's try with generalized co-Büchi for instance:

#+NAME: autfiltsm4
#+BEGIN_SRC sh :results verbatim :exports code
autfilt -S --sat-minimize='acc="generalized-co-Buchi 2"' output.hoa --dot=.a
#+END_SRC

#+RESULTS: autfiltsm4
#+begin_example
digraph G {
  rankdir=LR
  label=<Fin(<font color="#5DA5DA">⓿</font>)|Fin(<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]
  I [label="", style=invis, width=0]
  I -> 0
  0 [label=<0<br/><font color="#5DA5DA">⓿</font>>]
  0 -> 0 [label=<a>]
  0 -> 1 [label=<!a>]
  1 [label=<1<br/><font color="#F17CB0">❶</font>>]
  1 -> 0 [label=<!b>]
  1 -> 1 [label=<b>]
}
#+end_example

#+BEGIN_SRC dot :file autfiltsm4.png :cmdline -Tpng :var txt=autfiltsm4 :exports results
$txt
#+END_SRC

#+RESULTS:
[[file:autfiltsm4.png]]


Note that instead of naming the acceptance condition, you can actually
give an acceptance formula in the [[http://adl.github.io/hoaf/#acceptance][HOA syntax]].  For example we can
attempt to create a co-Büchi automaton with

#+NAME: autfiltsm5
#+BEGIN_SRC sh :results verbatim :exports code
autfilt -S --sat-minimize='acc="Fin(0)"' output.hoa --dot=.a
#+END_SRC
#+RESULTS: autfiltsm5

#+BEGIN_SRC dot :file autfiltsm5.png :cmdline -Tpng :var txt=autfiltsm5 :exports results
$txt
#+END_SRC

#+RESULTS:
[[file:autfiltsm5.png]]


When forcing an acceptance condition, you should keep in mind that the
SAT-based minimization algorithm will look for automata that have
fewer states than the original automaton (after preliminary
simplifications).  This is not always reasonable.  For instance
constructing a Streett automaton from a Rabin automaton might require
561
more states.  An upper bound on the number of state can be passed
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
using a =max-states=123= argument to =--sat-minimize=.

If the input automaton is transition-based, but option =-S= is used to
produce a state-based automaton, then the original automaton is
temporarily converted into an automaton with state-based acceptance to
obtain an upper bound on the number of states if you haven't specified
=max-state=.  This upper bound might be larger than the one you would
specify by hand.

Here is an example demonstrating the case where the input automaton is
smaller than the output.   Let's take this small TGBA as input:

#+NAME: autfiltsm6
#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba 'GFa & GFb' -H > output2.hoa
autfilt output2.hoa --dot=.a
#+END_SRC

#+RESULTS: autfiltsm6
#+begin_example
digraph G {
  rankdir=LR
  label=<Inf(<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]
  I [label="", style=invis, width=0]
  I -> 0
  0 [label="0"]
  0 -> 0 [label=<a &amp; b<br/><font color="#5DA5DA">⓿</font><font color="#F17CB0">❶</font>>]
  0 -> 0 [label=<!a &amp; !b>]
  0 -> 0 [label=<!a &amp; b<br/><font color="#F17CB0">❶</font>>]
  0 -> 0 [label=<a &amp; !b<br/><font color="#5DA5DA">⓿</font>>]
}
#+end_example

#+BEGIN_SRC dot :file autfiltsm6.png :cmdline -Tpng :var txt=autfiltsm6 :exports results
$txt
#+END_SRC

#+RESULTS:
[[file:autfiltsm6.png]]


If we attempt to minimize it into a transition-based Büchi automaton,
with fewer states, it will fail, output no result, and return with a
non-zero exit code (because no automata where output).

#+NAME: autfiltsm7
#+BEGIN_SRC sh :results verbatim :exports both
autfilt --sat-minimize='acc="Buchi"' output2.hoa
echo $?
#+END_SRC
#+RESULTS: autfiltsm7
: 1

However if we allow more states, it will work:

#+NAME: autfiltsm8
#+BEGIN_SRC sh :results verbatim :exports code
autfilt --sat-minimize='acc="Buchi",max-states=3' output2.hoa --dot=.a
#+END_SRC

#+RESULTS: autfiltsm8
#+begin_example
digraph G {
  rankdir=LR
  label=<Inf(<font color="#5DA5DA">⓿</font>)>
  labelloc="t"
  node [shape="circle"]
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
  I [label="", style=invis, width=0]
  I -> 0
  0 [label="0"]
  0 -> 0 [label=<!b>]
  0 -> 0 [label=<a &amp; b<br/><font color="#5DA5DA">⓿</font>>]
  0 -> 1 [label=<!a &amp; b<br/><font color="#5DA5DA">⓿</font>>]
  1 [label="1"]
  1 -> 0 [label=<a>]
  1 -> 1 [label=<!a>]
}
#+end_example

#+BEGIN_SRC dot :file autfiltsm8.png :cmdline -Tpng :var txt=autfiltsm8 :exports results
$txt
#+END_SRC

#+RESULTS:
[[file:autfiltsm8.png]]


The =--sat-minimize= option takes a comma separated list of arguments
that can be any of the following:

- =acc=DOUBLEQUOTEDSTRING= :: where the =DOUBLEQUOTEDSTRING= is an
     acceptance formula in the [[http://adl.github.io/hoaf/#acceptance][HOA syntax]], or a parametrized acceptance
     name (the different [[http://adl.github.io/hoaf/#acceptance-specifications][=acc-name:= options from HOA]]).
- =max-states=N= :: where =N= is an upper-bound on the maximum
     number of states of the constructed automaton.
- =states=M= :: where =M= is a fixed number of states to use in the
     result (all the states needs not be accessible in the result,
     so the output might be smaller nonetheless).  If this option is
     used the SAT-based procedure is just used once to synthesize
     one automaton, and no further minimization is attempted.
- =dichotomy= :: instead of looking for a smaller automaton starting
     from =N=, and then checking =N-1=, =N-2=, etc., do a binary
     search starting from =N/2=.
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
- =colored= :: force all transitions (or all states if =-S= is used)
     to belong to exactly one acceptance condition.


The =colored= option is useful when used in conjunction with a parity
acceptance condition.  Indeed, the parity acceptance condition by
itself does not require that the acceptance sets form a partition of
the automaton (which is expected from parity automata).

Compare the following, where parity acceptance is used, but the
automaton is not colored:

#+NAME: autfiltsm9
#+BEGIN_SRC sh :results verbatim :exports code
autfilt -S --sat-minimize='acc="parity max even 3"' output2.hoa --dot=.a
#+END_SRC
#+RESULTS: autfiltsm9
#+begin_example
digraph G {
  rankdir=LR
  label=<Inf(<font color="#FAA43A">❷</font>) | (Fin(<font color="#F17CB0">❶</font>) &amp; Inf(<font color="#5DA5DA">⓿</font>))>
  labelloc="t"
  node [shape="circle"]
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
  I [label="", style=invis, width=0]
  I -> 0
  0 [label=<0>]
  0 -> 0 [label=<!a>]
  0 -> 1 [label=<a &amp; !b>]
  0 -> 2 [label=<a &amp; b>]
  1 [label=<1>]
  1 -> 1 [label=<!b>]
  1 -> 2 [label=<b>]
  2 [label=<2<br/><font color="#5DA5DA">⓿</font>>]
  2 -> 0 [label=<1>]
}
#+end_example

#+BEGIN_SRC dot :file autfiltsm9.png :cmdline -Tpng :var txt=autfiltsm9 :exports results
$txt
#+END_SRC

#+RESULTS:
[[file:autfiltsm9.png]]

... to the following, where the automaton is colored, i.e., each state
belong to exactly one acceptance set:

#+NAME: autfiltsm10
#+BEGIN_SRC sh :results verbatim :exports code
autfilt -S --sat-minimize='acc="parity max even 3",colored' output2.hoa --dot=.a
#+END_SRC
#+RESULTS: autfiltsm10
#+begin_example
digraph G {
  rankdir=LR
  label=<Inf(<font color="#FAA43A">❷</font>) | (Fin(<font color="#F17CB0">❶</font>) &amp; Inf(<font color="#5DA5DA">⓿</font>))>
  labelloc="t"
  node [shape="circle"]
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
  I [label="", style=invis, width=0]
  I -> 0
  0 [label=<0<br/><font color="#F17CB0">❶</font>>]
  0 -> 0 [label=<!b>]
  0 -> 1 [label=<b>]
  1 [label=<1<br/><font color="#F17CB0">❶</font>>]
  1 -> 1 [label=<!a>]
  1 -> 2 [label=<a>]
  2 [label=<2<br/><font color="#FAA43A">❷</font>>]
  2 -> 0 [label=<1>]
}
#+end_example

#+BEGIN_SRC dot :file autfiltsm10.png :cmdline -Tpng :var txt=autfiltsm10 :exports results
$txt
#+END_SRC

#+RESULTS:
[[file:autfiltsm10.png]]
760
761
762
763
764
765
766
767
768
769
770

* Logging statistics

If the environment variable =SPOT_SATLOG= is set to the name of a
file, the minimization function will append statistics about each of
its iterations in this file.

#+BEGIN_SRC sh :results verbatim :exports both
rm -f stats.csv
export SPOT_SATLOG=stats.csv
ltlfilt -f "Ga R (F!b & (c U b))" -l |
771
ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - |
772
773
774
775
dstar2tgba -D -x sat-minimize,sat-acc=2 --stats='input(states=%S) output(states=%s, acc-sets=%a, det=%d)'
cat stats.csv
#+END_SRC
#+RESULTS:
776
: input(states=11) output(states=5, acc-sets=2, det=1)
777
778
779
780
: 9,9,36,72,44064,9043076,616,18,258,24
: 8,7,29,56,19712,3493822,236,9,135,6
: 6,6,25,48,10512,1362749,97,4,42,2
: 5,,,,7200,784142,65,2,40,2
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798

The generated CSV file use the following columns:
- the n passed to the SAT-based minimization algorithm
  (it means the input automaton had n+1 states)
- number of reachable states in the output of
  the minimization.
- number of edges in the output
- number of transitions
- number of variables in the SAT problem
- number of clauses in the SAT problem
- user time for encoding the SAT problem
- system time for encoding the SAT problem
- user time for solving the SAT problem
- system time for solving the SAT problem

Times are measured with the times() function, and expressed
in ticks (usually: 1/100 of seconds).

799
In the above example, the input DRA had 11
800
states.  In the first line of the =stats.csv= file, you can see the
801
802
minimization function searching for a 9 state DTBA and obtaining a
8-state solution.  (Since the minimization function searched for a
803
9-state DTBA, it means it received a 10-state complete DTBA, so the
804
processings performed before the minimization procedure managed to
805
806
807
808
809
810
811
convert the 11-state DRA into a 10-state DTBA.)  Starting from the
8-state solution, it looked for (and found) a 7-state solution, and
then a 6-state solution.  The search for a 5-state complete DTBA
failed.  The final output is reported with 5 states, because by
default we output trim automata. If the =--complete= option had been
given, the useless sink state would have been kept and the output
automaton would have 6 states.
812
813


Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
814
#+BEGIN_SRC sh :results silent :exports results
815
816
rm -f output.hoa output2.hoa
#+END_SRC