From e87d308eba366db5bda2a7210d0d27639106ddcb Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 30 May 2018 10:01:52 +0200 Subject: [PATCH] improve alternation removal to match G&O construction When dealternating the VWAA for GFa, our result had two states that could not be fused by simulation because of unmatched acceptance mark. With this change, the result can be simplified. * spot/twaalgos/alternation.cc: Here. * tests/core/alternating.test, tests/python/alternation.ipynb: Update test case. * NEWS: Mention it. --- NEWS | 5 +++ spot/twaalgos/alternation.cc | 28 ++++++++++++++- tests/core/alternating.test | 2 +- tests/python/alternation.ipynb | 62 +++++++++++++++------------------- 4 files changed, 61 insertions(+), 36 deletions(-) diff --git a/NEWS b/NEWS index 23c15f3d1..ff2925ce6 100644 --- a/NEWS +++ b/NEWS @@ -110,6 +110,11 @@ New in spot 2.5.3.dev (not yet released) The code was buggy, hard to maintain, and these functions do not seem to be used. + - spot::remove_alternation() was slightly improved on very-weak + alternating automata: the labeling of the outgoing transitions in + the resulting TGBA makes it more likely that simulation-based + reductions will reduce it. + Python: - New spot.jupyter package. This currently contains a function for diff --git a/spot/twaalgos/alternation.cc b/spot/twaalgos/alternation.cc index 40f0a2a42..290e80f8a 100644 --- a/spot/twaalgos/alternation.cc +++ b/spot/twaalgos/alternation.cc @@ -184,6 +184,7 @@ namespace spot std::map var_to_state_; std::vector scc_to_var_; std::map var_to_mark_; + std::vector mark_to_state_; bdd all_vars_; bdd all_marks_; bdd all_states_; @@ -223,6 +224,7 @@ namespace spot unsigned nc = si_.scc_count(); scc_to_var_.reserve(nc); unsigned mark_pos = has_reject_more_; + mark_to_state_.resize(mark_pos); bdd all_marks = bddtrue; for (unsigned s = 0; s < nc; ++s) { @@ -231,6 +233,7 @@ namespace spot { int v = d->register_anonymous_variables(1, this); scc_to_var_.emplace_back(v); + mark_to_state_.push_back(si_.one_state_of(c)); var_to_mark_.emplace(v, acc_cond::mark_t({mark_pos++})); bdd bv = bdd_ithvar(v); all_marks &= bv; @@ -270,7 +273,7 @@ namespace spot marked && (scc_s == scc_d) && (c == scc_class::reject_more); dest &= bdd_ithvar(state_to_var_[d] + mark); if (c == scc_class::reject_1 && scc_s == scc_d) - dest &= bdd_ithvar(scc_to_var_[scc_s]); + dest &= bdd_ithvar(scc_to_var_[scc_d]); } res |= e.cond & dest; } @@ -464,6 +467,29 @@ namespace spot bdd dest = bdd_existcomp(cube, all_vars_); v.clear(); acc_cond::mark_t m = bdd_to_state(dest, v); + + // if there is no promise "f" is between a state + // that does not have f, and a state that have + // "f", we can add one. Doing so will help later + // simplifications performed by postprocessor. An + // example where this is needed is the VWAA + // generated by ltl[23]ba for GFa. Without the + // next loop, the final TGBA has 2 states instead + // of 1. + for (unsigned m1: (all_marks - m).sets()) + { + if (has_reject_more_ && m1 == 0) + continue; + auto& sv = s_to_ss[s]; + unsigned ms = mark_to_state_[m1]; + if (std::find(v.begin(), v.end(), ms) != v.end()) + { + unsigned ms = mark_to_state_[m1]; + if (std::find(sv.begin(), sv.end(), ms) == sv.end()) + m.set(m1); + } + } + unsigned d = new_state(v, has_mark); if (has_mark) m.set(0); diff --git a/tests/core/alternating.test b/tests/core/alternating.test index feb95aa59..6a1798f0f 100755 --- a/tests/core/alternating.test +++ b/tests/core/alternating.test @@ -195,7 +195,7 @@ Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc complete --BODY-- State: 0 -[t] 1 {0} +[t] 1 State: 1 [t] 1 [0] 1 {0} diff --git a/tests/python/alternation.ipynb b/tests/python/alternation.ipynb index c96896f59..10be77db2 100644 --- a/tests/python/alternation.ipynb +++ b/tests/python/alternation.ipynb @@ -1373,7 +1373,7 @@ }, { "cell_type": "code", - "execution_count": 9, + "execution_count": 5, "metadata": {}, "outputs": [ { @@ -1961,7 +1961,7 @@ }, { "cell_type": "code", - "execution_count": 10, + "execution_count": 6, "metadata": {}, "outputs": [ { @@ -2784,37 +2784,37 @@ "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1,3\n", + "\n", + "1,3\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "1\n", - "⓿\n", - "❶\n", + "\n", + "\n", + "1\n", + "⓿\n", + "❶\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "b\n", - "⓿\n", + "\n", + "\n", + "b\n", + "⓿\n", "\n", "\n", "\n", @@ -2825,8 +2825,8 @@ "\n", "\n", "1->2\n", - "\n", - "\n", + "\n", + "\n", "a & b\n", "⓿\n", "❶\n", @@ -2840,10 +2840,9 @@ "\n", "\n", "1->3\n", - "\n", - "\n", - "!b\n", - "⓿\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n", @@ -2854,11 +2853,9 @@ "\n", "\n", "1->4\n", - "\n", + "\n", "\n", - "a & !b\n", - "⓿\n", - "❶\n", + "a & !b\n", "\n", "\n", "\n", @@ -2874,15 +2871,13 @@ "2->4\n", "\n", "\n", - "a & !b\n", - "⓿\n", - "❶\n", + "a & !b\n", "\n", "\n", "\n", "3->1\n", - "\n", - "\n", + "\n", + "\n", "b\n", "⓿\n", "\n", @@ -3028,8 +3023,7 @@ "2->4\n", "\n", "\n", - "a & !b\n", - "⓿\n", + "a & !b\n", "\n", "\n", "\n",