# -*- coding: utf-8 -*- #+TITLE: SAT-based Minimization of Deterministic ω-Automata #+DESCRIPTION: Spot command-line tools for minimizing ω-automata #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html 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. 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. 2) Spot actually implements two SAT-based minimization procedures: one that builds a deterministic transition-based Büchi automaton (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. 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.) 5) [[file:ltl2tgba.org][=ltl2tgba=]] and [[file:dstar2tgba.org][=dstar2tgba=]] will always try to output an automaton. 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 killed by a signal. [[file:autfilt.org][=autfilt --sat-minimize=]] will only output an automaton if the SAT-based minimization was successful. 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. * How to change the SAT solver used The environment variable =SPOT_SATSOLVER= can be used to change the 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. * Enabling SAT-based minimization in =ltl2tgba= or =dstar2tgba= 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: #+NAME: gfaexxb3 #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba -D -x sat-minimize 'GF(a <-> XXb)' -d #+END_SRC #+RESULTS: gfaexxb3 #+begin_example digraph G { rankdir=LR 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 -> 1 [label=⓿>] 0 -> 2 [label=] 0 -> 3 [label=] 0 -> 3 [label=⓿>] 1 [label="1"] 1 -> 0 [label=] 1 -> 0 [label=⓿>] 1 -> 1 [label=] 1 -> 1 [label=⓿>] 2 [label="2"] 2 -> 0 [label=] 2 -> 1 [label=⓿>] 2 -> 1 [label=] 2 -> 3 [label=⓿>] 3 [label="3"] 3 -> 2 [label=⓿>] 3 -> 2 [label=] 3 -> 3 [label=⓿>] 3 -> 3 [label=] } #+end_example #+BEGIN_SRC dot :file gfaexxb3.png :cmdline -Tpng :var txt=gfaexxb3 :exports results $txt #+END_SRC #+RESULTS: [[file:gfaexxb3.png]] Clearly this automaton benefits from the transition-based 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. #+NAME: gfaexxb4 #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba -BD -x sat-minimize 'GF(a <-> XXb)' -d #+END_SRC #+RESULTS: gfaexxb4 #+begin_example digraph G { rankdir=LR 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=] 0 -> 1 [label=] 0 -> 2 [label=] 1 [label="1", peripheries=2] 1 -> 4 [label=] 1 -> 5 [label=] 2 [label="2"] 2 -> 1 [label=] 2 -> 4 [label=] 2 -> 5 [label=] 3 [label="3", peripheries=2] 3 -> 0 [label=] 3 -> 1 [label=] 3 -> 2 [label=] 4 [label="4"] 4 -> 0 [label=] 4 -> 1 [label=] 4 -> 2 [label=] 4 -> 3 [label=] 5 [label="5"] 5 -> 1 [label=] 5 -> 3 [label=] 5 -> 4 [label=] 5 -> 5 [label=] } #+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 'G(F(!b & (X!a M (F!a & F!b))) U !b)' --stats='states=%s, det=%d' #+END_SRC #+RESULTS: : states=5, det=0 The question, of course, is whether there exist a deterministic automaton for this formula, in other words: is this a recurrence property? There are two ways to answer this question using Spot and some help from [[http://www.ltl2dstar.de/][=ltl2dstar=]]. 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 'G(F(!b & (X!a M (F!a & F!b))) U !b)' #+END_SRC #+RESULTS: : G(F(!b & (X!a M (F!a & F!b))) 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 --remove-wm -f 'G(F(!b & (X!a M (F!a & F!b))) U !b)' -l | ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - | 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) #+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 - - | dstar2tgba -D --stats=$arg #+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. As far as SAT-based minimization goes, =dstar2tgba= will take the same options as =ltl2tgba=. For instance we can see that the smallest DTBA has call_size(arg="%s -x sat-minimize")[:results raw] states: #+BEGIN_SRC sh :results verbatim :exports both ltlfilt --remove-wm -f 'G(F(!b & (X!a M (F!a & F!b))) U !b)' -l | ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - | 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=4, acc-sets=1, det=1) * More acceptance sets 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. 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 --remove-wm -f 'G(F(!b & (X!a M (F!a & F!b))) U !b)' -l | ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - | 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=3, acc-sets=2, det=1) 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). 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 The following figure (from our [[https://www.lrde.epita.fr/~adl/dl/adl/baarir.14.forte.pdf][FORTE'14 paper]]) gives an overview of 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=. [[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 default (use option =--complete= to output a complete automaton). 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. When options =-B= and =-x sat-minimize= are both used, =-x 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. * 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. For our example, let us first generate a deterministic Rabin automaton with [[http://www.ltl2dstar.de/][=ltl2dstar=]]. #+BEGIN_SRC sh :results silent :exports both ltlfilt -f 'FGa | FGb' -l | ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds --output-format=hoa - - > output.hoa #+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 label=<(Fin(⓿) & Inf(❶)) | (Fin(❷) & Inf(❸))> 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=] 0 -> 1 [label=] 0 -> 2 [label=] 0 -> 3 [label=] 1 [label=<1
❶❷>] 1 -> 0 [label=] 1 -> 1 [label=] 1 -> 2 [label=] 1 -> 3 [label=] 2 [label=<2
⓿❸>] 2 -> 0 [label=] 2 -> 1 [label=] 2 -> 2 [label=] 2 -> 3 [label=] 3 [label=<3
❶❸>] 3 -> 0 [label=] 3 -> 1 [label=] 3 -> 2 [label=] 3 -> 3 [label=] } #+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 label=<(Fin(⓿) & Inf(❶)) | (Fin(❷) & Inf(❸))> 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=❶>] 0 -> 0 [label=⓿❷>] 0 -> 0 [label=❶❷>] 0 -> 0 [label=⓿❸>] } #+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 label=<(Fin(⓿) & Inf(❶)) | (Fin(❷) & Inf(❸))> 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=] 0 -> 1 [label=] 1 [label=<1
⓿❸>] 1 -> 0 [label=] 1 -> 1 [label=] } #+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(❶)> 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=] 0 -> 1 [label=] 1 [label=<1
❶>] 1 -> 0 [label=] 1 -> 1 [label=] } #+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 more states. An upper bound on the number of state can be passed 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' >output2.hoa autfilt output2.hoa --dot=.a #+END_SRC #+RESULTS: autfiltsm6 #+begin_example digraph G { rankdir=LR label=⓿)&Inf(❶)> 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=⓿❶>] 0 -> 0 [label=] 0 -> 0 [label=❶>] 0 -> 0 [label=⓿>] } #+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=⓿)> 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=] 0 -> 0 [label=⓿>] 0 -> 1 [label=⓿>] 1 [label="1"] 1 -> 0 [label=] 1 -> 1 [label=] } #+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=. - =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=❷) | (Fin(❶) & Inf(⓿))> 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=] 0 -> 1 [label=] 0 -> 2 [label=] 1 [label=<1>] 1 -> 1 [label=] 1 -> 2 [label=] 2 [label=<2
⓿>] 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=❷) | (Fin(❶) & Inf(⓿))> 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=] 0 -> 1 [label=] 1 [label=<1
❶>] 1 -> 1 [label=] 1 -> 2 [label=] 2 [label=<2
❷>] 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]] * 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 | ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - | 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: : input(states=11) output(states=5, acc-sets=2, det=1) : 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 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). In the above example, the input DRA had 11 states. In the first line of the =stats.csv= file, you can see the minimization function searching for a 9 state DTBA and obtaining a 8-state solution. (Since the minimization function searched for a 9-state DTBA, it means it received a 10-state complete DTBA, so the processings performed before the minimization procedure managed to 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. #+BEGIN_SRC sh :results silent :exports results rm -f output.hoa output2.hoa #+END_SRC