* iface/gspn/ltlgspn.cc (connected_component_eesrg,
connected_component_eesrg_factory, numbered_state_heap_eesrg_semi, numbered_state_heap_eesrg_const_iterator, numbered_state_heap_eesrg_factory_semi): New classes. (emptiness_check_eesrg_semi, emptiness_check_eesrg_shy_semi, counter_example_eesrg): New functions. * iface/gspn/eesrg.hh (emptiness_check_eesrg_semi, emptiness_check_eesrg_shy_semi, counter_example_eesrg): New functions. * iface/gspn/ltlgspn.cc [EESRG]: Adjust to call these new functions.
This commit is contained in:
Alexandre Duret-Lutz
parent
5d4affc5d7
commit
1e360ec689
4 changed files with 331 additions and 3 deletions
14
ChangeLog
14
ChangeLog
|
|
@ -1,3 +1,17 @@
|
|||
2004-04-14 Soheib Baarir <Souheib.Baarir@lip6.fr>
|
||||
Alexandre Duret-Lutz <adl@src.lip6.fr>
|
||||
|
||||
* iface/gspn/ltlgspn.cc (connected_component_eesrg,
|
||||
connected_component_eesrg_factory, numbered_state_heap_eesrg_semi,
|
||||
numbered_state_heap_eesrg_const_iterator,
|
||||
numbered_state_heap_eesrg_factory_semi): New classes.
|
||||
(emptiness_check_eesrg_semi, emptiness_check_eesrg_shy_semi,
|
||||
counter_example_eesrg): New functions.
|
||||
* iface/gspn/eesrg.hh (emptiness_check_eesrg_semi,
|
||||
emptiness_check_eesrg_shy_semi, counter_example_eesrg): New
|
||||
functions.
|
||||
* iface/gspn/ltlgspn.cc [EESRG]: Adjust to call these new functions.
|
||||
|
||||
2004-04-14 Soheib Baarir <Souheib.Baarir@lip6.fr>
|
||||
|
||||
* iface/gspn/eesrg.cc (tgba_succ_iterator_gspn_eesrg,
|
||||
|
|
|
|||
|
|
@ -26,6 +26,8 @@
|
|||
#include "eesrg.hh"
|
||||
#include "misc/bddlt.hh"
|
||||
#include <bdd.h>
|
||||
#include "tgbaalgos/gtec/explscc.hh"
|
||||
#include "tgbaalgos/gtec/nsheap.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -553,4 +555,298 @@ namespace spot
|
|||
return new tgba_gspn_eesrg(dict_, env_, operand);
|
||||
}
|
||||
|
||||
|
||||
//////////////////////////////////////////////////////////////////////
|
||||
|
||||
class connected_component_eesrg: public explicit_connected_component
|
||||
{
|
||||
public:
|
||||
virtual
|
||||
~connected_component_eesrg()
|
||||
{
|
||||
}
|
||||
|
||||
virtual const state*
|
||||
has_state(const state* s) const
|
||||
{
|
||||
set_type::iterator i;
|
||||
|
||||
for (i = states.begin(); i !=states.end(); i++)
|
||||
{
|
||||
const state_gspn_eesrg* old_state = (const state_gspn_eesrg*)(*i);
|
||||
const state_gspn_eesrg* new_state = (const state_gspn_eesrg*)(s);
|
||||
|
||||
if ((old_state->right())->compare(new_state->right()) == 0
|
||||
&& old_state->left()
|
||||
&& new_state->left())
|
||||
if (spot_inclusion(new_state->left(), old_state->left()))
|
||||
return (*i);
|
||||
}
|
||||
return 0;
|
||||
}
|
||||
|
||||
virtual void
|
||||
insert(const state* s)
|
||||
{
|
||||
states.insert(s);
|
||||
}
|
||||
|
||||
protected:
|
||||
typedef Sgi::hash_set<const state*,
|
||||
state_ptr_hash, state_ptr_equal> set_type;
|
||||
set_type states;
|
||||
};
|
||||
|
||||
class connected_component_eesrg_factory :
|
||||
public explicit_connected_component_factory
|
||||
{
|
||||
public:
|
||||
virtual connected_component_eesrg*
|
||||
build() const
|
||||
{
|
||||
return new connected_component_eesrg();
|
||||
}
|
||||
|
||||
/// Get the unique instance of this class.
|
||||
static const connected_component_eesrg_factory*
|
||||
instance()
|
||||
{
|
||||
static connected_component_eesrg_factory f;
|
||||
return &f;
|
||||
}
|
||||
|
||||
protected:
|
||||
virtual
|
||||
~connected_component_eesrg_factory()
|
||||
{
|
||||
}
|
||||
/// Construction is forbiden.
|
||||
connected_component_eesrg_factory()
|
||||
{
|
||||
}
|
||||
};
|
||||
|
||||
//////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
class numbered_state_heap_eesrg_semi : public numbered_state_heap
|
||||
{
|
||||
public:
|
||||
virtual
|
||||
~numbered_state_heap_eesrg_semi()
|
||||
{
|
||||
// Free keys in H.
|
||||
hash_type::iterator i = h.begin();
|
||||
while (i != h.end())
|
||||
{
|
||||
// Advance the iterator before deleting the key.
|
||||
const state* s = i->first;
|
||||
++i;
|
||||
delete s;
|
||||
}
|
||||
}
|
||||
|
||||
virtual const int*
|
||||
find(const state* s) const
|
||||
{
|
||||
hash_type::const_iterator i;
|
||||
for (i = h.begin(); i != h.end(); ++i)
|
||||
{
|
||||
const state_gspn_eesrg* old_state =
|
||||
dynamic_cast<const state_gspn_eesrg*>(i->first);
|
||||
const state_gspn_eesrg* new_state =
|
||||
dynamic_cast<const state_gspn_eesrg*>(s);
|
||||
assert(old_state);
|
||||
assert(new_state);
|
||||
|
||||
if ((old_state->right())->compare(new_state->right()) == 0)
|
||||
{
|
||||
if (old_state->left() == new_state->left())
|
||||
break;
|
||||
|
||||
if (old_state->left()
|
||||
&& new_state->left()
|
||||
&& spot_inclusion(new_state->left(),old_state->left()))
|
||||
break;
|
||||
}
|
||||
}
|
||||
if (i == h.end())
|
||||
return 0;
|
||||
return &i->second;
|
||||
}
|
||||
|
||||
virtual int*
|
||||
find(const state* s)
|
||||
{
|
||||
return const_cast<int*>
|
||||
(const_cast<const numbered_state_heap_eesrg_semi*>(this)->find(s));
|
||||
}
|
||||
|
||||
virtual void
|
||||
insert(const state* s, int index)
|
||||
{
|
||||
h[s] = index;
|
||||
}
|
||||
|
||||
virtual int
|
||||
size() const
|
||||
{
|
||||
return h.size();
|
||||
}
|
||||
|
||||
virtual numbered_state_heap_const_iterator* iterator() const;
|
||||
|
||||
virtual const state*
|
||||
filter(const state* s) const
|
||||
{
|
||||
hash_type::const_iterator i;
|
||||
for (i = h.begin(); i != h.end(); ++i)
|
||||
{
|
||||
const state_gspn_eesrg* old_state =
|
||||
dynamic_cast<const state_gspn_eesrg*>(i->first);
|
||||
const state_gspn_eesrg* new_state =
|
||||
dynamic_cast<const state_gspn_eesrg*>(s);
|
||||
assert(old_state);
|
||||
assert(new_state);
|
||||
|
||||
if ((old_state->right())->compare(new_state->right()) == 0)
|
||||
{
|
||||
if (old_state->left() == new_state->left())
|
||||
break;
|
||||
|
||||
if (old_state->left()
|
||||
&& new_state->left()
|
||||
&& spot_inclusion(new_state->left(),old_state->left()))
|
||||
break;
|
||||
}
|
||||
}
|
||||
assert(i != h.end());
|
||||
if (s != i->first)
|
||||
delete s;
|
||||
return i->first;
|
||||
}
|
||||
|
||||
protected:
|
||||
typedef Sgi::hash_map<const state*, int,
|
||||
state_ptr_hash, state_ptr_equal> hash_type;
|
||||
hash_type h; ///< Map of visited states.
|
||||
|
||||
friend class numbered_state_heap_eesrg_const_iterator;
|
||||
};
|
||||
|
||||
|
||||
class numbered_state_heap_eesrg_const_iterator :
|
||||
public numbered_state_heap_const_iterator
|
||||
{
|
||||
public:
|
||||
numbered_state_heap_eesrg_const_iterator
|
||||
(const numbered_state_heap_eesrg_semi::hash_type& h)
|
||||
: numbered_state_heap_const_iterator(), h(h)
|
||||
{
|
||||
}
|
||||
|
||||
~numbered_state_heap_eesrg_const_iterator()
|
||||
{
|
||||
}
|
||||
|
||||
virtual void
|
||||
first()
|
||||
{
|
||||
i = h.begin();
|
||||
}
|
||||
|
||||
virtual void
|
||||
next()
|
||||
{
|
||||
++i;
|
||||
}
|
||||
|
||||
virtual bool
|
||||
done() const
|
||||
{
|
||||
return i == h.end();
|
||||
}
|
||||
|
||||
virtual const state*
|
||||
get_state() const
|
||||
{
|
||||
return i->first;
|
||||
}
|
||||
|
||||
virtual int
|
||||
get_index() const
|
||||
{
|
||||
return i->second;
|
||||
}
|
||||
|
||||
private:
|
||||
numbered_state_heap_eesrg_semi::hash_type::const_iterator i;
|
||||
const numbered_state_heap_eesrg_semi::hash_type& h;
|
||||
};
|
||||
|
||||
numbered_state_heap_const_iterator*
|
||||
numbered_state_heap_eesrg_semi::iterator() const
|
||||
{
|
||||
return new numbered_state_heap_eesrg_const_iterator(h);
|
||||
}
|
||||
|
||||
|
||||
/// \brief Factory for numbered_state_heap_eesrg_semi
|
||||
///
|
||||
/// This class is a singleton. Retrieve the instance using instance().
|
||||
class numbered_state_heap_eesrg_factory_semi:
|
||||
public numbered_state_heap_factory
|
||||
{
|
||||
public:
|
||||
virtual numbered_state_heap_eesrg_semi*
|
||||
build() const
|
||||
{
|
||||
return new numbered_state_heap_eesrg_semi();
|
||||
}
|
||||
|
||||
/// Get the unique instance of this class.
|
||||
static const numbered_state_heap_eesrg_factory_semi*
|
||||
instance()
|
||||
{
|
||||
static numbered_state_heap_eesrg_factory_semi f;
|
||||
return &f;
|
||||
}
|
||||
|
||||
protected:
|
||||
virtual
|
||||
~numbered_state_heap_eesrg_factory_semi()
|
||||
{
|
||||
}
|
||||
|
||||
numbered_state_heap_eesrg_factory_semi()
|
||||
{
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
emptiness_check*
|
||||
emptiness_check_eesrg_semi(const tgba* eesrg_automata)
|
||||
{
|
||||
assert(dynamic_cast<const tgba_gspn_eesrg*>(eesrg_automata));
|
||||
return
|
||||
new emptiness_check(eesrg_automata,
|
||||
numbered_state_heap_eesrg_factory_semi::instance());
|
||||
}
|
||||
|
||||
emptiness_check*
|
||||
emptiness_check_eesrg_shy_semi(const tgba* eesrg_automata)
|
||||
{
|
||||
assert(dynamic_cast<const tgba_gspn_eesrg*>(eesrg_automata));
|
||||
return
|
||||
new emptiness_check_shy
|
||||
(eesrg_automata,
|
||||
numbered_state_heap_eesrg_factory_semi::instance());
|
||||
}
|
||||
|
||||
counter_example*
|
||||
counter_example_eesrg(const emptiness_check_status* status)
|
||||
{
|
||||
return new counter_example(status,
|
||||
connected_component_eesrg_factory::instance());
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -28,6 +28,8 @@
|
|||
# include <string>
|
||||
# include "tgba/tgba.hh"
|
||||
# include "common.hh"
|
||||
# include "tgbaalgos/gtec/gtec.hh"
|
||||
# include "tgbaalgos/gtec/ce.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -44,6 +46,9 @@ namespace spot
|
|||
const gspn_environment& env_;
|
||||
};
|
||||
|
||||
emptiness_check* emptiness_check_eesrg_semi(const tgba* eesrg_automata);
|
||||
emptiness_check* emptiness_check_eesrg_shy_semi(const tgba* eesrg_automata);
|
||||
counter_example* counter_example_eesrg(const emptiness_check_status* status);
|
||||
}
|
||||
|
||||
#endif // SPOT_IFACE_GSPN_EESRG_GSPN_EESRG_HH
|
||||
|
|
|
|||
|
|
@ -172,10 +172,17 @@ main(int argc, char **argv)
|
|||
{
|
||||
spot::emptiness_check* ec;
|
||||
|
||||
#ifndef EESRG
|
||||
if (check == Couvreur)
|
||||
ec = new spot::emptiness_check(prod);
|
||||
else
|
||||
ec = new spot::emptiness_check_shy(prod);
|
||||
#else
|
||||
if (check == Couvreur)
|
||||
ec = spot::emptiness_check_eesrg_semi(prod);
|
||||
else
|
||||
ec = spot::emptiness_check_eesrg_shy_semi(prod);
|
||||
#endif
|
||||
|
||||
bool res = ec->check();
|
||||
|
||||
|
|
@ -184,9 +191,15 @@ main(int argc, char **argv)
|
|||
{
|
||||
if (compute_counter_example)
|
||||
{
|
||||
spot::counter_example ce(ecs);
|
||||
ce.print_result(std::cout, proj ? model : 0);
|
||||
ce.print_stats(std::cout);
|
||||
spot::counter_example* ce;
|
||||
#ifndef EESRG
|
||||
ce = new spot::counter_example(ecs);
|
||||
#else
|
||||
ce = spot::counter_example_eesrg(ecs);
|
||||
#endif
|
||||
ce->print_result(std::cout, proj ? model : 0);
|
||||
ce->print_stats(std::cout);
|
||||
delete ce;
|
||||
}
|
||||
else
|
||||
{
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue