diff --git a/src/tgba/tgbagraph.hh b/src/tgba/tgbagraph.hh index 222a10707..1a9b0a7aa 100644 --- a/src/tgba/tgbagraph.hh +++ b/src/tgba/tgbagraph.hh @@ -77,7 +77,7 @@ namespace spot { } - tgba_graph_trans_data(bdd cond, bdd acc) + tgba_graph_trans_data(bdd cond, bdd acc = bddfalse) : cond(cond), acc(acc) { } @@ -162,7 +162,10 @@ namespace spot public: tgba_digraph(bdd_dict* dict) - : dict_(dict), init_(nullptr) + : dict_(dict), + all_acceptance_conditions_(bddfalse), + neg_acceptance_conditions_(bddtrue), + init_(nullptr) { } diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc index 69b1115a5..e36a78eaa 100644 --- a/src/tgbaalgos/minimize.cc +++ b/src/tgbaalgos/minimize.cc @@ -209,7 +209,7 @@ namespace spot bool - wdba_scc_is_accepting(const tgba_explicit_number* det_a, unsigned scc_n, + wdba_scc_is_accepting(const tgba_digraph* det_a, unsigned scc_n, const tgba* orig_a, scc_map& sm, power_map& pm) { // Get some state from the SCC #n. @@ -244,24 +244,25 @@ namespace spot bool accepting = false; // Iterate on each original state corresponding to start. - const power_map::power_state& ps = pm.states_of(det_a->get_label(start)); - for (power_map::power_state::const_iterator it = ps.begin(); - it != ps.end() && !accepting; ++it) + const power_map::power_state& ps = + pm.states_of(det_a->state_number(start)); + for (auto& it: ps) { // Contrustruct a product between // LOOP_A, and ORIG_A starting in *IT. - tgba* p = new tgba_product_init(&loop_a, orig_a, - loop_a_init, *it); - + tgba* p = new tgba_product_init(&loop_a, orig_a, loop_a_init, it); emptiness_check* ec = couvreur99(p); emptiness_check_result* res = ec->check(); - - if (res) - accepting = true; delete res; delete ec; delete p; + + if (res) + { + accepting = true; + break; + } } loop_a_init->destroy(); @@ -270,7 +271,7 @@ namespace spot } - sba_explicit_number* minimize_dfa(const tgba_explicit_number* det_a, + sba_explicit_number* minimize_dfa(const tgba_digraph* det_a, hash_set* final, hash_set* non_final) { typedef std::list partition_t; @@ -481,7 +482,7 @@ namespace spot { hash_set* final = new hash_set; hash_set* non_final = new hash_set; - tgba_explicit_number* det_a; + tgba_digraph* det_a; { power_map pm; @@ -500,7 +501,7 @@ namespace spot hash_set* final = new hash_set; hash_set* non_final = new hash_set; - tgba_explicit_number* det_a; + tgba_digraph* det_a; { power_map pm; diff --git a/src/tgbaalgos/powerset.cc b/src/tgbaalgos/powerset.cc index 75cace0bc..f9a1e882c 100644 --- a/src/tgbaalgos/powerset.cc +++ b/src/tgbaalgos/powerset.cc @@ -42,7 +42,7 @@ namespace spot { - tgba_explicit_number* + tgba_digraph* tgba_powerset(const tgba* aut, power_map& pm, bool merge) { typedef power_map::power_state power_state; @@ -51,19 +51,22 @@ namespace spot power_set seen; todo_list todo; - tgba_explicit_number* res = new tgba_explicit_number(aut->get_dict()); + auto d = aut->get_dict(); + auto res = new tgba_digraph(d); + d->register_all_variables_of(aut, res); + d->unregister_all_typed_variables(bdd_dict::acc, res); + auto& g = res->get_graph(); { power_state ps; const state* s = pm.canonicalize(aut->get_init_state()); ps.insert(s); todo.push_back(ps); - seen[ps] = 1; - pm.map_[1] = ps; + unsigned num = g.new_state(); + seen[ps] = num; + pm.map_[num] = ps; } - unsigned state_num = 1; - while (!todo.empty()) { power_state src = todo.front(); @@ -92,21 +95,18 @@ namespace spot // Add that transition. power_set::const_iterator i = seen.find(dest); int dest_num; - state_explicit_number::transition* t; if (i != seen.end()) { dest_num = i->second; - t = res->create_transition(seen[src], dest_num); } else { - dest_num = ++state_num; + dest_num = g.new_state(); seen[dest] = dest_num; pm.map_[dest_num] = dest; todo.push_back(dest); - t = res->create_transition(seen[src], dest_num); } - res->add_conditions(t, cond); + g.new_transition(seen[src], dest_num, cond); } } if (merge) @@ -114,7 +114,7 @@ namespace spot return res; } - tgba_explicit_number* + tgba_digraph* tgba_powerset(const tgba* aut) { power_map pm; @@ -129,7 +129,7 @@ namespace spot { public: typedef dfs_stack::const_iterator cycle_iter; - typedef state_explicit_number::transition trans; + typedef tgba_graph_trans_data trans; typedef std::set trans_set; typedef std::vector set_set; protected: @@ -170,31 +170,32 @@ namespace spot bdd acc = aut_->all_acceptance_conditions(); for (auto i: all_) - i->acceptance_conditions = acc; + i->acc = acc; return threshold_ != 0 && cycles_left_ == 0; } bool is_cycle_accepting(cycle_iter begin, trans_set& ts) const { - tgba_explicit_number* a = - down_cast(const_cast(aut_)); + auto a = down_cast(const_cast(aut_)); + // Build an automaton representing this loop. - tgba_explicit_number loop_a(aut_->get_dict()); + tgba_digraph loop_a(aut_->get_dict()); + auto& g = loop_a.get_graph(); int loop_size = std::distance(begin, dfs_.end()); + g.new_states(loop_size); int n; cycle_iter i; for (n = 1, i = begin; n <= loop_size; ++n, ++i) { - trans* t = a->get_transition(i->succ); - loop_a.create_transition(n - 1, n % loop_size)->condition = - t->condition; + trans* t = &a->trans_data(i->succ); + g.new_transition(n - 1, n % loop_size, t->cond); if (reject_.find(t) == reject_.end()) ts.insert(t); } assert(i == dfs_.end()); const state* loop_a_init = loop_a.get_init_state(); - assert(loop_a.get_label(loop_a_init) == 0); + assert(loop_a.state_number(loop_a_init) == 0); // Check if the loop is accepting in the original automaton. bool accepting = false; @@ -202,7 +203,7 @@ namespace spot // Iterate on each original state corresponding to the // start of the loop in the determinized automaton. const power_map::power_state& ps = - refmap_.states_of(a->get_label(begin->ts->first)); + refmap_.states_of(a->state_number(begin->ts->first)); for (auto s: ps) { // Construct a product between @@ -213,13 +214,14 @@ namespace spot couvreur99_check* ec = down_cast(couvreur99(p)); assert(ec); emptiness_check_result* res = ec->check(); - if (res) - accepting = true; delete res; delete ec; delete p; - if (accepting) - break; + if (res) + { + accepting = true; + break; + } } loop_a_init->destroy(); @@ -277,7 +279,7 @@ namespace spot }; static bool - fix_dba_acceptance(tgba_explicit_number* det, + fix_dba_acceptance(tgba_digraph* det, const tgba* ref, power_map& refmap, unsigned threshold) { @@ -298,7 +300,7 @@ namespace spot } } - tgba_explicit_number* + tgba_digraph* tba_determinize(const tgba* aut, unsigned threshold_states, unsigned threshold_cycles) { @@ -306,7 +308,7 @@ namespace spot // Do not merge transitions in the deterministic automaton. If we // add two self-loops labeled by "a" and "!a", we do not want // these to be merged as "1" before the acceptance has been fixed. - tgba_explicit_number* det = tgba_powerset(aut, pm, false); + auto det = tgba_powerset(aut, pm, false); if ((threshold_states > 0) && (pm.map_.size() > pm.states_.size() * threshold_states)) @@ -336,8 +338,7 @@ namespace spot if (aut->number_of_acceptance_conditions() > 1) return 0; - tgba_explicit_number* det = - tba_determinize(aut, threshold_states, threshold_cycles); + auto det = tba_determinize(aut, threshold_states, threshold_cycles); if (!det) return 0; diff --git a/src/tgbaalgos/powerset.hh b/src/tgbaalgos/powerset.hh index a8dd4a33b..2c9dc9a7b 100644 --- a/src/tgbaalgos/powerset.hh +++ b/src/tgbaalgos/powerset.hh @@ -25,7 +25,7 @@ # include # include -# include "tgba/tgbaexplicit.hh" +# include "tgba/tgbagraph.hh" namespace spot { @@ -33,12 +33,12 @@ namespace spot struct SPOT_API power_map { typedef std::set power_state; - typedef std::map power_map_data; + typedef std::map power_map_data; const power_state& - states_of(int s) const + states_of(unsigned s) const { - return map_.find(s)->second; + return map_.at(s); } const state* @@ -64,9 +64,9 @@ namespace spot /// The \a merge argument can be set to false to prevent merging of /// transitions. //@{ - SPOT_API tgba_explicit_number* + SPOT_API tgba_digraph* tgba_powerset(const tgba* aut, power_map& pm, bool merge = true); - SPOT_API tgba_explicit_number* + SPOT_API tgba_digraph* tgba_powerset(const tgba* aut); //@} @@ -106,7 +106,7 @@ namespace spot /// If \a threshold_cycles is non null, abort the construction /// whenever an SCC of the constructed automaton has more than \a /// threshold_cycles cycles. - SPOT_API tgba_explicit_number* + SPOT_API tgba_digraph* tba_determinize(const tgba* aut, unsigned threshold_states = 0, unsigned threshold_cycles = 0); diff --git a/src/tgbatest/powerset.cc b/src/tgbatest/powerset.cc index ea9cd0cc4..5f9bcb931 100644 --- a/src/tgbatest/powerset.cc +++ b/src/tgbatest/powerset.cc @@ -55,7 +55,7 @@ main(int argc, char** argv) #ifndef DOTTY - spot::tgba_explicit_number* e = spot::tgba_powerset(a); + auto e = spot::tgba_powerset(a); spot::tgba_save_reachable(std::cout, e); delete e; #else