From f9e75de647432ea81bc80e1ac406e62b3a11e1ba Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 3 Feb 2020 11:01:01 +0100 Subject: [PATCH] partial_degeneralize: a support for disjunction of Fin * spot/twaalgos/degen.cc, spot/twaalgos/degen.hh: Implement this. Also throw a runtime error in case were todegen does not match any subformula. * tests/python/pdegen.py: Add tests. --- NEWS | 3 +- spot/twaalgos/degen.cc | 78 +++++++++++++++++++++++++++++------------- spot/twaalgos/degen.hh | 9 ++++- tests/python/pdegen.py | 56 +++++++++++++++++++++++++++++- 4 files changed, 120 insertions(+), 26 deletions(-) diff --git a/NEWS b/NEWS index e056b813d..3a9fad387 100644 --- a/NEWS +++ b/NEWS @@ -59,7 +59,8 @@ New in spot 2.8.5.dev (not yet released) - partial_degeneralize() is a new function performing partial degeneralization to get rid of conjunctions of Inf terms in - acceptance conditions. + acceptance conditions. This also works with disjunctions of + Fin terms in deterministic automata. - simplify_acceptance_here() and simplify_acceptance() learned to simplify subformulas like Fin(i)&Fin(j) or Inf(i)|Inf(j), or some diff --git a/spot/twaalgos/degen.cc b/spot/twaalgos/degen.cc index 29743fbab..9ed050dae 100644 --- a/spot/twaalgos/degen.cc +++ b/spot/twaalgos/degen.cc @@ -29,6 +29,7 @@ #include #include #include +#include //#define DEGEN_DEBUG @@ -738,7 +739,8 @@ namespace spot namespace { static acc_cond::mark_t - to_strip(const acc_cond::acc_code& code, acc_cond::mark_t todegen) + to_strip(const acc_cond::acc_code& code, acc_cond::mark_t todegen, + bool also_fin) { if (code.empty()) return todegen; @@ -753,38 +755,42 @@ namespace spot case acc_cond::acc_op::Or: --pos; break; + case acc_cond::acc_op::Fin: + case acc_cond::acc_op::FinNeg: + if (!also_fin) + { + pos -= 2; + tostrip -= code[pos].mark; + break; + } + // Handle Fin and Inf in the same way + SPOT_FALLTHROUGH; case acc_cond::acc_op::Inf: case acc_cond::acc_op::InfNeg: pos -= 2; if (code[pos].mark != todegen) tostrip -= code[pos].mark; break; - case acc_cond::acc_op::Fin: - case acc_cond::acc_op::FinNeg: - pos -= 2; - tostrip -= code[pos].mark; - break; } } while (pos > 0); return tostrip; } - static void + static bool update_acc_for_partial_degen(acc_cond::acc_code& code, acc_cond::mark_t todegen, acc_cond::mark_t tostrip, - acc_cond::mark_t accmark) + acc_cond::mark_t accmark, + bool also_fin) { - if (!todegen) + if (!todegen || code.empty()) { code &= acc_cond::acc_code::inf(accmark); - return; + return true; } - if (code.empty()) - return; - + bool updated = false; unsigned pos = code.size(); do { @@ -794,26 +800,46 @@ namespace spot case acc_cond::acc_op::Or: --pos; break; + case acc_cond::acc_op::Fin: + case acc_cond::acc_op::FinNeg: + if (!also_fin) + { + pos -= 2; + code[pos].mark = code[pos].mark.strip(tostrip); + break; + } + // Handle Fin and Inf in the same way + SPOT_FALLTHROUGH; case acc_cond::acc_op::Inf: case acc_cond::acc_op::InfNeg: pos -= 2; if (code[pos].mark == todegen) - code[pos].mark = accmark; + { + code[pos].mark = accmark; + updated = true; + } else - code[pos].mark = code[pos].mark.strip(tostrip); - break; - case acc_cond::acc_op::Fin: - case acc_cond::acc_op::FinNeg: - pos -= 2; - code[pos].mark = code[pos].mark.strip(tostrip); + { + code[pos].mark = code[pos].mark.strip(tostrip); + } break; } } while (pos > 0); + return updated; } - + [[noreturn]] static void + report_invalid_partial_degen_arg(acc_cond::mark_t todegen, + acc_cond::acc_code& cond) + { + std::ostringstream err; + err << "partial_degeneralize(): " << todegen + << " does not match any degeneralizable subformula of " + << cond << '.'; + throw std::runtime_error(err.str()); + } } @@ -825,11 +851,17 @@ namespace spot res->copy_ap_of(a); acc_cond::acc_code acc = a->get_acceptance(); - acc_cond::mark_t tostrip = to_strip(acc, todegen); + // We can also degeneralize disjunctions of Fin if the input is + // deterministic. + bool also_fin = a->acc().uses_fin_acceptance() && is_deterministic(a); + + acc_cond::mark_t tostrip = to_strip(acc, todegen, also_fin); acc_cond::mark_t keep = a->acc().all_sets() - tostrip; acc_cond::mark_t degenmark = {keep.count()}; - update_acc_for_partial_degen(acc, todegen, tostrip, degenmark); + if (!update_acc_for_partial_degen(acc, todegen, tostrip, degenmark, + also_fin)) + report_invalid_partial_degen_arg(todegen, acc); res->set_acceptance(acc); // auto* names = new std::vector; diff --git a/spot/twaalgos/degen.hh b/spot/twaalgos/degen.hh index f3a6f3e30..66608d5cc 100644 --- a/spot/twaalgos/degen.hh +++ b/spot/twaalgos/degen.hh @@ -99,7 +99,14 @@ namespace spot /// Fin(2). /// /// Cases where the sets listed in \a todegen also occur outside - /// of the Inf-conjunction are also supported. + /// of the Inf-conjunction are also supported. Subformulas that + /// are disjunctions of Fin(.) terms (e.g., Fin(1)|Fin(2)) can + /// also be degeneralized if the input automaton is deterministic. + /// + /// If this functions is called with a value of \a todegen that does + /// not match a (complete) conjunction of Inf(.), or in a + /// deterministic automaton a (complete) disjunction of Fin(.), an + /// std::runtime_error exception is thrown. SPOT_API twa_graph_ptr partial_degeneralize(const const_twa_graph_ptr& a, acc_cond::mark_t todegen); diff --git a/tests/python/pdegen.py b/tests/python/pdegen.py index d8771d9c4..eb6a21e06 100644 --- a/tests/python/pdegen.py +++ b/tests/python/pdegen.py @@ -24,7 +24,7 @@ import spot -a, b, d = spot.automata(""" +a, b, d, f = spot.automata(""" HOA: v1 States: 2 Start: 0 @@ -59,6 +59,18 @@ Acceptance: 1 Fin(0) State: 0 [0] 0 {0} --END-- +HOA: v1 +States: 2 +Start: 0 +AP: 1 "p0" +Acceptance: 2 Fin(0)|Fin(1) +--BODY-- +State: 0 +[0] 0 {0} +[0] 1 {1} +State: 1 +[!0] 0 +--END-- """) da = spot.partial_degeneralize(a, [0, 1]) @@ -97,6 +109,42 @@ assert dd.equivalent_to(d) assert dd.num_states() == 1 assert str(dd.get_acceptance()) == 'Inf(1) & Fin(0)' +e = spot.dualize(b) +de = spot.partial_degeneralize(e, [0, 1]) +assert de.equivalent_to(e) +assert de.num_states() == 4 + +de.copy_state_names_from(e) +dehoa = de.to_str('hoa') +assert dehoa == """HOA: v1 +States: 4 +Start: 0 +AP: 1 "p0" +acc-name: parity max even 2 +Acceptance: 2 Fin(1) & Inf(0) +properties: trans-labels explicit-labels trans-acc complete +properties: deterministic +--BODY-- +State: 0 "0#0" +[0] 1 +[!0] 2 +State: 1 "1#0" +[!0] 2 +[0] 3 {0 1} +State: 2 "3#0" +[t] 2 {0} +State: 3 "2#0" +[0] 1 {0 1} +[!0] 2 +--END--""" + +try: + df = spot.partial_degeneralize(f, [0, 1]) +except RuntimeError as e: + assert 'partial_degeneralize(): {0,1} does not' in str(e) +else: + raise RuntimeError("missing exception") + aut5 = spot.automaton(""" HOA: v1 States: 8 Start: 0 AP: 3 "p0" "p1" "p2" acc-name: generalized-Buchi 10 Acceptance: 10 Inf(0)&Inf(1)&Inf(2)&Inf(3)&Inf(4)&Inf(5)&Inf(6)&Inf(7)&Inf(8)&Inf(9) @@ -158,3 +206,9 @@ pdaut8 = spot.partial_degeneralize(aut8, sets) assert pdaut8.equivalent_to(aut8) assert daut8.num_states() == 22 assert pdaut8.num_states() == 9 + +aut9 = spot.dualize(aut8) +pdaut9 = spot.partial_degeneralize(aut9, sets) +assert pdaut9.equivalent_to(aut9) +# one more state than aut9, because dualize completed the automaton. +assert pdaut9.num_states() == 10