From 7e9325866f5e170f74368a1083cd81f74d581fd3 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 8 Jun 2018 15:09:10 +0200 Subject: [PATCH] gf_guarantee_to_ba: save states using histories MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This improves gf_guarantee_to_ba() on formulas GF(φ) where the automaton for F(φ) as several leading transiant SCCs. E.g., GF(a <-> XXXa) where we know get results that are as good as those of delag without loosing on the cases where delag's technique would actually produce two big automata. * spot/twaalgos/gfguarantee.cc: Implement this. * spot/twaalgos/gfguarantee.hh, NEWS: Document it. * tests/core/ltl2tgba2.test, tests/core/ltl3ba.test: Add test cases. --- NEWS | 28 ++++-- spot/twaalgos/gfguarantee.cc | 181 ++++++++++++++++++++++++++++++++--- spot/twaalgos/gfguarantee.hh | 11 ++- tests/core/ltl2tgba2.test | 16 ++++ tests/core/ltl3ba.test | 11 ++- 5 files changed, 221 insertions(+), 26 deletions(-) diff --git a/NEWS b/NEWS index 5c73448ee..e4ce3de0a 100644 --- a/NEWS +++ b/NEWS @@ -94,17 +94,27 @@ New in spot 2.5.3.dev (not yet released) simplified to {1} or {SERE} depending on whether SERE accepts the empty word or not. - - gf_guarantee_to_ba() is a specialized construction for - translating formulas of the form GF(guarantee) to BA or DBA, - and fg_safety_to_dca() is a specialized construction for - translating formulas of the form FG(safety) to DCA. These - are slight generalizations of some constructions proposed - by J. Esparza, J. Křentínský, and S. Sickert (LICS'18). + - gf_guarantee_to_ba() is a specialized construction for translating + formulas of the form GF(guarantee) to BA or DBA, and + fg_safety_to_dca() is a specialized construction for translating + formulas of the form FG(safety) to DCA. These are generalizations + of some constructions proposed by J. Esparza, J. Křentínský, and + S. Sickert (LICS'18). These are now used by the main translation routine, and can be - disabled by passing -x '!gf-guarantee' to ltl2tgba. As an - example, the translation of GF(a <-> XXb) to transition-based - Büchi went from 9 to 5 states using that construction. + disabled by passing -x '!gf-guarantee' to ltl2tgba. For example, + here are the size of deterministic transition-based Büchi automata + constructed from four GF(guarantee) formulas with two versions of + Spot, and converted to other types of deterministic automata by + other tools. + + ltl2tgba -D rabinizer 4 + 2.5 2.6 delag ltl2dra + ------------------------- ----------- ------------- + GF(a <-> XXa) 9 4 4 9 + GF(a <-> XXXa) 27 8 8 25 + GF(((a & Xb) | XXc) & Xd) 6 4 16 5 + GF((b | Fa) & (b R Xb)) 6 2 3 3 - Slightly improved log output for the SAT-based minimization functions. The CSV log files now include an additional column diff --git a/spot/twaalgos/gfguarantee.cc b/spot/twaalgos/gfguarantee.cc index 137d513b4..b17e7c991 100644 --- a/spot/twaalgos/gfguarantee.cc +++ b/spot/twaalgos/gfguarantee.cc @@ -75,13 +75,113 @@ namespace spot if (!state_based) { bool is_det = is_deterministic(aut); - bool initial_state_reachable = false; - for (auto& e: aut->edges()) - if (e.dst == init) + + // If the initial state is a trivial SCC, we will be able to + // remove it by combining the transitions leading to the + // terminal state on the transitions leaving the initial + // 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). + std::vector> histories; + bool initial_state_trivial = si.is_trivial(si.initial()); + + if (is_det && initial_state_trivial) + { + // 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; { - initial_state_reachable = true; - break; + std::vector depths(ns, 0U); + for (unsigned d: si.succ(ns - 1)) + depths[d] = 2; + for (int scc = ns - 2; scc >= 0; --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 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. + 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; + } + // remove all bddfalse, and 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. + unsigned historypos = 0; + while (should_continue && historypos + 1 < max_histories) + { + ++historypos; + for (auto& e: aut->edges()) + { + std::vector& hd = histories[e.dst]; + if (hd.size() >= historypos) + { + std::vector& hs = histories[e.src]; + if (hd.size() == historypos) + { + if (hs.size() >= historypos) + hd.push_back(hs[historypos - 1]); + else + hd.push_back(bddfalse); + } + else if (hs.size() < historypos + || hd[historypos] != hs[historypos - 1]) + { + hd[historypos] = bddfalse; + } + } + } + should_continue = false; + 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) + h.pop_back(); + else + should_continue = true; + } + } + // std::cerr << "computed histories:\n"; + // for (unsigned n = 0; n < numstates; ++n) + // { + // std::cerr << n << ": ["; + // for (bdd b: histories[n]) + // bdd_print_formula(std::cerr, aut->get_dict(), b) << ", "; + // std::cerr << '\n'; + // } + } + unsigned nedges = aut->num_edges(); unsigned new_init = -1U; // The loop might add new edges, but we just want to iterate @@ -89,9 +189,14 @@ namespace spot for (unsigned edge = 1; edge <= nedges; ++edge) { auto& e = aut->edge_storage(edge); + // Don't bother with terminal states, they won't be + // reachable anymore. + if (term[si.scc_of(e.src)]) + continue; + // It will loop if (term[si.scc_of(e.dst)]) { - if (initial_state_reachable + if (!initial_state_trivial // If the source state is the initial state, we // should not try to combine it with itself... || e.src == init) @@ -105,11 +210,55 @@ namespace spot // state of the automaton, we can get rid of it by // combining the edge reaching the terminal state // with the edges leaving the initial state. - bdd econd = e.cond; - bool first = true; + // + // However if we have some histories for e.src + // (which implies that the automaton is + // deterministic), we can try to replay that from + // the initial state first. + // + // One problem with those histories, is that we do + // not know how much of it to replay. It's possible + // that we cannot find a matching transition (e.g. if + // the history if "b" but the choices are "!a" or "a"), + // and its also possible to that playing too much of + // history will get us back the terminal state. In both + // cases, we should try again with a smaller history. + unsigned moved_init = init; + if (is_det) + { + auto& h = histories[e.src]; + int hsize = h.size(); + for (int hlen = hsize - 1; hlen > 0; --hlen) + { + for (int pos = hlen - 1; pos >= 0; --pos) + { + for (auto& e: aut->out(moved_init)) + if (bdd_implies(h[pos], e.cond)) + { + if (term[si.scc_of(e.dst)]) + goto failed; + moved_init = e.dst; + goto moved; + } + // if we reach this place, we failed to follow + // one step of the history. + goto failed; + moved: + continue; + } + // we have successfully played all history + // to a non-terminal state. + break; + failed: + moved_init = init; + continue; + } + } // Combine this edge with any compatible edge from // the initial state. - for (auto& ei: aut->out(init)) + bdd econd = e.cond; + bool first = true; + for (auto& ei: aut->out(moved_init)) { bdd cond = ei.cond & econd; if (cond != bddfalse) @@ -196,12 +345,22 @@ namespace spot f = nest_f(f); } twa_graph_ptr aut = ltl_to_tgba_fm(f, dict, true); - twa_graph_ptr reduced = minimize_obligation(aut, f, nullptr, - !deterministic); + twa_graph_ptr reduced = minimize_obligation(aut, f); + if (reduced == aut) + return nullptr; scc_info si(reduced); if (!is_terminal_automaton(reduced, &si, true)) return nullptr; do_g_f_terminal_inplace(si, state_based); + if (!deterministic) + { + scc_info si2(aut); + if (!is_terminal_automaton(aut, &si2, true)) + return reduced; + do_g_f_terminal_inplace(si2, state_based); + if (aut->num_states() <= reduced->num_states()) + return aut; + } return reduced; } diff --git a/spot/twaalgos/gfguarantee.hh b/spot/twaalgos/gfguarantee.hh index 8e163dce8..5124667f4 100644 --- a/spot/twaalgos/gfguarantee.hh +++ b/spot/twaalgos/gfguarantee.hh @@ -49,9 +49,10 @@ namespace spot /// /// If the formula \a gf has the form GΦ where Φ matches either F(φ) /// or F(φ₁)|F(φ₂)|...|F(φₙ), we translate Φ into A_Φ and attempt to - /// minimize it to a WDBA. If \a deterministic is not set, we keep - /// the minimized automaton only if A_Φ is larger. If the resulting - /// automaton is terminal, we then call g_f_terminal_inplace(). + /// minimize it to a WDBA W_Φ. If the resulting automaton is + /// terminal, we then call g_f_terminal_inplace(W_Φ). If \a + /// deterministic is not set, we keep the minimized automaton only + /// if g_f_terminal_inplace(A_Φ) is larger. /// /// Return nullptr if the input formula is not of the supported /// form. @@ -59,7 +60,9 @@ namespace spot /// This construction generalizes a construction in the LICS'18 /// paper of J. Esparza, J. Křetínský, and S. Sickert. This version /// will work if Φ represent a safety property, even if it is not a - /// syntactic safety. + /// syntactic safety. When building deterministic transition-based + /// automata, it will also try to remove useless trivial components + /// at the beginning of wdba(A_Φ). SPOT_API twa_graph_ptr gf_guarantee_to_ba_maybe(formula gf, const bdd_dict_ptr& dict, bool deterministic = true, bool state_based = false); diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test index 18cd9b31d..d2b8e87fe 100755 --- a/tests/core/ltl2tgba2.test +++ b/tests/core/ltl2tgba2.test @@ -360,3 +360,19 @@ p-patterns,20, 1,8, 1,8, 3,24, 3,24 EOF diff output expected + + +# These four formulas appear in a NEWS entry for Spot 2.6 +cat >formulas < output + +diff formulas output diff --git a/tests/core/ltl3ba.test b/tests/core/ltl3ba.test index be875a14f..105a34b7b 100755 --- a/tests/core/ltl3ba.test +++ b/tests/core/ltl3ba.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement +# Copyright (C) 2016, 2017, 2018 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -39,8 +39,15 @@ export SPOT_HOA_TOLERANT # compatible with Spin's syntax. ( echo _x +# Some formula used by Spot's GF(guarantee) translation. + cat <