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

* iface/gspn/ssp.cc (couvreur99_check_shy_ssp::find_state,

Browse source 
numbered_state_heap_ssp_semi): Implement a double hash_map using
greatspn's new container() function.
* iface/gspn/ssp.hh (gspn_ssp_interface): Add a doublehash option.
* iface/gspn/ltlgspn.cc: Add option -1 to disable this optimization.
This commit is contained in:
Alexandre Duret-Lutz 2006-02-14 17:07:23 +00:00
parent ea9ee5d5c7
commit 857f0ac54e
4 changed files with 285 additions and 144 deletions
Download patch file Download diff file Expand all files Collapse all files

9
ChangeLog
View file

@ -1,3 +1,12 @@
2006-02-14 Alexandre Duret-Lutz <adl@src.lip6.fr>
Soheib Baarir <Souheib.Baarir@lip6.fr>
* iface/gspn/ssp.cc (couvreur99_check_shy_ssp::find_state,
numbered_state_heap_ssp_semi): Implement a double hash_map using
greatspn's new container() function.
* iface/gspn/ssp.hh (gspn_ssp_interface): Add a doublehash option.
* iface/gspn/ltlgspn.cc: Add option -1 to disable this optimization.
2006-02-11 Alexandre Duret-Lutz <adl@src.lip6.fr> 2006-02-11 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbatest/ltl2tgba.cc: Pacify sanity.test. * src/tgbatest/ltl2tgba.cc: Pacify sanity.test.

16
iface/gspn/ltlgspn.cc
View file

@ -50,6 +50,10 @@ syntax(char* prog)
<< " [OPTIONS...] model formula automata props..." << std::endl << " [OPTIONS...] model formula automata props..." << std::endl
#endif #endif
<< std::endl << std::endl
#ifdef SSP
<< " -1 do not use a double hash (for inclusion check)"
<< std::endl
#endif
<< " -c compute an example" << std::endl << " -c compute an example" << std::endl
<< " (instead of just checking for emptiness)" << std::endl << " (instead of just checking for emptiness)" << std::endl
<< std::endl << std::endl
@ -99,12 +103,22 @@ main(int argc, char **argv)
enum { Lacim, Fm } trans = Lacim; enum { Lacim, Fm } trans = Lacim;
bool compute_counter_example = false; bool compute_counter_example = false;
bool proj = true; bool proj = true;
#ifdef SSP
bool doublehash = true;
#endif
std::string dead = "true"; std::string dead = "true";
spot::ltl::declarative_environment env; spot::ltl::declarative_environment env;
while (formula_index < argc && *argv[formula_index] == '-') while (formula_index < argc && *argv[formula_index] == '-')
{ {
#ifdef SSP
if (!strcmp(argv[formula_index], "-1"))
{
doublehash = false;
}
else
#endif
if (!strcmp(argv[formula_index], "-c")) if (!strcmp(argv[formula_index], "-c"))
{ {
compute_counter_example = true; compute_counter_example = true;
@ -187,7 +201,7 @@ main(int argc, char **argv)
#if SSP #if SSP
bool inclusion = (check != Couvreur && check != Couvreur2); bool inclusion = (check != Couvreur && check != Couvreur2);
spot::gspn_ssp_interface gspn(2, argv, dict, env, inclusion); spot::gspn_ssp_interface gspn(2, argv, dict, env, inclusion, doublehash);
spot::tgba_parse_error_list pel1; spot::tgba_parse_error_list pel1;
spot::tgba_explicit* control = spot::tgba_parse(argv[formula_index + 2], spot::tgba_explicit* control = spot::tgba_parse(argv[formula_index + 2],

395
iface/gspn/ssp.cc
View file

@ -25,6 +25,7 @@
#include <gspnlib.h> #include <gspnlib.h>
#include "ssp.hh" #include "ssp.hh"
#include "misc/bddlt.hh" #include "misc/bddlt.hh"
#include "misc/hash.hh"
#include <bdd.h> #include <bdd.h>
#include "tgbaalgos/gtec/explscc.hh" #include "tgbaalgos/gtec/explscc.hh"
#include "tgbaalgos/gtec/nsheap.hh" #include "tgbaalgos/gtec/nsheap.hh"
@ -46,6 +47,8 @@ namespace spot
delete[] t; delete[] t;
return tmp; return tmp;
} }
static bool doublehash;
} }
// state_gspn_ssp // state_gspn_ssp
@ -238,8 +241,8 @@ namespace spot
{ {
return return
new state_gspn_ssp(successors_[current_succ_].succ_, new state_gspn_ssp(successors_[current_succ_].succ_,
(state_array_[successors_[current_succ_] (state_array_[successors_[current_succ_]
.arc->curr_state])->clone()); .arc->curr_state])->clone());
} }
virtual bdd virtual bdd
@ -339,8 +342,8 @@ namespace spot
tgba_succ_iterator* tgba_succ_iterator*
tgba_gspn_ssp::succ_iter(const state* state_, tgba_gspn_ssp::succ_iter(const state* state_,
const state* global_state, const state* global_state,
const tgba* global_automaton) const const tgba* global_automaton) const
{ {
const state_gspn_ssp* s = dynamic_cast<const state_gspn_ssp*>(state_); const state_gspn_ssp* s = dynamic_cast<const state_gspn_ssp*>(state_);
assert(s); assert(s);
@ -380,8 +383,9 @@ namespace spot
props_[nb_arc_props].arc->curr_acc_conds = size_bdd; props_[nb_arc_props].arc->curr_acc_conds = size_bdd;
++size_bdd; ++size_bdd;
state_array = (state**) realloc(state_array, state_array =
(size_states + 1) * sizeof(state*)); (state**) realloc(state_array,
(size_states + 1) * sizeof(state*));
state_array[size_states] = i->current_state(); state_array[size_states] = i->current_state();
props_[nb_arc_props].arc->curr_state = size_states; props_[nb_arc_props].arc->curr_state = size_states;
++size_states; ++size_states;
@ -434,24 +438,24 @@ namespace spot
++nb_arc_props; ++nb_arc_props;
} }
} }
Succ_* succ_tgba_ = 0; Succ_* succ_tgba_ = 0;
size_t size_tgba_ = 0; size_t size_tgba_ = 0;
int j, conj; int j, conj;
succ(s->left(), props_, nb_arc_props, &succ_tgba_, &size_tgba_); succ(s->left(), props_, nb_arc_props, &succ_tgba_, &size_tgba_);
for (j = 0; j < nb_arc_props; j++) for (j = 0; j < nb_arc_props; j++)
{ {
for (conj = 0; conj < props_[j].nb_conj; conj++) for (conj = 0; conj < props_[j].nb_conj; conj++)
free(props_[j].prop[conj]); free(props_[j].prop[conj]);
free(props_[j].prop); free(props_[j].prop);
} }
delete i; delete i;
return new tgba_succ_iterator_gspn_ssp(succ_tgba_, size_tgba_, return new tgba_succ_iterator_gspn_ssp(succ_tgba_, size_tgba_,
bdd_array, state_array, bdd_array, state_array,
size_states, props_, size_states, props_,
nb_arc_props); nb_arc_props);
} }
bdd bdd
@ -534,9 +538,11 @@ namespace spot
bdd_dict* dict, bdd_dict* dict,
const const
ltl::declarative_environment& env, ltl::declarative_environment& env,
bool inclusion) bool inclusion,
bool doublehash_)
: dict_(dict), env_(env) : dict_(dict), env_(env)
{ {
doublehash = doublehash_;
if (inclusion) if (inclusion)
inclusion_version(); inclusion_version();
@ -635,6 +641,14 @@ namespace spot
////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////
namespace
{
inline void*
container_(const State s)
{
return doublehash ? container(s) : 0;
}
}
class numbered_state_heap_ssp_semi : public numbered_state_heap class numbered_state_heap_ssp_semi : public numbered_state_heap
{ {
@ -656,42 +670,66 @@ namespace spot
virtual numbered_state_heap::state_index virtual numbered_state_heap::state_index
find(const state* s) const find(const state* s) const
{ {
state_index res; const void* cont =
container_(dynamic_cast<const state_gspn_ssp*>(s)->left());
hash_type::const_iterator i; contained_map::const_iterator i = contained.find(cont);
for (i = h.begin(); i != h.end(); ++i) if (i != contained.end())
{ {
const state_gspn_ssp* old_state = const state_list& l = i->second;
dynamic_cast<const state_gspn_ssp*>(i->first);
const state_gspn_ssp* new_state =
dynamic_cast<const state_gspn_ssp*>(s);
assert(old_state);
assert(new_state);
if ((old_state->right())->compare(new_state->right()) == 0) state_list::const_iterator j;
for (j = l.begin(); j != l.end(); ++j)
{ {
if (old_state->left() == new_state->left()) const state_gspn_ssp* old_state =
break; dynamic_cast<const state_gspn_ssp*>(*j);
const state_gspn_ssp* new_state =
dynamic_cast<const state_gspn_ssp*>(s);
assert(old_state);
assert(new_state);
if (old_state->left() if ((old_state->right())->compare(new_state->right()) == 0)
&& new_state->left() {
&& spot_inclusion(new_state->left(), old_state->left())) if (old_state->left() == new_state->left())
break; break;
if (old_state->left()
&& new_state->left()
&& spot_inclusion(new_state->left(), old_state->left()))
break;
}
}
if (j != l.end())
{
if (s != *j)
{
delete s;
s = *j;
}
}
else
{
s = 0;
} }
} }
else
{
s = 0;
}
if (i == h.end()) state_index res;
if (s == 0)
{ {
res.first = 0; res.first = 0;
res.second = 0; res.second = 0;
} }
else else
{ {
hash_type::const_iterator i = h.find(s);
assert(i != h.end());
assert(s == i->first);
res.first = i->first; res.first = i->first;
res.second = i->second; res.second = i->second;
if (s != i->first)
delete s;
} }
return res; return res;
} }
@ -699,42 +737,66 @@ namespace spot
virtual numbered_state_heap::state_index_p virtual numbered_state_heap::state_index_p
find(const state* s) find(const state* s)
{ {
state_index_p res; const void* cont =
container_(dynamic_cast<const state_gspn_ssp*>(s)->left());
hash_type::iterator i; contained_map::const_iterator i = contained.find(cont);
for (i = h.begin(); i != h.end(); ++i) if (i != contained.end())
{ {
const state_gspn_ssp* old_state = const state_list& l = i->second;
dynamic_cast<const state_gspn_ssp*>(i->first);
const state_gspn_ssp* new_state =
dynamic_cast<const state_gspn_ssp*>(s);
assert(old_state);
assert(new_state);
if ((old_state->right())->compare(new_state->right()) == 0) state_list::const_iterator j;
for (j = l.begin(); j != l.end(); ++j)
{ {
if (old_state->left() == new_state->left()) const state_gspn_ssp* old_state =
break; dynamic_cast<const state_gspn_ssp*>(*j);
const state_gspn_ssp* new_state =
dynamic_cast<const state_gspn_ssp*>(s);
assert(old_state);
assert(new_state);
if (old_state->left() if ((old_state->right())->compare(new_state->right()) == 0)
&& new_state->left() {
&& spot_inclusion(new_state->left(), old_state->left())) if (old_state->left() == new_state->left())
break; break;
if (old_state->left()
&& new_state->left()
&& spot_inclusion(new_state->left(), old_state->left()))
break;
}
}
if (j != l.end())
{
if (s != *j)
{
delete s;
s = *j;
}
}
else
{
s = 0;
} }
} }
else
{
s = 0;
}
if (i == h.end()) state_index_p res;
if (s == 0)
{ {
res.first = 0; res.first = 0;
res.second = 0; res.second = 0;
} }
else else
{ {
hash_type::iterator i = h.find(s);
assert(i != h.end());
assert(s == i->first);
res.first = i->first; res.first = i->first;
res.second = &i->second; res.second = &i->second;
if (s != i->first)
delete s;
} }
return res; return res;
} }
@ -781,23 +843,17 @@ namespace spot
return res; return res;
} }
virtual int&
index_and_insert(const state*& s)
{
std::pair<hash_type::iterator, bool> r
= h.insert(hash_type::value_type(s, 0));
if (!r.second)
{
delete s;
s = r.first->first;
}
return r.first->second;
}
virtual void virtual void
insert(const state* s, int index) insert(const state* s, int index)
{ {
h[s] = index; h[s] = index;
State sg = dynamic_cast<const state_gspn_ssp*>(s)->left();
if (sg)
{
const void* cont = container_(sg);
contained[cont].push_front(s);
}
} }
virtual int virtual int
@ -813,8 +869,14 @@ namespace spot
state_ptr_hash, state_ptr_equal> hash_type; state_ptr_hash, state_ptr_equal> hash_type;
hash_type h; ///< Map of visited states. hash_type h; ///< Map of visited states.
typedef std::list<const state*> state_list;
typedef Sgi::hash_map<const void*, state_list,
ptr_hash<void> > contained_map;
contained_map contained;
friend class numbered_state_heap_ssp_const_iterator; friend class numbered_state_heap_ssp_const_iterator;
friend class couvreur99_check_shy_ssp; friend class couvreur99_check_shy_ssp;
friend class couvreur99_check_shy_semi_ssp;
}; };
@ -823,8 +885,8 @@ namespace spot
{ {
public: public:
numbered_state_heap_ssp_const_iterator numbered_state_heap_ssp_const_iterator
(const numbered_state_heap_ssp_semi::hash_type& h) (const numbered_state_heap_ssp_semi::hash_type& h)
: numbered_state_heap_const_iterator(), h(h) : numbered_state_heap_const_iterator(), h(h)
{ {
} }
@ -917,14 +979,17 @@ namespace spot
numbered_state_heap_ssp_factory_semi::instance()), numbered_state_heap_ssp_factory_semi::instance()),
inclusion_count_heap(0), inclusion_count_heap(0),
inclusion_count_stack(0) inclusion_count_stack(0)
{ {
stats["inclusion count heap"] = stats["inclusion count heap"] =
static_cast<spot::unsigned_statistics::unsigned_fun> static_cast<spot::unsigned_statistics::unsigned_fun>
(&couvreur99_check_shy_ssp::get_inclusion_count_heap); (&couvreur99_check_shy_ssp::get_inclusion_count_heap);
stats["inclusion count stack"] = stats["inclusion count stack"] =
static_cast<spot::unsigned_statistics::unsigned_fun> static_cast<spot::unsigned_statistics::unsigned_fun>
(&couvreur99_check_shy_ssp::get_inclusion_count_stack); (&couvreur99_check_shy_ssp::get_inclusion_count_stack);
} stats["contained map size"] =
static_cast<spot::unsigned_statistics::unsigned_fun>
(&couvreur99_check_shy_ssp::get_contained_map_size);
}
private: private:
unsigned inclusion_count_heap; unsigned inclusion_count_heap;
@ -941,6 +1006,12 @@ namespace spot
{ {
return inclusion_count_stack; return inclusion_count_stack;
}; };
unsigned
get_contained_map_size() const
{
return
dynamic_cast<numbered_state_heap_ssp_semi*>(ecs_->h)->contained.size();
}
// If a new state includes an older state, we may have to add new // If a new state includes an older state, we may have to add new
// children to the list of children of that older state. We cannot // children to the list of children of that older state. We cannot
@ -951,76 +1022,113 @@ namespace spot
{ {
typedef numbered_state_heap_ssp_semi::hash_type hash_type; typedef numbered_state_heap_ssp_semi::hash_type hash_type;
hash_type& h = dynamic_cast<numbered_state_heap_ssp_semi*>(ecs_->h)->h; hash_type& h = dynamic_cast<numbered_state_heap_ssp_semi*>(ecs_->h)->h;
typedef numbered_state_heap_ssp_semi::contained_map contained_map;
typedef numbered_state_heap_ssp_semi::state_list state_list;
const contained_map& contained =
dynamic_cast<numbered_state_heap_ssp_semi*>(ecs_->h)->contained;
hash_type::iterator i; const void* cont =
for (i = h.begin(); i != h.end(); ++i) container_(dynamic_cast<const state_gspn_ssp*>(s)->left());
contained_map::const_iterator i = contained.find(cont);
if (i != contained.end())
{ {
const state_gspn_ssp* old_state = const state_list& l = i->second;
dynamic_cast<const state_gspn_ssp*>(i->first); state_list::const_iterator j;
const state_gspn_ssp* new_state =
dynamic_cast<const state_gspn_ssp*>(s);
assert(old_state);
assert(new_state);
if ((old_state->right())->compare(new_state->right()) == 0) for (j = l.begin(); j != l.end(); ++j)
{ {
if (old_state->left() == new_state->left()) const state_gspn_ssp* old_state =
break; dynamic_cast<const state_gspn_ssp*>(*j);
const state_gspn_ssp* new_state =
dynamic_cast<const state_gspn_ssp*>(s);
assert(old_state);
assert(new_state);
if (old_state->left() && new_state->left()) if ((old_state->right())->compare(new_state->right()) == 0)
{ {
if (i->second == -1) if (old_state->left() == new_state->left())
break;
if (old_state->left() && new_state->left())
{ {
if (spot_inclusion(new_state->left(), old_state->left())) hash_type::const_iterator i = h.find(*j);
assert(i != h.end());
if (i->second == -1)
{ {
++inclusion_count_heap; if (spot_inclusion(new_state->left(),
break; old_state->left()))
}
}
else
{
if (spot_inclusion(old_state->left(), new_state->left()))
{
++inclusion_count_stack;
State* succ_tgba_ = 0;
size_t size_tgba_ = 0;
succ_queue& queue = todo.back().q;
Diff_succ(old_state->left(), new_state->left(),
&succ_tgba_, &size_tgba_);
for (size_t i = 0; i < size_tgba_; i++)
{ {
state_gspn_ssp* s = ++inclusion_count_heap;
new state_gspn_ssp break;
(succ_tgba_[i], }
old_state->right()->clone()); }
queue.push_back(successor(queue.begin()->acc, s)); else
inc_depth(); {
if (spot_inclusion(old_state->left(),
new_state->left()))
{
++inclusion_count_stack;
State* succ_tgba_ = 0;
size_t size_tgba_ = 0;
succ_queue& queue = todo.back().q;
Diff_succ(old_state->left(), new_state->left(),
&succ_tgba_, &size_tgba_);
for (size_t i = 0; i < size_tgba_; i++)
{
state_gspn_ssp* s =
new state_gspn_ssp
(succ_tgba_[i],
old_state->right()->clone());
queue.push_back(successor(queue.begin()->acc,
s));
inc_depth();
}
if (size_tgba_ != 0)
diff_succ_free(succ_tgba_);
break;
} }
if (size_tgba_ != 0)
diff_succ_free(succ_tgba_);
break;
} }
} }
} }
} }
if (j != l.end())
{
if (s != *j)
{
delete s;
s = *j;
}
}
else
{
s = 0;
}
}
else
{
s = 0;
} }
// s points to the resulting state, or to 0 if we didn't find
// the state in the list.
numbered_state_heap::state_index_p res; numbered_state_heap::state_index_p res;
if (i == h.end()) if (s == 0)
{ {
res.first = 0; res.first = 0;
res.second = 0; res.second = 0;
} }
else else
{ {
res.first = i->first; hash_type::iterator k = h.find(s);
res.second = &i->second; assert(k != h.end());
assert(s == k->first);
if (s != i->first) res.first = k->first;
delete s; res.second = &k->second;
} }
return res; return res;
} }
@ -1036,11 +1144,14 @@ namespace spot
option_map(), option_map(),
numbered_state_heap_ssp_factory_semi::instance()), numbered_state_heap_ssp_factory_semi::instance()),
inclusion_count(0) inclusion_count(0)
{ {
stats["inclusion count"] = stats["find_state count"] =
static_cast<spot::unsigned_statistics::unsigned_fun> static_cast<spot::unsigned_statistics::unsigned_fun>
(&couvreur99_check_shy_semi_ssp::get_inclusion_count); (&couvreur99_check_shy_semi_ssp::get_inclusion_count);
} stats["contained map size"] =
static_cast<spot::unsigned_statistics::unsigned_fun>
(&couvreur99_check_shy_semi_ssp::get_contained_map_size);
}
private: private:
unsigned inclusion_count; unsigned inclusion_count;
@ -1051,6 +1162,12 @@ namespace spot
{ {
return inclusion_count; return inclusion_count;
}; };
unsigned
get_contained_map_size() const
{
return
dynamic_cast<numbered_state_heap_ssp_semi*>(ecs_->h)->contained.size();
}
virtual numbered_state_heap::state_index_p virtual numbered_state_heap::state_index_p
find_state(const state* s) find_state(const state* s)

9
iface/gspn/ssp.hh
View file

@ -1,6 +1,6 @@
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// et Marie Curie. // Université Pierre et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -40,7 +40,8 @@ namespace spot
public: public:
gspn_ssp_interface(int argc, char **argv, gspn_ssp_interface(int argc, char **argv,
bdd_dict* dict, const ltl::declarative_environment& env, bdd_dict* dict, const ltl::declarative_environment& env,
bool inclusion = false); bool inclusion = false,
bool doublehash = true);
~gspn_ssp_interface(); ~gspn_ssp_interface();
tgba* automaton(const tgba* operand) const; tgba* automaton(const tgba* operand) const;
private: private: