From b434ac7f8a4c1394b3333771258af54eced9389c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 23 May 2020 12:00:56 +0200 Subject: [PATCH] simplify_acc: perform unit-propagation earlier 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. --- spot/twaalgos/cleanacc.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spot/twaalgos/cleanacc.cc b/spot/twaalgos/cleanacc.cc index 667f2e59e..5a59dad6d 100644 --- a/spot/twaalgos/cleanacc.cc +++ b/spot/twaalgos/cleanacc.cc @@ -622,9 +622,9 @@ namespace spot if (aut->acc().is_generalized_buchi()) break; acc_cond::acc_code old = aut->get_acceptance(); + aut->set_acceptance(aut->acc().unit_propagation()); simplify_complementary_marks_here(aut); fuse_marks_here(aut); - aut->set_acceptance(aut->acc().unit_propagation()); if (old == aut->get_acceptance()) break; }