Commit 0f15d28f authored by Denis Poitrenaud's avatar Denis Poitrenaud
Browse files

* src/tgbaalgos/emptiness_stats.hh, src/tgbaalgos/weight.cc,

src/tgbaalgos/weight.hh: New files.
* src/tgbaalgos/Makefile.am: Add them.
* src/tgbaalgos/magic.cc, src/tgbaalgos/se05.cc,
src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc,
src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/status.cc,
src/tgbaalgos/gtec/status.hh, : Add emptiness check statistics
capability.
* src/tgbatest/randtgba.cc: Print these statistics.
* src/tgbatest/ltl2tgba.cc: tau03opt search can deal without acceptance
condition.
* src/tgbatest/emptchk.test: Test tau03opt search.
parent fc775a8b
2004-11-22 Poitrenaud Denis <denis@src.lip6.fr>
* src/tgbaalgos/emptiness_stats.hh, src/tgbaalgos/weight.cc,
src/tgbaalgos/weight.hh: New files.
* src/tgbaalgos/Makefile.am: Add them.
* src/tgbaalgos/magic.cc, src/tgbaalgos/se05.cc,
src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc,
src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/status.cc,
src/tgbaalgos/gtec/status.hh, : Add emptiness check statistics
capability.
* src/tgbatest/randtgba.cc: Print these statistics.
* src/tgbatest/ltl2tgba.cc: tau03opt search can deal without acceptance
condition.
* src/tgbatest/emptchk.test: Test tau03opt search.
2004-11-19 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-11-19 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/magic.hh, src/tgbaalgos/magic.cc, * src/tgbaalgos/magic.hh, src/tgbaalgos/magic.cc,
......
...@@ -31,6 +31,7 @@ tgbaalgos_HEADERS = \ ...@@ -31,6 +31,7 @@ tgbaalgos_HEADERS = \
dottydec.hh \ dottydec.hh \
dupexp.hh \ dupexp.hh \
emptiness.hh \ emptiness.hh \
emptiness_stats.hh \
lbtt.hh \ lbtt.hh \
ltl2tgba_fm.hh \ ltl2tgba_fm.hh \
ltl2tgba_lacim.hh \ ltl2tgba_lacim.hh \
...@@ -47,7 +48,8 @@ tgbaalgos_HEADERS = \ ...@@ -47,7 +48,8 @@ tgbaalgos_HEADERS = \
stats.hh \ stats.hh \
tau03.hh \ tau03.hh \
tau03opt.hh \ tau03opt.hh \
reductgba_sim.hh reductgba_sim.hh \
weight.hh
noinst_LTLIBRARIES = libtgbaalgos.la noinst_LTLIBRARIES = libtgbaalgos.la
libtgbaalgos_la_SOURCES = \ libtgbaalgos_la_SOURCES = \
...@@ -72,6 +74,7 @@ libtgbaalgos_la_SOURCES = \ ...@@ -72,6 +74,7 @@ libtgbaalgos_la_SOURCES = \
tau03.cc \ tau03.cc \
tau03opt.cc \ tau03opt.cc \
reductgba_sim.cc \ reductgba_sim.cc \
reductgba_sim_del.cc reductgba_sim_del.cc \
weight.cc
libtgbaalgos_la_LIBADD = gtec/libgtec.la libtgbaalgos_la_LIBADD = gtec/libgtec.la
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#ifndef SPOT_TGBAALGOS_EC_STATS_HH
# define SPOT_TGBAALGOS_EC_STATS_HH
namespace spot
{
/// \addtogroup ec_misc
/// @{
class ec_statistics
{
public :
ec_statistics()
: states_(0), transitions_(0), depth_(0), max_depth_(0)
{
}
void set_states(int n)
{
states_ = n;
}
void inc_states()
{
++states_;
}
void inc_transitions()
{
++transitions_;
}
void inc_depth()
{
++depth_;
if (depth_ > max_depth_)
max_depth_ = depth_;
}
void dec_depth()
{
--depth_;
}
int states() const
{
return states_;
}
int transitions() const
{
return transitions_;
}
int max_depth() const
{
return max_depth_;
}
private :
unsigned states_; /// number of disctint visited states
unsigned transitions_; /// number of visited transitions
unsigned depth_; /// maximal depth of the stack(s)
unsigned max_depth_; /// maximal depth of the stack(s)
};
/// @}
}
#endif // SPOT_TGBAALGOS_EC_STATS_HH
...@@ -221,6 +221,7 @@ namespace spot ...@@ -221,6 +221,7 @@ namespace spot
delete todo.top().second; delete todo.top().second;
todo.pop(); todo.pop();
} }
set_states(ecs_->states());
return new couvreur99_check_result(ecs_); return new couvreur99_check_result(ecs_);
} }
} }
...@@ -344,6 +345,7 @@ namespace spot ...@@ -344,6 +345,7 @@ namespace spot
} }
todo.pop(); todo.pop();
} }
set_states(ecs_->states());
return new couvreur99_check_result(ecs_); return new couvreur99_check_result(ecs_);
} }
} }
......
...@@ -24,6 +24,7 @@ ...@@ -24,6 +24,7 @@
#include "status.hh" #include "status.hh"
#include "tgbaalgos/emptiness.hh" #include "tgbaalgos/emptiness.hh"
#include "tgbaalgos/emptiness_stats.hh"
namespace spot namespace spot
{ {
...@@ -71,7 +72,7 @@ namespace spot ...@@ -71,7 +72,7 @@ namespace spot
/// tgba_succ_iterators: it must compute all successors of a state /// tgba_succ_iterators: it must compute all successors of a state
/// at once in order to decide which to explore first, and must keep /// at once in order to decide which to explore first, and must keep
/// a list of all unexplored successors in its DFS stack. /// a list of all unexplored successors in its DFS stack.
class couvreur99_check: public emptiness_check class couvreur99_check: public emptiness_check, public ec_statistics
{ {
public: public:
couvreur99_check(const tgba* a, couvreur99_check(const tgba* a,
......
...@@ -45,4 +45,10 @@ namespace spot ...@@ -45,4 +45,10 @@ namespace spot
<< " strongly connected components in search stack" << " strongly connected components in search stack"
<< std::endl; << std::endl;
} }
int
couvreur99_check_status::states() const
{
return h->size();
}
} }
...@@ -47,6 +47,9 @@ namespace spot ...@@ -47,6 +47,9 @@ namespace spot
/// Output statistics about this object. /// Output statistics about this object.
void print_stats(std::ostream& os) const; void print_stats(std::ostream& os) const;
/// Return the number of states visited by the search
int states() const;
}; };
} }
......
...@@ -19,11 +19,18 @@ ...@@ -19,11 +19,18 @@
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA. // 02111-1307, USA.
//#define TRACE
#ifdef TRACE
#include <iostream>
#endif
#include <cassert> #include <cassert>
#include <list> #include <list>
#include "misc/hash.hh" #include "misc/hash.hh"
#include "tgba/tgba.hh" #include "tgba/tgba.hh"
#include "emptiness.hh" #include "emptiness.hh"
#include "emptiness_stats.hh"
#include "magic.hh" #include "magic.hh"
namespace spot namespace spot
...@@ -35,7 +42,7 @@ namespace spot ...@@ -35,7 +42,7 @@ namespace spot
/// \brief Emptiness checker on spot::tgba automata having at most one /// \brief Emptiness checker on spot::tgba automata having at most one
/// accepting condition (i.e. a TBA). /// accepting condition (i.e. a TBA).
template <typename heap> template <typename heap>
class magic_search : public emptiness_check class magic_search : public emptiness_check, public ec_statistics
{ {
public: public:
/// \brief Initialize the Magic Search algorithm on the automaton \a a /// \brief Initialize the Magic Search algorithm on the automaton \a a
...@@ -43,7 +50,10 @@ namespace spot ...@@ -43,7 +50,10 @@ namespace spot
/// \pre The automaton \a a must have at most one accepting /// \pre The automaton \a a must have at most one accepting
/// condition (i.e. it is a TBA). /// condition (i.e. it is a TBA).
magic_search(const tgba *a, size_t size) magic_search(const tgba *a, size_t size)
: h(size), a(a), all_cond(a->all_acceptance_conditions()) : ec_statistics(),
h(size),
a(a),
all_cond(a->all_acceptance_conditions())
{ {
assert(a->number_of_acceptance_conditions() <= 1); assert(a->number_of_acceptance_conditions() <= 1);
} }
...@@ -75,13 +85,11 @@ namespace spot ...@@ -75,13 +85,11 @@ namespace spot
/// visits only a finite set of accepting paths. /// visits only a finite set of accepting paths.
virtual emptiness_check_result* check() virtual emptiness_check_result* check()
{ {
nbn = nbt = 0;
sts = mdp = st_blue.size() + st_red.size();
if (st_red.empty()) if (st_red.empty())
{ {
assert(st_blue.empty()); assert(st_blue.empty());
const state* s0 = a->get_init_state(); const state* s0 = a->get_init_state();
++nbn; inc_states();
h.add_new_state(s0, BLUE); h.add_new_state(s0, BLUE);
push(st_blue, s0, bddfalse, bddfalse); push(st_blue, s0, bddfalse, bddfalse);
if (dfs_blue()) if (dfs_blue())
...@@ -90,8 +98,7 @@ namespace spot ...@@ -90,8 +98,7 @@ namespace spot
else else
{ {
h.pop_notify(st_red.front().s); h.pop_notify(st_red.front().s);
delete st_red.front().it; pop(st_red);
st_red.pop_front();
if (!st_red.empty() && dfs_red()) if (!st_red.empty() && dfs_red())
return new result(*this); return new result(*this);
else else
...@@ -103,9 +110,9 @@ namespace spot ...@@ -103,9 +110,9 @@ namespace spot
virtual std::ostream& print_stats(std::ostream &os) const virtual std::ostream& print_stats(std::ostream &os) const
{ {
os << nbn << " distinct nodes visited" << std::endl; os << states() << " distinct nodes visited" << std::endl;
os << nbt << " transitions explored" << std::endl; os << transitions() << " transitions explored" << std::endl;
os << mdp << " nodes for the maximal stack depth" << std::endl; os << max_depth() << " nodes for the maximal stack depth" << std::endl;
if (!st_red.empty()) if (!st_red.empty())
{ {
assert(!st_blue.empty()); assert(!st_blue.empty());
...@@ -116,9 +123,6 @@ namespace spot ...@@ -116,9 +123,6 @@ namespace spot
} }
private: private:
/// \brief counters for statistics (number of distinct nodes, of
/// transitions and maximal stacks size.
int nbn, nbt, mdp, sts;
struct stack_item struct stack_item
{ {
...@@ -141,14 +145,19 @@ namespace spot ...@@ -141,14 +145,19 @@ namespace spot
void push(stack_type& st, const state* s, void push(stack_type& st, const state* s,
const bdd& label, const bdd& acc) const bdd& label, const bdd& acc)
{ {
++sts; inc_depth();
if (sts>mdp)
mdp = sts;
tgba_succ_iterator* i = a->succ_iter(s); tgba_succ_iterator* i = a->succ_iter(s);
i->first(); i->first();
st.push_front(stack_item(s, i, label, acc)); st.push_front(stack_item(s, i, label, acc));
} }
void pop(stack_type& st)
{
dec_depth();
delete st.front().it;
st.pop_front();
}
/// \brief Stack of the blue dfs. /// \brief Stack of the blue dfs.
stack_type st_blue; stack_type st_blue;
...@@ -173,64 +182,98 @@ namespace spot ...@@ -173,64 +182,98 @@ namespace spot
while (!st_blue.empty()) while (!st_blue.empty())
{ {
stack_item& f = st_blue.front(); stack_item& f = st_blue.front();
# ifdef TRACE
std::cout << "DFS_BLUE treats: "
<< a->format_state(f.s) << std::endl;
# endif
if (!f.it->done()) if (!f.it->done())
{ {
++nbt;
const state *s_prime = f.it->current_state(); const state *s_prime = f.it->current_state();
# ifdef TRACE
std::cout << " Visit the successor: "
<< a->format_state(s_prime) << std::endl;
# endif
bdd label = f.it->current_condition(); bdd label = f.it->current_condition();
bdd acc = f.it->current_acceptance_conditions(); bdd acc = f.it->current_acceptance_conditions();
// Go down the edge (f.s, <label, acc>, s_prime)
f.it->next(); f.it->next();
inc_transitions();
typename heap::color_ref c = h.get_color_ref(s_prime); typename heap::color_ref c = h.get_color_ref(s_prime);
if (c.is_white()) if (c.is_white())
// Go down the edge (f.s, <label, acc>, s_prime)
{ {
++nbn; # ifdef TRACE
std::cout << " It is white, go down" << std::endl;
# endif
inc_states();
h.add_new_state(s_prime, BLUE); h.add_new_state(s_prime, BLUE);
push(st_blue, s_prime, label, acc); push(st_blue, s_prime, label, acc);
} }
else // Backtrack the edge (f.s, <label, acc>, s_prime) else
{ {
if (c.get() != RED && acc == all_cond) if (acc == all_cond && c.get_color() != RED)
// the test 'c.get() != RED' is added to limit
// the number of runs reported by successive
// calls to the check method. Without this
// functionnality, the test can be ommited.
{ {
// the test 'c.get_color() != RED' is added to limit
// the number of runs reported by successive
// calls to the check method. Without this
// functionnality, the test can be ommited.
# ifdef TRACE
std::cout << " It is blue and the arc is "
<< "accepting, start a red dfs" << std::endl;
# endif
target = f.s; target = f.s;
c.set(RED); c.set_color(RED);
push(st_red, s_prime, label, acc); push(st_red, s_prime, label, acc);
if (dfs_red()) if (dfs_red())
return true; return true;
} }
else else
h.pop_notify(s_prime); {
# ifdef TRACE
std::cout << " It is blue or red, pop it" << std::endl;
# endif
h.pop_notify(s_prime);
}
} }
} }
else else
// Backtrack the edge // Backtrack the edge
// (predecessor of f.s in st_blue, <f.label, f.acc>, f.s) // (predecessor of f.s in st_blue, <f.label, f.acc>, f.s)
{ {
--sts; # ifdef TRACE
std::cout << " All the successors have been visited"
<< std::endl;
# endif
stack_item f_dest(f); stack_item f_dest(f);
delete f.it; pop(st_blue);
st_blue.pop_front();
typename heap::color_ref c = h.get_color_ref(f_dest.s); typename heap::color_ref c = h.get_color_ref(f_dest.s);
assert(!c.is_white()); assert(!c.is_white());
if (c.get() != RED && f_dest.acc == all_cond if (!st_blue.empty() &&
&& !st_blue.empty()) f_dest.acc == all_cond && c.get_color() != RED)
// the test 'c.get() != RED' is added to limit
// the number of runs reported by successive
// calls to the check method. Without this
// functionnality, the test can be ommited.
{ {
// the test 'c.get_color() != RED' is added to limit
// the number of runs reported by successive
// calls to the check method. Without this
// functionnality, the test can be ommited.
# ifdef TRACE
std::cout << " It is blue and the arc from "
<< a->format_state(st_blue.front().s)
<< " to it is accepting, start a red dfs"
<< std::endl;
# endif
target = st_blue.front().s; target = st_blue.front().s;
c.set(RED); c.set_color(RED);
push(st_red, f_dest.s, f_dest.label, f_dest.acc); push(st_red, f_dest.s, f_dest.label, f_dest.acc);
if (dfs_red()) if (dfs_red())
return true; return true;
} }
else else
h.pop_notify(f_dest.s); {
# ifdef TRACE
std::cout << " Pop it"
<< std::endl;
# endif
h.pop_notify(f_dest.s);
}
} }
} }
return false; return false;
...@@ -245,40 +288,63 @@ namespace spot ...@@ -245,40 +288,63 @@ namespace spot
while (!st_red.empty()) while (!st_red.empty())
{ {
stack_item& f = st_red.front(); stack_item& f = st_red.front();
if (!f.it->done()) // Go down # ifdef TRACE
std::cout << "DFS_RED treats: "
<< a->format_state(f.s) << std::endl;
# endif
if (!f.it->done())
{ {
++nbt;
const state *s_prime = f.it->current_state(); const state *s_prime = f.it->current_state();
# ifdef TRACE
std::cout << " Visit the successor: "
<< a->format_state(s_prime) << std::endl;
# endif
bdd label = f.it->current_condition(); bdd label = f.it->current_condition();
bdd acc = f.it->current_acceptance_conditions(); bdd acc = f.it->current_acceptance_conditions();
// Go down the edge (f.s, <label, acc>, s_prime)
f.it->next(); f.it->next();
inc_transitions();
typename heap::color_ref c = h.get_color_ref(s_prime); typename heap::color_ref c = h.get_color_ref(s_prime);
if (c.is_white()) if (c.is_white())
// Go down the edge (f.s, <label, acc>, s_prime)
{ {
++nbn; // If the red dfs find a white here, it must have crossed
h.add_new_state(s_prime, RED); // the blue stack and the target must be reached soon.
// Notice that this property holds only for explicit search.
// Collisions in bit-state hashing search can also lead
// to the visit of white state. Anyway, it is not necessary
// to visit white states either if a cycle can be missed
// with bit-state hashing search.
# ifdef TRACE
std::cout << " It is white, pop it" << std::endl;
# endif
delete s_prime;
}
else if (c.get_color() == BLUE)
{
# ifdef TRACE
std::cout << " It is blue, go down" << std::endl;
# endif
c.set_color(RED);
push(st_red, s_prime, label, acc); push(st_red, s_prime, label, acc);
if (target->compare(s_prime) == 0)
return true;
} }
else // Go down the edge (f.s, <label, acc>, s_prime) else
{ {
if (c.get() != RED) # ifdef TRACE
{ std::cout << " It is red, pop it" << std::endl;
c.set(RED); # endif
push(st_red, s_prime, label, acc); h.pop_notify(s_prime);
if (target->compare(s_prime) == 0)
return true;
}
else
h.pop_notify(s_prime);
} }
} }
else // Backtrack else // Backtrack
{ {
--sts; # ifdef TRACE
std::cout << " All the successors have been visited, pop it"
<< std::endl;
# endif
h.pop_notify(f.s); h.pop_notify(f.s);
delete f.it;