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

simplify_acc: perform unit-propagation earlier

Browse source 
Closes #405.   This shows no difference on the test suite,
but that is thanks to the previous patch: without it, an
example in automata.ipynb would have an extra edge.

* spot/twaalgos/cleanacc.cc (simplify_acceptance): Call
unit_propagation() before simplify_complementary_marks_here() and
fuse_marks_here(), because that is simpler to perform.
This commit is contained in:
Alexandre Duret-Lutz 2020-05-23 12:00:56 +02:00
parent b762f54228
commit b434ac7f8a
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
spot/twaalgos/cleanacc.cc
View file

@ -622,9 +622,9 @@ namespace spot
if (aut->acc().is_generalized_buchi()) if (aut->acc().is_generalized_buchi())
break; break;
acc_cond::acc_code old = aut->get_acceptance(); acc_cond::acc_code old = aut->get_acceptance();
aut->set_acceptance(aut->acc().unit_propagation());
simplify_complementary_marks_here(aut); simplify_complementary_marks_here(aut);
fuse_marks_here(aut); fuse_marks_here(aut);
aut->set_acceptance(aut->acc().unit_propagation());
if (old == aut->get_acceptance()) if (old == aut->get_acceptance())
break; break;
} }