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

Introduce tgba_explicit_labelled<label> so that we can build

tgba_explicit instances labelled by other objects than strings.

* src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh:
Split tgba_explicit in two levels: tgba_explicit with unlabelled
states, and tgba_explicit_labelled templated by the type of
the label.  Define tgba_explicit_string (with the interface
of the former tgba_explicit class) and tgba_explicit_formula
for future use in ltl2tgba.cc.
* src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh,
src/tgbaalgos/cutscc.cc, src/tgbaalgos/dupexp.cc,
src/tgbaalgos/emptiness.cc, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/powerset.cc, src/tgbaalgos/randomgraph.cc,
src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy,
src/tgbatest/explicit.cc, src/tgbatest/ltl2tgba.cc: Adjust to
use tgba_explicit_string when appropriate.
parent d3dcecc6
2009-11-10 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Introduce tgba_explicit_labelled<label> so that we can build
tgba_explicit instances labelled by other objects than strings.
* src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh:
Split tgba_explicit in two levels: tgba_explicit with unlabelled
states, and tgba_explicit_labelled templated by the type of
the label. Define tgba_explicit_string (with the interface
of the former tgba_explicit class) and tgba_explicit_formula
for future use in ltl2tgba.cc.
* src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh,
src/tgbaalgos/cutscc.cc, src/tgbaalgos/dupexp.cc,
src/tgbaalgos/emptiness.cc, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/powerset.cc, src/tgbaalgos/randomgraph.cc,
src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy,
src/tgbatest/explicit.cc, src/tgbatest/ltl2tgba.cc: Adjust to
use tgba_explicit_string when appropriate.
2009-11-09 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2009-11-09 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Do not use the Boost macro from the Autoconf macro archive. Do not use the Boost macro from the Autoconf macro archive.
......
...@@ -25,6 +25,7 @@ ...@@ -25,6 +25,7 @@
#include "tgba/formula2bdd.hh" #include "tgba/formula2bdd.hh"
#include "misc/bddop.hh" #include "misc/bddop.hh"
#include <cassert> #include <cassert>
#include "ltlvisit/tostring.hh"
namespace spot namespace spot
{ {
...@@ -121,45 +122,9 @@ namespace spot ...@@ -121,45 +122,9 @@ namespace spot
tgba_explicit::~tgba_explicit() tgba_explicit::~tgba_explicit()
{ {
ns_map::iterator i;
for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
{
tgba_explicit::state::iterator i2;
for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
delete *i2;
delete i->second;
}
dict_->unregister_all_my_variables(this); dict_->unregister_all_my_variables(this);
} }
tgba_explicit::state*
tgba_explicit::add_state(const std::string& name)
{
ns_map::iterator i = name_state_map_.find(name);
if (i == name_state_map_.end())
{
tgba_explicit::state* s = new tgba_explicit::state;
name_state_map_[name] = s;
state_name_map_[s] = name;
// The first state we add is the inititial state.
// It can also be overridden with set_init_state().
if (!init_)
init_ = s;
return s;
}
return i->second;
}
tgba_explicit::state*
tgba_explicit::set_init_state(const std::string& state)
{
tgba_explicit::state* s = add_state(state);
init_ = s;
return s;
}
tgba_explicit::transition* tgba_explicit::transition*
tgba_explicit::create_transition(state* source, const state* dest) tgba_explicit::create_transition(state* source, const state* dest)
{ {
...@@ -170,18 +135,6 @@ namespace spot ...@@ -170,18 +135,6 @@ namespace spot
source->push_back(t); source->push_back(t);
return t; return t;
} }
tgba_explicit::transition*
tgba_explicit::create_transition(const std::string& source,
const std::string& dest)
{
// It's important that the source be created before the
// destination, so the first encountered source becomes the
// default initial state.
state* s = add_state(source);
return create_transition(s, add_state(dest));
}
void void
tgba_explicit::add_condition(transition* t, const ltl::formula* f) tgba_explicit::add_condition(transition* t, const ltl::formula* f)
{ {
...@@ -196,26 +149,6 @@ namespace spot ...@@ -196,26 +149,6 @@ namespace spot
t->condition &= f; t->condition &= f;
} }
void
tgba_explicit::declare_acceptance_condition(const ltl::formula* f)
{
int v = dict_->register_acceptance_variable(f, this);
f->destroy();
bdd neg = bdd_nithvar(v);
neg_acceptance_conditions_ &= neg;
// Append neg to all acceptance conditions.
ns_map::iterator i;
for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
{
tgba_explicit::state::iterator i2;
for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
(*i2)->acceptance_conditions &= neg;
}
all_acceptance_conditions_computed_ = false;
}
void void
tgba_explicit::copy_acceptance_conditions_of(const tgba *a) tgba_explicit::copy_acceptance_conditions_of(const tgba *a)
{ {
...@@ -226,52 +159,6 @@ namespace spot ...@@ -226,52 +159,6 @@ namespace spot
neg_acceptance_conditions_ = f; neg_acceptance_conditions_ = f;
} }
void
tgba_explicit::complement_all_acceptance_conditions()
{
bdd all = all_acceptance_conditions();
ns_map::iterator i;
for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
{
tgba_explicit::state::iterator i2;
for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
{
(*i2)->acceptance_conditions = all - (*i2)->acceptance_conditions;
}
}
}
void
tgba_explicit::merge_transitions()
{
ns_map::iterator i;
for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
{
state::iterator t1;
for (t1 = i->second->begin(); t1 != i->second->end(); ++t1)
{
bdd acc = (*t1)->acceptance_conditions;
const state* dest = (*t1)->dest;
// Find another transition with the same destination and
// acceptance conditions.
state::iterator t2 = t1;
++t2;
while (t2 != i->second->end())
{
state::iterator t2copy = t2++;
if ((*t2copy)->acceptance_conditions == acc
&& (*t2copy)->dest == dest)
{
(*t1)->condition |= (*t2copy)->condition;
delete *t2copy;
i->second->erase(t2copy);
}
}
}
}
}
bool bool
tgba_explicit::has_acceptance_condition(const ltl::formula* f) const tgba_explicit::has_acceptance_condition(const ltl::formula* f) const
{ {
...@@ -317,7 +204,7 @@ namespace spot ...@@ -317,7 +204,7 @@ namespace spot
{ {
// Fix empty automata by adding a lone initial state. // Fix empty automata by adding a lone initial state.
if (!init_) if (!init_)
const_cast<tgba_explicit*>(this)->add_state("empty"); const_cast<tgba_explicit*>(this)->add_default_init();
return new state_explicit(init_); return new state_explicit(init_);
} }
...@@ -368,16 +255,6 @@ namespace spot ...@@ -368,16 +255,6 @@ namespace spot
return dict_; return dict_;
} }
std::string
tgba_explicit::format_state(const spot::state* s) const
{
const state_explicit* se = dynamic_cast<const state_explicit*>(s);
assert(se);
sn_map::const_iterator i = state_name_map_.find(se->get_state());
assert(i != state_name_map_.end());
return i->second;
}
bdd bdd
tgba_explicit::all_acceptance_conditions() const tgba_explicit::all_acceptance_conditions() const
{ {
...@@ -396,4 +273,42 @@ namespace spot ...@@ -396,4 +273,42 @@ namespace spot
return neg_acceptance_conditions_; return neg_acceptance_conditions_;
} }
tgba_explicit::state*
tgba_explicit_string::add_default_init()
{
return add_state("empty");
}
std::string
tgba_explicit_string::format_state(const spot::state* s) const
{
const state_explicit* se = dynamic_cast<const state_explicit*>(s);
assert(se);
sn_map::const_iterator i = state_name_map_.find(se->get_state());
assert(i != state_name_map_.end());
return i->second;
}
tgba_explicit_formula::~tgba_explicit_formula()
{
ns_map::iterator i;
for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
i->first->destroy();
}
tgba_explicit::state* tgba_explicit_formula::add_default_init()
{
return add_state(ltl::constant::true_instance());
}
std::string
tgba_explicit_formula::format_state(const spot::state* s) const
{
const state_explicit* se = dynamic_cast<const state_explicit*>(s);
assert(se);
sn_map::const_iterator i = state_name_map_.find(se->get_state());
assert(i != state_name_map_.end());
return ltl::to_string(i->second);
}
} }
// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004, 2006, 2009 Laboratoire d'Informatique de
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// et Marie Curie. // Université Pierre et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
...@@ -26,12 +26,14 @@ ...@@ -26,12 +26,14 @@
#include <list> #include <list>
#include "tgba.hh" #include "tgba.hh"
#include "ltlast/formula.hh" #include "ltlast/formula.hh"
#include <cassert>
namespace spot namespace spot
{ {
// Forward declarations. See below. // Forward declarations. See below.
class state_explicit; class state_explicit;
class tgba_explicit_succ_iterator; class tgba_explicit_succ_iterator;
class tgba_explicit;
/// Explicit representation of a spot::tgba. /// Explicit representation of a spot::tgba.
/// \ingroup tgba_representation /// \ingroup tgba_representation
...@@ -51,17 +53,15 @@ namespace spot ...@@ -51,17 +53,15 @@ namespace spot
const state* dest; const state* dest;
}; };
state* set_init_state(const std::string& state); /// Add a default initial state.
virtual state* add_default_init() = 0;
transition*
create_transition(const std::string& source, const std::string& dest);
transition* transition*
create_transition(state* source, const state* dest); create_transition(state* source, const state* dest);
void add_condition(transition* t, const ltl::formula* f); void add_condition(transition* t, const ltl::formula* f);
/// This assumes that all variables in \a f are known from dict. /// This assumes that all variables in \a f are known from dict.
void add_conditions(transition* t, bdd f); void add_conditions(transition* t, bdd f);
void declare_acceptance_condition(const ltl::formula* f);
/// \brief Copy the acceptance conditions of a tgba. /// \brief Copy the acceptance conditions of a tgba.
/// ///
...@@ -73,12 +73,6 @@ namespace spot ...@@ -73,12 +73,6 @@ namespace spot
void add_acceptance_condition(transition* t, const ltl::formula* f); void add_acceptance_condition(transition* t, const ltl::formula* f);
/// This assumes that all acceptance conditions in \a f are known from dict. /// This assumes that all acceptance conditions in \a f are known from dict.
void add_acceptance_conditions(transition* t, bdd f); void add_acceptance_conditions(transition* t, bdd f);
void complement_all_acceptance_conditions();
void merge_transitions();
/// Return the tgba_explicit::state for \a name, creating the state if
/// it does not exist.
state* add_state(const std::string& name);
// tgba interface // tgba interface
virtual ~tgba_explicit(); virtual ~tgba_explicit();
...@@ -88,23 +82,18 @@ namespace spot ...@@ -88,23 +82,18 @@ namespace spot
const spot::state* global_state = 0, const spot::state* global_state = 0,
const tgba* global_automaton = 0) const; const tgba* global_automaton = 0) const;
virtual bdd_dict* get_dict() const; virtual bdd_dict* get_dict() const;
virtual std::string format_state(const spot::state* state) const;
virtual bdd all_acceptance_conditions() const; virtual bdd all_acceptance_conditions() const;
virtual bdd neg_acceptance_conditions() const; virtual bdd neg_acceptance_conditions() const;
virtual std::string format_state(const spot::state* s) const = 0;
protected: protected:
virtual bdd compute_support_conditions(const spot::state* state) const; virtual bdd compute_support_conditions(const spot::state* state) const;
virtual bdd compute_support_variables(const spot::state* state) const; virtual bdd compute_support_variables(const spot::state* state) const;
bdd get_acceptance_condition(const ltl::formula* f); bdd get_acceptance_condition(const ltl::formula* f);
typedef Sgi::hash_map<const std::string, tgba_explicit::state*,
string_hash> ns_map;
typedef Sgi::hash_map<const tgba_explicit::state*, std::string,
ptr_hash<tgba_explicit::state> > sn_map;
ns_map name_state_map_;
sn_map state_name_map_;
bdd_dict* dict_; bdd_dict* dict_;
tgba_explicit::state* init_; tgba_explicit::state* init_;
mutable bdd all_acceptance_conditions_; mutable bdd all_acceptance_conditions_;
...@@ -118,6 +107,7 @@ namespace spot ...@@ -118,6 +107,7 @@ namespace spot
}; };
/// States used by spot::tgba_explicit. /// States used by spot::tgba_explicit.
/// \ingroup tgba_representation /// \ingroup tgba_representation
class state_explicit : public spot::state class state_explicit : public spot::state
...@@ -168,6 +158,177 @@ namespace spot ...@@ -168,6 +158,177 @@ namespace spot
bdd all_acceptance_conditions_; bdd all_acceptance_conditions_;
}; };
/// A tgba_explicit instance with states labeled by a given type.
template<typename label, typename label_hash>
class tgba_explicit_labelled: public tgba_explicit
{
protected:
typedef label label_t;
typedef Sgi::hash_map<label, tgba_explicit::state*,
label_hash> ns_map;
typedef Sgi::hash_map<const tgba_explicit::state*, label,
ptr_hash<tgba_explicit::state> > sn_map;
ns_map name_state_map_;
sn_map state_name_map_;
public:
tgba_explicit_labelled(bdd_dict* dict) : tgba_explicit(dict) {};
bool has_state(const label& name)
{
return name_state_map_.find(name) != name_state_map_.end();
}
/// Return the tgba_explicit::state for \a name, creating the state if
/// it does not exist.
state* add_state(const label& name)
{
typename ns_map::iterator i = name_state_map_.find(name);
if (i == name_state_map_.end())
{
tgba_explicit::state* s = new tgba_explicit::state;
name_state_map_[name] = s;
state_name_map_[s] = name;
// The first state we add is the inititial state.
// It can also be overridden with set_init_state().
if (!init_)
init_ = s;
return s;
}
return i->second;
}
state*
set_init_state(const label& state)
{
tgba_explicit::state* s = add_state(state);
init_ = s;
return s;
}
transition*
create_transition(state* source, const state* dest)
{
return tgba_explicit::create_transition(source, dest);
}
transition*
create_transition(const label& source, const label& dest)
{
// It's important that the source be created before the
// destination, so the first source encountered becomes the
// default initial state.
state* s = add_state(source);
return tgba_explicit::create_transition(s, add_state(dest));
}
void
complement_all_acceptance_conditions()
{
bdd all = all_acceptance_conditions();
typename ns_map::iterator i;
for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
{
tgba_explicit::state::iterator i2;
for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
{
(*i2)->acceptance_conditions = all - (*i2)->acceptance_conditions;
}
}
}
void
declare_acceptance_condition(const ltl::formula* f)
{
int v = dict_->register_acceptance_variable(f, this);
f->destroy();
bdd neg = bdd_nithvar(v);
neg_acceptance_conditions_ &= neg;
// Append neg to all acceptance conditions.
typename ns_map::iterator i;
for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
{
tgba_explicit::state::iterator i2;
for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
(*i2)->acceptance_conditions &= neg;
}
all_acceptance_conditions_computed_ = false;
}
void
merge_transitions()
{
typename ns_map::iterator i;
for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
{
state::iterator t1;
for (t1 = i->second->begin(); t1 != i->second->end(); ++t1)
{
bdd acc = (*t1)->acceptance_conditions;
const state* dest = (*t1)->dest;
// Find another transition with the same destination and
// acceptance conditions.
state::iterator t2 = t1;
++t2;
while (t2 != i->second->end())
{
state::iterator t2copy = t2++;
if ((*t2copy)->acceptance_conditions == acc
&& (*t2copy)->dest == dest)
{
(*t1)->condition |= (*t2copy)->condition;
delete *t2copy;
i->second->erase(t2copy);
}
}
}
}
}
virtual
~tgba_explicit_labelled()
{
typename ns_map::iterator i;
for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
{
tgba_explicit::state::iterator i2;
for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
delete *i2;
delete i->second;
}
}
};
class tgba_explicit_string:
public tgba_explicit_labelled<std::string, string_hash>
{
public:
tgba_explicit_string(bdd_dict* dict):
tgba_explicit_labelled<std::string, string_hash>(dict)
{};
virtual state* add_default_init();
virtual std::string format_state(const spot::state* s) const;
};
class tgba_explicit_formula:
public tgba_explicit_labelled<const ltl::formula*, ltl::formula_ptr_hash>
{
public:
tgba_explicit_formula(bdd_dict* dict):
tgba_explicit_labelled<const ltl::formula*, ltl::formula_ptr_hash>(dict)
{};
virtual ~tgba_explicit_formula();
virtual state* add_default_init();
virtual std::string format_state(const spot::state* s) const;
};
} }
#endif // SPOT_TGBA_TGBAEXPLICIT_HH #endif // SPOT_TGBA_TGBAEXPLICIT_HH
// Copyright (C) 2004, 2005, 2008 Laboratoire d'Informatique de Paris // Copyright (C) 2004, 2005, 2008, 2009 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie. // Université Pierre et Marie Curie.
// //
...@@ -31,7 +31,7 @@ namespace spot ...@@ -31,7 +31,7 @@ namespace spot
tgba_reduc::tgba_reduc(const tgba* a, tgba_reduc::tgba_reduc(const tgba* a,
const numbered_state_heap_factory* nshf) const numbered_state_heap_factory* nshf)
: tgba_explicit(a->get_dict()), : tgba_explicit_string(a->get_dict()),
tgba_reachable_iterator_breadth_first(a), tgba_reachable_iterator_breadth_first(a),
h_(nshf->build()) h_(nshf->build())
{ {
...@@ -203,10 +203,8 @@ namespace spot ...@@ -203,10 +203,8 @@ namespace spot
const std::string ss = automata_->format_state(source); const std::string ss = automata_->format_state(source);
const std::string sd = automata_->format_state(dest);