From 7e7c2575977c13a66c60f103388c46c20cb5dea6 Mon Sep 17 00:00:00 2001 From: Thomas Medioni Date: Fri, 30 Jun 2017 15:01:04 +0200 Subject: [PATCH] spot::sbacc() works on alternating automata, fix dualize Fixes #273. * NEWS: Mention this. * spot/twaalgos/dualize.cc, tests/python/dualize.py: Adapt dualize. * spot/twaalgos/sbacc.cc, tests/core/sbacc.test: sbacc support alternating automata --- NEWS | 2 ++ spot/twaalgos/dualize.cc | 7 +++- spot/twaalgos/sbacc.cc | 78 ++++++++++++++++++++++++---------------- tests/core/sbacc.test | 43 ++++++++++++++++++++++ tests/python/dualize.py | 73 +++++++++++++++++++++++++++++-------- 5 files changed, 157 insertions(+), 46 deletions(-) diff --git a/NEWS b/NEWS index 0dbd03bff..e30744b97 100644 --- a/NEWS +++ b/NEWS @@ -148,6 +148,8 @@ New in spot 2.3.5.dev (not yet released) input automaton with generalized Büchi/co-Büchi acceptance and convert it to a weak alternating automaton. + - spot::sbacc() is now able to work on alternating automata. + Python: - The 'spot.gen' package exports the functions from libspotgen. diff --git a/spot/twaalgos/dualize.cc b/spot/twaalgos/dualize.cc index 26fe1a32a..47b05a85a 100644 --- a/spot/twaalgos/dualize.cc +++ b/spot/twaalgos/dualize.cc @@ -24,6 +24,9 @@ #include #include #include +#include + +#include namespace spot { @@ -272,7 +275,9 @@ namespace spot public: dualizer(const const_twa_graph_ptr& aut) - : aut_(aut), + : aut_(is_universal(aut) + ? aut + : sbacc(std::const_pointer_cast(aut))), state_to_var_(aut_->num_states(), bddfalse), true_state_(-1U), acc_(0U), diff --git a/spot/twaalgos/sbacc.cc b/spot/twaalgos/sbacc.cc index 552c1e453..271a30d96 100644 --- a/spot/twaalgos/sbacc.cc +++ b/spot/twaalgos/sbacc.cc @@ -30,9 +30,6 @@ namespace spot { if (old->prop_state_acc()) return old; - if (!old->is_existential()) - throw std::runtime_error - ("sbacc() does not support alternation"); // We will need a mark that is rejecting to mark rejecting states. // If no such mark exist, our work is actually quite simple: we @@ -56,16 +53,18 @@ namespace spot // Marks that label one incoming transition from the same SCC. std::vector one_in(ns, 0U); for (auto& e: old->edges()) - if (si.scc_of(e.src) == si.scc_of(e.dst)) - { - common_in[e.dst] &= e.acc; - common_out[e.src] &= e.acc; - } + for (unsigned d: old->univ_dests(e.dst)) + if (si.scc_of(e.src) == si.scc_of(d)) + { + common_in[d] &= e.acc; + common_out[e.src] &= e.acc; + } for (unsigned s = 0; s < ns; ++s) common_out[s] |= common_in[s]; for (auto& e: old->edges()) - if (si.scc_of(e.src) == si.scc_of(e.dst)) - one_in[e.dst] = e.acc - common_out[e.src]; + for (unsigned d: old->univ_dests(e.dst)) + if (si.scc_of(e.src) == si.scc_of(d)) + one_in[d] = e.acc - common_out[e.src]; auto res = make_twa_graph(old->get_dict()); res->copy_ap_of(old); @@ -92,14 +91,24 @@ namespace spot return p.first->second; }; - unsigned old_init = old->get_init_state_number(); - acc_cond::mark_t init_acc = 0U; - if (!si.is_rejecting_scc(si.scc_of(old_init))) - // Use any edge going into the initial state to set the first - // acceptance mark. - init_acc = one_in[old_init] | common_out[old_init]; + std::vector old_init; + for (unsigned d: old->univ_dests(old->get_init_state_number())) + old_init.push_back(d); + + std::vector old_st; + internal::univ_dest_mapper uniq(res->get_graph()); + for (unsigned s: old_init) + { + acc_cond::mark_t init_acc = 0U; + if (!si.is_rejecting_scc(si.scc_of(s))) + // Use any edge going into the initial state to set the first + // acceptance mark. + init_acc = one_in[s] | common_out[s]; + + old_st.push_back(new_state(s, init_acc)); + } + res->set_init_state(uniq.new_univ_dests(old_st.begin(), old_st.end())); - res->set_init_state(new_state(old_init, init_acc)); while (!todo.empty()) { auto one = todo.back(); @@ -108,20 +117,27 @@ namespace spot bool maybe_accepting = !si.is_rejecting_scc(scc_src); for (auto& t: old->out(one.first.first)) { - unsigned scc_dst = si.scc_of(t.dst); - acc_cond::mark_t acc = 0U; - bool dst_acc = !si.is_rejecting_scc(scc_dst); - if (maybe_accepting && scc_src == scc_dst) - acc = t.acc - common_out[t.src]; - else if (dst_acc) - // We enter a new accepting SCC. Use any edge going into - // t.dst from this SCC to set the initial acceptance mark. - acc = one_in[t.dst]; - if (dst_acc) - acc |= common_out[t.dst]; - else - acc = unsat_mark.second; - res->new_edge(one.second, new_state(t.dst, acc), + std::vector dests; + for (unsigned d: old->univ_dests(t.dst)) + { + unsigned scc_dst = si.scc_of(d); + acc_cond::mark_t acc = 0U; + bool dst_acc = !si.is_rejecting_scc(scc_dst); + if (maybe_accepting && scc_src == scc_dst) + acc = t.acc - common_out[t.src]; + else if (dst_acc) + // We enter a new accepting SCC. Use any edge going into + // t.dst from this SCC to set the initial acceptance mark. + acc = one_in[d]; + if (dst_acc) + acc |= common_out[d]; + else + acc = unsat_mark.second; + + dests.push_back(new_state(d, acc)); + } + res->new_edge(one.second, + uniq.new_univ_dests(dests.begin(), dests.end()), t.cond, one.first.second); } } diff --git a/tests/core/sbacc.test b/tests/core/sbacc.test index ca960a9ae..c2c715581 100755 --- a/tests/core/sbacc.test +++ b/tests/core/sbacc.test @@ -224,3 +224,46 @@ State: 1 EOF autfilt --sbacc taut.hoa > out.hoa diff out.hoa expect.hoa + +cat >alt.hoa <expect.hoa < out.hoa +diff out.hoa expect.hoa diff --git a/tests/python/dualize.py b/tests/python/dualize.py index d06e9f6ad..825b78139 100755 --- a/tests/python/dualize.py +++ b/tests/python/dualize.py @@ -394,12 +394,11 @@ State: 2 [0] 2 --END--""") - dual = spot.dualize(aut) h = dual.to_str('hoa') assert h == """HOA: v1 -States: 2 +States: 3 Start: 0 AP: 2 "a" "b" acc-name: all @@ -407,9 +406,11 @@ Acceptance: 0 t properties: trans-labels explicit-labels state-acc deterministic --BODY-- State: 0 -[!0 | !1] 1 +[0&1] 1 +[!0 | !1] 2 State: 1 -[t] 1 +State: 2 +[t] 2 --END--""" aut = spot.automaton(""" @@ -492,6 +493,45 @@ State: 2 {0} [t] 2 --END--""" +aut = spot.automaton(""" +HOA: v1 +States: 3 +Start: 0 +AP: 1 "a" +Acceptance: 2 Fin(0) & Inf(1) +properties: trans-labels explicit-labels +--BODY-- +State: 0 +[!0] 0 +[0] 1 {0} +[0] 2 {1} +State: 1 +[t] 0 +State: 2 +[t] 0 +--END--""") + +dual = spot.dualize(aut) +assert dualtype(aut, dual) +h = dual.to_str('hoa') + +assert h == """HOA: v1 +States: 3 +Start: 0 +AP: 1 "a" +acc-name: parity min even 2 +Acceptance: 2 Inf(0) | Fin(1) +properties: univ-branch trans-labels explicit-labels state-acc complete +properties: deterministic +--BODY-- +State: 0 +[!0] 0 +[0] 1&2 +State: 1 {0} +[t] 0 +State: 2 {1} +[t] 0 +--END--""" aut = spot.translate('G!a R XFb') test_assert(aut) @@ -499,12 +539,12 @@ dual = spot.dualize(aut) h = dual.to_str('hoa') assert h == """HOA: v1 -States: 5 +States: 6 Start: 0 AP: 2 "a" "b" acc-name: co-Buchi Acceptance: 1 Fin(0) -properties: univ-branch trans-labels explicit-labels trans-acc complete +properties: univ-branch trans-labels explicit-labels state-acc complete properties: deterministic --BODY-- State: 0 @@ -512,17 +552,22 @@ State: 0 [!0] 1&2 State: 1 [0&!1] 1 -[0&1] 1 {0} +[0&1] 4 +[!0&1] 2&4 [!0&!1] 1&2 -[!0&1] 1&2 {0} State: 2 [!0&1] 3 -[0 | !1] 4 -State: 3 -[!0] 3 {0} -[0] 4 -State: 4 -[t] 4 +[0 | !1] 5 +State: 3 {0} +[!0] 3 +[0] 5 +State: 4 {0} +[0&!1] 1 +[0&1] 4 +[!0&1] 2&4 +[!0&!1] 1&2 +State: 5 +[t] 5 --END--"""