diff --git a/ChangeLog b/ChangeLog index 3bffad152..79e707bbb 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,13 @@ +2011-01-04 Alexandre Duret-Lutz + + Move the logic for detecting when the minimize() algorithm is + correct from ltl2tgba to the library. + + * src/tgbaalgos/minimize.hh, + src/tgbaalgos/minimize.cc (minimize_obligation): New function. + * src/tgbatests/ltl2tgba.cc (main): Fix constness of automata, + and call minimize_obligation() for -R3b. + 2010-12-26 Alexandre Duret-Lutz Make minimization of obligation properties and deterministic diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc index 92748de0e..3664fadad 100644 --- a/src/tgbaalgos/minimize.cc +++ b/src/tgbaalgos/minimize.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2010 Laboratoire de Recherche et Développement +// Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -22,7 +22,13 @@ #include "minimize.hh" #include "ltlast/allnodes.hh" #include "misc/hash.hh" +#include "tgba/tgbaproduct.hh" +#include "tgba/tgbatba.hh" #include "tgbaalgos/powerset.hh" +#include "tgbaalgos/gtec/gtec.hh" +#include "tgbaalgos/safety.hh" +#include "tgbaalgos/sccfilter.hh" +#include "tgbaalgos/ltl2tgba_fm.hh" namespace spot { @@ -300,4 +306,87 @@ namespace spot return res; } + + const tgba* + minimize_obligation(const tgba* aut_f, + const ltl::formula* f, const tgba* aut_neg_f) + { + // WDBA minimization + tgba* min_aut_f = minimize(aut_f); + + // If aut_f is a safety automaton, the WDBA minimization must be + // correct. + if (is_safety_automaton(aut_f)) + { + return min_aut_f; + } + + if (!f && !aut_neg_f) + { + // We do not now if the minimization is safe. + return 0; + } + + const tgba* to_free = 0; + + // Build negation automaton if not supplied. + if (!aut_neg_f) + { + assert(f); + + ltl::formula* neg_f = ltl::unop::instance(ltl::unop::Not, f->clone()); + aut_neg_f = ltl_to_tgba_fm(neg_f, aut_f->get_dict()); + neg_f->destroy(); + + // Remove useless SCCs. + const tgba* tmp = scc_filter(aut_neg_f, true); + delete aut_neg_f; + to_free = aut_neg_f = tmp; + } + + // If the negation is a safety automaton, then the + // minimization is correct. + if (is_safety_automaton(aut_neg_f)) + { + delete to_free; + return min_aut_f; + } + + bool ok = false; + + tgba* p = new tgba_product(min_aut_f, aut_neg_f); + emptiness_check* ec = couvreur99(p); + emptiness_check_result* res = ec->check(); + if (!res) + { + delete ec; + delete p; + tgba* min_aut_neg_f = minimize(aut_neg_f); + tgba* p = new tgba_product(aut_f, min_aut_neg_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; + + delete res; + delete ec; + delete p; + delete min_aut_neg_f; + } + else + { + delete res; + delete ec; + delete p; + } + delete to_free; + + if (ok) + return min_aut_f; + delete min_aut_f; + return aut_f; + } } diff --git a/src/tgbaalgos/minimize.hh b/src/tgbaalgos/minimize.hh index 185dfdeae..3bf34b710 100644 --- a/src/tgbaalgos/minimize.hh +++ b/src/tgbaalgos/minimize.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement +// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -22,77 +22,129 @@ # define SPOT_TGBAALGOS_MINIMIZE_HH # include "tgba/tgbaexplicit.hh" +# include "ltlast/formula.hh" namespace spot { - // \brief Use the powerset construction to minimize a TGBA. - // - // If \a monitor is set of \c false (the default), then the - // minimized automaton is correct only for properties that belong to - // the class of "obligation properties". This algorithm assumes - // that the given automaton expresses an obligation properties and - // will return an automaton that is bogus (i.e. not equivalent to - // the original) if that is not the case. - // - // Please see the following paper for a discussion of this - // technique. - // - // \verbatim - // @InProceedings{ dax.07.atva, - // author = {Christian Dax and Jochen Eisinger and Felix Klaedtke}, - // title = {Mechanizing the Powerset Construction for Restricted - // Classes of {$\omega$}-Automata}, - // year = 2007, - // series = {Lecture Notes in Computer Science}, - // publisher = {Springer-Verlag}, - // volume = 4762, - // booktitle = {Proceedings of the 5th International Symposium on - // Automated Technology for Verification and Analysis - // (ATVA'07)}, - // editor = {Kedar S. Namjoshi and Tomohiro Yoneda and Teruo Higashino - // and Yoshio Okamura}, - // month = oct - // } - // \endverbatim - // - // Dax et al. suggest one way to check whether a property - // \f$\varphi\f$ expressed as an LTL formula is an obligation: - // translate the formula and its negation as two automata \f$A_f\f$ - // and \f$A_{\lnot f}\f$, then minimize both automata and check that - // the two products $\f \mathrm{minimize(A_{\lnot f})\otimes A_f\f$ - // and $\f \mathrm{minimize(A_f)\otimes A_{\lnot f}\f$ are empty. - // If that is the case, then the minimization was correct. - // - // You may also want to check if \$A_f\$ is a safety automaton using - // the is_safety_automaton() function. Since safety properties are - // a subclass of obligation properties, you can apply the - // minimization without further test. Note however that this is - // only a sufficient condition. - // - // If \a monitor is set to \c true, the automaton will be converted - // into minimal deterministic monitor. All useless SCCs should have - // been previously removed (using scc_filter() for instance). Then - // the automaton will be reduced as if all states where accepting - // states. - // - // For more detail about monitors, see the following paper: - // \verbatim - // @InProceedings{ tabakov.10.rv, - // author = {Deian Tabakov and Moshe Y. Vardi}, - // title = {Optimized Temporal Monitors for SystemC{$^*$}}, - // booktitle = {Proceedings of the 10th International Conferance on - // Runtime Verification}, - // pages = {436--451}, - // year = 2010, - // volume = {6418}, - // series = {Lecture Notes in Computer Science}, - // month = nov, - // publisher = {Spring-Verlag} - // } - // \endverbatim - // (Note: although the above paper uses Spot, this function did not - // exist at that time.) + /// \brief Use the powerset construction to minimize a TGBA. + /// + /// If \a monitor is set to \c false (the default), then the + /// minimized automaton is correct only for properties that belong + /// to the class of "obligation properties". This algorithm assumes + /// that the given automaton expresses an obligation properties and + /// will return an automaton that is bogus (i.e. not equivalent to + /// the original) if that is not the case. + /// + /// Please see the following paper for a discussion of this + /// technique. + /// + /// \verbatim + /// @InProceedings{ dax.07.atva, + /// author = {Christian Dax and Jochen Eisinger and Felix Klaedtke}, + /// title = {Mechanizing the Powerset Construction for Restricted + /// Classes of {$\omega$}-Automata}, + /// year = 2007, + /// series = {Lecture Notes in Computer Science}, + /// publisher = {Springer-Verlag}, + /// volume = 4762, + /// booktitle = {Proceedings of the 5th International Symposium on + /// Automated Technology for Verification and Analysis + /// (ATVA'07)}, + /// editor = {Kedar S. Namjoshi and Tomohiro Yoneda and Teruo Higashino + /// and Yoshio Okamura}, + /// month = oct + /// } + /// \endverbatim + /// + /// Dax et al. suggest one way to check whether a property + /// \f$\varphi\f$ expressed as an LTL formula is an obligation: + /// translate the formula and its negation as two automata \f$A_f\f$ + /// and \f$A_{\lnot f}\f$, then minimize both automata and check + /// that the two products $\f \mathrm{minimize(A_{\lnot f})\otimes + /// A_f\f$ and $\f \mathrm{minimize(A_f)\otimes A_{\lnot f}\f$ are + /// empty. If that is the case, then the minimization was correct. + /// + /// You may also want to check if \$A_f\$ is a safety automaton + /// using the is_safety_automaton() function. Since safety + /// properties are a subclass of obligation properties, you can + /// apply the minimization without further test. Note however that + /// this is only a sufficient condition. + /// + /// If \a monitor is set to \c true, the automaton will be converted + /// into minimal deterministic monitor. All useless SCCs should + /// have been previously removed (using scc_filter() for instance). + /// Then the automaton will be reduced as if all states where + /// accepting states. + /// + /// For more detail about monitors, see the following paper: + /// \verbatim + /// @InProceedings{ tabakov.10.rv, + /// author = {Deian Tabakov and Moshe Y. Vardi}, + /// title = {Optimized Temporal Monitors for SystemC{$^*$}}, + /// booktitle = {Proceedings of the 10th International Conferance + /// on Runtime Verification}, + /// pages = {436--451}, + /// year = 2010, + /// volume = {6418}, + /// series = {Lecture Notes in Computer Science}, + /// month = nov, + /// publisher = {Spring-Verlag} + /// } + /// \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); + + + /// \brief Minimize an automaton if it represents an obligation property. + /// + /// This function attempt to minimize the automaton \a aut_f using the + /// algorithm implemented in the minimize() function, and presented + /// by the following paper: + /// + /// \verbatim + /// @InProceedings{ dax.07.atva, + /// author = {Christian Dax and Jochen Eisinger and Felix Klaedtke}, + /// title = {Mechanizing the Powerset Construction for Restricted + /// Classes of {$\omega$}-Automata}, + /// year = 2007, + /// series = {Lecture Notes in Computer Science}, + /// publisher = {Springer-Verlag}, + /// volume = 4762, + /// booktitle = {Proceedings of the 5th International Symposium on + /// Automated Technology for Verification and Analysis + /// (ATVA'07)}, + /// editor = {Kedar S. Namjoshi and Tomohiro Yoneda and Teruo Higashino + /// and Yoshio Okamura}, + /// month = oct + /// } + /// \endverbatim + /// + /// Because it is hard to determine if an automaton correspond + /// to an obligation property, you should supply either the formula + /// \a f expressed by the automaton \a aut_f, or \a aut_neg_f the negation + /// of the automaton \a aut_neg_f. + /// + /// \param aut_f the automaton to minimize + /// \param f the LTL formula represented by the automaton \a aut_f + /// \param aut_neg_f an automaton representing the negation of \a aut_f + /// \return a new tgba if the automaton could be minimized, aut_f if + /// the automaton cannot be minimized, 0 if we do not if if the + /// minimization is correct because neither \a f nor \a aut_neg_f + /// were supplied. + /// + /// The function proceeds as follows. If the formula \a f or the + /// automaton \a aut can easily be proved to represent an obligation + /// 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 + /// 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, + const ltl::formula* f = 0, + const tgba* aut_neg_f = 0); + } #endif /* !SPOT_TGBAALGOS_MINIMIZE_HH */ diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 495117a97..aef3d223f 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2007, 2008, 2009, 2010 Laboratoire de Recherche et +// Copyright (C) 2007, 2008, 2009, 2010, 2011 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis @@ -327,8 +327,8 @@ main(int argc, char** argv) spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::atomic_prop_set* unobservables = 0; spot::tgba_explicit_string* system = 0; - spot::tgba* product = 0; - spot::tgba* product_to_free = 0; + const spot::tgba* product = 0; + const spot::tgba* product_to_free = 0; spot::bdd_dict* dict = new spot::bdd_dict(); spot::timer_map tm; bool use_timer = false; @@ -789,9 +789,9 @@ main(int argc, char** argv) } if (f || from_file) { - spot::tgba_bdd_concrete* concrete = 0; - spot::tgba* to_free = 0; - spot::tgba* a = 0; + const spot::tgba_bdd_concrete* concrete = 0; + const spot::tgba* to_free = 0; + const spot::tgba* a = 0; if (from_file) { @@ -867,7 +867,7 @@ main(int argc, char** argv) if (opt_monitor && ((reduc_aut & spot::Reduce_Scc) == 0)) { - if (dynamic_cast(a)) + if (dynamic_cast(a)) symbolic_scc_pruning = true; else reduc_aut |= spot::Reduce_Scc; @@ -875,8 +875,8 @@ main(int argc, char** argv) if (symbolic_scc_pruning) { - spot::tgba_bdd_concrete* bc = - dynamic_cast(a); + const spot::tgba_bdd_concrete* bc = + dynamic_cast(a); if (!bc) { std::cerr << ("Error: Automaton is not symbolic: cannot " @@ -890,14 +890,15 @@ main(int argc, char** argv) { tm.start("reducing A_f w/ symbolic SCC pruning"); if (bc) - bc->delete_unaccepting_scc(); + const_cast(bc) + ->delete_unaccepting_scc(); tm.stop("reducing A_f w/ symbolic SCC pruning"); } } // Remove dead SCCs and useless acceptance conditions before // degeneralization. - spot::tgba* aut_scc = 0; + const spot::tgba* aut_scc = 0; if (reduc_aut & spot::Reduce_Scc) { tm.start("reducing A_f w/ SCC"); @@ -905,8 +906,8 @@ main(int argc, char** argv) tm.stop("reducing A_f w/ SCC"); } - spot::tgba_tba_proxy* degeneralized = 0; - spot::tgba_sgba_proxy* state_labeled = 0; + const spot::tgba_tba_proxy* degeneralized = 0; + const spot::tgba_sgba_proxy* state_labeled = 0; unsigned int n_acc = a->number_of_acceptance_conditions(); if (echeck_inst @@ -923,74 +924,31 @@ main(int argc, char** argv) a = state_labeled = new spot::tgba_sgba_proxy(a); } - spot::tgba_explicit* minimized = 0; + const spot::tgba* minimized = 0; if (opt_minimize) { - tm.start("WDBA-minimization"); - minimized = minimize(a); - tm.stop("WDBA-minimization"); - tm.start("WDBA-check"); - // If A is a safety automaton, the WDBA minimization - // must be correct. - if (is_safety_automaton(a)) + tm.start("obligation minimization"); + minimized = minimize_obligation(a, f); + tm.stop("obligation minimization"); + + if (minimized == 0) { - a = minimized; - } - else // We don't know if A is a safety automaton. - { - if (!f) + // if (!f) { std::cerr << "Error: Without a formula I cannot make " << "sure that the automaton built with -Rm\n" << " is correct." << std::endl; exit(2); } - // Let's make sure that A recognizes the same language - // as MINIMIZED. - spot::ltl::formula* neg = - spot::ltl::unop::instance(spot::ltl::unop::Not, f->clone()); - spot::tgba* n = spot::ltl_to_tgba_fm(neg, dict, fm_exprop_opt, - fm_symb_merge_opt, - post_branching, - fair_loop_approx, - unobservables, fm_red); - neg->destroy(); - spot::tgba* nscc = spot::scc_filter(n, true); - // If the negation is a safety automaton, - // then the minimization is correct. - if (is_safety_automaton(n)) - { - a = minimized; - } - else - { - spot::tgba* p = new spot::tgba_product(minimized, nscc); - spot::emptiness_check* ec = couvreur99(p); - spot::emptiness_check_result* res = ec->check(); - if (!res) - { - delete ec; - delete p; - spot::tgba* nm = minimize(nscc); - p = new spot::tgba_product(a, nm); - ec = couvreur99(p); - res = ec->check(); - if (!res) - { - // Finally, we are now sure that it was safe - // to minimize the automaton. - a = minimized; - } - delete nm; - } - delete res; - delete ec; - delete p; - } - delete nscc; - delete n; } - tm.stop("WDBA-check"); + else if (minimized == a) + { + minimized = 0; + } + else + { + a = minimized; + } } if (opt_monitor) @@ -1059,7 +1017,7 @@ main(int argc, char** argv) } } - spot::tgba_explicit* expl = 0; + const spot::tgba_explicit* expl = 0; switch (dupexp) { case NoneDup: @@ -1072,7 +1030,7 @@ main(int argc, char** argv) break; } - spot::tgba* product_degeneralized = 0; + const spot::tgba* product_degeneralized = 0; if (system) {