diff --git a/NEWS b/NEWS index 9396e1f92..3dc7f3c2f 100644 --- a/NEWS +++ b/NEWS @@ -5,7 +5,7 @@ New in spot 1.99b (not yet released) - Spot now works with automata that can represent more than generalized Büchi acceptance. Older versions were built around the concept of TGBA (Transition-based Generalized Büchi - Automata) while this is version now deal with what we call TωA + Automata) while this version now deals with what we call TωA (Transition-based ω-Automata). TωA support arbitrary acceptance conditions specified as a Boolean formula of transition sets that must be visited infinitely often or finitely often. This @@ -239,6 +239,14 @@ New in spot 1.99b (not yet released) whether an automaton is unambigous, and this is used by autfilt --is-unmabiguous. + - The SAT-based minimization algorithm for deterministic automata + has been updated to work with ω-Automaton with any acceptance. + The input and the output acceptance can be different, so for + instance it is possible to create a minimal deterministic + Streett automaton starting from a deterministic Rabin automaton. + This functionnality is available via autfilt's --sat-minimize + option. See doc/userdoc/satmin.html for details. + * Noteworthy code changes - Boost is not used anymore. diff --git a/doc/org/satmin.org b/doc/org/satmin.org index 46b04cd74..4483e0b06 100644 --- a/doc/org/satmin.org +++ b/doc/org/satmin.org @@ -1,26 +1,29 @@ -#+TITLE: SAT-based Minimization of Deterministic (Generalized) Büchi Automata +#+TITLE: SAT-based Minimization of Deterministic ω-Automata #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html -This page explains how to use [[file:ltl2tgba.org][=ltl2tgba=]] or [[file:dstar2tgba.org][=dstar2tgba=]] to minimize -deterministic automata using a SAT solver. +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 implement two SAT-based minimization procedures: one +2) Spot actually implements two SAT-based minimization procedures: one that builds a deterministic transition-based Büchi automaton - (DTBA), and one the builds a deterministic transition-based - generalized Büchi automaton (DTGBA). For the latter, we can supply - the number $m$ of acceptance sets to use. + (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 +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 @@ -29,9 +32,12 @@ Let us first state a few facts about this minimization procedure. 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. -6) Details about the SAT encoding used in the two procedures can be - found in our [[http://www.lrde.epita.fr/~adl/dl/adl/baarir.14.forte.pdf][FORTE'14 paper]]. + killed by a signal. [[file:autfilt.org][=autfilt --sat-minimize=]] will only output an + automaton if the SAT-based minimization was successful. +6) Our [[http://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. Since then, the technique used in + the SAT encoding for deterministic TGBA has been generalized to + deal with any deterministic TωA. * How to change the SAT solver used @@ -46,7 +52,7 @@ 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 for deterministic automata +* 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= @@ -205,8 +211,8 @@ ltl2tgba -D -x sat-minimize "Ga R (F!b & (c U b))" --stats='states=%s, det=%d' 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=]]). +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. @@ -274,7 +280,9 @@ dstar2tgba -D -x sat-minimize,sat-acc=2 --stats='input(states=%S) output(states= #+RESULTS: : input(states=11) output(states=5, acc-sets=2, det=1) -Beware that the size of the SAT problem is exponential in the number of acceptance sets. +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 @@ -283,11 +291,11 @@ degeneralized in the meantime for the purpose of determinization. * Low-level details -The following figure 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=. +The following figure (from our [[http://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]] @@ -343,8 +351,327 @@ The following options can be used to fine-tune this procedure: - =-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. +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 an deterministic Rabin +automaton with [[http://www.ltl2dstar.de/][=ltl2dstar=]]. + +#+BEGIN_SRC sh :results verbatim :exports code +ltlfilt -f "FGa | FGb" -l | +ltl2dstar --ltl2nba=spin:../../src/bin/ltl2tgba@-Ds --output-format=hoa - - > output.hoa +#+END_SRC +#+RESULTS: + +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 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' -H > 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=. * Logging statistics @@ -397,3 +724,8 @@ 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 verbatim :exports none +rm -f output.hoa output2.hoa +#+END_SRC diff --git a/doc/org/tools.org b/doc/org/tools.org index fa36dc43c..69f76bc71 100644 --- a/doc/org/tools.org +++ b/doc/org/tools.org @@ -54,7 +54,7 @@ corresponding commands are hidden. * Advanced use-cases - [[file:csv.org][Reading and writing CSV files]] -- [[file:satmin.org][SAT-based minimization of Deterministic (Generalized) Büchi automata]] +- [[file:satmin.org][SAT-based minimization of Deterministic ω-Automata]] * Citing diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index 835efc765..d408a7202 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -585,7 +585,7 @@ namespace if (opt_sat_minimize) { - aut = spot::sat_minimize(aut, opt_sat_minimize); + aut = spot::sat_minimize(aut, opt_sat_minimize, sbacc); if (!aut) return 0; } diff --git a/src/tests/satmin2.test b/src/tests/satmin2.test index d7eb8b272..a970b1fa0 100755 --- a/src/tests/satmin2.test +++ b/src/tests/satmin2.test @@ -108,7 +108,7 @@ $autfilt --sat-minimize='acc="Fin(0)|Inf(1)"' test.hoa --stats=%s >output test `cat output` = 1 # How about a state-based DSA? -$autfilt --sat-minimize='state-based,acc="Fin(0)|Inf(1)"' test.hoa \ +$autfilt -S --sat-minimize='acc="Fin(0)|Inf(1)"' test.hoa \ --stats=%s > output test `cat output` = 3 diff --git a/src/twa/twagraph.hh b/src/twa/twagraph.hh index 6d49b39a0..5ad66f5c4 100644 --- a/src/twa/twagraph.hh +++ b/src/twa/twagraph.hh @@ -436,6 +436,16 @@ namespace spot /// Remove all unreachable states. void purge_unreachable_states(); + acc_cond::mark_t state_acc_sets(unsigned s) const + { + assert(has_state_based_acc() || acc_.num_sets() == 0); + for (auto& t: g_.out(s)) + // Stop at the first transition, since the remaining should be + // labeled identically. + return t.acc; + return 0U; + } + bool state_is_accepting(unsigned s) const { assert(has_state_based_acc() || acc_.num_sets() == 0); diff --git a/src/twaalgos/dotty.cc b/src/twaalgos/dotty.cc index eb2d11f7f..0737f1d4a 100644 --- a/src/twaalgos/dotty.cc +++ b/src/twaalgos/dotty.cc @@ -417,7 +417,10 @@ namespace spot else os_ << s; os_ << '"'; - if (mark_states_ && aut_->state_is_accepting(s)) + // Use state_acc_sets(), not state_is_accepting() because + // on co-Büchi automata we want to mark the rejecting + // states. + if (mark_states_ && aut_->state_acc_sets(s)) os_ << ", peripheries=2"; os_ << "]\n"; } diff --git a/src/twaalgos/dtbasat.cc b/src/twaalgos/dtbasat.cc index 5b7743289..91a117b96 100644 --- a/src/twaalgos/dtbasat.cc +++ b/src/twaalgos/dtbasat.cc @@ -641,6 +641,7 @@ namespace spot acc_cond::mark_t acc = a->set_buchi(); if (state_based) a->prop_state_based_acc(); + a->prop_deterministic(); a->new_states(satdict.cand_size); unsigned last_aut_trans = -1U; diff --git a/src/twaalgos/dtgbasat.cc b/src/twaalgos/dtgbasat.cc index da8ac354c..87cbc6a8d 100644 --- a/src/twaalgos/dtgbasat.cc +++ b/src/twaalgos/dtgbasat.cc @@ -39,6 +39,7 @@ #include "dtbasat.hh" #include "sccfilter.hh" #include "sbacc.hh" +#include "postproc.hh" // If you set the SPOT_TMPKEEP environment variable the temporary // file used to communicate with the sat solver will be left in @@ -988,6 +989,7 @@ namespace spot a->copy_ap_of(aut); if (state_based) a->prop_state_based_acc(); + a->prop_deterministic(); a->set_acceptance(satdict.cand_nacc, satdict.cand_acc); a->new_states(satdict.cand_size); @@ -1075,7 +1077,6 @@ namespace spot #endif a->merge_transitions(); - return a; } } @@ -1209,7 +1210,7 @@ namespace spot } twa_graph_ptr - sat_minimize(twa_graph_ptr a, const char* opt) + sat_minimize(twa_graph_ptr a, const char* opt, bool state_based) { option_map om; auto err = om.parse_options(opt); @@ -1224,20 +1225,22 @@ namespace spot throw std::runtime_error ("SAT-based minimization only work with deterministic automata"); - bool sb = om.get("state-based", 0); bool dicho = om.get("dichotomy", 0); int states = om.get("states", -1); int max_states = om.get("max-states", -1); - int nacc = om.get("gba", -1); auto accstr = om.get_str("acc"); - if (nacc != -1 && !accstr.empty()) - throw std::runtime_error("options 'gba' and 'acc' cannot " - "be both passed to sat_minimize()"); - + // Assume we are going to use the input automaton acceptance... + bool user_supplied_acc = false; acc_cond::acc_code target_acc = a->get_acceptance(); + int nacc = a->acc().num_sets(); + + if (accstr == "same") + accstr.clear(); + // ... unless the user specified otherwise if (!accstr.empty()) { + user_supplied_acc = true; target_acc = parse_acc_code(accstr.c_str()); // Just in case we were given something like // Fin(1) | Inf(3) @@ -1249,50 +1252,96 @@ namespace spot target_acc = target_acc.strip(a.comp(used), true); nacc = used.count(); } - else if (nacc != -1) + + bool target_is_buchi = false; + { + acc_cond acccond(nacc); + acccond.set_acceptance(target_acc); + target_is_buchi = acccond.is_buchi(); + } + + if (int preproc = om.get("preproc", 3)) { - target_acc = acc_cond::generalized_buchi(nacc); + postprocessor post; + auto sba = (state_based && a->has_state_based_acc()) ? + postprocessor::SBAcc : postprocessor::Any; + post.set_pref(postprocessor::Deterministic + | postprocessor::Complete + | sba); + post.set_type(postprocessor::Generic); + postprocessor::optimization_level level; + switch (preproc) + { + case 1: + level = postprocessor::Low; + break; + case 2: + level = postprocessor::Medium; + break; + case 3: + level = postprocessor::High; + break; + default: + throw + std::runtime_error("preproc should be a value between 0 and 3."); + } + post.set_level(level); + a = post.run(a, nullptr); + // If we have WDBA, it is necessarily minimal because + // postprocessor always run WDBA minimization in Deterministic + // mode. If the desired output is a Büchi automaton, or not + // desired acceptance was specified, stop here. There is not + // point in minimizing a minimal automaton. + if (a->is_inherently_weak() && a->is_deterministic() + && (target_is_buchi || !user_supplied_acc)) + return a; } else { - nacc = a->acc().num_sets(); + tgba_complete_here(a); } - bool target_is_buchi = - (nacc == 1 && target_acc.size() == 2 && - target_acc[1].op == acc_cond::acc_op::Inf - && target_acc[0].mark.has(0)); + if (states == -1 && max_states == -1) + { + if (state_based) + max_states = sbacc(a)->num_states(); + else + max_states = a->num_states(); + // If we have not user-supplied acceptance, the input + // automaton is a valid one, so we start the search with one + // less state. + max_states -= !user_supplied_acc; + } - tgba_complete_here(a); - - if (sb && states == -1 && max_states == -1) - max_states = sbacc(a)->num_states(); if (states == -1) { + auto orig = a; if (!target_is_buchi || !a->acc().is_buchi()) a = (dicho ? dtgba_sat_minimize_dichotomy : dtgba_sat_minimize) - (a, nacc, target_acc, sb, max_states); + (a, nacc, target_acc, state_based, max_states); else a = (dicho ? dtba_sat_minimize_dichotomy : dtba_sat_minimize) - (a, sb, max_states); + (a, state_based, max_states); + + if (!a && !user_supplied_acc) + a = orig; } else { if (!target_is_buchi || !a->acc().is_buchi()) - a = dtgba_sat_synthetize(a, nacc, target_acc, states, sb); + a = dtgba_sat_synthetize(a, nacc, target_acc, states, state_based); else - a = dtba_sat_synthetize(a, states, sb); + a = dtba_sat_synthetize(a, states, state_based); } if (a) { - if (a->acc().is_generalized_buchi()) - a = scc_filter(a); + if (state_based) + a = scc_filter_states(a); else - a->purge_dead_states(); + a = scc_filter(a); } - return a; } diff --git a/src/twaalgos/dtgbasat.hh b/src/twaalgos/dtgbasat.hh index 4d2bfc58c..36495b27c 100644 --- a/src/twaalgos/dtgbasat.hh +++ b/src/twaalgos/dtgbasat.hh @@ -81,15 +81,16 @@ namespace spot /// \brief High-level interface to SAT-based minimization /// /// Minimize the automaton \a aut, using options \a opt. - /// These options are given a comma-separated list of + /// These options are given as a comma-separated list of /// assignments of the form: /// - /// state-based = 1 - /// states = 10 - /// acc = generalized-Buchi 2 - /// acc = Rabin 3 - /// acc = same /* default */ + /// states = 10 // synthetize automaton with fixed number of states + /// max-states = 20 // minimize starting from this upper bound + /// acc = "generalized-Buchi 2" + /// acc = "Rabin 3" + /// acc = "same" /* default */ + /// dichotomy = 1 // use dichotomy instead of decreasing loop /// SPOT_API twa_graph_ptr - sat_minimize(twa_graph_ptr aut, const char* opt); + sat_minimize(twa_graph_ptr aut, const char* opt, bool state_based = false); } diff --git a/src/twaalgos/postproc.cc b/src/twaalgos/postproc.cc index fd762adbe..ff96d3be1 100644 --- a/src/twaalgos/postproc.cc +++ b/src/twaalgos/postproc.cc @@ -32,6 +32,7 @@ #include "complete.hh" #include "totgba.hh" #include "sbacc.hh" +#include "sepsets.hh" namespace spot { @@ -93,6 +94,8 @@ namespace spot twa_graph_ptr postprocessor::do_simul(const twa_graph_ptr& a, int opt) { + if (!has_separate_sets(a)) + return a; switch (opt) { case 0: