diff --git a/src/dstarparse/dra2ba.cc b/src/dstarparse/dra2ba.cc index a90356440..08364e12f 100644 --- a/src/dstarparse/dra2ba.cc +++ b/src/dstarparse/dra2ba.cc @@ -238,6 +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 = diff --git a/src/dstarparse/nra2nba.cc b/src/dstarparse/nra2nba.cc index 3df34ad28..7c539a850 100644 --- a/src/dstarparse/nra2nba.cc +++ b/src/dstarparse/nra2nba.cc @@ -52,6 +52,8 @@ namespace spot int accvar = bd->register_acceptance_variable(ltl::constant::true_instance(), out_); + out_->set_bprop(tgba_digraph::StateBasedAcc); + acc_ = bdd_ithvar(accvar); out_->set_acceptance_conditions(acc_); out_->new_states(num_states_ * (d_->accpair_count + 1)); diff --git a/src/neverparse/neverclaimparse.yy b/src/neverparse/neverclaimparse.yy index d5ec008b8..9cec1a443 100644 --- a/src/neverparse/neverclaimparse.yy +++ b/src/neverparse/neverclaimparse.yy @@ -309,6 +309,8 @@ namespace spot bdd acc = bdd_ithvar(dict->register_acceptance_variable(t, result)); result->set_acceptance_conditions(acc); + result->set_bprop(tgba_digraph::SBA); + neverclaimyy::parser parser(error_list, env, result, namer, fcache); parser.set_debug_level(debug); parser.parse(); diff --git a/src/taalgos/tgba2ta.cc b/src/taalgos/tgba2ta.cc index 0cc1fdaef..1b970c6d1 100644 --- a/src/taalgos/tgba2ta.cc +++ b/src/taalgos/tgba2ta.cc @@ -29,7 +29,6 @@ #include "ltlast/atomic_prop.hh" #include "ltlast/constant.hh" #include "tgba/formula2bdd.hh" -#include "tgba/sba.hh" #include "misc/bddop.hh" #include #include "ltlvisit/tostring.hh" diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index 15fbba016..e60c205a0 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -30,7 +30,6 @@ tgba_HEADERS = \ bddprint.hh \ formula2bdd.hh \ futurecondcol.hh \ - sba.hh \ state.hh \ succiter.hh \ taatgba.hh \ diff --git a/src/tgba/sba.hh b/src/tgba/sba.hh deleted file mode 100644 index b2166c41c..000000000 --- a/src/tgba/sba.hh +++ /dev/null @@ -1,43 +0,0 @@ -// Copyright (C) 2012 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// -// 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 . - -#ifndef SPOT_TGBA_SBA_HH -# define SPOT_TGBA_SBA_HH - -#include "tgba.hh" - -namespace spot -{ - /// \ingroup tgba_essentials - /// \brief A State-based Generalized Büchi Automaton. - /// - /// An SBA is a TGBA in which the outgoing transitions of - /// a state are either all accepting (in which case the - /// source state is said "accepting"(, or all non-accepting. - class sba: public tgba - { - public: - /// \brief is \a s an accepting state? - /// - /// If a state is accepting all its outgoing transitions are - /// accepting. - virtual bool state_is_accepting(const spot::state* s) const = 0; - }; -} - -#endif // SPOT_TGBA_SBA_HH diff --git a/src/tgba/tgbagraph.hh b/src/tgba/tgbagraph.hh index 986d0a497..1e026b297 100644 --- a/src/tgba/tgbagraph.hh +++ b/src/tgba/tgbagraph.hh @@ -314,6 +314,11 @@ namespace spot } 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); } unsigned new_state() diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc index 8bb4f3b00..7cd9b1770 100644 --- a/src/tgbaalgos/dotty.cc +++ b/src/tgbaalgos/dotty.cc @@ -21,8 +21,7 @@ // along with this program. If not, see . #include -#include "tgba/tgba.hh" -#include "tgba/sba.hh" +#include "tgba/tgbagraph.hh" #include "dotty.hh" #include "dottydec.hh" #include "tgba/bddprint.hh" @@ -42,7 +41,7 @@ namespace spot dotty_decorator* dd) : tgba_reachable_iterator_breadth_first(a), os_(os), mark_accepting_states_(mark_accepting_states), dd_(dd), - sba_(dynamic_cast(a)) + sba_(dynamic_cast(a)) { } @@ -120,7 +119,7 @@ namespace spot std::ostream& os_; bool mark_accepting_states_; dotty_decorator* dd_; - const sba* sba_; + const tgba_digraph* sba_; }; } diff --git a/src/tgbaalgos/lbtt.cc b/src/tgbaalgos/lbtt.cc index 607ad2ce0..3a4ce30ef 100644 --- a/src/tgbaalgos/lbtt.cc +++ b/src/tgbaalgos/lbtt.cc @@ -244,6 +244,7 @@ namespace spot auto aut = std::unique_ptr(new tgba_digraph(dict)); acc_mapper_int acc_b(aut.get(), num_acc, envacc); aut->new_states(num_states); + aut->set_bprop(tgba_digraph::StateBasedAcc); for (unsigned n = 0; n < num_states; ++n) { diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc index 1b4836b14..99b3f9c83 100644 --- a/src/tgbaalgos/minimize.cc +++ b/src/tgbaalgos/minimize.cc @@ -143,7 +143,6 @@ namespace spot bdd allacc = bddfalse; if (!final->empty()) { - res->set_bprop(tgba_digraph::SingleAccSet); int accvar = dict->register_acceptance_variable(ltl::constant::true_instance(), res); diff --git a/src/tgbaalgos/neverclaim.cc b/src/tgbaalgos/neverclaim.cc index ecc6dfce2..3a81338f7 100644 --- a/src/tgbaalgos/neverclaim.cc +++ b/src/tgbaalgos/neverclaim.cc @@ -23,7 +23,7 @@ #include #include #include "bdd.h" -#include "tgba/sba.hh" +#include "tgba/tgbagraph.hh" #include "neverclaim.hh" #include "tgba/bddprint.hh" #include "reachiter.hh" @@ -42,8 +42,9 @@ namespace spot : tgba_reachable_iterator_breadth_first(a), os_(os), f_(f), accept_all_(-1), fi_needed_(false), comments_(comments), all_acc_conds_(a->all_acceptance_conditions()), - sba_(dynamic_cast(a)) + sba_(dynamic_cast(a)) { + assert(!sba_ || sba_->get_bprop(tgba_digraph::StateBasedAcc)); } void @@ -193,7 +194,7 @@ namespace spot state* init_; bool comments_; bdd all_acc_conds_; - const sba* sba_; + const tgba_digraph* sba_; }; } // anonymous diff --git a/src/tgbaalgos/sccfilter.cc b/src/tgbaalgos/sccfilter.cc index 4c9c63f99..5aed42152 100644 --- a/src/tgbaalgos/sccfilter.cc +++ b/src/tgbaalgos/sccfilter.cc @@ -499,7 +499,11 @@ namespace spot tgba_digraph* scc_filter_states(const tgba_digraph* aut, scc_info* given_si) { - return scc_filter_apply>(aut, given_si); + bool sb = aut->get_bprop(tgba_digraph::StateBasedAcc); + auto res = scc_filter_apply>(aut, given_si); + if (sb) + res->set_bprop(tgba_digraph::StateBasedAcc); + return res; } tgba_digraph* diff --git a/src/tgbaalgos/simulation.cc b/src/tgbaalgos/simulation.cc index d8053c496..2d8418717 100644 --- a/src/tgbaalgos/simulation.cc +++ b/src/tgbaalgos/simulation.cc @@ -550,6 +550,8 @@ namespace spot tgba_digraph* res = new tgba_digraph(d); d->register_all_variables_of(a_, res); res->set_acceptance_conditions(all_acceptance_conditions_); + if (Sba) + res->set_bprop(tgba_digraph::StateBasedAcc); bdd sup_all_acc = bdd_support(all_acceptance_conditions_); // Non atomic propositions variables (= acc and class) diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index c8df4f274..8ee42b88f 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -1089,10 +1089,13 @@ main(int argc, char** argv) { if (daut->type == spot::Rabin) { + spot::tgba_digraph* res; if (dra2dba) - to_free = a = spot::dstar_to_tgba(daut); + res = spot::dstar_to_tgba(daut); else - to_free = a = spot::nra_to_nba(daut); + res = spot::nra_to_nba(daut); + to_free = a = res; + assert(res->get_bprop(spot::tgba_digraph::SBA)); assume_sba = true; } else diff --git a/wrap/python/spot.i b/wrap/python/spot.i index 6750052e3..69d38cc31 100644 --- a/wrap/python/spot.i +++ b/wrap/python/spot.i @@ -77,7 +77,6 @@ namespace std { #include "tgba/state.hh" #include "tgba/succiter.hh" #include "tgba/tgba.hh" -#include "tgba/sba.hh" #include "tgba/taatgba.hh" #include "tgba/tgbaproduct.hh" #include "tgba/tgbatba.hh" @@ -218,7 +217,6 @@ using namespace spot; %include "tgba/state.hh" %include "tgba/succiter.hh" %include "tgba/tgba.hh" -%include "tgba/sba.hh" %include "tgba/taatgba.hh" %include "tgba/tgbaproduct.hh" %include "tgba/tgbatba.hh"