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

ltl2aa: place new state in var_to_state map

Browse source
This commit is contained in:
Antoine Martin 2022-09-06 16:31:50 +02:00
parent bb7a30f1fd
commit e7df1ac42e
1 changed files with 2 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

6
spot/twaalgos/translate_aa.cc
View file

@ -294,10 +294,10 @@ namespace spot
{ {
int v = dict->register_anonymous_variables(1, this); int v = dict->register_anonymous_variables(1, this);
p.first->second = v; p.first->second = v;
var_to_state.emplace(v, st);
unsigned new_st = aut_->new_state(); unsigned new_st = aut_->new_state();
old_to_new.emplace(st, new_st); old_to_new.emplace(st, new_st);
var_to_state.emplace(v, new_st);
vars &= bdd_ithvar(v); vars &= bdd_ithvar(v);
} }
@ -326,9 +326,7 @@ namespace spot
assert(bdd_high(dest) == bddtrue); assert(bdd_high(dest) == bddtrue);
auto it = var_to_state.find(bdd_var(dest)); auto it = var_to_state.find(bdd_var(dest));
assert(it != var_to_state.end()); assert(it != var_to_state.end());
auto it2 = old_to_new.find(it->second); univ_dest.push_back(it->second);
assert(it2 != old_to_new.end());
univ_dest.push_back(it2->second);
dest = bdd_low(dest); dest = bdd_low(dest);
} }