Commit 7c20d8ae authored by Damien Lefortier's avatar Damien Lefortier
Browse files

Introduce taa_tgba_labelled<label> so that we can build

taa_tgba instances labelled by other objects than strings
in the same way Alexandre did for tgba_explicit.

* src/tgba/taatgba.cc, src/tgba/taatgba.hh: Split taa_tgba in two
levels: taa_tgba with no label and taa_tgba_labelled templated by
the type of the label.  Define taa_tgba_string (with the interface
of the former taa_tgba class) and taa_tgba_formula for future use
in ltl2taa.cc.
* src/tgbaalgos/ltl2taa.cc, src/tgbatest/taatgba.cc: Adjust to use
taa_tgba_string.
parent 88df8c0a
2010-01-16 Damien Lefortier <dam@lrde.epita.fr>
Introduce taa_tgba_labelled<label> so that we can build
taa_tgba instances labelled by other objects than strings
in the same way Alexandre did for tgba_explicit.
* src/tgba/taatgba.cc, src/tgba/taatgba.hh: Split taa_tgba in two
levels: taa_tgba with no label and taa_tgba_labelled templated by
the type of the label. Define taa_tgba_string (with the interface
of the former taa_tgba class) and taa_tgba_formula for future use
in ltl2taa.cc.
* src/tgbaalgos/ltl2taa.cc, src/tgbatest/taatgba.cc: Adjust to use
taa_tgba_string.
2010-01-06 Damien Lefortier <dam@lrde.epita.fr>
Fix a longstanding bug reported by Guillaume Sadegh.
......
......@@ -24,6 +24,7 @@
#include <iterator>
#include <iostream>
#include "tgba/formula2bdd.hh"
#include "ltlvisit/tostring.hh"
#include "misc/bddop.hh"
#include "taatgba.hh"
......@@ -34,7 +35,7 @@ namespace spot
`--------*/
taa_tgba::taa_tgba(bdd_dict* dict)
: name_state_map_(), state_name_map_(), dict_(dict),
: dict_(dict),
all_acceptance_conditions_(bddfalse),
all_acceptance_conditions_computed_(false),
neg_acceptance_conditions_(bddtrue),
......@@ -44,56 +45,12 @@ namespace spot
taa_tgba::~taa_tgba()
{
ns_map::iterator i;
for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
{
taa_tgba::state::iterator i2;
for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
delete *i2;
delete i->second;
}
ss_vec::iterator j;
for (j = state_set_vec_.begin(); j != state_set_vec_.end(); ++j)
delete *j;
dict_->unregister_all_my_variables(this);
}
void
taa_tgba::set_init_state(const std::string& s)
{
std::vector<std::string> v(1);
v[0] = s;
set_init_state(v);
}
void
taa_tgba::set_init_state(const std::vector<std::string>& s)
{
init_ = add_state_set(s);
}
taa_tgba::transition*
taa_tgba::create_transition(const std::string& s,
const std::vector<std::string>& d)
{
state* src = add_state(s);
state_set* dst = add_state_set(d);
transition* t = new transition;
t->dst = dst;
t->condition = bddtrue;
t->acceptance_conditions = bddfalse;
src->push_back(t);
return t;
}
taa_tgba::transition*
taa_tgba::create_transition(const std::string& s, const std::string& d)
{
std::vector<std::string> vec;
vec.push_back(d);
return create_transition(s, vec);
}
void
taa_tgba::add_condition(transition* t, const ltl::formula* f)
{
......@@ -101,51 +58,6 @@ namespace spot
f->destroy();
}
void
taa_tgba::add_acceptance_condition(transition* t, const ltl::formula* f)
{
if (dict_->acc_map.find(f) == dict_->acc_map.end())
{
int v = dict_->register_acceptance_variable(f, this);
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)
{
taa_tgba::state::iterator i2;
for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
(*i2)->acceptance_conditions &= neg;
}
all_acceptance_conditions_computed_ = false;
}
bdd_dict::fv_map::iterator i = dict_->acc_map.find(f);
assert(i != dict_->acc_map.end());
f->destroy();
bdd v = bdd_ithvar(i->second);
t->acceptance_conditions |= v & bdd_exist(neg_acceptance_conditions_, v);
}
void
taa_tgba::output(std::ostream& os) const
{
ns_map::const_iterator i;
for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
{
taa_tgba::state::const_iterator i2;
os << "State: " << i->first << std::endl;
for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
{
os << " " << format_state_set((*i2)->dst)
<< ", C:" << (*i2)->condition
<< ", A:" << (*i2)->acceptance_conditions << std::endl;
}
}
}
state*
taa_tgba::get_init_state() const
{
......@@ -171,15 +83,6 @@ namespace spot
return dict_;
}
std::string
taa_tgba::format_state(const spot::state* s) const
{
const spot::state_set* se = dynamic_cast<const spot::state_set*>(s);
assert(se);
const state_set* ss = se->get_state();
return format_state_set(ss);
}
bdd
taa_tgba::all_acceptance_conditions() const
{
......@@ -230,58 +133,6 @@ namespace spot
return res;
}
taa_tgba::state*
taa_tgba::add_state(const std::string& name)
{
ns_map::iterator i = name_state_map_.find(name);
if (i == name_state_map_.end())
{
taa_tgba::state* s = new taa_tgba::state;
name_state_map_[name] = s;
state_name_map_[s] = name;
return s;
}
return i->second;
}
taa_tgba::state_set*
taa_tgba::add_state_set(const std::vector<std::string>& names)
{
state_set* ss = new state_set;
for (unsigned i = 0; i < names.size(); ++i)
ss->insert(add_state(names[i]));
state_set_vec_.push_back(ss);
return ss;
}
std::string
taa_tgba::format_state_set(const taa_tgba::state_set* ss) const
{
state_set::const_iterator i1 = ss->begin();
sn_map::const_iterator i2;
if (ss->empty())
return std::string("{}");
if (ss->size() == 1)
{
i2 = state_name_map_.find(*i1);
assert(i2 != state_name_map_.end());
return "{" + i2->second + "}";
}
else
{
std::string res("{");
while (i1 != ss->end())
{
i2 = state_name_map_.find(*i1++);
assert(i2 != state_name_map_.end());
res += i2->second;
res += ",";
}
res[res.size() - 1] = '}';
return res;
}
}
/*----------.
| state_set |
`----------*/
......@@ -493,4 +344,24 @@ namespace spot
return all_acceptance_conditions_ -
((*i_)->acceptance_conditions & all_acceptance_conditions_);
}
/*----------------.
| taa_tgba_string |
`----------------*/
std::string
taa_tgba_string::label_to_string(const std::string& label) const
{
return label;
}
/*-----------------.
| taa_tgba_formula |
`-----------------*/
std::string
taa_tgba_formula::label_to_string(const ltl::formula* label) const
{
return ltl::to_string(label);
}
}
......@@ -32,7 +32,8 @@
namespace spot
{
/// \brief A Transition-based Alternating Automaton (TAA).
/// \brief A self-loop Transition-based Alternating Automaton (TAA)
/// which is seen as a TGBA (abstract class, see below).
class taa_tgba : public tgba
{
public:
......@@ -50,20 +51,7 @@ namespace spot
const state_set* dst;
};
void set_init_state(const std::string& state);
void set_init_state(const std::vector<std::string>& state);
transition*
create_transition(const std::string& src,
const std::vector<std::string>& dst);
transition*
create_transition(const std::string& src, const std::string& dst);
void add_condition(transition* t, const ltl::formula* f);
void add_acceptance_condition(transition* t, const ltl::formula* f);
/// \brief Output a TAA.
void output(std::ostream& os) const;
/// TGBA interface.
virtual ~taa_tgba();
......@@ -73,17 +61,7 @@ namespace spot
const spot::state* global_state = 0,
const tgba* global_automaton = 0) const;
virtual bdd_dict* get_dict() const;
/// \brief Format the state as a string for printing.
///
/// If state is a spot::state_set of only one element, then the
/// string corresponding to state->get_state() is returned.
///
/// Otherwise a string composed of each string corresponding to
/// each state->get_state() in the spot::state_set is returned,
/// e.g. like {string_1,...,string_n}.
virtual std::string format_state(const spot::state* state) const;
virtual std::string format_state(const spot::state* state) const = 0;
virtual bdd all_acceptance_conditions() const;
virtual bdd neg_acceptance_conditions() const;
......@@ -91,18 +69,8 @@ namespace spot
virtual bdd compute_support_conditions(const spot::state* state) const;
virtual bdd compute_support_variables(const spot::state* state) const;
typedef Sgi::hash_map<
const std::string, taa_tgba::state*, string_hash
> ns_map;
typedef Sgi::hash_map<
const taa_tgba::state*, std::string, ptr_hash<taa_tgba::state>
> sn_map;
typedef std::vector<taa_tgba::state_set*> ss_vec;
ns_map name_state_map_;
sn_map state_name_map_;
bdd_dict* dict_;
mutable bdd all_acceptance_conditions_;
mutable bool all_acceptance_conditions_computed_;
......@@ -114,17 +82,6 @@ namespace spot
// Disallow copy.
taa_tgba(const taa_tgba& other);
taa_tgba& operator=(const taa_tgba& other);
/// \brief Return the taa_tgba::state for \a name, creating it if it
/// does not exist. The first state added is the initial state
/// which can be overridden with set_init_state.
taa_tgba::state* add_state(const std::string& name);
/// \brief Return the taa::state_set for \a names.
taa_tgba::state_set* add_state_set(const std::vector<std::string>& names);
/// \brief Format a taa::state_set as a string for printing.
std::string format_state_set(const taa_tgba::state_set* ss) const;
};
/// Set of states deriving from spot::state.
......@@ -193,6 +150,206 @@ namespace spot
bdd all_acceptance_conditions_;
seen_map seen_;
};
/// A taa_tgba instance with states labeled by a given type.
/// Still an abstract class, see below.
template<typename label, typename label_hash>
class taa_tgba_labelled : public taa_tgba
{
public:
taa_tgba_labelled(bdd_dict* dict) : taa_tgba(dict) {};
virtual ~taa_tgba_labelled()
{
typename ns_map::iterator i;
for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
{
taa_tgba::state::iterator i2;
for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
delete *i2;
delete i->second;
}
}
void set_init_state(const label& s)
{
std::vector<label> v(1);
v[0] = s;
set_init_state(v);
}
void set_init_state(const std::vector<label>& s)
{
init_ = add_state_set(s);
}
transition*
create_transition(const label& s,
const std::vector<label>& d)
{
state* src = add_state(s);
state_set* dst = add_state_set(d);
transition* t = new transition;
t->dst = dst;
t->condition = bddtrue;
t->acceptance_conditions = bddfalse;
src->push_back(t);
return t;
}
transition*
create_transition(const label& s, const label& d)
{
std::vector<std::string> vec;
vec.push_back(d);
return create_transition(s, vec);
}
void add_acceptance_condition(transition* t, const ltl::formula* f)
{
if (dict_->acc_map.find(f) == dict_->acc_map.end())
{
int v = dict_->register_acceptance_variable(f, this);
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)
{
taa_tgba::state::iterator i2;
for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
(*i2)->acceptance_conditions &= neg;
}
all_acceptance_conditions_computed_ = false;
}
bdd_dict::fv_map::iterator i = dict_->acc_map.find(f);
assert(i != dict_->acc_map.end());
f->destroy();
bdd v = bdd_ithvar(i->second);
t->acceptance_conditions |= v & bdd_exist(neg_acceptance_conditions_, v);
}
/// \brief Format the state as a string for printing.
///
/// If state is a spot::state_set of only one element, then the
/// string corresponding to state->get_state() is returned.
///
/// Otherwise a string composed of each string corresponding to
/// each state->get_state() in the spot::state_set is returned,
/// e.g. like {string_1,...,string_n}.
virtual std::string format_state(const spot::state* s) const
{
const spot::state_set* se = dynamic_cast<const spot::state_set*>(s);
assert(se);
const state_set* ss = se->get_state();
return format_state_set(ss);
}
/// \brief Output a TAA in a stream.
void output(std::ostream& os) const
{
typename ns_map::const_iterator i;
for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
{
taa_tgba::state::const_iterator i2;
os << "State: " << label_to_string(i->first) << std::endl;
for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
{
os << " " << format_state_set((*i2)->dst)
<< ", C:" << (*i2)->condition
<< ", A:" << (*i2)->acceptance_conditions << std::endl;
}
}
}
protected:
typedef Sgi::hash_map<
const label, taa_tgba::state*, label_hash
> ns_map;
typedef Sgi::hash_map<
const taa_tgba::state*, label, ptr_hash<taa_tgba::state>
> sn_map;
ns_map name_state_map_;
sn_map state_name_map_;
/// \brief Return a label as a string.
virtual std::string label_to_string(const label lbl) const = 0;
private:
/// \brief Return the taa_tgba::state for \a name, creating it
/// when it does not exist already.
taa_tgba::state* add_state(const label& name)
{
typename ns_map::iterator i = name_state_map_.find(name);
if (i == name_state_map_.end())
{
taa_tgba::state* s = new taa_tgba::state;
name_state_map_[name] = s;
state_name_map_[s] = name;
return s;
}
return i->second;
}
/// \brief Return the taa::state_set for \a names.
taa_tgba::state_set* add_state_set(const std::vector<label>& names)
{
state_set* ss = new state_set;
for (unsigned i = 0; i < names.size(); ++i)
ss->insert(add_state(names[i]));
state_set_vec_.push_back(ss);
return ss;
}
std::string format_state_set(const taa_tgba::state_set* ss) const
{
state_set::const_iterator i1 = ss->begin();
typename sn_map::const_iterator i2;
if (ss->empty())
return std::string("{}");
if (ss->size() == 1)
{
i2 = state_name_map_.find(*i1);
assert(i2 != state_name_map_.end());
return "{" + label_to_string(i2->second) + "}";
}
else
{
std::string res("{");
while (i1 != ss->end())
{
i2 = state_name_map_.find(*i1++);
assert(i2 != state_name_map_.end());
res += label_to_string(i2->second);
res += ",";
}
res[res.size() - 1] = '}';
return res;
}
}
};
class taa_tgba_string :
public taa_tgba_labelled<std::string, string_hash>
{
public:
taa_tgba_string(bdd_dict* dict) :
taa_tgba_labelled<std::string, string_hash>(dict) {};
protected:
std::string label_to_string(const std::string& label) const;
};
class taa_tgba_formula :
public taa_tgba_labelled<const ltl::formula*, ltl::formula_ptr_hash>
{
public:
taa_tgba_formula(bdd_dict* dict):
taa_tgba_labelled<const ltl::formula*, ltl::formula_ptr_hash>(dict) {};
protected:
std::string label_to_string(const ltl::formula* label) const;
};
}
#endif // SPOT_TGBA_TAATGBA_HH
......@@ -39,7 +39,7 @@ namespace spot
class ltl2taa_visitor : public const_visitor
{
public:
ltl2taa_visitor(taa_tgba* res, language_containment_checker* lcc,
ltl2taa_visitor(taa_tgba_string* res, language_containment_checker* lcc,
bool refined = false, bool negated = false)
: res_(res), refined_(refined), negated_(negated),
lcc_(lcc), init_(), succ_(), to_free_()
......@@ -51,7 +51,7 @@ namespace spot
{
}
taa_tgba*
taa_tgba_string*
result()
{
for (unsigned i = 0; i < to_free_.size(); ++i)
......@@ -305,7 +305,7 @@ namespace spot
}
private:
taa_tgba* res_;
taa_tgba_string* res_;
bool refined_;
bool negated_;
language_containment_checker* lcc_;
......@@ -381,7 +381,7 @@ namespace spot
const ltl::formula* f2 = ltl::negative_normal_form(f1);
f1->destroy();
spot::taa_tgba* res = new spot::taa_tgba(dict);
spot::taa_tgba_string* res = new spot::taa_tgba_string(dict);
bdd_dict b;
language_containment_checker* lcc =
new language_containment_checker(&b, false, false, false, false);
......
......@@ -34,7 +34,7 @@ main()
spot::ltl::default_environment& e =
spot::ltl::default_environment::instance();
spot::taa_tgba* a = new spot::taa_tgba(dict);
spot::taa_tgba_string* a = new spot::taa_tgba_string(dict);
typedef spot::taa_tgba::transition trans;
typedef spot::taa_tgba::state state;
......
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