satmin.org 27.2 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
#+DESCRIPTION: Spot command-line tools for minimizing ω-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
9
10
11
12
#+NAME: version
#+BEGIN_SRC sh :exports none
head -n 1 ../../picosat/VERSION | tr -d '\n'
#+END_SRC

13
14
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.
15
16
17
18
19
20

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.
21
2) Spot actually implements two SAT-based minimization procedures: one
22
   that builds a deterministic transition-based Büchi automaton
23
24
25
26
27
28
   (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.
29
30
31
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.)
32
4) Spot is built using PicoSAT call_version()[:results raw].
33
   This solver was chosen for its performance, simplicity of
34
35
   integration and license compatibility.  However, it is
   still possible to use an external SAT solver (as described below).
36
5) [[file:ltl2tgba.org][=ltl2tgba=]] and [[file:dstar2tgba.org][=dstar2tgba=]] will always try to output an automaton.
37
38
39
40
41
42
43
44
   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
45
46
   killed by a signal. [[file:autfilt.org][=autfilt --sat-minimize=]] will only output an
   automaton if the SAT-based minimization was successful.
47
48
49
50
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.
51

52
* How to change the SAT solver used
53

54
By default Spot uses PicoSAT call_version()[:results raw], this SAT-solver
55
56
57
is built into the Spot library, so that no temporary files are used to
store the problem.

58
The environment variable =SPOT_SATSOLVER= can be used to change the
59
60
61
62
SAT solver used by Spot.  This variable should describe a shell command
to run the SAT-solver on an input file called =%I= so that a model satisfying
the formula will be written in =%O=.  For instance to use [[http://www.labri.fr/perso/lsimon/glucose/][Glucose 3.0]], instead
of the builtin version of PicoSAT, define
63
#+BEGIN_SRC sh :exports code
64
65
66
67
export SPOT_SATSOLVER='glucose -verb=0 -model %I >%O'
#+END_SRC
We assume the SAT solver follows the input/output conventions of the
[[http://www.satcompetition.org/][SAT competition]]
68

69
* Enabling SAT-based minimization in =ltl2tgba= or =dstar2tgba=
70
71
72
73
74
75
76
77
78
79
80
81
82
83

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
84
deterministic automaton for =a U X(b | GF!b)=.  Instead we get a 4-state
85
86
non-deterministic automaton.

87
88
#+BEGIN_SRC sh
ltl2tgba -D 'a U X(b | GF!b)' --stats='states=%s, det=%d'
89
90
#+END_SRC
#+RESULTS:
91
: states=4, det=0
92
93
94
95
96
97
98
99
100
101

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:

102
103
#+BEGIN_SRC sh
ltl2tgba -D -x tba-det 'a U X(b | GF!b)' --stats='states=%s, det=%d'
104
105
#+END_SRC
#+RESULTS:
106
: states=9, det=1
107
108
109
110

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.

111
112
#+BEGIN_SRC sh
ltl2tgba -D -x sat-minimize 'a U X(b | GF!b)' --stats='states=%s, det=%d'
113
114
#+END_SRC
#+RESULTS:
115
: states=5, det=1
116
117
118

We can draw it:

119
#+NAME: gfaexxb3
120
121
122
#+BEGIN_SRC sh :exports code
ltl2tgba -D -x sat-minimize 'a U X(b | GF!b)' -d
#+END_SRC
123

124
#+BEGIN_SRC dot :file gfaexxb3.svg :var txt=gfaexxb3 :exports results
125
126
127
$txt
#+END_SRC
#+RESULTS:
128
[[file:gfaexxb3.svg]]
129

130
Clearly this automaton benefits from the transition-based
131
132
133
134
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.

135
#+NAME: gfaexxb4
136
#+BEGIN_SRC sh :results verbatim :exports code
137
138
ltl2tgba -BD -x sat-minimize 'a U X(b | GF!b)' -d
#+END_SRC
139

140
#+BEGIN_SRC dot :file gfaexxb4.svg :var txt=gfaexxb4 :exports results
141
142
143
$txt
#+END_SRC
#+RESULTS:
144
[[file:gfaexxb4.svg]]
145
146


147
148
149
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:
150

151
#+BEGIN_SRC sh
152
ltl2tgba -D -x sat-minimize 'G(F(!b & (X!a M (F!a & F!b))) U !b)' --stats='states=%s, det=%d'
153
154
#+END_SRC
#+RESULTS:
155
: states=5, det=0
156
157
158

The question, of course, is whether there exist a deterministic
automaton for this formula, in other words: is this a recurrence
159
160
property?  There are two ways to answer this question using Spot and
some help from [[http://www.ltl2dstar.de/][=ltl2dstar=]].
161
162
163
164
165
166
167

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:

168
#+BEGIN_SRC sh
169
ltlfilt --syntactic-recurrence -f 'G(F(!b & (X!a M (F!a & F!b))) U !b)'
170
171
#+END_SRC
#+RESULTS:
172
: G(F(!b & (X!a M (F!a & F!b))) U !b)
173
174
175
176
177
178
179
180

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.

181
#+BEGIN_SRC sh
182
ltlfilt --remove-wm -f 'G(F(!b & (X!a M (F!a & F!b))) U !b)' -l |
183
ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - |
184
185
186
187
188
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)

189
190
191
192
#+NAME: size
#+BEGIN_SRC sh :exports none
ltlfilt --remove-wm -f 'G(F(!b & (X!a M (F!a & F!b))) U !b)' -l |
ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - |
193
dstar2tgba -D --stats=$arg | tr -d '\n'
194
195
196
197
198
199
200
201
202
#+END_SRC

In the above command, =ltldo= 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 call_size(arg="%S")[:results raw]-state DRA is converted
into a call_size(arg="%s")[:results raw]-state DTBA by =dstar2tgba=.
Since that result is deterministic, we can conclude that the formula
was a recurrence.
203
204

As far as SAT-based minimization goes, =dstar2tgba= will take the same
205
options as =ltl2tgba=.  For instance we can see that the smallest DTBA
206
has call_size(arg="%s -x sat-minimize")[:results raw] states:
207

208
#+BEGIN_SRC sh
209
ltlfilt --remove-wm -f 'G(F(!b & (X!a M (F!a & F!b))) U !b)' -l |
210
ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - |
211
212
213
dstar2tgba -D -x sat-minimize --stats='input(states=%S) output(states=%s, acc-sets=%a, det=%d)'
#+END_SRC
#+RESULTS:
214
: input(states=11) output(states=4, acc-sets=1, det=1)
215
216
217

* More acceptance sets

218
219
220
The formula "=G(F(!b & (X!a M (F!a & F!b))) U !b)=" can in fact be
minimized into an even smaller automaton if we use multiple acceptance
sets.
221
222
223
224
225
226
227
228

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:

229
#+BEGIN_SRC sh
230
ltlfilt --remove-wm -f 'G(F(!b & (X!a M (F!a & F!b))) U !b)' -l |
231
ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - |
232
233
234
dstar2tgba -D -x sat-minimize,sat-acc=2 --stats='input(states=%S) output(states=%s, acc-sets=%a, det=%d)'
#+END_SRC
#+RESULTS:
235
: input(states=11) output(states=3, acc-sets=2, det=1)
236

237
238
239
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).
240
241
242
243
244
245
246
247

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
248
The following figure (from our [[https://www.lrde.epita.fr/~adl/dl/adl/baarir.14.forte.pdf][FORTE'14 paper]]) gives an overview of
249
250
251
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
252
253
to =dstar2tgba -D -x stat-minimize= (but =autfilt= support similar
options).
254

255
[[file:satmin.svg]]
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283

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
284
285
286
287
288
289
290
291
292
293
294
295
296
297
                  there exists an acceptance set such that the
                  resulting DTBA is equivalent to the input.
- =-x sat-minimize= :: enable SAT-based minimization. It is the same as
     =-x sat-minimize=1= (which is the default value). It performs a dichotomy
     to find the correct automaton size.This option implies =-x tba-det=.
- =-x sat-minimize=[2|3]= :: enable SAT-based
     minimization. Let us consider each intermediate automaton as a =step=
     towards the minimal automaton and assume =N= as the size of the starting
     automaton. =2= and =3= have been implemented with the aim of not
     restarting the encoding from scratch at each step. To do so, both restart
     the encoding after =N-1-(sat-incr-steps)= states have been won. Now,
     where is the difference? They both start by encoding the research of the
     =N-1= step and then:
       - =2= uses PicoSAT assumptions. It adds =sat-incr-steps= assumptions
298
         (each of them removing one more state) and then checks directly the
299
300
301
302
303
304
305
306
307
308
309
310
         =N-1-(sat-incr-steps)= step. If such automaton is found, the process is
         restarted. Otherwise, a binary search begins between =N-1= and
         =N-1-sat-incr-steps=. If not provided, =sat-incr-steps= default value
         is 6.
       - =3= checks incrementally each =N-(2+i)= step, =i= ranging from =0= to
         =sat-incr-steps=. This process is fully repeated until the minimal
         automaton is found. The last SAT problem solved correspond to the
         minimal automaton. =sat-incr-steps= defaults to 2.
     Both implies =-x tba-det=.
- =-x sat-minimize=4= :: enable SAT-based minimization. It tries to reduce the
     size of the automaton one state at a time. This option implies
     =-x tba-det=.
311
- =-x sat-incr-steps=N= :: set the value of =sat-incr-steps= to N. It does not
312
     make sense to use it without =-x sat-minimize=2= or =-x sat-minimize=3=.
313
314
315
316
317
318
319
- =-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
320
     default (use option =--complete= to output a complete automaton).
321
322
323
324
325
326
327
     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.

328
When options =-B= and =-x sat-minimize= are both used, =-x
329
330
331
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.
332

333
334
335
336
337
338
339
340
* 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.

341
For our example, let us first generate a deterministic Rabin
342
343
automaton with [[http://www.ltl2dstar.de/][=ltl2dstar=]].

344
#+BEGIN_SRC sh :results silent
345
ltlfilt -f 'FGa | FGb' -l |
346
ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds --output-format=hoa - - > output.hoa
347
348
349
350
#+END_SRC

Let's draw it:
#+NAME: autfiltsm1
351
#+BEGIN_SRC sh :exports code
352
autfilt output.hoa --dot
353
354
#+END_SRC

355
#+BEGIN_SRC dot :file autfiltsm1.svg :var txt=autfiltsm1 :exports results
356
357
358
$txt
#+END_SRC
#+RESULTS:
359
[[file:autfiltsm1.svg]]
360
361
362
363
364
365
366

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
367
#+BEGIN_SRC sh :exports code
368
autfilt --sat-minimize output.hoa --dot
369
370
#+END_SRC

371
#+BEGIN_SRC dot :file autfiltsm2.svg :var txt=autfiltsm2 :exports results
372
373
374
$txt
#+END_SRC
#+RESULTS:
375
[[file:autfiltsm2.svg]]
376
377
378
379

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

#+NAME: autfiltsm3
380
#+BEGIN_SRC sh :exports code
381
autfilt -S --sat-minimize output.hoa --dot
382
383
#+END_SRC

384
#+BEGIN_SRC dot :file autfiltsm3.svg :var txt=autfiltsm3 :exports results
385
386
387
$txt
#+END_SRC
#+RESULTS:
388
[[file:autfiltsm3.svg]]
389
390
391
392
393
394
395
396
397
398
399
400

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
401
#+BEGIN_SRC sh :exports code
402
autfilt -S --sat-minimize='acc="generalized-co-Buchi 2"' output.hoa --dot
403
404
#+END_SRC

405
#+BEGIN_SRC dot :file autfiltsm4.svg :var txt=autfiltsm4 :exports results
406
407
408
409
$txt
#+END_SRC

#+RESULTS:
410
[[file:autfiltsm4.svg]]
411
412
413
414
415
416
417


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
418
#+BEGIN_SRC sh :exports code
419
autfilt -S --sat-minimize='acc="Fin(0)"' output.hoa --dot
420
421
422
#+END_SRC
#+RESULTS: autfiltsm5

423
#+BEGIN_SRC dot :file autfiltsm5.svg :var txt=autfiltsm5 :exports results
424
425
426
427
$txt
#+END_SRC

#+RESULTS:
428
[[file:autfiltsm5.svg]]
429
430
431
432
433
434
435


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
436
more states.  An upper bound on the number of state can be passed
437
438
439
440
441
442
443
444
445
446
447
448
449
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
450
#+BEGIN_SRC sh :exports code
451
ltl2tgba 'GFa & GFb' >output2.hoa
452
autfilt output2.hoa --dot
453
454
#+END_SRC

455
#+BEGIN_SRC dot :file autfiltsm6.svg :var txt=autfiltsm6 :exports results
456
457
458
459
$txt
#+END_SRC

#+RESULTS:
460
[[file:autfiltsm6.svg]]
461
462
463
464


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
465
non-zero exit code (because no automata were output).
466
467

#+NAME: autfiltsm7
468
#+BEGIN_SRC sh
469
470
471
472
473
474
475
476
477
autfilt --sat-minimize='acc="Buchi"' output2.hoa
echo $?
#+END_SRC
#+RESULTS: autfiltsm7
: 1

However if we allow more states, it will work:

#+NAME: autfiltsm8
478
#+BEGIN_SRC sh :exports code
479
autfilt --sat-minimize='acc="Buchi",max-states=3' output2.hoa --dot
480
481
#+END_SRC

482
#+BEGIN_SRC dot :file autfiltsm8.svg :var txt=autfiltsm8 :exports results
483
484
485
486
$txt
#+END_SRC

#+RESULTS:
487
[[file:autfiltsm8.svg]]
488
489


490
491
492
493
494
495
496
By default, the SAT-based minimization tries to find a smaller automaton by
performing a binary search starting from =N/2= (N being the size of the
starting automaton). After various benchmarks, this algorithm proves to be the
best. However, in some cases, other rather similar methods might be better. The
algorithm to execute and some other parameters can be set thanks to the
=--sat-minimize= option.

497
498
499
500
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
501
     acceptance formula in the [[http://adl.github.io/hoaf/#acceptance][HOA syntax]], or a parameterized acceptance
502
503
504
505
506
507
508
509
     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.
510
511
512
513
514
515
516
517
518
- =sat-incr=[1|2]= :: =1= and =2= correspond respectively to
     =-x sat-minimize=2= and =-x sat-minimize=3= options.
     They have been implemented with the aim of not restarting the
     encoding from scratch at each step - a step is a minimized intermediate
     automaton. To do so, both restart the encoding after
     =N-1-(sat-incr-steps)= states have been won - =N= being the size of the
     starting automaton. Now, where is the difference? They both start by
     encoding the research of the =N-1= step and then:
       - =1= uses PicoSAT assumptions. It adds =steps= assumptions (each of
519
         them removing one more state) and then checks directly the
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
         =N-1-(sat-incr-steps)= step. If such automaton is found, the process is
         restarted. Otherwise, a binary search begins between =N-1= and
         =N-1-sat-incr-steps=. If not provided, =sat-incr-steps= defaults to 6.
       - =2= checks incrementally each =N-(2+i)= step, =i= ranging from =0= to
         =sat-incr-steps=. This process is fully repeated until the minimal
         automaton is found. The last SAT problem solved correspond to the
         minimal automaton. =sat-incr-steps= defaults to 2.
     Both implies =-x tba-det=.
- =sat-incr-steps=N= :: set the value of =sat-incr-steps= to =N=.
     This is used by =sat-incr= option.
- =sat-naive= :: use the =naive= algorithm to find a smaller automaton. It starts
     from =N= and then checks =N-1=, =N-2=, etc. until the last successful
     check.
- =sat-langmap= :: Find  the lower bound of default sat-minimize procedure. This
     relies on the fact that the size of the minimal automaton is at least equal
     to the  total  number  of different languages recognized by the automaton's
     states.
537
538
539
540
541
542
543
544
545
546
547
548
549
- =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
550
#+BEGIN_SRC sh :exports code
551
autfilt -S --sat-minimize='acc="parity max even 3"' output2.hoa --dot
552
553
#+END_SRC

554
#+BEGIN_SRC dot :file autfiltsm9.svg :var txt=autfiltsm9 :exports results
555
556
557
558
$txt
#+END_SRC

#+RESULTS:
559
[[file:autfiltsm9.svg]]
560
561
562
563
564

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

#+NAME: autfiltsm10
565
#+BEGIN_SRC sh :exports code
566
autfilt -S --sat-minimize='acc="parity max even 3",colored' output2.hoa --dot
567
568
#+END_SRC

569
#+BEGIN_SRC dot :file autfiltsm10.svg :var txt=autfiltsm10 :exports results
570
571
572
573
$txt
#+END_SRC

#+RESULTS:
574
[[file:autfiltsm10.svg]]
575
576
577
578
579
580
581

* 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.

582
#+BEGIN_SRC sh
583
584
rm -f stats.csv
export SPOT_SATLOG=stats.csv
585
ltlfilt -f 'Ga R (F!b & (c U b))' -l |
586
ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - |
587
588
589
dstar2tgba -D -x sat-minimize,sat-acc=2 --stats='input(states=%S) output(states=%s, acc-sets=%a, det=%d)'
#+END_SRC
#+RESULTS:
590
: input(states=11) output(states=5, acc-sets=2, det=1)
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606

Here is the contents of the =stats.csv= file:
#+begin_src sh :exports results :results output raw
sed '1a\
|-|
s/^/|/
s/$/|/
s/,/|/g
s/"HOA:.*--END--"/HOA:.../' stats.csv
#+end_src
#+RESULTS:
| input.states | target.states | reachable.states | edges | transitions | variables | clauses | enc.user | enc.sys | sat.user | sat.sys | automaton |
|--------------+---------------+------------------+-------+-------------+-----------+---------+----------+---------+----------+---------+-----------|
|            8 |             4 |                  |       |             |      5120 |  446320 |       22 |       1 |       17 |       0 |           |
|            8 |             6 |                6 |    29 |          48 |     11520 | 1515749 |       50 |       4 |      234 |       0 | HOA:...   |
|            8 |             5 |                  |       |             |      8000 |  874992 |       29 |       0 |       67 |       0 |           |
607
608

The generated CSV file use the following columns:
609
610
- =input.states=: the number of states of the reference automaton at this step
- =target.states=: the n passed to the SAT-based minimization algorithm
611
  (it means the input automaton had n+1 states)
612
613
614
615
616
617
618
619
620
621
622
623
624
625
- =reachable.states=: number of reachable states in the output of
  the minimization (with any luck this can be smaller than =target.states=)
- =edges=, =transitions=: number of edges or transitions in the output
- =variables=, =clauses=: size of the SAT problem
- =enc.user=, =enc.sys=: user and system time for encoding the SAT problem
- =sat.user=, =sat.sys=: user and system time for solving the SAT problem
- =automaton=: the automaton produced in HOA format.

Times are measured with the times() function, and expressed in ticks
(usually: 1/100 of seconds).  The encoding of the automaton in the CSV
file follows RFC4180 in escaping double-quote by doubling them.

In the above example, the DRA produced by =ltl2dstar= had 11 states.
In the first line of the =stats.csv= file, you can see the
626
627
628
629
630
631
632
633
634
635
636
minimization function had a 8-state input, which means that
=dstar2tgba= first reduced the 11-state (complete) DRA into a 8-state
(complete) DBA before calling the SAT-based minimization (the fact
that the input was reduced to a *DBA* is not very obvious from this
trace), This first line shows the SAT-based minimization for a
(complete) 5-state DTGBA and failing to find one.  Then on the next
line it looks for a 6-state solution, finds one.  Finally, it looks
for a 5-state solution, and cannot find one.  The reason the 5-state
attempt uses the 8-state automaton as input rather than the 6-state
automaton is because the 8-state automaton uses 1 acceptance states
(it's a DBA) while the 6-state automaton uses 2.
637
638
639
640
641

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.
642

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
643
#+BEGIN_SRC sh :results silent :exports results
644
645
rm -f output.hoa output2.hoa
#+END_SRC
646
647
648
* Python interface

See the [[https://spot.lrde.epita.fr/ipynb/satmin.html][=satmin.ipynb=]] notebook.
649
650
651
652
653
654
655

#  LocalWords:  utf html args SRC tgba dstar DTBA DT PicoSAT LPAR GF
#  LocalWords:  unminimized SATSOLVER det tba degeneralized gfaexxb
#  LocalWords:  svg txt BD ltlfilt DRA wm nba acc arg ltldo DBA WDBA
#  LocalWords:  SCC TCONG powerset incr DTGBA wdba FGa FGb autfiltsm
#  LocalWords:  Buchi GFa GFb DOUBLEQUOTEDSTRING langmap SATLOG csv
#  LocalWords:  src sed sys satmin ipynb