alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

tgba_explicit: fix support for aliases

Browse source 
This had been broken in the 0.9 reorganization of the tgba_explicit
hierarchy.  The output of 'spin -f' was incorrectly parsed as a
consequence.

* src/tgba/tgbaexplicit.hh: Introduce an alias_ map and use it.
This commit is contained in:
Alexandre Duret-Lutz 2012-09-30 22:19:48 +02:00
parent 0fed46b796
commit dd4d03e3a9
1 changed files with 16 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

40
src/tgba/tgbaexplicit.hh
View file

@ -250,7 +250,7 @@ namespace spot
bdd all_acceptance_conditions_; bdd all_acceptance_conditions_;
}; };
/// Graph implementation for explicit automgon /// Graph implementation for explicit automaton
/// \ingroup tgba_representation /// \ingroup tgba_representation
template<typename State, typename Type> template<typename State, typename Type>
class explicit_graph: public Type class explicit_graph: public Type
@ -263,6 +263,7 @@ namespace spot
typedef State state; typedef State state;
protected: protected:
typedef Sgi::hash_map<label_t, State, label_hash_t> ls_map; typedef Sgi::hash_map<label_t, State, label_hash_t> ls_map;
typedef Sgi::hash_map<label_t, State*> alias_map;
typedef Sgi::hash_map<const State*, label_t, ptr_hash<State> > sl_map; typedef Sgi::hash_map<const State*, label_t, ptr_hash<State> > sl_map;
public: public:
@ -285,7 +286,6 @@ namespace spot
size_t num_states() const size_t num_states() const
{ {
// Do not use ls_.size() because it may contain aliases.
return sl_.size(); return sl_.size();
} }
@ -358,16 +358,6 @@ namespace spot
return get_label(se); return get_label(se);
} }
transition*
create_trainsition(const label_t& source, const label_t& 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 create_transition(s, add_state(dest));
}
void void
complement_all_acceptance_conditions() complement_all_acceptance_conditions()
{ {
@ -419,16 +409,19 @@ namespace spot
typename ls_map::iterator i = ls_.find(name); typename ls_map::iterator i = ls_.find(name);
if (i == ls_.end()) if (i == ls_.end())
{ {
State s(name); typename alias_map::iterator j = alias_.find(name);
ls_[name] = s; if (j != alias_.end())
sl_[&ls_[name]] = name; return j->second;
// The first state we add is the inititial state. State s(name);
State* res =
&(ls_.insert(std::make_pair(name, State(name))).first->second);
sl_[res] = name;
// The first state we add is the initial state.
// It can also be overridden with set_init_state(). // It can also be overridden with set_init_state().
if (!init_) if (!init_)
init_ = &ls_[name]; init_ = res;
return res;
return &(ls_[name]);
} }
return &(i->second); return &(i->second);
} }
@ -449,11 +442,7 @@ namespace spot
while (i != ls_.end()) while (i != ls_.end())
{ {
label_t s = i->first; label_t s = i->first;
// Do not erase the same state twice(Because of possible aliases).
if (sl_.erase(&(i->second)))
i->second.destroy(); i->second.destroy();
++i; ++i;
destroy_key<label_t> dest; destroy_key<label_t> dest;
dest.destroy(s); dest.destroy(s);
@ -518,7 +507,7 @@ namespace spot
/// will act as a reference to \a real_name. /// will act as a reference to \a real_name.
void add_state_alias(const label_t& alias, const label_t& real) void add_state_alias(const label_t& alias, const label_t& real)
{ {
ls_[alias] = *(add_state(real)); alias_[alias] = add_state(real);
} }
@ -536,7 +525,7 @@ namespace spot
} }
/// Acceptance conditions handlingx /// Acceptance conditions handling
void set_acceptance_conditions(bdd acc) void set_acceptance_conditions(bdd acc)
{ {
assert(neg_acceptance_conditions_ == bddtrue); assert(neg_acceptance_conditions_ == bddtrue);
@ -653,6 +642,7 @@ namespace spot
} }
ls_map ls_; ls_map ls_;
alias_map alias_;
sl_map sl_; sl_map sl_;
State* init_; State* init_;