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",