diff --git a/src/dstarparse/dra2ba.cc b/src/dstarparse/dra2ba.cc index 08364e12f..22ae56e32 100644 --- a/src/dstarparse/dra2ba.cc +++ b/src/dstarparse/dra2ba.cc @@ -23,7 +23,6 @@ #include "tgbaalgos/reachiter.hh" #include "tgbaalgos/gtec/gtec.hh" #include "tgbaalgos/sccfilter.hh" -#include "ltlast/constant.hh" namespace spot { @@ -239,13 +238,7 @@ namespace spot bdd_dict* bd = a->aut->get_dict(); bd->register_all_variables_of(a->aut, out_); out_->set_bprop(tgba_digraph::StateBasedAcc); - - // Invent a new acceptance set for the degeneralized automaton. - int accvar = - bd->register_acceptance_variable(ltl::constant::true_instance(), - out_); - acc_ = bdd_ithvar(accvar); - out_->set_acceptance_conditions(acc_); + acc_ = out_->set_single_acceptance_set(); out_->new_states(num_states_ * (a->accpair_count + 1)); out_->set_init_state(a->aut->get_init_state_number()); } @@ -299,10 +292,9 @@ namespace spot // accepting cycle. out_->new_transition(in, out + shift, cond); - bdd acc = bddfalse; - if (l.get(i)) // In the Li set. (Löding's Fi set.) - acc = acc_; - out_->new_transition(in + shift, out + shift, cond, acc); + // Acceptance transitions are those in the Li set. (Löding's Fi set.) + out_->new_acc_transition(in + shift, out + shift, cond, + l.get(i)); } } } diff --git a/src/dstarparse/nra2nba.cc b/src/dstarparse/nra2nba.cc index 7c539a850..513b4c64e 100644 --- a/src/dstarparse/nra2nba.cc +++ b/src/dstarparse/nra2nba.cc @@ -20,7 +20,6 @@ #include "public.hh" #include "tgbaalgos/reachiter.hh" #include "tgbaalgos/sccfilter.hh" -#include "ltlast/constant.hh" namespace spot { @@ -49,13 +48,8 @@ namespace spot bd->register_all_variables_of(aut, out_); // Invent a new acceptance set for the degeneralized automaton. - int accvar = - bd->register_acceptance_variable(ltl::constant::true_instance(), - out_); + out_->set_single_acceptance_set(); out_->set_bprop(tgba_digraph::StateBasedAcc); - - acc_ = bdd_ithvar(accvar); - out_->set_acceptance_conditions(acc_); out_->new_states(num_states_ * (d_->accpair_count + 1)); auto i = aut->get_init_state(); @@ -104,10 +98,10 @@ namespace spot // accepting cycle. out_->new_transition(in, out + shift, cond); - bdd acc = bddfalse; - if (l.get(i)) // In the Li set. (Löding's Fi set.) - acc = acc_; - out_->new_transition(in + shift, out + shift, cond, acc); + // A transition is accepting if it is in the Li + // set. (Löding's Fi set.) + out_->new_acc_transition(in + shift, out + shift, cond, + l.get(i)); } } } @@ -116,7 +110,6 @@ namespace spot tgba_digraph* out_; const dstar_aut* d_; size_t num_states_; - bdd acc_; }; } diff --git a/src/neverparse/neverclaimparse.yy b/src/neverparse/neverclaimparse.yy index 9cec1a443..ed4985091 100644 --- a/src/neverparse/neverclaimparse.yy +++ b/src/neverparse/neverclaimparse.yy @@ -31,7 +31,6 @@ { #include #include -#include "ltlast/constant.hh" #include "public.hh" #include "tgba/formula2bdd.hh" @@ -168,7 +167,6 @@ state: | ident_list "false" { delete $1; } | ident_list transition_block { - std::list::iterator it; bdd acc = !strncmp("accept", $1->c_str(), 6) ? result->all_acceptance_conditions() : static_cast(bddfalse); @@ -304,11 +302,7 @@ namespace spot formula_cache fcache; tgba_digraph* result = new tgba_digraph(dict); auto namer = result->create_namer(); - - const ltl::formula* t = ltl::constant::true_instance(); - bdd acc = bdd_ithvar(dict->register_acceptance_variable(t, result)); - result->set_acceptance_conditions(acc); - + result->set_single_acceptance_set(); result->set_bprop(tgba_digraph::SBA); neverclaimyy::parser parser(error_list, env, result, namer, fcache); @@ -319,7 +313,7 @@ namespace spot if (accept_all_needed && !accept_all_seen) { unsigned n = namer->new_state("accept_all"); - result->new_transition(n, n, bddtrue, acc); + result->new_acc_transition(n, n, bddtrue); } accept_all_needed = false; accept_all_seen = false; diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index a2c2d4843..285961554 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -53,6 +53,7 @@ libtgba_la_SOURCES = \ futurecondcol.cc \ taatgba.cc \ tgba.cc \ + tgbagraph.cc \ tgbakvcomplement.cc \ tgbaproduct.cc \ tgbamask.cc \ diff --git a/src/tgba/tgbagraph.cc b/src/tgba/tgbagraph.cc new file mode 100644 index 000000000..570612577 --- /dev/null +++ b/src/tgba/tgbagraph.cc @@ -0,0 +1,102 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2014 Laboratoire de Recherche et Développement de +// l'Epita. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 3 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with this program. If not, see . + +#include "tgbagraph.hh" +#include "ltlast/constant.hh" + +namespace spot +{ + + void tgba_digraph::set_acceptance_conditions(bdd all) + { + if (all_acceptance_conditions_ != bddfalse) + dict_->unregister_all_typed_variables(bdd_dict::acc, this); + + bdd sup = bdd_support(all); + dict_->register_acceptance_variables(sup, this); + neg_acceptance_conditions_ = bddtrue; + while (sup != bddtrue) + { + neg_acceptance_conditions_ &= bdd_nithvar(bdd_var(sup)); + sup = bdd_high(sup); + } + all_acceptance_conditions_ = + compute_all_acceptance_conditions(neg_acceptance_conditions_); + + if (number_of_acceptance_conditions() == 1) + set_bprop(tgba_digraph::SingleAccSet); + else + clear_bprop(tgba_digraph::SingleAccSet); + } + + bdd tgba_digraph::set_single_acceptance_set() + { + if (all_acceptance_conditions_ != bddfalse) + dict_->unregister_all_typed_variables(bdd_dict::acc, this); + + set_bprop(tgba_digraph::SingleAccSet); + int accvar = + dict_->register_acceptance_variable(ltl::constant::true_instance(), + this); + bdd degen_acc = bdd_ithvar(accvar); + all_acceptance_conditions_ = degen_acc; + neg_acceptance_conditions_ = bdd_nithvar(accvar); + return degen_acc; + } + + void tgba_digraph::merge_transitions() + { + for (auto& s: g_.states()) + { + // Map a pair (dest state, acc) to the first transition seen + // with such characteristic. + + typedef std::pair key_t; + std::unordered_map trmap; + + auto t = g_.out_iteraser(s); + while (t) + { + // Simply skip false transitions. + if (t->cond == bddfalse) + { + t.erase(); + continue; + } + + key_t k(t->dst, t->acc.id()); + auto p = trmap.emplace(k, t.trans()); + if (!p.second) + { + // A previous transitions exist for k, merge the + // condition, and schedule the transition for + // removal. + g_.trans_data(p.first->second).cond |= t->cond; + t.erase(); + } + else + { + ++t; + } + } + } + g_.defrag(); + } + +} diff --git a/src/tgba/tgbagraph.hh b/src/tgba/tgbagraph.hh index 1e026b297..01c153095 100644 --- a/src/tgba/tgbagraph.hh +++ b/src/tgba/tgbagraph.hh @@ -90,7 +90,7 @@ namespace spot template - class tgba_digraph_succ_iterator: public tgba_succ_iterator + class SPOT_API tgba_digraph_succ_iterator: public tgba_succ_iterator { private: typedef typename Graph::transition transition; @@ -153,7 +153,7 @@ namespace spot }; - class tgba_digraph: public tgba + class SPOT_API tgba_digraph: public tgba { public: typedef digraph graph_t; @@ -302,24 +302,8 @@ namespace spot return g_.trans_data(t); } - void set_acceptance_conditions(bdd all) - { - bdd sup = bdd_support(all); - this->dict_->register_acceptance_variables(sup, this); - neg_acceptance_conditions_ = bddtrue; - while (sup != bddtrue) - { - neg_acceptance_conditions_ &= bdd_nithvar(bdd_var(sup)); - sup = bdd_high(sup); - } - all_acceptance_conditions_ = - compute_all_acceptance_conditions(neg_acceptance_conditions_); - - if (number_of_acceptance_conditions() == 1) - set_bprop(tgba_digraph::SingleAccSet); - else - clear_bprop(tgba_digraph::SingleAccSet); - } + void set_acceptance_conditions(bdd all); + bdd set_single_acceptance_set(); unsigned new_state() { @@ -337,6 +321,15 @@ namespace spot return g_.new_transition(src, dst, cond, acc); } + unsigned new_acc_transition(unsigned src, unsigned dst, + bdd cond, bool acc = true) + { + if (acc) + return g_.new_transition(src, dst, cond, all_acceptance_conditions_); + else + return g_.new_transition(src, dst, cond); + } + auto out(unsigned src) const SPOT_RETURN(g_.out(src)); auto out(unsigned src) @@ -378,45 +371,7 @@ namespace spot /// Iterate over all transitions, and merge those with compatible /// extremities and acceptance. - void merge_transitions() - { - for (auto& s: g_.states()) - { - // Map a pair (dest state, acc) to the first transition seen - // with such characteristic. - - typedef std::pair key_t; - std::unordered_map trmap; - - auto t = g_.out_iteraser(s); - while (t) - { - // Simply skip false transitions. - if (t->cond == bddfalse) - { - t.erase(); - continue; - } - - key_t k(t->dst, t->acc.id()); - auto p = trmap.emplace(k, t.trans()); - if (!p.second) - { - // A previous transitions exist for k, merge the - // condition, and schedule the transition for - // removal. - g_.trans_data(p.first->second).cond |= t->cond; - t.erase(); - } - else - { - ++t; - } - } - } - g_.defrag(); - } - + void merge_transitions(); protected: unsigned bprops_ = 0; diff --git a/src/tgbaalgos/complete.cc b/src/tgbaalgos/complete.cc index b4bb4bda4..9b58f695c 100644 --- a/src/tgbaalgos/complete.cc +++ b/src/tgbaalgos/complete.cc @@ -18,7 +18,6 @@ // along with this program. If not, see . #include "complete.hh" -#include "ltlast/constant.hh" #include "dupexp.hh" namespace spot @@ -33,10 +32,7 @@ namespace spot // We cannot safely complete an automaton if it has no // acceptance set as the added sink would become accepting. // In this case, add an acceptance set to all transitions. - const ltl::formula* t = ltl::constant::true_instance(); - int v = aut->get_dict()->register_acceptance_variable(t, aut); - allacc = bdd_ithvar(v); - aut->set_acceptance_conditions(allacc); + allacc = aut->set_single_acceptance_set(); for (auto& t: aut->transitions()) t.acc = allacc; } diff --git a/src/tgbaalgos/degen.cc b/src/tgbaalgos/degen.cc index e3100176b..f6a3c78a6 100644 --- a/src/tgbaalgos/degen.cc +++ b/src/tgbaalgos/degen.cc @@ -22,7 +22,6 @@ #include "tgba/tgbagraph.hh" #include "misc/hash.hh" #include "misc/hashfunc.hh" -#include "ltlast/constant.hh" #include #include #include @@ -261,19 +260,13 @@ namespace spot // The result automaton is an SBA. auto res = new tgba_digraph(dict); + res->set_single_acceptance_set(); if (want_sba) res->set_bprop(tgba_digraph::StateBasedAcc); // We use the same BDD variables as the input, except for the // acceptance. dict->register_all_variables_of(a, res); - dict->unregister_all_typed_variables(bdd_dict::acc, res); - - // Invent a new acceptance set for the degeneralized automaton. - int accvar = - dict->register_acceptance_variable(ltl::constant::true_instance(), res); - bdd degen_acc = bdd_ithvar(accvar); - res->set_acceptance_conditions(degen_acc); // Create an order of acceptance conditions. Each entry in this // vector correspond to an acceptance set. Each index can @@ -600,23 +593,11 @@ namespace spot unsigned& t = tr_cache[dest * 2 + is_acc]; - if (t == 0) - { - // Actually create the transition. If the source - // state is accepting, we have to put degen_acc on all - // outgoing transitions. (We are still building a - // TGBA; we only assure that it can be used as an - // SBA.) - bdd acc = bddfalse; - if (is_acc) - acc = degen_acc; - t = res->new_transition(src, dest, - i->current_condition(), acc); - } - else - { - res->trans_data(t).cond |= i->current_condition(); - } + if (t == 0) // Create transition. + t = res->new_acc_transition(src, dest, + i->current_condition(), is_acc); + else // Update existing transition. + res->trans_data(t).cond |= i->current_condition(); } tr_cache.clear(); } diff --git a/src/tgbaalgos/dtbasat.cc b/src/tgbaalgos/dtbasat.cc index 230aa2eb6..bd9fedb75 100644 --- a/src/tgbaalgos/dtbasat.cc +++ b/src/tgbaalgos/dtbasat.cc @@ -26,7 +26,6 @@ #include #include "scc.hh" #include "tgba/bddprint.hh" -#include "ltlast/constant.hh" #include "stats.hh" #include "misc/satsolver.hh" #include "misc/timer.hh" @@ -673,11 +672,7 @@ namespace spot auto autdict = aut->get_dict(); auto a = new tgba_digraph(autdict); autdict->register_all_variables_of(aut, a); - - const ltl::formula* t = ltl::constant::true_instance(); - bdd acc = bdd_ithvar(autdict->register_acceptance_variable(t, a)); - a->set_acceptance_conditions(acc); - + bdd acc = a->set_single_acceptance_set(); a->new_states(satdict.cand_size); unsigned last_aut_trans = -1U; @@ -710,16 +705,13 @@ namespace spot if (seen_trans.insert(src_cond(t->second.src, t->second.cond)).second) { - bdd accept = bddfalse; // Mark the transition as accepting if the source is. - if (state_based - && acc_states.find(t->second.src) != acc_states.end()) - accept = acc; + bool accept = state_based + && acc_states.find(t->second.src) != acc_states.end(); - last_aut_trans = a->new_transition(t->second.src - 1, - t->second.dst - 1, - t->second.cond, - accept); + last_aut_trans = + a->new_acc_transition(t->second.src - 1, t->second.dst - 1, + t->second.cond, accept); last_sat_trans = &t->second; dout << v << '\t' << t->second << "δ\n"; diff --git a/src/tgbaalgos/dtgbacomp.cc b/src/tgbaalgos/dtgbacomp.cc index 15eed8d34..32d9828a4 100644 --- a/src/tgbaalgos/dtgbacomp.cc +++ b/src/tgbaalgos/dtgbacomp.cc @@ -18,7 +18,6 @@ // along with this program. If not, see . #include "dtgbacomp.hh" -#include "ltlast/constant.hh" #include "dupexp.hh" namespace spot @@ -28,18 +27,12 @@ namespace spot // Clone the original automaton. tgba_digraph* res = tgba_dupexp_dfs(aut); - auto dict = res->get_dict(); - bdd oldaccs = aut->all_acceptance_conditions(); bdd oldnegs = aut->neg_acceptance_conditions(); // We will modify res in place, and the resulting // automaton will only have one acceptance set. - dict->unregister_all_typed_variables(bdd_dict::acc, res); - bdd theacc = - bdd_ithvar(dict->register_acceptance_variable - (ltl::constant::true_instance(), res)); - res->set_acceptance_conditions(theacc); + res->set_single_acceptance_set(); unsigned num_acc = aut->number_of_acceptance_conditions(); unsigned n = res->num_states(); @@ -48,7 +41,7 @@ namespace spot res->new_states(num_acc * n + 1); unsigned sink = res->num_states() - 1; // The sink state has an accepting self-loop. - res->new_transition(sink, sink, bddtrue, theacc); + res->new_acc_transition(sink, sink, bddtrue); for (unsigned src = 0; src < n; ++src) { @@ -85,7 +78,7 @@ namespace spot if (h == bddfalse) { // Clone the transition - res->new_transition(src + add, dst + add, cond, theacc); + res->new_acc_transition(src + add, dst + add, cond); assert(dst + add < sink); // Using `t' is disallowed from now on as it is a // reference to a transition that may have been