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

* src/tgbaalgos/compsusp.cc: Use tgba_digraph.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2014-08-05 17:15:49 +02:00
parent 5dd731eab6
commit 38887f4960
1 changed files with 11 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/tgbaalgos/compsusp.cc
View file

@ -20,7 +20,7 @@
#include "compsusp.hh" #include "compsusp.hh"
#include "sccfilter.hh" #include "sccfilter.hh"
#include "scc.hh" #include "scc.hh"
#include "tgba/tgbaexplicit.hh" #include "tgba/tgbagraph.hh"
#include "ltl2tgba_fm.hh" #include "ltl2tgba_fm.hh"
#include "minimize.hh" #include "minimize.hh"
#include "simulation.hh" #include "simulation.hh"
@ -207,7 +207,7 @@ namespace spot
typedef std::pair<const state*, const state*> state_pair; typedef std::pair<const state*, const state*> state_pair;
typedef std::map<state_pair, int> pair_map; typedef std::map<state_pair, unsigned> pair_map;
typedef std::deque<state_pair> pair_queue; typedef std::deque<state_pair> pair_queue;
static static
@ -222,7 +222,7 @@ namespace spot
const tgba* right = iterated_simulations(a2); const tgba* right = iterated_simulations(a2);
delete a2; delete a2;
tgba_explicit_number* res = new tgba_explicit_number(dict); tgba_digraph* res = new tgba_digraph(dict);
dict->register_all_variables_of(left, res); dict->register_all_variables_of(left, res);
dict->register_all_variables_of(right, res); dict->register_all_variables_of(right, res);
dict->unregister_variable(bdd_var(v), res); dict->unregister_variable(bdd_var(v), res);
@ -263,11 +263,10 @@ namespace spot
state_pair p(left->get_init_state(), 0); state_pair p(left->get_init_state(), 0);
state* ris = right->get_init_state(); state* ris = right->get_init_state();
p.second = ris; p.second = ris;
seen[p] = 0; unsigned i = res->new_state();
seen[p] = i;
todo.push_back(p); todo.push_back(p);
res->set_init_state(0); res->set_init_state(i);
typedef state_explicit_number::transition trans;
while (!todo.empty()) while (!todo.empty())
{ {
@ -317,22 +316,21 @@ namespace spot
ra = (ri->current_acceptance_conditions() & rma) | radd; ra = (ri->current_acceptance_conditions() & rma) | radd;
} }
int dest = seen.size(); int dest;
pair_map::const_iterator i = seen.find(d); pair_map::const_iterator i = seen.find(d);
if (i != seen.end()) if (i != seen.end()) // Is this an existing state?
{ {
dest = i->second; dest = i->second;
} }
else else
{ {
dest = res->new_state();
seen[d] = dest; seen[d] = dest;
todo.push_back(d); todo.push_back(d);
} }
trans* t = res->create_transition(src, dest);
t->condition = bdd_exist(cond, v);
bdd la = (li->current_acceptance_conditions() & lma) | ladd; bdd la = (li->current_acceptance_conditions() & lma) | ladd;
t->acceptance_conditions = ra & la; res->new_transition(src, dest, bdd_exist(cond, v), ra & la);
if (ri) if (ri)
ri->next(); ri->next();
@ -345,11 +343,11 @@ namespace spot
} }
delete left; delete left;
delete right; delete right;
return res; return res;
} }
} }
tgba* tgba*
compsusp(const ltl::formula* f, bdd_dict* dict, compsusp(const ltl::formula* f, bdd_dict* dict,
bool no_wdba, bool no_simulation, bool no_wdba, bool no_simulation,