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

* src/twaalgos/simulation.cc: Preserve the unambiguous flag.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2015-05-21 14:30:44 +02:00
parent ef7f96a545
commit 8f2865070e
1 changed files with 2 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/twaalgos/simulation.cc
View file

@ -489,8 +489,6 @@ namespace spot
twa_graph_ptr res = make_twa_graph(a_->get_dict()); twa_graph_ptr res = make_twa_graph(a_->get_dict());
res->copy_ap_of(a_); res->copy_ap_of(a_);
res->copy_acceptance_of(a_); res->copy_acceptance_of(a_);
if (Sba)
res->prop_state_based_acc();
// Non atomic propositions variables (= acc and class) // Non atomic propositions variables (= acc and class)
bdd nonapvars = all_proms_ & bdd_support(all_class_var_); bdd nonapvars = all_proms_ & bdd_support(all_class_var_);
@ -637,7 +635,8 @@ namespace spot
res->prop_copy(original_, res->prop_copy(original_,
{ false, // state-based acc forced below { false, // state-based acc forced below
true, // weakness preserved, true, // weakness preserved,
false, // determinism checked and set below true, // determinism checked and overridden below
// and "unambiguous" property preserved
true, // stutter inv. true, // stutter inv.
}); });
if (nb_minato == nb_satoneset && !Cosimulation) if (nb_minato == nb_satoneset && !Cosimulation)