From ef317685c8217d75b867553b97b34ee22efa98da Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 5 Jan 2011 14:15:15 +0100 Subject: [PATCH] Speed up the obligation test. * src/tgbaalgos/minimize.cc (minimize_obligation): Do not minimize aut_neg_f, complement min_aut_f instead. * src/tgbaalgos/minimize.hh: Adjust description. --- ChangeLog | 8 ++++++++ src/tgbaalgos/minimize.cc | 20 ++++++++++++-------- src/tgbaalgos/minimize.hh | 4 ++-- 3 files changed, 22 insertions(+), 10 deletions(-) diff --git a/ChangeLog b/ChangeLog index a0bb0670c..5a1d6dad4 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,11 @@ +2011-01-05 Alexandre Duret-Lutz + + Speed up the obligation test. + + * src/tgbaalgos/minimize.cc (minimize_obligation): Do not + minimize aut_neg_f, complement min_aut_f instead. + * src/tgbaalgos/minimize.hh: Adjust description. + 2011-01-05 Alexandre Duret-Lutz * src/tgbaalgos/minimize.cc (minimize): Use the Loeding algorithm diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc index 27662b702..8b61bd10c 100644 --- a/src/tgbaalgos/minimize.cc +++ b/src/tgbaalgos/minimize.cc @@ -271,7 +271,7 @@ namespace spot - tgba_explicit* minimize(const tgba* a, bool monitor) + tgba_explicit_number* minimize(const tgba* a, bool monitor) { std::queue todo; // The list of equivalent states. @@ -496,7 +496,7 @@ namespace spot const ltl::formula* f, const tgba* aut_neg_f) { // WDBA minimization - tgba* min_aut_f = minimize(aut_f); + tgba_explicit_number* min_aut_f = minimize(aut_f); // If aut_f is a safety automaton, the WDBA minimization must be // correct. @@ -545,20 +545,24 @@ namespace spot { delete ec; delete p; - tgba* min_aut_neg_f = minimize(aut_neg_f); - tgba* p = new tgba_product(aut_f, min_aut_neg_f); + // Complement the minimized WDBA. + min_aut_f->complement_all_acceptance_conditions(); + tgba* p = new tgba_product(aut_f, min_aut_f); emptiness_check* ec = couvreur99(p); res = ec->check(); if (!res) - // Finally, we are now sure that it was safe - // to minimize the automaton. - ok = true; + { + // Finally, we are now sure that it was safe + // to minimize the automaton. + ok = true; + // Get the original automaton back. + min_aut_f->complement_all_acceptance_conditions(); + } delete res; delete ec; delete p; - delete min_aut_neg_f; } else { diff --git a/src/tgbaalgos/minimize.hh b/src/tgbaalgos/minimize.hh index 3bf34b710..f0cfecc1c 100644 --- a/src/tgbaalgos/minimize.hh +++ b/src/tgbaalgos/minimize.hh @@ -93,7 +93,7 @@ namespace spot /// \endverbatim /// (Note: although the above paper uses Spot, this function did not /// exist at that time.) - tgba_explicit* minimize(const tgba* a, bool monitor = false); + tgba_explicit_number* minimize(const tgba* a, bool monitor = false); /// \brief Minimize an automaton if it represents an obligation property. @@ -138,7 +138,7 @@ namespace spot /// formula, then the result of \code minimize(aut) is returned. /// Otherwise, if \a aut_neg_f was not supplied but \a f was, \a /// aut_neg_f is built from the negation of \a f. Then we check - /// that \code product(aut,minimize(aut_neg_f)) and \code + /// that \code product(aut,!minimize(aut_f)) and \code /// product(aut_neg_f,minize(aut)) are both empty. If they are, the /// the minimization was sound. (See the paper for full details.) const tgba* minimize_obligation(const tgba* aut_f,