From 3378d72a8884e2338df8b69551e250d4ef8f7b2a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 3 Sep 2015 17:26:55 +0200 Subject: [PATCH] dtgbasat: add a colored option This was suggested by one of the reviewers of our LPAR'15 paper. * src/twaalgos/dtgbasat.cc, src/twaalgos/dtgbasat.hh: Implement the colored option. * src/tests/satmin2.test: Test it. * doc/org/satmin.org, NEWS: Document it. --- NEWS | 5 ++- doc/org/satmin.org | 93 ++++++++++++++++++++++++++++++++++++++-- src/tests/satmin2.test | 9 ++++ src/twaalgos/dtgbasat.cc | 70 ++++++++++++++++++++++++------ src/twaalgos/dtgbasat.hh | 13 ++++-- 5 files changed, 169 insertions(+), 21 deletions(-) diff --git a/NEWS b/NEWS index 19b0ac6fb..0b5888c0f 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,9 @@ New in spot 1.99.3a (not yet released) - Nothing yet. + * autfilt's --sat-minimize now takes a "colored" option to constrain + all transitions (or states) in the output automaton to belong to + exactly one acceptance sets. This is useful when targeting parity + acceptance. New in spot 1.99.3 (2015-08-26) diff --git a/doc/org/satmin.org b/doc/org/satmin.org index e3ad94822..3d2ae919f 100644 --- a/doc/org/satmin.org +++ b/doc/org/satmin.org @@ -35,10 +35,10 @@ Let us first state a few facts about this minimization procedure. 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%0A][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. +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 @@ -672,6 +672,91 @@ that can be any of the following: - =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 diff --git a/src/tests/satmin2.test b/src/tests/satmin2.test index 451bbd694..dc5f0bb35 100755 --- a/src/tests/satmin2.test +++ b/src/tests/satmin2.test @@ -112,6 +112,15 @@ $autfilt -S --sat-minimize='acc="Fin(0)|Inf(1)"' test.hoa \ --stats=%s > output test `cat output` = 3 +# How about a state-based DPA? +$autfilt -S --sat-minimize='acc="parity max even 3",colored' -H test.hoa \ + > output +cat output +grep 'properties:.*colored' output +grep 'States: 3' output +grep 'acc-name: parity max even 3' output +grep 'Acceptance: 3 Inf(2) | (Fin(1) & Inf(0))' output +test 3 = `grep -c 'State: [012] {[012]}' output` # I get headaches whenever I think about this acceptance condition, so # it should be a good test case. diff --git a/src/twaalgos/dtgbasat.cc b/src/twaalgos/dtgbasat.cc index 00cda5d10..ee6e774c2 100644 --- a/src/twaalgos/dtgbasat.cc +++ b/src/twaalgos/dtgbasat.cc @@ -604,7 +604,7 @@ namespace spot static sat_stats dtgba_to_sat(std::ostream& out, const_twa_graph_ptr ref, - dict& d, bool state_based) + dict& d, bool state_based, bool colored) { #if DEBUG debug_dict = ref->get_dict(); @@ -714,6 +714,45 @@ namespace spot ++nclauses; } + if (colored) + { + unsigned nacc = d.cand_nacc; + dout << "transitions belong to exactly one of the " + << nacc << " acceptance set\n"; + bdd all = bddtrue; + while (all != bddfalse) + { + bdd l = bdd_satoneset(all, ap, bddfalse); + all -= l; + for (unsigned q1 = 0; q1 < d.cand_size; ++q1) + for (unsigned q2 = 0; q2 < d.cand_size; ++q2) + { + for (unsigned i = 0; i < nacc; ++i) + { + transition_acc ti(q1, l, {i}, q2); + int tai = d.transaccid[ti]; + + for (unsigned j = 0; j < nacc; ++j) + if (i != j) + { + transition_acc tj(q1, l, {j}, q2); + int taj = d.transaccid[tj]; + out << -tai << ' ' << -taj << " 0\n"; + ++nclauses; + } + } + for (unsigned i = 0; i < nacc; ++i) + { + transition_acc ti(q1, l, {i}, q2); + int tai = d.transaccid[ti]; + out << tai << ' '; + } + out << "0\n"; + ++nclauses; + } + } + } + if (!d.all_silly_cand_acc.empty()) { dout << "no transition with silly acceptance\n"; @@ -1084,7 +1123,8 @@ namespace spot dtgba_sat_synthetize(const const_twa_graph_ptr& a, unsigned target_acc_number, const acc_cond::acc_code& target_acc, - int target_state_number, bool state_based) + int target_state_number, + bool state_based, bool colored) { if (target_state_number == 0) return nullptr; @@ -1103,7 +1143,7 @@ namespace spot timer_map t; t.start("encode"); - sat_stats s = dtgba_to_sat(solver(), a, d, state_based); + sat_stats s = dtgba_to_sat(solver(), a, d, state_based, colored); t.stop("encode"); t.start("solve"); solution = solver.get_solution(); @@ -1156,8 +1196,8 @@ namespace spot dtgba_sat_minimize(const const_twa_graph_ptr& a, unsigned target_acc_number, const acc_cond::acc_code& target_acc, - bool state_based, - int max_states) + bool state_based, int max_states, + bool colored) { int n_states = (max_states < 0) ? stats_reachable(a).states : max_states + 1; @@ -1167,7 +1207,8 @@ namespace spot { auto next = dtgba_sat_synthetize(prev ? prev : a, target_acc_number, - target_acc, --n_states, state_based); + target_acc, --n_states, + state_based, colored); if (!next) return prev; else @@ -1181,8 +1222,8 @@ namespace spot dtgba_sat_minimize_dichotomy(const const_twa_graph_ptr& a, unsigned target_acc_number, const acc_cond::acc_code& target_acc, - bool state_based, - int max_states) + bool state_based, int max_states, + bool colored) { if (max_states < 1) max_states = stats_reachable(a).states - 1; @@ -1194,7 +1235,8 @@ namespace spot int target = (max_states + min_states) / 2; auto next = dtgba_sat_synthetize(prev ? prev : a, target_acc_number, - target_acc, target, state_based); + target_acc, target, state_based, + colored); if (!next) { min_states = target + 1; @@ -1228,6 +1270,7 @@ namespace spot int states = om.get("states", -1); int max_states = om.get("max-states", -1); auto accstr = om.get_str("acc"); + bool colored = om.get("colored", 0); // Assume we are going to use the input automaton acceptance... bool user_supplied_acc = false; @@ -1316,9 +1359,9 @@ namespace spot if (states == -1) { auto orig = a; - if (!target_is_buchi || !a->acc().is_buchi()) + if (!target_is_buchi || !a->acc().is_buchi() || colored) a = (dicho ? dtgba_sat_minimize_dichotomy : dtgba_sat_minimize) - (a, nacc, target_acc, state_based, max_states); + (a, nacc, target_acc, state_based, max_states, colored); else a = (dicho ? dtba_sat_minimize_dichotomy : dtba_sat_minimize) (a, state_based, max_states); @@ -1328,8 +1371,9 @@ namespace spot } else { - if (!target_is_buchi || !a->acc().is_buchi()) - a = dtgba_sat_synthetize(a, nacc, target_acc, states, state_based); + if (!target_is_buchi || !a->acc().is_buchi() || colored) + a = dtgba_sat_synthetize(a, nacc, target_acc, states, + state_based, colored); else a = dtba_sat_synthetize(a, states, state_based); } diff --git a/src/twaalgos/dtgbasat.hh b/src/twaalgos/dtgbasat.hh index 36495b27c..ba04ce1c0 100644 --- a/src/twaalgos/dtgbasat.hh +++ b/src/twaalgos/dtgbasat.hh @@ -41,6 +41,9 @@ namespace spot /// of a state to share the same acceptance conditions, effectively /// turning the TGBA into a TBA. /// + /// \param colored if true, force all transitions to belong to + /// exactly one acceptance set. + /// /// This functions attempts to find a TGBA with \a target_acc_number /// acceptance sets and target_state_number states that is /// equivalent to \a a. If no such TGBA is found, a null pointer is @@ -50,7 +53,8 @@ namespace spot unsigned target_acc_number, const acc_cond::acc_code& target_acc, int target_state_number, - bool state_based = false); + bool state_based = false, + bool colored = false); /// \brief Attempt to minimize a deterministic TGBA with a SAT solver. /// @@ -63,7 +67,8 @@ namespace spot unsigned target_acc_number, const acc_cond::acc_code& target_acc, bool state_based = false, - int max_states = -1); + int max_states = -1, + bool colored = false); /// \brief Attempt to minimize a deterministic TGBA with a SAT solver. /// @@ -76,7 +81,8 @@ namespace spot unsigned target_acc_number, const acc_cond::acc_code& target_acc, bool state_based = false, - int max_states = -1); + int max_states = -1, + bool colored = false); /// \brief High-level interface to SAT-based minimization /// @@ -90,6 +96,7 @@ namespace spot /// acc = "Rabin 3" /// acc = "same" /* default */ /// dichotomy = 1 // use dichotomy instead of decreasing loop + /// colored = 1 // build a colored TωA /// SPOT_API twa_graph_ptr sat_minimize(twa_graph_ptr aut, const char* opt, bool state_based = false);