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

* tgbaalgos/reachiter.hh, tgbaalgos/reachiter.cc

(tgba_reachable_iterator::process_link): Take the state* as arguments
in addition to the state numbers.
* src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc
(tgba_explicit::copy_acceptance_conditions_of): New method.
* tgbaalgos/dupexp.cc (dupexp_iter::dupexp_iter): Call
copy_acceptance_conditions_of.
(dupexp_iter::process_state, duplex_iter::declare_state,
dupexp_iter::name_): Remove.
(dupexp_iter::process_link): Adjust prototype, and format
the state here rather than in process_state.
* tgbaalgos/stats.cc, tgbaalgos/dotty.cc: Adjust prototype
of process_link.
parent b6f3faba
2004-11-03 Alexandre Duret-Lutz <adl@src.lip6.fr>
* tgbaalgos/reachiter.hh, tgbaalgos/reachiter.cc
(tgba_reachable_iterator::process_link): Take the state* as arguments
in addition to the state numbers.
* src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc
(tgba_explicit::copy_acceptance_conditions_of): New method.
* tgbaalgos/dupexp.cc (dupexp_iter::dupexp_iter): Call
copy_acceptance_conditions_of.
(dupexp_iter::process_state, duplex_iter::declare_state,
dupexp_iter::name_): Remove.
(dupexp_iter::process_link): Adjust prototype, and format
the state here rather than in process_state.
* tgbaalgos/stats.cc, tgbaalgos/dotty.cc: Adjust prototype
of process_link.
2004-11-02 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-11-02 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/ltlvisit/reduce.hh (is_eventual, is_universal): More doc. * src/ltlvisit/reduce.hh (is_eventual, is_universal): More doc.
......
...@@ -208,6 +208,16 @@ namespace spot ...@@ -208,6 +208,16 @@ namespace spot
all_acceptance_conditions_computed_ = false; all_acceptance_conditions_computed_ = false;
} }
void
tgba_explicit::copy_acceptance_conditions_of(const tgba *a)
{
assert(neg_acceptance_conditions_ == bddtrue);
assert(all_acceptance_conditions_computed_ == false);
bdd f = a->neg_acceptance_conditions();
dict_->register_acceptance_variables(f, this);
neg_acceptance_conditions_ = f;
}
void void
tgba_explicit::complement_all_acceptance_conditions() tgba_explicit::complement_all_acceptance_conditions()
{ {
......
// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
...@@ -59,6 +59,13 @@ namespace spot ...@@ -59,6 +59,13 @@ namespace spot
/// 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); void declare_acceptance_condition(const ltl::formula* f);
/// \brief Copy the acceptance conditions of a tgba.
///
/// If used, this function should be called before creating any
/// transition.
void copy_acceptance_conditions_of(const tgba *a);
bool has_acceptance_condition(const ltl::formula* f) const; bool has_acceptance_condition(const ltl::formula* f) const;
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.
......
...@@ -60,7 +60,8 @@ namespace spot ...@@ -60,7 +60,8 @@ namespace spot
} }
void void
process_link(int in, int out, const tgba_succ_iterator* si) process_link(const state*, int in,
const state*, int out, const tgba_succ_iterator* si)
{ {
os_ << " " << in << " -> " << out << " [label=\""; os_ << " " << in << " -> " << out << " [label=\"";
escape_str(os_, bdd_format_formula(automata_->get_dict(), escape_str(os_, bdd_format_formula(automata_->get_dict(),
......
...@@ -36,6 +36,7 @@ namespace spot ...@@ -36,6 +36,7 @@ namespace spot
dupexp_iter(const tgba* a) dupexp_iter(const tgba* a)
: T(a), out_(new tgba_explicit(a->get_dict())) : T(a), out_(new tgba_explicit(a->get_dict()))
{ {
out_->copy_acceptance_conditions_of(a);
} }
tgba_explicit* tgba_explicit*
...@@ -45,54 +46,23 @@ namespace spot ...@@ -45,54 +46,23 @@ namespace spot
} }
void void
process_state(const state* s, int n, tgba_succ_iterator*) process_link(const state* in_s, int in,
const state* out_s, int out,
const tgba_succ_iterator* si)
{ {
std::ostringstream os; std::ostringstream in_name;
os << "(#" << n << ") " << this->automata_->format_state(s); in_name << "(#" << in << ") " << this->automata_->format_state(in_s);
name_[n] = os.str(); std::ostringstream out_name;
} out_name << "(#" << out << ") " << this->automata_->format_state(out_s);
std::string
declare_state(const state* s, int n)
{
std::string str;
name_map_::const_iterator i = name_.find(n);
if (i == name_.end())
{
std::ostringstream os;
os << "(#" << n << ") " << this->automata_->format_state(s);
name_[n] = str = os.str();
}
else
{
str = i->second;
}
delete s;
return str;
}
void
process_link(int in, int out, const tgba_succ_iterator* si)
{
// We might need to format out before process_state is called.
name_map_::const_iterator i = name_.find(out);
if (i == name_.end())
{
const state* s = si->current_state();
process_state(s, out, 0);
delete s;
}
tgba_explicit::transition* t = tgba_explicit::transition* t =
out_->create_transition(name_[in], name_[out]); out_->create_transition(in_name.str(), out_name.str());
out_->add_conditions(t, si->current_condition()); out_->add_conditions(t, si->current_condition());
out_->add_acceptance_conditions(t, si->current_acceptance_conditions()); out_->add_acceptance_conditions(t, si->current_acceptance_conditions());
} }
private: private:
tgba_explicit* out_; tgba_explicit* out_;
typedef std::map<int, std::string> name_map_;
std::map<int, std::string> name_;
}; };
} // anonymous } // anonymous
......
...@@ -67,11 +67,11 @@ namespace spot ...@@ -67,11 +67,11 @@ namespace spot
{ {
seen[current] = ++n; seen[current] = ++n;
add_state(current); add_state(current);
process_link(tn, n, si); process_link(t, tn, current, n, si);
} }
else else
{ {
process_link(tn, s->second, si); process_link(t, tn, s->first, s->second, si);
delete current; delete current;
} }
} }
...@@ -97,7 +97,9 @@ namespace spot ...@@ -97,7 +97,9 @@ namespace spot
} }
void void
tgba_reachable_iterator::process_link(int, int, const tgba_succ_iterator*) tgba_reachable_iterator::process_link(const state*, int,
const state*, int,
const tgba_succ_iterator*)
{ {
} }
......
...@@ -63,16 +63,24 @@ namespace spot ...@@ -63,16 +63,24 @@ namespace spot
/// Called by run() to process a state. /// Called by run() to process a state.
/// ///
/// \param s The current state. /// \param s The current state.
/// \param n An unique number assigned to \a s. /// \param n A unique number assigned to \a s.
/// \param si The spot::tgba_succ_iterator for \a s. /// \param si The spot::tgba_succ_iterator for \a s.
virtual void process_state(const state* s, int n, tgba_succ_iterator* si); virtual void process_state(const state* s, int n, tgba_succ_iterator* si);
/// Called by run() to process a transition. /// Called by run() to process a transition.
/// ///
/// \param in_s The source state
/// \param in The source state number. /// \param in The source state number.
/// \param out_s The destination state
/// \param out The destination state number. /// \param out The destination state number.
/// \param si The spot::tgba_succ_iterator positionned on the current /// \param si The spot::tgba_succ_iterator positionned on the current
/// transition. /// transition.
virtual void process_link(int in, int out, const tgba_succ_iterator* si); ///
/// The in_s and out_s states are owned by the
/// spot::tgba_reachable_iterator instance and destroyed when the
/// instance is destroyed.
virtual void process_link(const state* in_s, int in,
const state* out_s, int out,
const tgba_succ_iterator* si);
protected: protected:
const tgba* automata_; ///< The spot::tgba to explore. const tgba* automata_; ///< The spot::tgba to explore.
......
...@@ -42,7 +42,8 @@ namespace spot ...@@ -42,7 +42,8 @@ namespace spot
} }
void void
process_link(int, int, const tgba_succ_iterator*) process_link(const state*, int, const state*, int,
const tgba_succ_iterator*)
{ {
++s_.transitions; ++s_.transitions;
} }
......
Supports Markdown
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