Commit 3378d72a authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

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.
parent 6b3de8af
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)
......
......@@ -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=<Inf(<font color="#FAA43A">❷</font>) | (Fin(<font color="#F17CB0">❶</font>) &amp; Inf(<font color="#5DA5DA">⓿</font>))>
labelloc="t"
node [shape="circle"]
fontname="Lato"
node [fontname="Lato"]
edge [fontname="Lato"]
node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
I [label="", style=invis, width=0]
I -> 0
0 [label=<0>]
0 -> 0 [label=<!a>]
0 -> 1 [label=<a &amp; !b>]
0 -> 2 [label=<a &amp; b>]
1 [label=<1>]
1 -> 1 [label=<!b>]
1 -> 2 [label=<b>]
2 [label=<2<br/><font color="#5DA5DA">⓿</font>>]
2 -> 0 [label=<1>]
}
#+end_example
#+BEGIN_SRC dot :file autfiltsm9.png :cmdline -Tpng :var txt=autfiltsm9 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:autfiltsm9.png]]
... to the following, where the automaton is colored, i.e., each state
belong to exactly one acceptance set:
#+NAME: autfiltsm10
#+BEGIN_SRC sh :results verbatim :exports code
autfilt -S --sat-minimize='acc="parity max even 3",colored' output2.hoa --dot=.a
#+END_SRC
#+RESULTS: autfiltsm10
#+begin_example
digraph G {
rankdir=LR
label=<Inf(<font color="#FAA43A">❷</font>) | (Fin(<font color="#F17CB0">❶</font>) &amp; Inf(<font color="#5DA5DA">⓿</font>))>
labelloc="t"
node [shape="circle"]
fontname="Lato"
node [fontname="Lato"]
edge [fontname="Lato"]
node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
I [label="", style=invis, width=0]
I -> 0
0 [label=<0<br/><font color="#F17CB0">❶</font>>]
0 -> 0 [label=<!b>]
0 -> 1 [label=<b>]
1 [label=<1<br/><font color="#F17CB0">❶</font>>]
1 -> 1 [label=<!a>]
1 -> 2 [label=<a>]
2 [label=<2<br/><font color="#FAA43A">❷</font>>]
2 -> 0 [label=<1>]
}
#+end_example
#+BEGIN_SRC dot :file autfiltsm10.png :cmdline -Tpng :var txt=autfiltsm10 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:autfiltsm10.png]]
* Logging statistics
......
......@@ -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.
......
......@@ -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);
}
......
......@@ -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);
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment