From 1a93166d15a8ed169671b2fa0d46ec4f8fd651d2 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 10 Jul 2014 10:23:48 +0200 Subject: [PATCH] tgbadigraph: delegate useful graph methods * src/tgba/tgbagraph.hh (new_state, new_states, new_transitions, out, trans_data): Delegate these useful graph methods so we do not have to call get_graph(). * src/graphtest/tgbagraph.cc, src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc, src/tgbaalgos/dupexp.cc, src/tgbaalgos/emptiness.cc, src/tgbaalgos/lbtt.cc, src/tgbaalgos/powerset.cc, src/tgbaalgos/randomgraph.cc, src/tgbaalgos/sccfilter.cc, src/tgbaalgos/sccinfo.cc,src/tgbaalgos/simulation.cc: Simplify. --- src/graphtest/tgbagraph.cc | 31 +++++++++++++++---------------- src/tgba/tgbagraph.hh | 33 ++++++++++++++++++++++++++++++++- src/tgbaalgos/dtbasat.cc | 13 ++++++------- src/tgbaalgos/dtgbasat.cc | 13 ++++++------- src/tgbaalgos/dupexp.cc | 8 ++++---- src/tgbaalgos/emptiness.cc | 7 +++---- src/tgbaalgos/lbtt.cc | 10 ++++------ src/tgbaalgos/powerset.cc | 12 +++++------- src/tgbaalgos/randomgraph.cc | 4 ++-- src/tgbaalgos/sccfilter.cc | 8 +++----- src/tgbaalgos/sccinfo.cc | 9 ++++----- src/tgbaalgos/simulation.cc | 19 ++++++++----------- 12 files changed, 92 insertions(+), 75 deletions(-) diff --git a/src/graphtest/tgbagraph.cc b/src/graphtest/tgbagraph.cc index ddbf7bdc0..a3dfb0bf4 100644 --- a/src/graphtest/tgbagraph.cc +++ b/src/graphtest/tgbagraph.cc @@ -30,7 +30,6 @@ void f1() auto& e = spot::ltl::default_environment::instance(); spot::tgba_digraph tg(&d); - auto& g = tg.get_graph(); auto* f1 = e.require("p1"); auto* f2 = e.require("p2"); @@ -41,21 +40,21 @@ void f1() f1->destroy(); f2->destroy(); - auto s1 = g.new_state(); - auto s2 = g.new_state(); - auto s3 = g.new_state(); - g.new_transition(s1, s1, bddfalse, bddfalse); - g.new_transition(s1, s2, p1, bddfalse); - g.new_transition(s1, s3, p2, !a1 & a2); - g.new_transition(s2, s3, p1 & p2, a1 & !a2); - g.new_transition(s3, s1, p1 | p2, (!a1 & a2) | (a1 & !a2)); - g.new_transition(s3, s2, p1 >> p2, bddfalse); - g.new_transition(s3, s3, bddtrue, (!a1 & a2) | (a1 & !a2)); + auto s1 = tg.new_state(); + auto s2 = tg.new_state(); + auto s3 = tg.new_state(); + tg.new_transition(s1, s1, bddfalse, bddfalse); + tg.new_transition(s1, s2, p1, bddfalse); + tg.new_transition(s1, s3, p2, !a1 & a2); + tg.new_transition(s2, s3, p1 & p2, a1 & !a2); + tg.new_transition(s3, s1, p1 | p2, (!a1 & a2) | (a1 & !a2)); + tg.new_transition(s3, s2, p1 >> p2, bddfalse); + tg.new_transition(s3, s3, bddtrue, (!a1 & a2) | (a1 & !a2)); spot::dotty_reachable(std::cout, &tg); { - auto i = g.out_iteraser(s3); + auto i = tg.get_graph().out_iteraser(s3); ++i; i.erase(); i.erase(); @@ -64,15 +63,15 @@ void f1() } { - auto i = g.out_iteraser(s3); + auto i = tg.get_graph().out_iteraser(s3); i.erase(); assert(!i); spot::dotty_reachable(std::cout, &tg); } - g.new_transition(s3, s1, p1 | p2, (!a1 & a2) | (a1 & !a2)); - g.new_transition(s3, s2, p1 >> p2, bddfalse); - g.new_transition(s3, s1, bddtrue, (!a1 & a2) | (a1 & !a2)); + tg.new_transition(s3, s1, p1 | p2, (!a1 & a2) | (a1 & !a2)); + tg.new_transition(s3, s2, p1 >> p2, bddfalse); + tg.new_transition(s3, s1, bddtrue, (!a1 & a2) | (a1 & !a2)); std::cerr << tg.num_transitions() << '\n'; assert(tg.num_transitions() == 7); diff --git a/src/tgba/tgbagraph.hh b/src/tgba/tgbagraph.hh index 1a9b0a7aa..cac98a9c1 100644 --- a/src/tgba/tgbagraph.hh +++ b/src/tgba/tgbagraph.hh @@ -221,7 +221,6 @@ namespace spot return g_.num_transitions(); } - void set_init_state(graph_t::state s) { init_ = &g_.state_data(s); @@ -296,6 +295,10 @@ namespace spot return g_.trans_data(i->pos()); } + tgba_graph_trans_data& trans_data(unsigned t) + { + return g_.trans_data(t); + } void set_acceptance_conditions(bdd all) { @@ -311,6 +314,34 @@ namespace spot compute_all_acceptance_conditions(neg_acceptance_conditions_); } + unsigned new_state() + { + return g_.new_state(); + } + + unsigned new_states(unsigned n) + { + return g_.new_states(n); + } + + unsigned new_transition(unsigned src, unsigned dst, + bdd cond, bdd acc = bddfalse) + { + return g_.new_transition(src, dst, cond, acc); + } + + internal::state_out + out(unsigned src) const + { + return g_.out(src); + } + + internal::state_out + out(unsigned src) + { + return g_.out(src); + } + /// \brief Copy the acceptance conditions of another tgba. void copy_acceptance_conditions_of(const tgba *a) { diff --git a/src/tgbaalgos/dtbasat.cc b/src/tgbaalgos/dtbasat.cc index c97056778..b0d1c1954 100644 --- a/src/tgbaalgos/dtbasat.cc +++ b/src/tgbaalgos/dtbasat.cc @@ -678,8 +678,7 @@ namespace spot bdd acc = bdd_ithvar(autdict->register_acceptance_variable(t, a)); a->set_acceptance_conditions(acc); - auto& g = a->get_graph(); - g.new_states(satdict.cand_size); + a->new_states(satdict.cand_size); unsigned last_aut_trans = -1U; const transition* last_sat_trans = nullptr; @@ -717,10 +716,10 @@ namespace spot && acc_states.find(t->second.src) != acc_states.end()) accept = acc; - last_aut_trans = g.new_transition(t->second.src - 1, - t->second.dst -1, - t->second.cond, - accept); + last_aut_trans = a->new_transition(t->second.src - 1, + t->second.dst - 1, + t->second.cond, + accept); last_sat_trans = &t->second; dout << v << '\t' << t->second << "δ\n"; @@ -737,7 +736,7 @@ namespace spot assert(!state_based); // This assumes that the SAT solvers output // variables in increasing order. - g.trans_data(last_aut_trans).acc = acc; + a->trans_data(last_aut_trans).acc = acc; } else if (state_based) { diff --git a/src/tgbaalgos/dtgbasat.cc b/src/tgbaalgos/dtgbasat.cc index 5fa1f6c89..cd9d87e20 100644 --- a/src/tgbaalgos/dtgbasat.cc +++ b/src/tgbaalgos/dtgbasat.cc @@ -851,8 +851,7 @@ namespace spot autdict->unregister_all_typed_variables(bdd_dict::acc, aut); a->set_acceptance_conditions(satdict.all_cand_acc.back()); - auto& g = a->get_graph(); - g.new_states(satdict.cand_size); + a->new_states(satdict.cand_size); // Last transition set in the automaton. unsigned last_aut_trans = -1U; @@ -894,10 +893,10 @@ namespace spot acc = i->second; } - last_aut_trans = g.new_transition(t->second.src - 1, - t->second.dst - 1, - t->second.cond, - acc); + last_aut_trans = a->new_transition(t->second.src - 1, + t->second.dst - 1, + t->second.cond, + acc); last_sat_trans = &t->second; dout << v << '\t' << t->second << "δ\n"; @@ -919,7 +918,7 @@ namespace spot ta->second.dst == last_sat_trans->dst) { assert(!state_based); - g.trans_data(last_aut_trans).acc |= ta->second.acc; + a->trans_data(last_aut_trans).acc |= ta->second.acc; } else if (state_based) { diff --git a/src/tgbaalgos/dupexp.cc b/src/tgbaalgos/dupexp.cc index abbfe9a2d..261d0bb76 100644 --- a/src/tgbaalgos/dupexp.cc +++ b/src/tgbaalgos/dupexp.cc @@ -50,7 +50,7 @@ namespace spot virtual void process_state(const state*, int n, tgba_succ_iterator*) { - unsigned ns = out_->get_graph().new_state(); + unsigned ns = out_->new_state(); assert(ns == static_cast(n) - 1); (void)ns; } @@ -60,9 +60,9 @@ namespace spot const state*, int out, const tgba_succ_iterator* si) { - out_->get_graph().new_transition(in - 1, out - 1, - si->current_condition(), - si->current_acceptance_conditions()); + out_->new_transition(in - 1, out - 1, + si->current_condition(), + si->current_acceptance_conditions()); } protected: diff --git a/src/tgbaalgos/emptiness.cc b/src/tgbaalgos/emptiness.cc index bb78cd2fb..d55caf55e 100644 --- a/src/tgbaalgos/emptiness.cc +++ b/src/tgbaalgos/emptiness.cc @@ -287,7 +287,6 @@ namespace spot { auto d = a->get_dict(); auto res = new tgba_digraph(d); - auto& g = res->get_graph(); d->register_all_variables_of(a, res); const state* s = a->get_init_state(); @@ -308,7 +307,7 @@ namespace spot tgba_run::steps::const_iterator i = l->begin(); assert(s->compare(i->s) == 0); - src = g.new_state(); + src = res->new_state(); seen.insert(std::make_pair(i->s, src)); for (; i != l->end();) @@ -358,10 +357,10 @@ namespace spot auto p = seen.insert(std::make_pair(next, 0)); if (p.second) - p.first->second = g.new_state(); + p.first->second = res->new_state(); dst = p.first->second; - g.new_transition(src, dst, label, acc); + res->new_transition(src, dst, label, acc); src = dst; // Sum acceptance conditions. diff --git a/src/tgbaalgos/lbtt.cc b/src/tgbaalgos/lbtt.cc index 67844b2d4..b4a7c4cad 100644 --- a/src/tgbaalgos/lbtt.cc +++ b/src/tgbaalgos/lbtt.cc @@ -177,8 +177,7 @@ namespace spot { auto aut = std::unique_ptr(new tgba_digraph(dict)); acc_mapper_int acc_b(aut.get(), num_acc, envacc); - auto& g = aut->get_graph(); - g.new_states(num_states); + aut->new_states(num_states); for (unsigned n = 0; n < num_states; ++n) { @@ -229,7 +228,7 @@ namespace spot } bdd cond = formula_to_bdd(f, dict, aut.get()); f->destroy(); - g.new_transition(src_state, dst_state, cond, acc); + aut->new_transition(src_state, dst_state, cond, acc); } } return aut.release(); @@ -243,8 +242,7 @@ namespace spot { auto aut = std::unique_ptr(new tgba_digraph(dict)); acc_mapper_int acc_b(aut.get(), num_acc, envacc); - auto& g = aut->get_graph(); - g.new_states(num_states); + aut->new_states(num_states); for (unsigned n = 0; n < num_states; ++n) { @@ -295,7 +293,7 @@ namespace spot } bdd cond = formula_to_bdd(f, dict, aut.get()); f->destroy(); - g.new_transition(src_state, dst_state, cond, acc); + aut->new_transition(src_state, dst_state, cond, acc); } } return aut.release(); diff --git a/src/tgbaalgos/powerset.cc b/src/tgbaalgos/powerset.cc index f9a1e882c..5ce9d1d82 100644 --- a/src/tgbaalgos/powerset.cc +++ b/src/tgbaalgos/powerset.cc @@ -55,14 +55,13 @@ namespace spot 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); - unsigned num = g.new_state(); + unsigned num = res->new_state(); seen[ps] = num; pm.map_[num] = ps; } @@ -101,12 +100,12 @@ namespace spot } else { - dest_num = g.new_state(); + dest_num = res->new_state(); seen[dest] = dest_num; pm.map_[dest_num] = dest; todo.push_back(dest); } - g.new_transition(seen[src], dest_num, cond); + res->new_transition(seen[src], dest_num, cond); } } if (merge) @@ -180,15 +179,14 @@ namespace spot // Build an automaton representing this loop. 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); + loop_a.new_states(loop_size); int n; cycle_iter i; for (n = 1, i = begin; n <= loop_size; ++n, ++i) { trans* t = &a->trans_data(i->succ); - g.new_transition(n - 1, n % loop_size, t->cond); + loop_a.new_transition(n - 1, n % loop_size, t->cond); if (reject_.find(t) == reject_.end()) ts.insert(t); } diff --git a/src/tgbaalgos/randomgraph.cc b/src/tgbaalgos/randomgraph.cc index ed1767d88..b12312ad2 100644 --- a/src/tgbaalgos/randomgraph.cc +++ b/src/tgbaalgos/randomgraph.cc @@ -76,7 +76,7 @@ namespace spot if (drand() < a) ac |= *i; - aut->get_graph().new_transition(src, dest, p, ac); + aut->new_transition(src, dest, p, ac); } } @@ -117,7 +117,7 @@ namespace spot node_set nodes_to_process; node_set unreachable_nodes; - res->get_graph().new_states(n); + res->new_states(n); std::vector state_randomizer(n); state_randomizer[0] = 0; diff --git a/src/tgbaalgos/sccfilter.cc b/src/tgbaalgos/sccfilter.cc index 63909252f..7d315987a 100644 --- a/src/tgbaalgos/sccfilter.cc +++ b/src/tgbaalgos/sccfilter.cc @@ -1023,15 +1023,13 @@ namespace spot bdd neg = aut->neg_acceptance_conditions(); filtered->set_acceptance_conditions(filter.accsets(all, neg).first); } - const tgba_digraph::graph_t& ing = aut->get_graph(); - tgba_digraph::graph_t& outg = filtered->get_graph(); - outg.new_states(out_n); + filtered->new_states(out_n); for (unsigned isrc = 0; isrc < in_n; ++isrc) { unsigned osrc = inout[isrc]; if (osrc >= out_n) continue; - for (auto& t: ing.out(isrc)) + for (auto& t: aut->out(isrc)) { unsigned odst = inout[t.dst]; if (odst >= out_n) @@ -1042,7 +1040,7 @@ namespace spot std::tie(want, cond, acc) = filter.trans(isrc, t.dst, t.cond, t.acc); if (want) - outg.new_transition(osrc, odst, cond, acc); + filtered->new_transition(osrc, odst, cond, acc); } } if (!given_si) diff --git a/src/tgbaalgos/sccinfo.cc b/src/tgbaalgos/sccinfo.cc index bcb799a92..2509a5575 100644 --- a/src/tgbaalgos/sccinfo.cc +++ b/src/tgbaalgos/sccinfo.cc @@ -81,7 +81,7 @@ namespace spot num_ = -1; h_[init] = num_; root_.emplace_front(num_, bddfalse, bddfalse); - todo_.emplace(init, aut->get_graph().out(init).begin()); + todo_.emplace(init, aut->out(init).begin()); } while (!todo_.empty()) @@ -148,7 +148,7 @@ namespace spot // for later processing. h_[dest] = --num_; root_.emplace_front(num_, cond, acc); - todo_.emplace(dest, aut->get_graph().out(dest).begin()); + todo_.emplace(dest, aut->out(dest).begin()); continue; } @@ -230,8 +230,7 @@ namespace spot std::vector scc_info::used_acc() const { - auto& g = aut_->get_graph(); - unsigned n = g.num_states(); + unsigned n = aut_->num_states(); std::vector result(scc_count()); acceptance_convertor conv(aut_->neg_acceptance_conditions()); @@ -240,7 +239,7 @@ namespace spot unsigned src_scc = scc_of(src); if (!is_accepting_scc(src_scc)) continue; - for (auto& t: g.out(src)) + for (auto& t: aut_->out(src)) { if (scc_of(t.dst) != src_scc) continue; diff --git a/src/tgbaalgos/simulation.cc b/src/tgbaalgos/simulation.cc index 21aee1394..ae5ff4733 100644 --- a/src/tgbaalgos/simulation.cc +++ b/src/tgbaalgos/simulation.cc @@ -236,14 +236,12 @@ namespace spot bd->register_all_variables_of(old_a_, a_); a_->copy_acceptance_conditions_of(old_a_); } - tgba_digraph::graph_t& gout = a_->get_graph(); - tgba_digraph::graph_t& gin = old_a_->get_graph(); - unsigned ns = gin.num_states(); + unsigned ns = old_a_->num_states(); if (Cosimulation) - gout.new_states(ns); + a_->new_states(ns); for (unsigned s = 0; s < ns; ++s) { - for (auto& t: gin.out(s)) + for (auto& t: old_a_->out(s)) { bdd acc; if (Sba && Cosimulation) @@ -255,7 +253,7 @@ namespace spot // (which now become outgoing arcs after // transposition). acc = bddfalse; - for (auto& td: gin.out(t.dst)) + for (auto& td: old_a_->out(t.dst)) { acc = ac.complement(td.acc); break; @@ -266,7 +264,7 @@ namespace spot acc = ac.complement(t.acc); } if (Cosimulation) - gout.new_transition(t.dst, s, t.cond, acc); + a_->new_transition(t.dst, s, t.cond, acc); else t.acc = acc; } @@ -378,7 +376,7 @@ namespace spot { bdd res = bddfalse; - for (auto& t: a_->get_graph().out(src)) + for (auto& t: a_->out(src)) { bdd acc = bddtrue; @@ -681,14 +679,13 @@ namespace spot // dealing with SBA in cosimulation. if (Sba && Cosimulation) { - tgba_digraph::graph_t& g = res->get_graph(); unsigned ns = res->num_states(); for (unsigned s = 0; s < ns; ++s) { bdd acc = accst[s]; if (acc == bddfalse) continue; - for (auto& t: g.out(s)) + for (auto& t: res->out(s)) t.acc = acc; } } @@ -831,7 +828,7 @@ namespace spot unsigned scc = scc_map_->scc_of_state(old_a_->state_from_number(src)); bool sccacc = scc_map_->accepting(scc); - for (auto& t: a_->get_graph().out(src)) + for (auto& t: a_->out(src)) { bdd cl = previous_class_[t.dst]; bdd acc;