From 621fb818e333c1a748fbcbacb4c657089c75f701 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 20 Jun 2018 17:46:11 +0200 Subject: [PATCH] improve translation of ms-phi-h=2..3 * spot/twaalgos/gfguarantee.cc: Rework the history computation to keep an overapproximation of the history, and a longer one. Also replay the history even if there is no initial trivial SCC. This helps with translating FG(!a|XXXb) where we need to keep the history of a, but we were previously unable to do so because some state had both "a" and "ab" as input. * spot/twaalgos/translate.cc: Optimize the product of suspendable automata by removing useless trivial SCCs. * tests/core/genltl.test, tests/core/satmin.test, NEWS: Adjust expected results. --- NEWS | 4 +- spot/twaalgos/gfguarantee.cc | 168 ++++++++++++++++++++++++----------- spot/twaalgos/translate.cc | 14 +++ tests/core/genltl.test | 6 +- tests/core/satmin.test | 4 +- 5 files changed, 135 insertions(+), 61 deletions(-) diff --git a/NEWS b/NEWS index 9fa1a4a2f..61d1023de 100644 --- a/NEWS +++ b/NEWS @@ -113,8 +113,8 @@ New in spot 2.5.3.dev (not yet released) (GFa1 & GFa2) -> GFz 12 1 1 (GFa1 & GFa2 & GFa3) -> GFz 41 1 1 FG(a|b)|FG(!a|Xb) 4 2 2 - FG(a|b)|FG(!a|Xb)|FG(a|XXb) 21 5 4 - FG(a|b)|FG(!a|Xb)|FG(a|XXb)|FG(!a|XXXb) 170 15 8 + FG(a|b)|FG(!a|Xb)|FG(a|XXb) 21 4 4 + FG(a|b)|FG(!a|Xb)|FG(a|XXb)|FG(!a|XXXb) 170 8 8 - print_dot(), used to print automata in GraphViz's format, underwent several changes: diff --git a/spot/twaalgos/gfguarantee.cc b/spot/twaalgos/gfguarantee.cc index b17e7c991..0c37cbf44 100644 --- a/spot/twaalgos/gfguarantee.cc +++ b/spot/twaalgos/gfguarantee.cc @@ -27,6 +27,7 @@ #include #include #include +// #include namespace spot { @@ -54,6 +55,7 @@ namespace spot static twa_graph_ptr do_g_f_terminal_inplace(scc_info& si, bool state_based) { + bool want_merge_edges = false; twa_graph_ptr aut = std::const_pointer_cast(si.get_aut()); if (!is_terminal_automaton(aut, &si, true)) @@ -82,56 +84,56 @@ namespace spot // state. However if some successor of the initial state is // also trivial, we might be able to remove it as well if we // are able to replay two step from the initial state: this - // can be generalized to more depth and require computing some - // history for each state (i.e., a common suffix to all finite - // words leading to this state). + // can be generalized to more depth and requires computing + // some history for each state (i.e., a common suffix to all + // finite words leading to this state). + // + // We will replay such histories regardless of whether there + // is actually some trivial leading SCCs that could be + // removed, because it reduces the size of cycles in the + // automaton, and this helps getting smaller products when + // combining several automata generated this way. std::vector> histories; bool initial_state_trivial = si.is_trivial(si.initial()); - if (is_det && initial_state_trivial) + if (is_det) { // Compute the max number of steps we want to keep in - // the history of each state. This is the largest - // number of trivial SCCs you can chain from the initial - // state. - unsigned max_histories = 1; + // the history of each state. This is the length of the + // maximal path we can build from the initial state. + unsigned max_histories; { std::vector depths(ns, 0U); - for (unsigned d: si.succ(ns - 1)) - depths[d] = 2; - for (int scc = ns - 2; scc >= 0; --scc) + for (unsigned scc = 0; scc < ns; ++scc) { - if (!si.is_trivial(scc)) - continue; - unsigned sccd = depths[scc]; - max_histories = std::max(max_histories, sccd); - ++sccd; - for (unsigned d: si.succ(scc)) - depths[d] = std::max(depths[d], sccd); + unsigned depth = 0; + for (unsigned succ: si.succ(scc)) + depth = std::max(depth, depths[succ]); + depths[scc] = depth + si.states_of(scc).size(); } + max_histories = depths[ns - 1] - 1; } unsigned numstates = aut->num_states(); histories.resize(numstates); // Compute the one-letter history of each state. If all - // transition entering a state have the same label, the history - // is that label. Otherwise set it to bddfalse. + // transition entering a state have the same label, the + // history is that label. Otherwise, we make a + // disjunction of all those labels, so that what we have + // is an over-approximation of the history. for (auto& e: aut->edges()) { std::vector& hd = histories[e.dst]; if (hd.empty()) hd.push_back(e.cond); - else if (hd[0] != e.cond) - hd[0] = bddfalse; + else + hd[0] |= e.cond; } - // remove all bddfalse, and check if there is a chance to build - // a larger history. + // check if there is a chance to build a larger history. bool should_continue = false; for (auto&h: histories) if (h.empty()) continue; - else if (h[0] == bddfalse) - h.pop_back(); else should_continue = true; // Augment those histories with more letters. @@ -152,10 +154,12 @@ namespace spot else hd.push_back(bddfalse); } - else if (hs.size() < historypos - || hd[historypos] != hs[historypos - 1]) + else { - hd[historypos] = bddfalse; + if (hs.size() >= historypos) + hd[historypos] |= hs[historypos - 1]; + else + hd[historypos] = bddfalse; } } } @@ -163,7 +167,6 @@ namespace spot for (unsigned n = 0; n < numstates; ++n) { auto& h = histories[n]; - //for (auto&h: histories) if (h.size() <= historypos) continue; else if (h[historypos] == bddfalse) @@ -196,10 +199,14 @@ namespace spot // It will loop if (term[si.scc_of(e.dst)]) { - if (!initial_state_trivial - // If the source state is the initial state, we - // should not try to combine it with itself... - || e.src == init) + // If the source state is the initial state, we + // should not try to combine it with itself... + // + // Also if the automaton is not deterministic + // and there is no trivial initial state, then + // we simply loop back to the initial state. + if (e.src == init + || (!is_det && !initial_state_trivial)) { e.dst = init; e.acc = {0}; @@ -224,11 +231,13 @@ namespace spot // history will get us back the terminal state. In both // cases, we should try again with a smaller history. unsigned moved_init = init; + bdd econd = e.cond; + bool first; if (is_det) { auto& h = histories[e.src]; int hsize = h.size(); - for (int hlen = hsize - 1; hlen > 0; --hlen) + for (int hlen = hsize - 1; hlen >= 0; --hlen) { for (int pos = hlen - 1; pos >= 0; --pos) { @@ -248,36 +257,85 @@ namespace spot } // we have successfully played all history // to a non-terminal state. + // + // Combine this edge with any compatible edge from + // the initial state. + first = true; + for (auto& ei: aut->out(moved_init)) + { + bdd cond = ei.cond & econd; + if (cond != bddfalse) + { + // We should never reach the terminal state, + // unless the history is empty. In that + // case (ts=true) we have to make a loop to + // the initial state without any + // combination. + bool ts = term[si.scc_of(ei.dst)]; + if (ts && hlen > 0) + goto failed; + if (ts) + want_merge_edges = true; + if (first) + { + e.acc = {0}; + e.cond = cond; + first = false; + if (!ts) + { + e.dst = ei.dst; + if (new_init == -1U) + new_init = e.src; + } + else + { + new_init = e.dst = init; + } + } + else + { + if (ts) + { + aut->new_edge(e.src, init, cond, {0}); + new_init = init; + } + else + { + aut->new_edge(e.src, ei.dst, + cond, {0}); + } + } + + } + } break; failed: moved_init = init; continue; } } - // Combine this edge with any compatible edge from - // the initial state. - bdd econd = e.cond; - bool first = true; - for (auto& ei: aut->out(moved_init)) + else { - bdd cond = ei.cond & econd; - if (cond != bddfalse) + first = true; + for (auto& ei: aut->out(moved_init)) { - if (first) + bdd cond = ei.cond & econd; + if (cond != bddfalse) { - e.dst = ei.dst; - e.acc = {0}; - e.cond = cond; - first = false; - if (new_init == -1U) - new_init = e.src; + if (first) + { + e.dst = ei.dst; + e.acc = {0}; + e.cond = cond; + first = false; + } + else + { + aut->new_edge(e.src, ei.dst, cond, {0}); + } } - else - { - aut->new_edge(e.src, ei.dst, cond, {0}); - } - } + } } else @@ -315,6 +373,8 @@ namespace spot } aut->purge_unreachable_states(); + if (want_merge_edges) + aut->merge_edges(); return aut; } } diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc index 603d77051..7fb429414 100644 --- a/spot/twaalgos/translate.cc +++ b/spot/twaalgos/translate.cc @@ -27,6 +27,7 @@ #include #include #include +#include namespace spot { @@ -264,6 +265,19 @@ namespace spot else susp_aut = product_or(susp_aut, one); } + if (susp_aut->prop_universal().is_true()) + { + // In a deterministic and suspendable automaton, all + // state recognize the same language, so we can move + // the initial state into a bottom accepting SCC. + scc_info si(susp_aut, scc_info_options::NONE); + if (si.is_trivial(si.scc_of(susp_aut->get_init_state_number()))) + { + assert(!si.is_trivial(0)); + susp_aut->set_init_state(si.one_state_of(0)); + susp_aut->purge_unreachable_states(); + } + } if (aut == nullptr) aut = susp_aut; else if (is_and) diff --git a/tests/core/genltl.test b/tests/core/genltl.test index 53c11e798..c157da3b9 100755 --- a/tests/core/genltl.test +++ b/tests/core/genltl.test @@ -191,9 +191,9 @@ cat >exp<expected <<'EOF' "!(G((p0) -> ((p1) U (p2))))","15",3 "!(G((p0) -> ((p1) U (p2))))","16",3 "!(G((p0) -> ((p1) U (p2))))","17",3 -"G(F((p0) <-> (X(X(p1)))))","1",6 -"G(F((p0) <-> (X(X(p1)))))","2",6 +"G(F((p0) <-> (X(X(p1)))))","1",4 +"G(F((p0) <-> (X(X(p1)))))","2",4 "G(F((p0) <-> (X(X(p1)))))","3",4 "G(F((p0) <-> (X(X(p1)))))","4",4 "G(F((p0) <-> (X(X(p1)))))","6",4