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

get rid of tgba_sba_proxy

* src/saba/sabacomplementtgba.cc, src/saba/sabacomplementtgba.hh,
src/tgba/tgbatba.cc, src/tgba/tgbatba.hh, src/tgbaalgos/degen.hh,
src/tgbatest/complementation.cc, src/tgbatest/ltl2tgba.cc: Here.
parent a63612a5
...@@ -24,6 +24,7 @@ ...@@ -24,6 +24,7 @@
#include <tgba/bddprint.hh> #include <tgba/bddprint.hh>
#include <tgba/state.hh> #include <tgba/state.hh>
#include "misc/hash.hh" #include "misc/hash.hh"
#include "tgbaalgos/degen.hh"
#include "tgbaalgos/bfssteps.hh" #include "tgbaalgos/bfssteps.hh"
#include "misc/hashfunc.hh" #include "misc/hashfunc.hh"
#include "ltlast/formula.hh" #include "ltlast/formula.hh"
...@@ -149,7 +150,7 @@ namespace spot ...@@ -149,7 +150,7 @@ namespace spot
typedef std::map<bdd, state_conjunction_list_t, bdd_less_than> typedef std::map<bdd, state_conjunction_list_t, bdd_less_than>
bdd_list_t; bdd_list_t;
saba_complement_tgba_succ_iterator(const tgba_sba_proxy* automaton, saba_complement_tgba_succ_iterator(const tgba_digraph* automaton,
bdd the_acceptance_cond, bdd the_acceptance_cond,
const saba_state_complement_tgba* const saba_state_complement_tgba*
origin); origin);
...@@ -166,7 +167,7 @@ namespace spot ...@@ -166,7 +167,7 @@ namespace spot
void state_conjunction(); void state_conjunction();
void delete_condition_list(); void delete_condition_list();
const tgba_sba_proxy* automaton_; const tgba_digraph* automaton_;
bdd the_acceptance_cond_; bdd the_acceptance_cond_;
const saba_state_complement_tgba* origin_; const saba_state_complement_tgba* origin_;
bdd_list_t condition_list_; bdd_list_t condition_list_;
...@@ -176,12 +177,13 @@ namespace spot ...@@ -176,12 +177,13 @@ namespace spot
}; };
saba_complement_tgba_succ_iterator:: saba_complement_tgba_succ_iterator::
saba_complement_tgba_succ_iterator(const tgba_sba_proxy* automaton, saba_complement_tgba_succ_iterator(const tgba_digraph* automaton,
bdd the_acceptance_cond, bdd the_acceptance_cond,
const saba_state_complement_tgba* origin) const saba_state_complement_tgba* origin)
: automaton_(automaton), the_acceptance_cond_(the_acceptance_cond), : automaton_(automaton), the_acceptance_cond_(the_acceptance_cond),
origin_(origin) origin_(origin)
{ {
assert(automaton->get_bprop(tgba_digraph::SBA));
// If state not accepting or rank is even // If state not accepting or rank is even
if (((origin_->get_rank() & 1) == 0) || if (((origin_->get_rank() & 1) == 0) ||
!automaton_->state_is_accepting(origin_->get_state())) !automaton_->state_is_accepting(origin_->get_state()))
...@@ -364,13 +366,13 @@ namespace spot ...@@ -364,13 +366,13 @@ namespace spot
} // end namespace anonymous. } // end namespace anonymous.
saba_complement_tgba::saba_complement_tgba(const tgba* a) saba_complement_tgba::saba_complement_tgba(const tgba* a)
: automaton_(new tgba_sba_proxy(a)) : automaton_(degeneralize(a))
{ {
get_dict()->register_all_variables_of(automaton_, this); get_dict()->register_all_variables_of(automaton_, this);
int v = get_dict() int v = get_dict()
->register_acceptance_variable(ltl::constant::true_instance(), this); ->register_acceptance_variable(ltl::constant::true_instance(), this);
the_acceptance_cond_ = bdd_ithvar(v); the_acceptance_cond_ = bdd_ithvar(v);
nb_states_ = count_states(automaton_); nb_states_ = automaton_->num_states();
} }
saba_complement_tgba::~saba_complement_tgba() saba_complement_tgba::~saba_complement_tgba()
......
// Copyright (C) 2009, 2010, 2013 Laboratoire de Recherche et Développement // Copyright (C) 2009, 2010, 2013, 2014 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
...@@ -66,7 +66,7 @@ namespace spot ...@@ -66,7 +66,7 @@ namespace spot
virtual std::string format_state(const saba_state* state) const; virtual std::string format_state(const saba_state* state) const;
virtual bdd all_acceptance_conditions() const; virtual bdd all_acceptance_conditions() const;
private: private:
const tgba_sba_proxy* automaton_; const tgba_digraph* automaton_;
bdd the_acceptance_cond_; bdd the_acceptance_cond_;
unsigned nb_states_; unsigned nb_states_;
}; // end class tgba_saba_complement. }; // end class tgba_saba_complement.
......
...@@ -169,19 +169,17 @@ namespace spot ...@@ -169,19 +169,17 @@ namespace spot
typedef tgba_tba_proxy::cycle_list list; typedef tgba_tba_proxy::cycle_list list;
typedef tgba_tba_proxy::cycle_list::const_iterator iterator; typedef tgba_tba_proxy::cycle_list::const_iterator iterator;
public: public:
tgba_tba_proxy_succ_iterator(const state* rs, tgba_tba_proxy_succ_iterator(tgba::succ_iterable&& iterable,
tgba::succ_iterable&& iterable,
iterator expected, iterator expected,
const list& cycle, const list& cycle,
bdd the_acceptance_cond, bdd the_acceptance_cond,
const tgba_tba_proxy* aut) const tgba_tba_proxy* aut)
: the_acceptance_cond_(the_acceptance_cond) : the_acceptance_cond_(the_acceptance_cond)
{ {
recycle(rs, std::move(iterable), expected, cycle, aut); recycle(std::move(iterable), expected, cycle, aut);
} }
void recycle(const state* rs, void recycle(tgba::succ_iterable&& iterable,
tgba::succ_iterable&& iterable,
iterator expected, iterator expected,
const list& cycle, const list& cycle,
const tgba_tba_proxy* aut) const tgba_tba_proxy* aut)
...@@ -204,110 +202,43 @@ namespace spot ...@@ -204,110 +202,43 @@ namespace spot
bdd otheracc = bdd otheracc =
aut->common_acceptance_conditions_of_original_state(odest); aut->common_acceptance_conditions_of_original_state(odest);
iterator next; // A transition in the *EXPECTED acceptance set should
// bddtrue is a special condition used for tgba_sba_proxy // be directed to the next acceptance set. If the
// to denote the (N+1)th copy of the state, after all // current transition is also in the next acceptance
// acceptance conditions have been traversed. Such state // set, then go to the one after, etc.
// is always accepting, so do not check acc for this. //
// bddtrue is also used by tgba_tba_proxy if the automaton // See Denis Oddoux's PhD thesis for a nice
// does not use acceptance conditions. In that case, all // explanation (in French).
// states are accepting. // @PhDThesis{ oddoux.03.phd,
if (*expected == bddtrue) // author = {Denis Oddoux},
// title = {Utilisation des automates alternants pour un
// model-checking efficace des logiques
// temporelles lin{\'e}aires.},
// school = {Universit{\'e}e Paris 7},
// year = {2003},
// address= {Paris, France},
// month = {December}
// }
iterator next = expected;
// Consider both the current acceptance sets, and the
// acceptance sets common to the outgoing transition of
// the destination state.
acc |= otheracc;
while (next != cycle.end() && bdd_implies(*next, acc))
++next;
if (next != cycle.end())
{ {
// When degeneralizing to SBA, ignore the last accepting = false;
// expected acceptance set (the value of *prev below)
// if it is common to all other outgoing transitions (of the
// current state) AND if it is not used by any outgoing
// transition of the destination state.
//
// 1) It's correct to do that, because this acceptance
// set is common to other outgoing transitions.
// Therefore if we make a cycle to this state we
// will eventually see that acceptance set thanks
// to the "pulling" of the common acceptance sets
// of the destination state (cf. "odest").
//
// 2) It's also desirable because it makes the
// degeneralization idempotent (up to a renaming of
// states). Consider the following automaton where
// 1 is initial and => marks accepting transitions:
// 1=>1, 1=>2, 2->2, 2->1 This is already an SBA,
// with 1 as accepting state. However if you try
// degeralize it without ignoring *prev, we'll get
// two copies of states 2, depending on whether we
// reach it using 1=>2 or from 2->2. If this
// example was not clear, uncomment this following
// "if" block, and play with the "degenid.test"
// test case.
//
// 3) Ignoring all common acceptance sets would also
// be correct, but it would make the
// degeneralization produce larger automata in some
// cases. The current condition to ignore only one
// acceptance set if is this not used by the next
// state is a heuristic that is compatible with
// point 2) above while not causing more states to
// be generated in our benchmark of 188 formulae
// from the literature.
if (expected != cycle.begin())
{
iterator prev = expected;
--prev;
bdd common = aut->
common_acceptance_conditions_of_original_state(rs);
if (bdd_implies(*prev, common))
{
bdd u = aut->
union_acceptance_conditions_of_original_state(odest);
if (!bdd_implies(*prev, u))
acc -= *prev;
}
}
// Use the acceptance sets common to all outgoing
// transition of the destination state. In case of a
// self-loop, we will be adding back the acceptance
// set we removed. This is what we want.
acc |= otheracc;
} }
else else
{ {
// A transition in the *EXPECTED acceptance set should // The transition is accepting.
// be directed to the next acceptance set. If the accepting = true;
// current transition is also in the next acceptance // Skip as much acceptance conditions as we can on our cycle.
// set, then go to the one after, etc. next = cycle.begin();
// while (next != expected && bdd_implies(*next, acc))
// See Denis Oddoux's PhD thesis for a nice
// explanation (in French).
// @PhDThesis{ oddoux.03.phd,
// author = {Denis Oddoux},
// title = {Utilisation des automates alternants pour un
// model-checking efficace des logiques
// temporelles lin{\'e}aires.},
// school = {Universit{\'e}e Paris 7},
// year = {2003},
// address= {Paris, France},
// month = {December}
// }
next = expected;
// Consider both the current acceptance sets, and the
// acceptance sets common to the outgoing transition of
// the destination state.
acc |= otheracc;
while (next != cycle.end() && bdd_implies(*next, acc))
++next; ++next;
if (next != cycle.end())
{
accepting = false;
goto next_is_set;
}
} }
// The transition is accepting.
accepting = true;
// Skip as much acceptance conditions as we can on our cycle.
next = cycle.begin();
while (next != expected && bdd_implies(*next, acc))
++next;
next_is_set:
state_tba_proxy* dest = state_tba_proxy* dest =
down_cast<state_tba_proxy*>(aut->create_state(odest, next)); down_cast<state_tba_proxy*>(aut->create_state(odest, next));
// Is DEST already reachable with the same value of ACCEPTING? // Is DEST already reachable with the same value of ACCEPTING?
...@@ -508,12 +439,12 @@ namespace spot ...@@ -508,12 +439,12 @@ namespace spot
{ {
tgba_tba_proxy_succ_iterator* res = tgba_tba_proxy_succ_iterator* res =
down_cast<tgba_tba_proxy_succ_iterator*>(iter_cache_); down_cast<tgba_tba_proxy_succ_iterator*>(iter_cache_);
res->recycle(rs, a_->succ(rs), res->recycle(a_->succ(rs),
s->acceptance_iterator(), acc_cycle_, this); s->acceptance_iterator(), acc_cycle_, this);
iter_cache_ = nullptr; iter_cache_ = nullptr;
return res; return res;
} }
return new tgba_tba_proxy_succ_iterator(rs, a_->succ(rs), return new tgba_tba_proxy_succ_iterator(a_->succ(rs),
s->acceptance_iterator(), s->acceptance_iterator(),
acc_cycle_, the_acceptance_cond_, acc_cycle_, the_acceptance_cond_,
this); this);
...@@ -608,64 +539,4 @@ namespace spot ...@@ -608,64 +539,4 @@ namespace spot
return a_->support_conditions(s->real_state()); return a_->support_conditions(s->real_state());
} }
////////////////////////////////////////////////////////////////////////
// tgba_sba_proxy
tgba_sba_proxy::tgba_sba_proxy(const tgba* a)
: tgba_tba_proxy(a)
{
if (a->number_of_acceptance_conditions() > 0)
{
cycle_start_ = acc_cycle_.insert(acc_cycle_.end(), bddtrue);
bdd all = a->all_acceptance_conditions();
state* init = a->get_init_state();
for (auto it: a->succ(init))
{
// Look only for transitions that are accepting.
if (all != it->current_acceptance_conditions())
continue;
// Look only for self-loops.
state* dest = it->current_state();
if (dest->compare(init) == 0)
{
// The initial state has an accepting self-loop.
// In that case it is better to start the accepting
// cycle on a "acceptance" state. This will avoid
// duplication of the initial state.
// The cycle_start_ points to the right starting
// point already, so just return.
dest->destroy();
init->destroy();
return;
}
dest->destroy();
}
init->destroy();
}
// If we arrive here either because the number of acceptance
// condition is 0, or because the initial state has no accepting
// self-loop, start the acceptance cycle on the first condition
// (that is a non-accepting state if the number of conditions is
// not 0).
cycle_start_ = acc_cycle_.begin();
}
state*
tgba_sba_proxy::get_init_state() const
{
return create_state(a_->get_init_state(), cycle_start_);
}
bool
tgba_sba_proxy::state_is_accepting(const state* state) const
{
const state_tba_proxy* s =
down_cast<const state_tba_proxy*>(state);
assert(s);
return bddtrue == s->acceptance_cond();
}
} }
...@@ -47,8 +47,6 @@ namespace spot ...@@ -47,8 +47,6 @@ namespace spot
/// If the input automaton uses N acceptance conditions, the output /// If the input automaton uses N acceptance conditions, the output
/// automaton can have at most max(N,1) times more states and /// automaton can have at most max(N,1) times more states and
/// transitions. /// transitions.
///
/// \see tgba_sba_proxy
class SPOT_API tgba_tba_proxy : public tgba class SPOT_API tgba_tba_proxy : public tgba
{ {
public: public:
...@@ -120,47 +118,5 @@ namespace spot ...@@ -120,47 +118,5 @@ namespace spot
tgba_tba_proxy& operator=(const tgba_tba_proxy&) SPOT_DELETED; tgba_tba_proxy& operator=(const tgba_tba_proxy&) SPOT_DELETED;
}; };
/// \ingroup tgba_on_the_fly_algorithms
/// \brief Degeneralize a spot::tgba on the fly, producing an SBA.
///
/// This class acts as a proxy in front of a spot::tgba, that should
/// be degeneralized on the fly.
///
/// This is similar to tgba_tba_proxy, except that automata produced
/// with this algorithms can also been seen as State-based Büchi
/// Automata (SBA). See tgba_sba_proxy::state_is_accepting(). (An
/// SBA is a TBA, and a TBA is a TGBA.)
///
/// This extra property has a small cost in size: if the input
/// automaton uses N acceptance conditions, the output automaton can
/// have at most max(N,1)+1 times more states and transitions.
/// (This is only max(N,1) for tgba_tba_proxy.)
///
/// If you want to degeneralize an automaton once for all, and not
/// on-the-fly, consider using degeneralize() instead because it is
/// usually faster. Also the degeneralize() function implements
/// several SCC-based optimizations that are not implemented in this
/// one.
///
/// \see degeneralize
class SPOT_API tgba_sba_proxy : public tgba_tba_proxy
{
public:
tgba_sba_proxy(const tgba* a);
/// \brief Whether the state is accepting.
///
/// A particularity of a spot::tgba_sba_proxy automaton is that
/// when a state has an outgoing accepting arc, all its outgoing
/// arcs are accepting. The state itself can therefore be
/// considered accepting. This is useful in algorithms working on
/// degeneralized automata with state acceptance conditions.
bool state_is_accepting(const state* state) const;
virtual state* get_init_state() const;
protected:
cycle_list::iterator cycle_start_;
};
} }
#endif // SPOT_TGBA_TGBATBA_HH #endif // SPOT_TGBA_TGBATBA_HH
...@@ -31,9 +31,6 @@ namespace spot ...@@ -31,9 +31,6 @@ namespace spot
/// This algorithms will build a new explicit automaton that has /// This algorithms will build a new explicit automaton that has
/// at most (N+1) times the number of states of the original automaton. /// at most (N+1) times the number of states of the original automaton.
/// ///
/// If you want to build a degeneralized automaton on-the-fly, see
/// spot::tgba_sba_proxy or spot::tgba_tba_proxy.
///
/// When \a use_z_lvl is set, the level of the degeneralized /// When \a use_z_lvl is set, the level of the degeneralized
/// automaton is reset everytime an accepting SCC is exited. If \a /// automaton is reset everytime an accepting SCC is exited. If \a
/// use_cust_acc_orders is set, the degeneralization will compute a /// use_cust_acc_orders is set, the degeneralization will compute a
...@@ -48,7 +45,7 @@ namespace spot ...@@ -48,7 +45,7 @@ namespace spot
/// Any of these three options will cause the SCCs of the automaton /// Any of these three options will cause the SCCs of the automaton
/// \a a to be computed prior to its actual degeneralization. /// \a a to be computed prior to its actual degeneralization.
/// ///
/// \see tgba_sba_proxy, tgba_tba_proxy /// \see tgba_tba_proxy
SPOT_API tgba_digraph* SPOT_API tgba_digraph*
degeneralize(const tgba* a, bool use_z_lvl = true, degeneralize(const tgba* a, bool use_z_lvl = true,
bool use_cust_acc_orders = false, bool use_cust_acc_orders = false,
......
...@@ -31,6 +31,7 @@ ...@@ -31,6 +31,7 @@
#include "ltlast/unop.hh" #include "ltlast/unop.hh"
#include "tgbaalgos/stats.hh" #include "tgbaalgos/stats.hh"
#include "tgbaalgos/emptiness_stats.hh" #include "tgbaalgos/emptiness_stats.hh"
#include "tgbaalgos/degen.hh"
#include "tgba/tgbatba.hh" #include "tgba/tgbatba.hh"
#include "tgba/tgbasafracomplement.hh" #include "tgba/tgbasafracomplement.hh"
...@@ -215,11 +216,10 @@ int main(int argc, char* argv[]) ...@@ -215,11 +216,10 @@ int main(int argc, char* argv[])
<< a->number_of_acceptance_conditions() << a->number_of_acceptance_conditions()
<< std::endl; << std::endl;
spot::tgba *buchi = new spot::tgba_sba_proxy(a); auto buchi = spot::degeneralize(a);
a_size = spot::stats_reachable(buchi);
std::cout << "Buchi: " std::cout << "Buchi: "
<< a_size.states << ", " << buchi->num_states()
<< a_size.transitions << ", " << buchi->num_transitions()
<< buchi->number_of_acceptance_conditions() << buchi->number_of_acceptance_conditions()
<< std::endl; << std::endl;
delete buchi; delete buchi;
......
...@@ -1660,7 +1660,7 @@ main(int argc, char** argv) ...@@ -1660,7 +1660,7 @@ main(int argc, char** argv)
case 8: case 8:
{ {
assert(degeneralize_opt == DegenSBA); assert(degeneralize_opt == DegenSBA);
if (assume_sba || dynamic_cast<const spot::tgba_sba_proxy*>(a)) if (assume_sba)
spot::never_claim_reachable(std::cout, a, f, spin_comments); spot::never_claim_reachable(std::cout, a, f, spin_comments);
else else
{ {
......
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