Commit e9893586 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

remove the sba interface

* src/tgba/tgbagraph.hh: Automatize the setting of the SingleAccSet
property.
* src/tgbaalgos/minimize.cc: Do not bother setting SingleAccSet.
* src/tgba/sba.hh: Delete.
* src/tgba/Makefile.am, wrap/python/spot.i: Adjust.
* src/taalgos/tgba2ta.cc: Do not include sba.hh.
* src/neverparse/neverclaimparse.yy: Set the SBA property on the output.
* src/tgbaalgos/lbtt.cc (lbtt_read_gba): Set the StateBasedAcc property
on output.
* src/tgbaalgos/dotty.cc, src/tgbaalgos/neverclaim.cc: Do not rely on
the sba interface.
* src/dstarparse/dra2ba.cc, src/dstarparse/nra2nba.cc,
src/tgbaalgos/simulation.cc, src/tgbaalgos/sccfilter.cc: Set
tgba_digraph::StateBasedAcc as appropriate.
* src/tgbatest/ltl2tgba.cc: Add extra assert.
parent cc38443e
...@@ -238,6 +238,7 @@ namespace spot ...@@ -238,6 +238,7 @@ namespace spot
{ {
bdd_dict* bd = a->aut->get_dict(); bdd_dict* bd = a->aut->get_dict();
bd->register_all_variables_of(a->aut, out_); bd->register_all_variables_of(a->aut, out_);
out_->set_bprop(tgba_digraph::StateBasedAcc);
// Invent a new acceptance set for the degeneralized automaton. // Invent a new acceptance set for the degeneralized automaton.
int accvar = int accvar =
......
...@@ -52,6 +52,8 @@ namespace spot ...@@ -52,6 +52,8 @@ namespace spot
int accvar = int accvar =
bd->register_acceptance_variable(ltl::constant::true_instance(), bd->register_acceptance_variable(ltl::constant::true_instance(),
out_); out_);
out_->set_bprop(tgba_digraph::StateBasedAcc);
acc_ = bdd_ithvar(accvar); acc_ = bdd_ithvar(accvar);
out_->set_acceptance_conditions(acc_); out_->set_acceptance_conditions(acc_);
out_->new_states(num_states_ * (d_->accpair_count + 1)); out_->new_states(num_states_ * (d_->accpair_count + 1));
......
...@@ -309,6 +309,8 @@ namespace spot ...@@ -309,6 +309,8 @@ namespace spot
bdd acc = bdd_ithvar(dict->register_acceptance_variable(t, result)); bdd acc = bdd_ithvar(dict->register_acceptance_variable(t, result));
result->set_acceptance_conditions(acc); result->set_acceptance_conditions(acc);
result->set_bprop(tgba_digraph::SBA);
neverclaimyy::parser parser(error_list, env, result, namer, fcache); neverclaimyy::parser parser(error_list, env, result, namer, fcache);
parser.set_debug_level(debug); parser.set_debug_level(debug);
parser.parse(); parser.parse();
......
...@@ -29,7 +29,6 @@ ...@@ -29,7 +29,6 @@
#include "ltlast/atomic_prop.hh" #include "ltlast/atomic_prop.hh"
#include "ltlast/constant.hh" #include "ltlast/constant.hh"
#include "tgba/formula2bdd.hh" #include "tgba/formula2bdd.hh"
#include "tgba/sba.hh"
#include "misc/bddop.hh" #include "misc/bddop.hh"
#include <cassert> #include <cassert>
#include "ltlvisit/tostring.hh" #include "ltlvisit/tostring.hh"
......
...@@ -30,7 +30,6 @@ tgba_HEADERS = \ ...@@ -30,7 +30,6 @@ tgba_HEADERS = \
bddprint.hh \ bddprint.hh \
formula2bdd.hh \ formula2bdd.hh \
futurecondcol.hh \ futurecondcol.hh \
sba.hh \
state.hh \ state.hh \
succiter.hh \ succiter.hh \
taatgba.hh \ taatgba.hh \
......
// 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 <http://www.gnu.org/licenses/>.
#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
...@@ -314,6 +314,11 @@ namespace spot ...@@ -314,6 +314,11 @@ namespace spot
} }
all_acceptance_conditions_ = all_acceptance_conditions_ =
compute_all_acceptance_conditions(neg_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() unsigned new_state()
......
...@@ -21,8 +21,7 @@ ...@@ -21,8 +21,7 @@
// along with this program. If not, see <http://www.gnu.org/licenses/>. // along with this program. If not, see <http://www.gnu.org/licenses/>.
#include <ostream> #include <ostream>
#include "tgba/tgba.hh" #include "tgba/tgbagraph.hh"
#include "tgba/sba.hh"
#include "dotty.hh" #include "dotty.hh"
#include "dottydec.hh" #include "dottydec.hh"
#include "tgba/bddprint.hh" #include "tgba/bddprint.hh"
...@@ -42,7 +41,7 @@ namespace spot ...@@ -42,7 +41,7 @@ namespace spot
dotty_decorator* dd) dotty_decorator* dd)
: tgba_reachable_iterator_breadth_first(a), os_(os), : tgba_reachable_iterator_breadth_first(a), os_(os),
mark_accepting_states_(mark_accepting_states), dd_(dd), mark_accepting_states_(mark_accepting_states), dd_(dd),
sba_(dynamic_cast<const sba*>(a)) sba_(dynamic_cast<const tgba_digraph*>(a))
{ {
} }
...@@ -120,7 +119,7 @@ namespace spot ...@@ -120,7 +119,7 @@ namespace spot
std::ostream& os_; std::ostream& os_;
bool mark_accepting_states_; bool mark_accepting_states_;
dotty_decorator* dd_; dotty_decorator* dd_;
const sba* sba_; const tgba_digraph* sba_;
}; };
} }
......
...@@ -244,6 +244,7 @@ namespace spot ...@@ -244,6 +244,7 @@ namespace spot
auto aut = std::unique_ptr<tgba_digraph>(new tgba_digraph(dict)); auto aut = std::unique_ptr<tgba_digraph>(new tgba_digraph(dict));
acc_mapper_int acc_b(aut.get(), num_acc, envacc); acc_mapper_int acc_b(aut.get(), num_acc, envacc);
aut->new_states(num_states); aut->new_states(num_states);
aut->set_bprop(tgba_digraph::StateBasedAcc);
for (unsigned n = 0; n < num_states; ++n) for (unsigned n = 0; n < num_states; ++n)
{ {
......
...@@ -143,7 +143,6 @@ namespace spot ...@@ -143,7 +143,6 @@ namespace spot
bdd allacc = bddfalse; bdd allacc = bddfalse;
if (!final->empty()) if (!final->empty())
{ {
res->set_bprop(tgba_digraph::SingleAccSet);
int accvar = int accvar =
dict->register_acceptance_variable(ltl::constant::true_instance(), dict->register_acceptance_variable(ltl::constant::true_instance(),
res); res);
......
...@@ -23,7 +23,7 @@ ...@@ -23,7 +23,7 @@
#include <ostream> #include <ostream>
#include <sstream> #include <sstream>
#include "bdd.h" #include "bdd.h"
#include "tgba/sba.hh" #include "tgba/tgbagraph.hh"
#include "neverclaim.hh" #include "neverclaim.hh"
#include "tgba/bddprint.hh" #include "tgba/bddprint.hh"
#include "reachiter.hh" #include "reachiter.hh"
...@@ -42,8 +42,9 @@ namespace spot ...@@ -42,8 +42,9 @@ namespace spot
: tgba_reachable_iterator_breadth_first(a), : tgba_reachable_iterator_breadth_first(a),
os_(os), f_(f), accept_all_(-1), fi_needed_(false), os_(os), f_(f), accept_all_(-1), fi_needed_(false),
comments_(comments), all_acc_conds_(a->all_acceptance_conditions()), comments_(comments), all_acc_conds_(a->all_acceptance_conditions()),
sba_(dynamic_cast<const sba*>(a)) sba_(dynamic_cast<const tgba_digraph*>(a))
{ {
assert(!sba_ || sba_->get_bprop(tgba_digraph::StateBasedAcc));
} }
void void
...@@ -193,7 +194,7 @@ namespace spot ...@@ -193,7 +194,7 @@ namespace spot
state* init_; state* init_;
bool comments_; bool comments_;
bdd all_acc_conds_; bdd all_acc_conds_;
const sba* sba_; const tgba_digraph* sba_;
}; };
} // anonymous } // anonymous
......
...@@ -499,7 +499,11 @@ namespace spot ...@@ -499,7 +499,11 @@ namespace spot
tgba_digraph* tgba_digraph*
scc_filter_states(const tgba_digraph* aut, scc_info* given_si) scc_filter_states(const tgba_digraph* aut, scc_info* given_si)
{ {
return scc_filter_apply<state_filter<>>(aut, given_si); bool sb = aut->get_bprop(tgba_digraph::StateBasedAcc);
auto res = scc_filter_apply<state_filter<>>(aut, given_si);
if (sb)
res->set_bprop(tgba_digraph::StateBasedAcc);
return res;
} }
tgba_digraph* tgba_digraph*
......
...@@ -550,6 +550,8 @@ namespace spot ...@@ -550,6 +550,8 @@ namespace spot
tgba_digraph* res = new tgba_digraph(d); tgba_digraph* res = new tgba_digraph(d);
d->register_all_variables_of(a_, res); d->register_all_variables_of(a_, res);
res->set_acceptance_conditions(all_acceptance_conditions_); res->set_acceptance_conditions(all_acceptance_conditions_);
if (Sba)
res->set_bprop(tgba_digraph::StateBasedAcc);
bdd sup_all_acc = bdd_support(all_acceptance_conditions_); bdd sup_all_acc = bdd_support(all_acceptance_conditions_);
// Non atomic propositions variables (= acc and class) // Non atomic propositions variables (= acc and class)
......
...@@ -1089,10 +1089,13 @@ main(int argc, char** argv) ...@@ -1089,10 +1089,13 @@ main(int argc, char** argv)
{ {
if (daut->type == spot::Rabin) if (daut->type == spot::Rabin)
{ {
spot::tgba_digraph* res;
if (dra2dba) if (dra2dba)
to_free = a = spot::dstar_to_tgba(daut); res = spot::dstar_to_tgba(daut);
else 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; assume_sba = true;
} }
else else
......
...@@ -77,7 +77,6 @@ namespace std { ...@@ -77,7 +77,6 @@ namespace std {
#include "tgba/state.hh" #include "tgba/state.hh"
#include "tgba/succiter.hh" #include "tgba/succiter.hh"
#include "tgba/tgba.hh" #include "tgba/tgba.hh"
#include "tgba/sba.hh"
#include "tgba/taatgba.hh" #include "tgba/taatgba.hh"
#include "tgba/tgbaproduct.hh" #include "tgba/tgbaproduct.hh"
#include "tgba/tgbatba.hh" #include "tgba/tgbatba.hh"
...@@ -218,7 +217,6 @@ using namespace spot; ...@@ -218,7 +217,6 @@ using namespace spot;
%include "tgba/state.hh" %include "tgba/state.hh"
%include "tgba/succiter.hh" %include "tgba/succiter.hh"
%include "tgba/tgba.hh" %include "tgba/tgba.hh"
%include "tgba/sba.hh"
%include "tgba/taatgba.hh" %include "tgba/taatgba.hh"
%include "tgba/tgbaproduct.hh" %include "tgba/tgbaproduct.hh"
%include "tgba/tgbatba.hh" %include "tgba/tgbatba.hh"
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment