From 8c48003943ee51a8741ce5fc45471821f3297050 Mon Sep 17 00:00:00 2001 From: Florian Renkin Date: Wed, 15 Apr 2020 11:15:27 +0200 Subject: [PATCH] to_parity: Use merge_states * spot/twaalgos/toparity.cc: Use merge_states at the end of to_parity. * tests/python/toparity.py: Update tests. --- spot/twaalgos/toparity.cc | 1 + tests/python/toparity.py | 8 ++++---- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/spot/twaalgos/toparity.cc b/spot/twaalgos/toparity.cc index 0351e12a8..056daaf40 100644 --- a/spot/twaalgos/toparity.cc +++ b/spot/twaalgos/toparity.cc @@ -1684,6 +1684,7 @@ run() res_->set_named_prop("state-names", names); reduce_parity_here(res_); res_->purge_unreachable_states(); + res_->merge_states(); return res_; } diff --git a/tests/python/toparity.py b/tests/python/toparity.py index 8301789b3..237dacb05 100644 --- a/tests/python/toparity.py +++ b/tests/python/toparity.py @@ -195,7 +195,7 @@ State: 13 [0&1] 5 [!0&!1] 10 {0 1 3 5} [0&!1] 13 {1 3} ---END--"""), [35, 28, 23, 30, 29, 25, 22]) +--END--"""), [31, 27, 23, 28, 28, 24, 22]) test(spot.automaton(""" HOA: v1 @@ -288,7 +288,7 @@ State: 4 [0&!1] 4 [0&1] 4 {1 2 4} --END-- -"""), [9, 6, 7, 7, 6, 6, 6]) +"""), [8, 6, 7, 7, 6, 6, 6]) test(spot.automaton(""" HOA: v1 @@ -341,7 +341,7 @@ explicit-labels trans-acc --BODY-- State: 0 [0&1] 2 {4 5} [0&1] 4 {0 4} p = spot.to_parity_old(a, True) assert p.num_states() == 22 assert spot.are_equivalent(a, p) -test(a, [8, 7, 8, 8, 6, 7, 6]) +test(a, [6, 6, 6, 6, 6, 6, 6]) # Force a few edges to false, to make sure to_parity() is OK with that. for e in a.out(2): @@ -371,4 +371,4 @@ for f in spot.randltl(5, 2000): a = spot.translate('!(GFa -> (GFb & GF(!b & !Xb)))', 'gen', 'det') b = spot.to_parity_old(a, True) assert a.equivalent_to(b) -test(a, [7, 7, 3, 7, 8, 7, 3]) +test(a, [6, 6, 3, 6, 7, 6, 3])