diff --git a/spot/twaalgos/simulation.cc b/spot/twaalgos/simulation.cc index 99c4ed778..9986e823d 100644 --- a/spot/twaalgos/simulation.cc +++ b/spot/twaalgos/simulation.cc @@ -344,10 +344,10 @@ namespace spot } // The core loop of the algorithm. - twa_graph_ptr run() + twa_graph_ptr run(std::map* implications = nullptr) { main_loop(); - return build_result(); + return build_result(implications); } // Take a state and compute its signature. @@ -484,7 +484,7 @@ namespace spot } // Build the minimal resulting automaton. - twa_graph_ptr build_result() + twa_graph_ptr build_result(std::map* implications = nullptr) { twa_graph_ptr res = make_twa_graph(a_->get_dict()); res->copy_ap_of(a_); @@ -503,6 +503,8 @@ namespace spot // its class, or by all the implied classes. auto s = gb->new_state(cl.id()); gb->alias_state(s, relation_[cl].id()); + if (implications) + (*implications)[s] = relation_[cl]; } // Acceptance of states. Only used if Sba && Cosimulation. @@ -631,7 +633,7 @@ namespace spot res->purge_unreachable_states(); - delete gb; + delete gb; res->prop_copy(original_, { false, // state-based acc forced below true, // weakness preserved, @@ -735,6 +737,14 @@ namespace spot return simul.run(); } + twa_graph_ptr + simulation(const const_twa_graph_ptr& t, + std::map* implications) + { + direct_simulation simul(t); + return simul.run(implications); + } + twa_graph_ptr simulation_sba(const const_twa_graph_ptr& t) { diff --git a/spot/twaalgos/simulation.hh b/spot/twaalgos/simulation.hh index 5e4731413..057c98b66 100644 --- a/spot/twaalgos/simulation.hh +++ b/spot/twaalgos/simulation.hh @@ -70,6 +70,9 @@ namespace spot SPOT_API twa_graph_ptr simulation(const const_twa_graph_ptr& automaton); SPOT_API twa_graph_ptr + simulation(const const_twa_graph_ptr& automaton, + std::map* implementation); + SPOT_API twa_graph_ptr simulation_sba(const const_twa_graph_ptr& automaton); /// @} diff --git a/src/tests/safra.cc b/src/tests/safra.cc index f38e278d9..3a9466d30 100644 --- a/src/tests/safra.cc +++ b/src/tests/safra.cc @@ -46,6 +46,7 @@ int help() int main(int argc, char* argv[]) { bool scc_opt = false; + bool use_bisim = false; bool sim = false; bool in_hoa = false; bool in_ltl = false; @@ -83,6 +84,8 @@ int main(int argc, char* argv[]) sim = true; else if (!strncmp(argv[i], "--scc_opt", 9)) scc_opt = true; + else if (!strncmp(argv[i], "--bisim_opt", 10)) + use_bisim = true; else { std::cerr << "Warning: " << argv[i] << " not used\n"; @@ -104,14 +107,16 @@ int main(int argc, char* argv[]) spot::translator trans(dict); trans.set_pref(spot::postprocessor::Deterministic); auto tmp = trans.run(f); - res = spot::tgba_determinisation(tmp, sim, pretty_print, scc_opt); + res = spot::tgba_determinisation(tmp, sim, pretty_print, scc_opt, + use_bisim); } else if (in_hoa) { auto aut = spot::parse_aut(input, dict); if (aut->format_errors(std::cerr)) return 2; - res = tgba_determinisation(aut->aut, sim, pretty_print, scc_opt); + res = tgba_determinisation(aut->aut, sim, pretty_print, scc_opt, + use_bisim); } res->merge_edges(); diff --git a/src/twaalgos/safra.cc b/src/twaalgos/safra.cc index 4e2a173cc..9ca4fbb28 100644 --- a/src/twaalgos/safra.cc +++ b/src/twaalgos/safra.cc @@ -25,6 +25,7 @@ #include "safra.hh" #include "twaalgos/degen.hh" +#include "twaalgos/sccfilter.hh" #include "twaalgos/simulation.hh" namespace spot @@ -186,7 +187,10 @@ safra_state::compute_succs(const const_twa_graph_ptr& aut, bdd_hash>& deltas, succs_t& res, const scc_info& scc, - bool scc_opt) const + const std::map& implications, + const std::vector& is_connected, + bool scc_opt, + bool use_bisimulation) const { // Given a bdd returns index of associated safra_state in res std::map bdd2num; @@ -242,11 +246,45 @@ safra_state::compute_succs(const const_twa_graph_ptr& aut, for (auto& s: res) { safra_state& tmp = s.first; + if (use_bisimulation) + tmp.merge_redundant_states(implications, scc, is_connected); tmp.ungreenify_last_brace(); s.first.color_ = tmp.finalize_construction(); } } + void + safra_state::merge_redundant_states(const std::map& implications, + const scc_info& scc, + const std::vector& is_connected) + { + std::vector to_remove; + for (auto& n1: nodes_) + { + for (auto& n2: nodes_) + { + if (n1 == n2) + continue; + // index to see if there is a path from scc2 -> scc1 + unsigned idx = scc.scc_count() * scc.scc_of(n2.first) + + scc.scc_of(n1.first); + if (bdd_implies(implications.at(n1.first), + implications.at(n2.first)) && !is_connected[idx]) + { + to_remove.push_back(n1.first); + } + } + } + for (auto& n: to_remove) + { + for (auto& brace: nodes_[n]) + { + --nb_braces_[brace]; + } + nodes_.erase(n); + } + } + void safra_state::ungreenify_last_brace() { // Step A4: For a brace to emit green it must surround other braces. @@ -438,17 +476,42 @@ safra_state::compute_succs(const const_twa_graph_ptr& aut, } } + std::vector + find_scc_paths(const scc_info& scc) + { + unsigned scccount = scc.scc_count(); + std::vector res(scccount * scccount, 0); + for (unsigned i = 0; i < scccount; ++i) + res[i + scccount * i] = 1; + for (unsigned i = 0; i < scccount; ++i) + { + std::stack s; + s.push(i); + while (!s.empty()) + { + unsigned src = s.top(); + s.pop(); + for (auto& d: scc.succ(src)) + { + s.push(d); + unsigned idx = scccount * i + d; + res[idx] = 1; + } + } + } + return res; + } + twa_graph_ptr tgba_determinisation(const const_twa_graph_ptr& a, bool bisimulation, - bool pretty_print, bool scc_opt) + bool pretty_print, bool scc_opt, bool use_bisimulation) { // Degeneralize - twa_graph_ptr aut = spot::degeneralize_tba(a); + twa_graph_ptr aut = spot::scc_filter(spot::degeneralize_tba(a)); + std::map implications; + aut = simulation(aut, &implications); scc_info scc = scc_info(aut); - // TODO - // if (emit_scc) - // emit_accepting_scc(aut, scc); - + std::vector is_connected = find_scc_paths(scc); bdd allap = bddtrue; { @@ -518,7 +581,8 @@ safra_state::compute_succs(const const_twa_graph_ptr& aut, safra_state curr = todo.front(); unsigned src_num = seen.find(curr)->second; todo.pop_front(); - curr.compute_succs(aut, bddnums, deltas, succs, scc, scc_opt); + curr.compute_succs(aut, bddnums, deltas, succs, scc, implications, + is_connected, scc_opt, use_bisimulation); for (auto s: succs) { auto i = seen.find(s.first); @@ -551,6 +615,7 @@ safra_state::compute_succs(const const_twa_graph_ptr& aut, res->set_acceptance(sets, acc_cond::acc_code::parity(false, true, sets)); res->prop_deterministic(true); res->prop_state_acc(false); + if (bisimulation) res = simulation(res); if (pretty_print) diff --git a/src/twaalgos/safra.hh b/src/twaalgos/safra.hh index a3f33b943..7fb323eb4 100644 --- a/src/twaalgos/safra.hh +++ b/src/twaalgos/safra.hh @@ -61,12 +61,19 @@ namespace spot bdd_hash>& deltas, succs_t& res, const scc_info& scc, - bool scc_opt = false) const; + const std::map& implications, + const std::vector& is_connected, + bool scc_opt = false, + bool use_bisimulation = false) const; // scc_id has to be an accepting SCC. This function tries to find a node // who lives in that SCC and if it does, we return the brace_id of that SCC. unsigned find_scc_brace_id(unsigned scc_id, const scc_info& scc); // The outermost brace of each node cannot be green void ungreenify_last_brace(); + // When a nodes a implies a node b, remove the node a. + void merge_redundant_states(const std::map& implications, + const scc_info& scc, + const std::vector& is_connected); // 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 @@ -90,5 +97,6 @@ namespace spot tgba_determinisation(const const_twa_graph_ptr& aut, bool bisimulation = false, bool pretty_print = false, - bool scc_opt = false); + bool scc_opt = false, + bool use_bisimulation = false); }