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

* src/tgba/tgba.hh, src/tgba/tgba.cc

(tgba::project_state): New method.
* src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc
(tgba_product::project_state): New method.
* src/tgba/tgbabta.hh, src/tgba/tgbabta.cc
(tgba_bta_proxy::project_state): New method.
* src/tgbaalgos/magic.cc (magic_search::print_result): Take
a restrict argument.
parent a66ad58b
2003-07-30 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgba/tgba.hh, src/tgba/tgba.cc
(tgba::project_state): New method.
* src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc
(tgba_product::project_state): New method.
* src/tgba/tgbabta.hh, src/tgba/tgbabta.cc
(tgba_bta_proxy::project_state): New method.
* src/tgbaalgos/magic.cc (magic_search::print_result): Take
a restrict argument.
2003-07-29 Alexandre Duret-Lutz <aduret@src.lip6.fr> 2003-07-29 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/ltlparse/ltlscan.ll: Allow /\, \/, and xor, used in LBTT. * src/ltlparse/ltlscan.ll: Allow /\, \/, and xor, used in LBTT.
......
...@@ -7,7 +7,7 @@ namespace spot ...@@ -7,7 +7,7 @@ namespace spot
last_support_variables_input_(0) last_support_variables_input_(0)
{ {
} }
tgba::~tgba() tgba::~tgba()
{ {
if (last_support_conditions_input_) if (last_support_conditions_input_)
...@@ -15,14 +15,14 @@ namespace spot ...@@ -15,14 +15,14 @@ namespace spot
if (last_support_variables_input_) if (last_support_variables_input_)
delete last_support_variables_input_; delete last_support_variables_input_;
} }
bdd bdd
tgba::support_conditions(const state* state) const tgba::support_conditions(const state* state) const
{ {
if (! last_support_conditions_input_ if (! last_support_conditions_input_
|| last_support_conditions_input_->compare(state) != 0) || last_support_conditions_input_->compare(state) != 0)
{ {
last_support_conditions_output_ = last_support_conditions_output_ =
compute_support_conditions(state); compute_support_conditions(state);
if (last_support_conditions_input_) if (last_support_conditions_input_)
delete last_support_conditions_input_; delete last_support_conditions_input_;
...@@ -37,7 +37,7 @@ namespace spot ...@@ -37,7 +37,7 @@ namespace spot
if (! last_support_variables_input_ if (! last_support_variables_input_
|| last_support_variables_input_->compare(state) != 0) || last_support_variables_input_->compare(state) != 0)
{ {
last_support_variables_output_ = last_support_variables_output_ =
compute_support_variables(state); compute_support_variables(state);
if (last_support_variables_input_) if (last_support_variables_input_)
delete last_support_variables_input_; delete last_support_variables_input_;
...@@ -46,4 +46,12 @@ namespace spot ...@@ -46,4 +46,12 @@ namespace spot
return last_support_variables_output_; return last_support_variables_output_;
} }
state*
tgba::project_state(const state* s, const tgba* t) const
{
if (t == this)
return s->clone();
return 0;
}
} }
...@@ -117,6 +117,21 @@ namespace spot ...@@ -117,6 +117,21 @@ namespace spot
/// who owns the state. /// who owns the state.
virtual std::string format_state(const state* state) const = 0; virtual std::string format_state(const state* state) const = 0;
/// \brief Project a state on an automata.
///
/// This converts \a s, into that corresponding spot::state for \a
/// t. This is useful when you have the state of a product, and
/// want restrict this state to a specific automata occuring in
/// the product.
///
/// It goes without saying that \a s and \a t should be compatible
/// (i.e., \a s is a state of \a t).
///
/// \return 0 if the projection fails (\a s is unrelated to \a t),
/// or a new \c state* (the projected state) that must be
/// deleted by the caller.
virtual state* project_state(const state* s, const tgba* t) const;
/// \brief Return the set of all accepting conditions used /// \brief Return the set of all accepting conditions used
/// by this automaton. /// by this automaton.
/// ///
......
...@@ -46,7 +46,7 @@ namespace spot ...@@ -46,7 +46,7 @@ namespace spot
virtual std::string format_state(const state* state) const; virtual std::string format_state(const state* state) const;
bdd_dict* get_dict() const; virtual bdd_dict* get_dict() const;
/// \brief Get the core data associated to this automaton. /// \brief Get the core data associated to this automaton.
/// ///
......
...@@ -234,6 +234,19 @@ namespace spot ...@@ -234,6 +234,19 @@ namespace spot
+ right_->format_state(s->right())); + right_->format_state(s->right()));
} }
state*
tgba_product::project_state(const state* s, const tgba* t) const
{
const state_bdd_product* s2 = dynamic_cast<const state_bdd_product*>(s);
assert(s2);
if (t == this)
return s2->clone();
state* res = left_->project_state(s2->left(), t);
if (res)
return res;
return right_->project_state(s2->right(), t);
}
bdd bdd
tgba_product::all_accepting_conditions() const tgba_product::all_accepting_conditions() const
{ {
......
...@@ -109,6 +109,8 @@ namespace spot ...@@ -109,6 +109,8 @@ namespace spot
virtual std::string format_state(const state* state) const; virtual std::string format_state(const state* state) const;
virtual state* project_state(const state* s, const tgba* t) const;
virtual bdd all_accepting_conditions() const; virtual bdd all_accepting_conditions() const;
virtual bdd neg_accepting_conditions() const; virtual bdd neg_accepting_conditions() const;
......
...@@ -213,13 +213,23 @@ namespace spot ...@@ -213,13 +213,23 @@ namespace spot
std::string std::string
tgba_tba_proxy::format_state(const state* state) const tgba_tba_proxy::format_state(const state* state) const
{ {
const state_tba_proxy* s = const state_tba_proxy* s = dynamic_cast<const state_tba_proxy*>(state);
dynamic_cast<const state_tba_proxy*>(state);
assert(s); assert(s);
return a_->format_state(s->real_state()) + "(" return a_->format_state(s->real_state()) + "("
+ bdd_format_set(get_dict(), s->accepting_cond()) + ")"; + bdd_format_set(get_dict(), s->accepting_cond()) + ")";
} }
state*
tgba_tba_proxy::project_state(const state* s, const tgba* t) const
{
const state_tba_proxy* s2 = dynamic_cast<const state_tba_proxy*>(s);
assert(s2);
if (t == this)
return s2->clone();
return a_->project_state(s2->real_state(), t);
}
bdd bdd
tgba_tba_proxy::all_accepting_conditions() const tgba_tba_proxy::all_accepting_conditions() const
{ {
......
...@@ -41,6 +41,8 @@ namespace spot ...@@ -41,6 +41,8 @@ namespace spot
virtual std::string format_state(const state* state) const; virtual std::string format_state(const state* state) const;
virtual state* project_state(const state* s, const tgba* t) const;
virtual bdd all_accepting_conditions() const; virtual bdd all_accepting_conditions() const;
virtual bdd neg_accepting_conditions() const; virtual bdd neg_accepting_conditions() const;
......
...@@ -122,7 +122,7 @@ namespace spot ...@@ -122,7 +122,7 @@ namespace spot
} }
std::ostream& std::ostream&
magic_search::print_result(std::ostream& os) const magic_search::print_result(std::ostream& os, const tgba* restrict) const
{ {
stack_type::const_reverse_iterator i; stack_type::const_reverse_iterator i;
tstack_type::const_reverse_iterator ti; tstack_type::const_reverse_iterator ti;
...@@ -133,10 +133,33 @@ namespace spot ...@@ -133,10 +133,33 @@ namespace spot
{ {
if (i->first.s->compare(x) == 0) if (i->first.s->compare(x) == 0)
os <<"Cycle:" <<std::endl; os <<"Cycle:" <<std::endl;
os << " " << a->format_state(i->first.s) << std::endl;
const state* s = i->first.s;
if (restrict)
{
s = a->project_state(s, restrict);
assert(s);
os << " " << restrict->format_state(s) << std::endl;
delete s;
}
else
{
os << " " << a->format_state(s) << std::endl;
}
os << " | " << bdd_format_set(d, *ti) << std::endl; os << " | " << bdd_format_set(d, *ti) << std::endl;
} }
os << " " << a->format_state(x) << std::endl;
if (restrict)
{
const state* s = a->project_state(x, restrict);
assert(s);
os << " " << restrict->format_state(s) << std::endl;
delete s;
}
else
{
os << " " << a->format_state(x) << std::endl;
}
return os; return os;
} }
......
...@@ -9,7 +9,7 @@ ...@@ -9,7 +9,7 @@
namespace spot namespace spot
{ {
/// \brief Emptiness check on spot::tgba_tba_proxy automata using /// \brief Emptiness check on spot::tgba_tba_proxy automata using
/// the Magic Search algorithm. /// the Magic Search algorithm.
/// ///
/// This algorithm comes from /// This algorithm comes from
/// \verbatim /// \verbatim
...@@ -38,7 +38,7 @@ namespace spot ...@@ -38,7 +38,7 @@ namespace spot
~magic_search(); ~magic_search();
/// \brief Perform a Magic Search. /// \brief Perform a Magic Search.
/// ///
/// \return true iff the algorithm has found a new accepting /// \return true iff the algorithm has found a new accepting
/// path. /// path.
/// ///
...@@ -46,8 +46,12 @@ namespace spot ...@@ -46,8 +46,12 @@ namespace spot
/// to enumerate all accepting paths. /// to enumerate all accepting paths.
bool check(); bool check();
/// Print the last accepting path found. /// \brief Print the last accepting path found.
std::ostream& print_result(std::ostream& os) const; ///
/// Restrict printed states to \a the state space of restrict if
/// supplied.
std::ostream& print_result(std::ostream& os,
const tgba* restrict = 0) const;
private: private:
...@@ -60,7 +64,7 @@ namespace spot ...@@ -60,7 +64,7 @@ namespace spot
bool seen_without : 1; bool seen_without : 1;
bool seen_with : 1; bool seen_with : 1;
}; };
/// \brief A state for the spot::magic_search algorithm. /// \brief A state for the spot::magic_search algorithm.
struct magic_state struct magic_state
{ {
...@@ -73,7 +77,7 @@ namespace spot ...@@ -73,7 +77,7 @@ namespace spot
stack_type stack; ///< Stack of visited states on the path. stack_type stack; ///< Stack of visited states on the path.
typedef std::list<bdd> tstack_type; typedef std::list<bdd> tstack_type;
/// \brief Stack of transitions. /// \brief Stack of transitions.
/// ///
/// This is an addition to the data from the paper. /// This is an addition to the data from the paper.
tstack_type tstack; tstack_type tstack;
...@@ -89,7 +93,7 @@ namespace spot ...@@ -89,7 +93,7 @@ namespace spot
const tgba_tba_proxy* a; ///< The automata to check. const tgba_tba_proxy* a; ///< The automata to check.
/// The state for which we are currently seeking an SCC. /// The state for which we are currently seeking an SCC.
const state* x; const state* x;
}; };
......
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