diff --git a/src/tests/safra.cc b/src/tests/safra.cc index 811324718..34c1d566f 100644 --- a/src/tests/safra.cc +++ b/src/tests/safra.cc @@ -20,14 +20,14 @@ #include #include +#include "ltlparse/public.hh" // ltl::parse +#include "parseaut/public.hh" #include "twa/twagraph.hh" +#include "twaalgos/degen.hh" +#include "twaalgos/dot.hh" // print_dot +#include "twaalgos/hoa.hh" // print_hoa #include "twaalgos/safra.hh" #include "twaalgos/translate.hh" -#include "hoaparse/public.hh" -#include "ltlparse/public.hh" -#include "twaalgos/dotty.hh" -#include "twaalgos/hoa.hh" -#include "twaalgos/degen.hh" int help() @@ -37,11 +37,14 @@ int help() std::cerr << "\t--hoa file.hoa\tinput file has hoa format\n"; std::cerr << "\t-p\tpretty print states\n"; std::cerr << "\t-H\toutput hoa format\n"; + std::cerr << "\t-b\treduce result using bisimulation\n"; + std::cerr << "\t--emit_scc\ttransitions to accpting scc are accepting\n"; return 1; } int main(int argc, char* argv[]) { + bool emit_scc = false; bool sim = false; bool in_hoa = false; bool in_ltl = false; @@ -77,6 +80,8 @@ int main(int argc, char* argv[]) pretty_print = true; else if (!strncmp(argv[i], "-b", 2)) sim = true; + else if (!strncmp(argv[i], "--emit_scc", 2)) + emit_scc = true; } if (!input) @@ -88,33 +93,32 @@ int main(int argc, char* argv[]) { spot::ltl::parse_error_list pel; const spot::ltl::formula* f = - spot::ltl::parse(input, pel, spot::ltl::default_environment::instance(), - false); + spot::ltl::parse_infix_psl(input, pel); if (spot::ltl::format_parse_errors(std::cerr, input, pel)) return 2; spot::translator trans(dict); trans.set_pref(spot::postprocessor::Deterministic); auto tmp = trans.run(f); - res = spot::tgba_determinisation(tmp, sim, pretty_print); + res = spot::tgba_determinisation(tmp, sim, pretty_print, emit_scc); f->destroy(); } else if (in_hoa) { - spot::hoa_parse_error_list pel; - auto aut = spot::hoa_parse(input, pel, dict); - if (spot::format_hoa_parse_errors(std::cerr, input, pel)) + spot::parse_aut_error_list pel; + auto aut = spot::parse_aut(input, pel, dict); + if (spot::format_parse_aut_errors(std::cerr, input, pel)) return 2; - res = tgba_determinisation(aut->aut, sim, pretty_print); + res = tgba_determinisation(aut->aut, sim, pretty_print, emit_scc); } - res->merge_transitions(); + res->merge_edges(); if (out_hoa) { - spot::hoa_reachable(std::cout, res, "t"); + spot::print_hoa(std::cout, res, "t"); std::cout << std::endl; } else if (out_dot) - spot::dotty_reachable(std::cout, res); + spot::print_dot(std::cout, res); else assert(false); } diff --git a/src/tests/safra.test b/src/tests/safra.test index 9b051b68e..448e42588 100755 --- a/src/tests/safra.test +++ b/src/tests/safra.test @@ -87,7 +87,7 @@ EOF cat >out.exp << EOF HOA: v1 -States: 6 +States: 5 Start: 0 AP: 2 "a" "b" acc-name: Buchi @@ -101,9 +101,9 @@ State: 1 [0&1] 2 [!0&1] 3 {0} State: 2 +[0&1] 1 {0} [!0&1] 3 {0} [0&!1] 4 -[0&1] 5 State: 3 [0&!1] 0 [0&1] 2 @@ -111,15 +111,52 @@ State: 3 State: 4 [0] 1 {0} [!0&1] 3 {0} -State: 5 -[0] 1 {0} -[!0&1] 3 {0} --END-- EOF run 0 ../safra --hoa double_b.hoa -H > out.hoa diff out.hoa out.exp +# Test emit_scc optim +cat > out.exp << EOF +HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels trans-acc deterministic +--BODY-- +State: 0 "{₀0₀}" +[0] 1 {0} +State: 1 "{₀0 1₀}" +[0] 1 {0} +[!0&1] 2 {0} +State: 2 "{₀1₀}" +[1] 2 {0} +[0&!1] 2 +--END-- +EOF + +cat > in.hoa << EOF +HOA: v1 +States: 2 +Start: 0 +AP: 2 "a" "b" +Acceptance: 1 Inf(0) +--BODY-- +State: 0 +[0] 0 {0} +[0] 1 +State: 1 +[1] 1 {0} +[0] 1 +--END-- +EOF + +run 0 ../safra --hoa in.hoa --emit_scc -p -H > out.hoa +diff out.hoa out.exp + # Formulas from bench/dtgbasat/formulas cat >formulae <transitions()) + for (auto& t: aut->edges()) { t.acc &= mask; } @@ -166,26 +167,30 @@ namespace spot } } - auto + + void safra_state::compute_succs(const const_twa_graph_ptr& aut, const std::vector& bddnums, std::unordered_map, - bdd_hash>& deltas) const -> succs_t + bdd_hash>& deltas, + succs_t& res) const { - succs_t res; // Given a bdd returns index of associated safra_state in res std::map bdd2num; for (auto& node: nodes_) { for (auto& t: aut->out(node.first)) { + // deltas precalculate all transitions in edge t auto p = deltas[t.cond]; for (unsigned j = p.first; j < p.second; ++j) { auto i = bdd2num.insert(std::make_pair(bddnums[j], res.size())); unsigned idx; if (!i.second) + // No new state added, so get pre-existing state whichi is an + // index in the vector of safra states (res) idx = i.first->second; else { @@ -203,9 +208,17 @@ namespace spot for (auto& s: res) { safra_state& tmp = s.first; + tmp.ungreenify_last_brace(); s.first.color_ = tmp.finalize_construction(); } - return res; + } + + void safra_state::ungreenify_last_brace() + { + // Step A4: For a brace to emit green it must surround other braces. + // Hence, the last brace cannot emit green as it is the most inside brace. + for (auto& n: nodes_) + is_green_[n.second.back()] = false; } unsigned safra_state::finalize_construction() @@ -218,7 +231,7 @@ namespace spot { if (nb_braces_[i] == 0) { - // It is impossible to emit red == -1 as those transitions would + // It is impossible to emit red == -1 as those edges would // lead us in a sink states which are not created here. assert(i >= 1); red = std::min(red, 2 * i - 1); @@ -301,12 +314,10 @@ namespace spot unsigned dst, const acc_cond::mark_t acc) { std::vector copy = braces; - // TODO handle multiple accepting sets if (acc.count()) { - assert(acc.has(0) && acc.count() == 1 && - "Only one TBA are accepted at the moment"); - // Accepting transition generate new braces: step A1 + assert(acc.has(0) && acc.count() == 1 && "Only one TBA are accepted"); + // Accepting edge generate new braces: step A1 copy.emplace_back(nb_braces_.size()); // nb_braces_ gets updated later so put 0 for now nb_braces_.emplace_back(0); @@ -333,9 +344,6 @@ namespace spot // After inserting new node, update the brace count per node for (auto b: i.first->second) ++nb_braces_[b]; - // Step A4: For a brace to emit green it must surround other braces. - // Hence, the last brace cannot emit green as it is the most inside brace. - is_green_[i.first->second.back()] = false; } // Called only to initialize first state @@ -367,16 +375,32 @@ namespace spot return nodes_ < other.nodes_; } + // All edge going into an accepting SCC are marked as accepting + // This helps safra make fewer trees as we immediately see the accepting + // edge and don't create useless states + void + emit_accepting_scc(twa_graph_ptr& aut, scc_info& scc) + { + for (auto& e: aut->edges()) + { + unsigned src_scc = scc.scc_of(e.src); + unsigned dst_scc = scc.scc_of(e.dst); + if (src_scc == dst_scc) + continue; + if (scc.is_accepting_scc(dst_scc)) + e.acc |= 1; + } + } + twa_graph_ptr tgba_determinisation(const const_twa_graph_ptr& a, bool bisimulation, - bool pretty_print) + bool pretty_print, bool emit_scc) { // Degeneralize - const_twa_graph_ptr aut; - if (a->acc().is_generalized_buchi()) - aut = spot::degeneralize_tba(a); - else - aut = a; + twa_graph_ptr aut = spot::degeneralize_tba(a); + scc_info scc = scc_info(aut); + if (emit_scc) + emit_accepting_scc(aut, scc); bdd allap = bddtrue; @@ -384,7 +408,7 @@ namespace spot typedef std::set sup_map; sup_map sup; // Record occurrences of all guards - for (auto& t: aut->transitions()) + for (auto& t: aut->edges()) sup.emplace(t.cond); for (auto& i: sup) allap &= bdd_support(i); @@ -398,7 +422,7 @@ namespace spot // Used to convert large bdd to indexes std::unordered_map, bdd_hash> deltas; std::vector bddnums; - for (auto& t: aut->transitions()) + for (auto& t: aut->edges()) { auto it = deltas.find(t.cond); if (it == deltas.end()) @@ -428,7 +452,7 @@ namespace spot }); // Given a safra_state get its associated state in output automata. - // Required to create new transitions from 2 safra-state + // Required to create new edges from 2 safra-state power_set seen; safra_state init(aut->get_init_state_number(), true); unsigned num = res->new_state(); @@ -437,13 +461,14 @@ namespace spot std::deque todo; todo.push_back(init); unsigned sets = 0; + using succs_t = safra_state::succs_t; + succs_t succs; while (!todo.empty()) { - using succs_t = safra_state::succs_t; safra_state curr = todo.front(); unsigned src_num = seen.find(curr)->second; todo.pop_front(); - succs_t succs = curr.compute_succs(aut, bddnums, deltas); + curr.compute_succs(aut, bddnums, deltas, succs); for (auto s: succs) { auto i = seen.find(s.first); @@ -461,15 +486,16 @@ namespace spot } if (s.first.color_ != -1U) { - res->new_transition(src_num, dst_num, num2bdd[s.second], + res->new_edge(src_num, dst_num, num2bdd[s.second], {s.first.color_}); // We only care about green acc if (s.first.color_ % 2 == 0) sets = std::max(s.first.color_ + 1, sets); } else - res->new_transition(src_num, dst_num, num2bdd[s.second]); + res->new_edge(src_num, dst_num, num2bdd[s.second]); } + succs.clear(); } remove_dead_acc(res, sets); res->set_acceptance(sets, acc_cond::acc_code::parity(false, false, sets)); diff --git a/src/twaalgos/safra.hh b/src/twaalgos/safra.hh index 3b6b02359..8b9bb9514 100644 --- a/src/twaalgos/safra.hh +++ b/src/twaalgos/safra.hh @@ -47,11 +47,14 @@ namespace spot safra_state(unsigned state_number, bool init_state = false); // Given a certain transition_label, compute all the successors of that // label, and return that new node. - succs_t compute_succs(const const_twa_graph_ptr& aut, + void compute_succs(const const_twa_graph_ptr& aut, const std::vector& bddnums, std::unordered_map, - bdd_hash>& deltas) const; + bdd_hash>& deltas, + succs_t& res) const; + // The outermost brace of each node cannot be green + void ungreenify_last_brace(); // Used when creating the list of successors // A new intermediate node is created with src's braces and with dst as id // A merge is done if dst already existed in *this @@ -74,5 +77,6 @@ namespace spot SPOT_API twa_graph_ptr tgba_determinisation(const const_twa_graph_ptr& aut, bool bisimulation = false, - bool pretty_print = false); + bool pretty_print = false, + bool emit_scc = false); }