From 192fb6c1e7232fe5f32161d80268616bf2452778 Mon Sep 17 00:00:00 2001 From: Laurent XU Date: Wed, 29 Mar 2017 00:49:22 +0200 Subject: [PATCH] parity: merge states having same cleaned matrices in parity_product Some states can become identical once their history matrix are cleaned. These states are merged and only store the cleaned matrix. * spot/twaalgos/parity.cc: Here. --- spot/twaalgos/parity.cc | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/spot/twaalgos/parity.cc b/spot/twaalgos/parity.cc index 783621415..f9bc1d298 100644 --- a/spot/twaalgos/parity.cc +++ b/spot/twaalgos/parity.cc @@ -359,18 +359,18 @@ namespace spot return 0; } - state_history make_succ(value_t left_acc_set, value_t right_acc_set) const + state_history make_succ(value_t left_acc_set, + value_t right_acc_set) const { - auto mat = state_history(*this); - mat.clean_here(); + auto mat = state_history(left_num_sets_, right_num_sets_); for (unsigned i = 0; i < right_num_sets_; ++i) { - auto old = mat.get_left(i); + auto old = get_left(i); mat.set_left(i, std::max(left_acc_set, old)); } for (unsigned i = 0; i < left_num_sets_; ++i) { - auto old = mat.get_right(i); + auto old = get_right(i); mat.set_right(i, std::max(right_acc_set, old)); } return mat; @@ -453,18 +453,19 @@ namespace spot } std::pair - push_state_history(sh_label_t label, - value_t left_acc_set, value_t right_acc_set) + push_state_history(sh_label_t label, value_t left_acc_set, + value_t right_acc_set) { state_history new_sh = l2sh_[label]->first; auto succ = new_sh.make_succ(left_acc_set, right_acc_set); auto max_acc_set = succ.get_max_acc_set(); + succ.clean_here(); return std::make_pair(push_state_history(succ), max_acc_set); } std::pair - get_succ(sh_label_t current_sh, - value_t left_acc_set, value_t right_acc_set) + get_succ(sh_label_t current_sh, value_t left_acc_set, + value_t right_acc_set) { auto f_args = std::make_tuple(current_sh, left_acc_set, right_acc_set); auto p = succ_.emplace(f_args, std::make_pair(0, 0));