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

* iface/gspn/eesrg.cc (connected_component_eesrg::has_state):

Browse source 
Free filtered states.
(emptiness_check_shy_eesrg): New class.
(emptiness_check_eesrg_shy): New function.
* iface/gspn/eesrg.hh (emptiness_check_eesrg_shy): New function.
* iface/gspn/ltlgspn.cc (main) [EESRG]: Handle -e3, -e4, and -e5.
* * src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gtec/gtec.cc
(emptiness_check_shy::check): Move arc, num, succ_queue, and todo
as attributes.
(emptiness_check_shy::find_state): New virtual function.
This commit is contained in:
Alexandre Duret-Lutz 2004-04-15 09:12:11 +00:00
parent 1e360ec689
commit be4f4e3370
6 changed files with 189 additions and 42 deletions
Download patch file Download diff file Expand all files Collapse all files

14
ChangeLog
View file

@ -1,3 +1,17 @@
2004-04-15 Soheib Baarir <Souheib.Baarir@lip6.fr>
Alexandre Duret-Lutz <adl@src.lip6.fr>
* iface/gspn/eesrg.cc (connected_component_eesrg::has_state):
Free filtered states.
(emptiness_check_shy_eesrg): New class.
(emptiness_check_eesrg_shy): New function.
* iface/gspn/eesrg.hh (emptiness_check_eesrg_shy): New function.
* iface/gspn/ltlgspn.cc (main) [EESRG]: Handle -e3, -e4, and -e5.
* * src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gtec/gtec.cc
(emptiness_check_shy::check): Move arc, num, succ_queue, and todo
as attributes.
(emptiness_check_shy::find_state): New virtual function.
2004-04-14 Soheib Baarir <Souheib.Baarir@lip6.fr>
Alexandre Duret-Lutz <adl@src.lip6.fr>

90
iface/gspn/eesrg.cc
View file

@ -440,7 +440,7 @@ namespace spot
size_t size_tgba_ = 0;
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++)
{
@ -580,7 +580,11 @@ namespace spot
&& old_state->left()
&& new_state->left())
if (spot_inclusion(new_state->left(), old_state->left()))
return (*i);
{
if (*i != s)
delete s;
return *i;
}
}
return 0;
}
@ -732,6 +736,7 @@ namespace spot
hash_type h; ///< Map of visited states.
friend class numbered_state_heap_eesrg_const_iterator;
friend class emptiness_check_shy_eesrg;
};
@ -784,6 +789,7 @@ namespace spot
const numbered_state_heap_eesrg_semi::hash_type& h;
};
numbered_state_heap_const_iterator*
numbered_state_heap_eesrg_semi::iterator() const
{
@ -824,6 +830,79 @@ namespace spot
};
class emptiness_check_shy_eesrg : public emptiness_check_shy
{
public:
emptiness_check_shy_eesrg(const tgba* a)
: emptiness_check_shy(a,
numbered_state_heap_eesrg_factory_semi::instance())
{
}
protected:
virtual int*
find_state(const state* s)
{
typedef numbered_state_heap_eesrg_semi::hash_type hash_type;
hash_type& h = dynamic_cast<numbered_state_heap_eesrg_semi*>(ecs_->h)->h;
hash_type::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())
{
if (i->second == -1)
{
if (spot_inclusion(new_state->left(), old_state->left()))
break;
}
else
{
if (spot_inclusion(old_state->left(), new_state->left()))
{
State* succ_tgba_ = NULL;
size_t size_tgba_ = 0;
succ_queue& queue = todo.top().second;
Diff_succ(old_state->left(), new_state->left(),
&succ_tgba_, &size_tgba_);
for (size_t i = 0; i < size_tgba_; i++)
{
state_gspn_eesrg* s =
new state_gspn_eesrg
(succ_tgba_[i],
old_state->right()->clone());
queue.push_back(successor(queue.begin()->acc, s));
}
if (size_tgba_ != 0)
diff_succ_free(succ_tgba_);
break;
}
}
}
}
}
if (i == h.end())
return 0;
return &i->second;
}
};
emptiness_check*
emptiness_check_eesrg_semi(const tgba* eesrg_automata)
{
@ -843,6 +922,13 @@ namespace spot
numbered_state_heap_eesrg_factory_semi::instance());
}
emptiness_check*
emptiness_check_eesrg_shy(const tgba* eesrg_automata)
{
assert(dynamic_cast<const tgba_gspn_eesrg*>(eesrg_automata));
return new emptiness_check_shy_eesrg(eesrg_automata);
}
counter_example*
counter_example_eesrg(const emptiness_check_status* status)
{

2
iface/gspn/eesrg.hh
View file

@ -48,6 +48,8 @@ namespace spot
emptiness_check* emptiness_check_eesrg_semi(const tgba* eesrg_automata);
emptiness_check* emptiness_check_eesrg_shy_semi(const tgba* eesrg_automata);
emptiness_check* emptiness_check_eesrg_shy(const tgba* eesrg_automata);
counter_example* counter_example_eesrg(const emptiness_check_status* status);
}

59
iface/gspn/ltlgspn.cc
View file

@ -53,7 +53,15 @@ syntax(char* prog)
<< " (instead of just checking for emptiness)" << std::endl
<< std::endl
<< " -e use Couvreur's emptiness-check (default)" << std::endl
<< " -e2 use Couvreur's emptiness-check variant" << std::endl
<< " -e2 use Couvreur's emptiness-check's shy variant" << std::endl
#ifdef EESRG
<< " -e3 use semi-d. incl. Couvreur's emptiness-check"
<< std::endl
<< " -e4 use semi-d. incl. Couvreur's emptiness-check's shy variant"
<< std::endl
<< " -e5 use d. incl. Couvreur's emptiness-check's shy variant"
<< std::endl
#endif
<< " -m degeneralize and perform a magic-search" << std::endl
<< std::endl
<< " -l use Couvreur's LaCIM algorithm for translation (default)"
@ -68,7 +76,8 @@ main(int argc, char **argv)
try
{
int formula_index = 1;
enum { Couvreur, Couvreur2, Magic } check = Couvreur;
enum { Couvreur, Couvreur2, Couvreur3,
Couvreur4, Couvreur5, Magic } check = Couvreur;
enum { Lacim, Fm } trans = Lacim;
bool compute_counter_example = false;
bool proj = true;
@ -89,6 +98,18 @@ main(int argc, char **argv)
{
check = Couvreur2;
}
else if (!strcmp(argv[formula_index], "-e3"))
{
check = Couvreur3;
}
else if (!strcmp(argv[formula_index], "-e4"))
{
check = Couvreur4;
}
else if (!strcmp(argv[formula_index], "-e5"))
{
check = Couvreur5;
}
else if (!strcmp(argv[formula_index], "-m"))
{
check = Magic;
@ -169,20 +190,34 @@ main(int argc, char **argv)
{
case Couvreur:
case Couvreur2:
case Couvreur3:
case Couvreur4:
case Couvreur5:
{
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);
switch (check)
{
case Couvreur:
ec = new spot::emptiness_check(prod);
break;
case Couvreur2:
ec = new spot::emptiness_check_shy(prod);
break;
#ifdef EESRG
case Couvreur3:
ec = spot::emptiness_check_eesrg_semi(prod);
break;
case Couvreur4:
ec = spot::emptiness_check_eesrg_shy_semi(prod);
break;
case Couvreur5:
ec = spot::emptiness_check_eesrg_shy(prod);
break;
#endif
default:
assert(0);
}
bool res = ec->check();

41
src/tgbaalgos/gtec/gtec.cc
View file

@ -237,43 +237,21 @@ namespace spot
emptiness_check_shy::emptiness_check_shy(const tgba* a,
const numbered_state_heap_factory*
nshf)
: emptiness_check(a, nshf)
: emptiness_check(a, nshf), num(1)
{
// Setup depth-first search from the initial state.
todo.push(pair_state_successors(0, succ_queue()));
todo.top().second.push_front(successor(bddtrue,
ecs_->aut->get_init_state()));
}
emptiness_check_shy::~emptiness_check_shy()
{
}
struct successor {
bdd acc;
const spot::state* s;
successor(bdd acc, const spot::state* s): acc(acc), s(s) {}
};
bool
emptiness_check_shy::check()
{
// We use five main data in this algorithm:
// * emptiness_check::root, a stack of strongly connected components (SCC),
// * emptiness_check::h, a hash of all visited nodes, with their order,
// (it is called "Hash" in Couvreur's paper)
// * arc, a stack of acceptance conditions between each of these SCC,
std::stack<bdd> arc;
// * num, the number of visited nodes. Used to set the order of each
// visited node,
int num = 1;
// * todo, the depth-first search stack. This holds pairs of the
// form (STATE, SUCCESSORS) where SUCCESSORS is a list of
// (ACCEPTANCE_CONDITIONS, STATE) pairs.
typedef std::list<successor> succ_queue;
typedef std::pair<const state*, succ_queue> pair_state_successors;
std::stack<pair_state_successors> todo;
// Setup depth-first search from the initial state.
todo.push(pair_state_successors(0, succ_queue()));
todo.top().second.push_front(successor(bddtrue,
ecs_->aut->get_init_state()));
for (;;)
{
@ -288,7 +266,7 @@ namespace spot
succ_queue::iterator q = queue.begin();
while (q != queue.end())
{
int* i = ecs_->h->find(q->s);
int* i = find_state(q->s);
if (!i)
{
// Skip unknown states.
@ -414,4 +392,11 @@ namespace spot
delete iter;
}
}
int*
emptiness_check_shy::find_state(const state* s)
{
return ecs_->h->find(s);
}
}

25
src/tgbaalgos/gtec/gtec.hh
View file

@ -111,6 +111,31 @@ namespace spot
virtual ~emptiness_check_shy();
virtual bool check();
protected:
struct successor {
bdd acc;
const spot::state* s;
successor(bdd acc, const spot::state* s): acc(acc), s(s) {}
};
// We use five main data in this algorithm:
// * emptiness_check::root, a stack of strongly connected components (SCC),
// * emptiness_check::h, a hash of all visited nodes, with their order,
// (it is called "Hash" in Couvreur's paper)
// * arc, a stack of acceptance conditions between each of these SCC,
std::stack<bdd> arc;
// * num, the number of visited nodes. Used to set the order of each
// visited node,
int num;
// * todo, the depth-first search stack. This holds pairs of the
// form (STATE, SUCCESSORS) where SUCCESSORS is a list of
// (ACCEPTANCE_CONDITIONS, STATE) pairs.
typedef std::list<successor> succ_queue;
typedef std::pair<const state*, succ_queue> pair_state_successors;
std::stack<pair_state_successors> todo;
virtual int* find_state(const state* s);
};
}