From 8c972ad3ce79fe0ab99a8983711c2534891b736c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 5 Jan 2011 22:35:38 +0100 Subject: [PATCH] Cleanup the minimize.hh interface. * src/tgbaalgos/minimize.hh, src/tgbaalgos/minimize.cc (minimize): Split into ... (minimize_wdba, minimize_monitor): ... these two functions. * src/tgbatest/ltl2tgba.cc (main): Adjust the call to minimize_monitor. * wrap/python/cgi-bin/ltl2tgba.in: Adjust the calls to minimize_monitor and minimize_obligation. * wrap/python/spot.i: Declare minimize_monitor, minimize_wdba, minimize_obligations. * src/tgba/tgbaexplicit.hh (tgba_explicit_string) (tgba_explicit_formula, tgba_explicit_number): Add fake declarations so that SWIG can see they inherits from tgba. --- ChangeLog | 17 ++++ src/tgba/tgbaexplicit.hh | 20 +++- src/tgbaalgos/minimize.cc | 101 +++++++++++--------- src/tgbaalgos/minimize.hh | 164 ++++++++++++++++---------------- src/tgbatest/ltl2tgba.cc | 2 +- wrap/python/cgi-bin/ltl2tgba.in | 8 +- wrap/python/spot.i | 6 +- 7 files changed, 182 insertions(+), 136 deletions(-) diff --git a/ChangeLog b/ChangeLog index 610ade58f..c0515eee5 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,20 @@ +2011-01-05 Alexandre Duret-Lutz + + Cleanup the minimize.hh interface. + + * src/tgbaalgos/minimize.hh, src/tgbaalgos/minimize.cc + (minimize): Split into ... + (minimize_wdba, minimize_monitor): ... these two functions. + * src/tgbatest/ltl2tgba.cc (main): Adjust the call to + minimize_monitor. + * wrap/python/cgi-bin/ltl2tgba.in: Adjust the calls to + minimize_monitor and minimize_obligation. + * wrap/python/spot.i: Declare minimize_monitor, minimize_wdba, + minimize_obligations. + * src/tgba/tgbaexplicit.hh (tgba_explicit_string) + (tgba_explicit_formula, tgba_explicit_number): Add fake + declarations so that SWIG can see they inherits from tgba. + 2011-01-05 Alexandre Duret-Lutz Cleanup the DFA minimization algorithm. diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh index 4e387c71b..f896438a5 100644 --- a/src/tgba/tgbaexplicit.hh +++ b/src/tgba/tgbaexplicit.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). // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -313,6 +313,7 @@ namespace spot }; +#ifndef SWIG class tgba_explicit_string: public tgba_explicit_labelled { @@ -333,7 +334,13 @@ namespace spot name_state_map_[alias_name] = add_state(real_name); } }; +#else + class tgba_explicit_string: public tgba + { + }; +#endif +#ifndef SWIG class tgba_explicit_formula: public tgba_explicit_labelled { @@ -345,7 +352,13 @@ namespace spot virtual state* add_default_init(); virtual std::string format_state(const spot::state* s) const; }; +#else + class tgba_explicit_formula: public tgba + { + }; +#endif +#ifndef SWIG class tgba_explicit_number: public tgba_explicit_labelled > { @@ -357,6 +370,11 @@ namespace spot virtual state* add_default_init(); virtual std::string format_state(const spot::state* s) const; }; +#else + class tgba_explicit_number: public tgba + { + }; +#endif } #endif // SPOT_TGBA_TGBAEXPLICIT_HH diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc index 266e512de..c19f7ff24 100644 --- a/src/tgbaalgos/minimize.cc +++ b/src/tgbaalgos/minimize.cc @@ -506,7 +506,20 @@ namespace spot } - tgba_explicit_number* minimize(const tgba* a, bool monitor) + tgba_explicit_number* minimize_monitor(const tgba* a) + { + hash_set* final = new hash_set; + tgba_explicit_number* det_a; + + { + power_map pm; + det_a = tgba_powerset(a, pm); + } + // final is empty: there is no acceptance condition + return minimize_dfa(det_a, final); + } + + tgba_explicit_number* minimize_wdba(const tgba* a) { hash_set* final = new hash_set; tgba_explicit_number* det_a; @@ -515,57 +528,54 @@ namespace spot power_map pm; det_a = tgba_powerset(a, pm); - if (!monitor) + // For each SCC of the deterministic automaton, determine if + // it is accepting or not. + scc_map sm(det_a); + sm.build_map(); + unsigned scc_count = sm.scc_count(); + std::vector accepting(scc_count); + // SCC are numbered in topological order + for (unsigned n = 0; n < scc_count; ++n) { - // For each SCC of the deterministic automaton, determine if - // it is accepting or not. - scc_map sm(det_a); - sm.build_map(); - unsigned scc_count = sm.scc_count(); - std::vector accepting(scc_count); - // SCC are numbered in topological order - for (unsigned n = 0; n < scc_count; ++n) + bool acc = true; + + if (sm.trivial(n)) { - bool acc = true; + // Trivial SCCs are accepting if all their + // successors are accepting. - if (sm.trivial(n)) + // This corresponds to the algorithm in Fig. 1 of + // "Efficient minimization of deterministic weak + // omega-automata" written by Christof Löding and + // published in Information Processing Letters 79 + // (2001) pp 105--109. Except we do not keep track + // of the actual color associated to each SCC. + + const scc_map::succ_type& succ = sm.succ(n); + for (scc_map::succ_type::const_iterator i = succ.begin(); + i != succ.end(); ++i) { - // Trivial SCCs are accepting if all their - // successors are accepting. - - // This corresponds to the algorithm in Fig. 1 of - // "Efficient minimization of deterministic weak - // omega-automata" written by Christof Löding and - // published in Information Processing Letters 79 - // (2001) pp 105--109. Except we do not keep track - // of the actual color associated to each SCC. - - const scc_map::succ_type& succ = sm.succ(n); - for (scc_map::succ_type::const_iterator i = succ.begin(); - i != succ.end(); ++i) + if (!accepting[i->first]) { - if (!accepting[i->first]) - { - acc = false; - break; - } + acc = false; + break; } } - else - { - // Regular SCCs are accepting if any of their loop - // corresponds to an accepting - acc = wdba_scc_is_accepting(det_a, n, a, sm, pm); - } + } + else + { + // Regular SCCs are accepting if any of their loop + // corresponds to an accepting + acc = wdba_scc_is_accepting(det_a, n, a, sm, pm); + } - accepting[n] = acc; - if (acc) - { - std::list l = sm.states_of(n); - std::list::const_iterator il; - for (il = l.begin(); il != l.end(); ++il) - final->insert((*il)->clone()); - } + accepting[n] = acc; + if (acc) + { + std::list l = sm.states_of(n); + std::list::const_iterator il; + for (il = l.begin(); il != l.end(); ++il) + final->insert((*il)->clone()); } } } @@ -577,8 +587,7 @@ namespace spot minimize_obligation(const tgba* aut_f, const ltl::formula* f, const tgba* aut_neg_f) { - // WDBA minimization - tgba_explicit_number* min_aut_f = minimize(aut_f); + tgba_explicit_number* min_aut_f = minimize_wdba(aut_f); // If aut_f is a safety automaton, the WDBA minimization must be // correct. diff --git a/src/tgbaalgos/minimize.hh b/src/tgbaalgos/minimize.hh index f0cfecc1c..8ac29091a 100644 --- a/src/tgbaalgos/minimize.hh +++ b/src/tgbaalgos/minimize.hh @@ -26,101 +26,99 @@ namespace spot { - /// \brief Use the powerset construction to minimize a TGBA. + /// \addtogroup tgba_reduction + /// @{ + + /// \brief Construct a minimal deterministic monitor. /// - /// 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. + /// 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 + /// determinized and minimized using the standard DFA construction + /// 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 in Spot at that time.) + /// + /// \param a the automaton to convert into a minimal deterministic monitor + /// \pre Dead SCCs should have been removed from \a a before + /// calling this function. + tgba_explicit_number* minimize_monitor(const tgba* a); + + /// \brief Minimize a Büchi automaton in the WDBA class. + /// + /// This takes a TGBA whose language is representable by + /// a Weak Deterministic Büchi Automaton, and construct + /// a minimal WDBA for this language. + /// + /// If the input automaton does not represent a WDBA language, + /// the resulting automaton is still a WDBA, but it will not + /// be equivalent to the original automaton. Use the + /// minimize_obligation() function if you are not sure whether + /// it is safe to call this function. /// /// 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 + /// 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_number* minimize(const tgba* a, bool monitor = false); - + tgba_explicit_number* minimize_wdba(const tgba* a); /// \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 + /// This function attempts to minimize the automaton \a aut_f using the + /// algorithm implemented in the minimize_wdba() 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 + /// 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 + /// Because it is hard to determine if an automaton corresponds /// 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. @@ -135,16 +133,18 @@ namespace spot /// /// 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_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.) + /// formula, then the result of 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 product(aut,!minimize(aut_f)) and + /// 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 aef3d223f..35e42353a 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -954,7 +954,7 @@ main(int argc, char** argv) if (opt_monitor) { tm.start("Monitor minimization"); - a = minimized = minimize(a, true); + a = minimized = minimize_monitor(a); tm.stop("Monitor minimization"); } diff --git a/wrap/python/cgi-bin/ltl2tgba.in b/wrap/python/cgi-bin/ltl2tgba.in index badae049b..7241623ca 100755 --- a/wrap/python/cgi-bin/ltl2tgba.in +++ b/wrap/python/cgi-bin/ltl2tgba.in @@ -1,7 +1,7 @@ #!@PYTHON@ # -*- mode: python; coding: iso-8859-1 -*- -# Copyright (C) 2007, 2009, 2010 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2007, 2009, 2010, 2011 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de # Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), # Université Pierre et Marie Curie. @@ -572,9 +572,9 @@ elif trans_taa: automaton = spot.ltl_to_taa(f, dict, refined_rules) if reduce_dmonitor: - automaton = spot.minimize(automaton, True) + automaton = spot.minimize_monitor(automaton) elif reduce_wdba: - automaton = spot.minimize(automaton, False) + automaton = spot.minimize_obligation(automaton) elif reduce_scc: # Do not suppress all useless acceptance conditions if # degeneralization is requested: keeping those that lead to diff --git a/wrap/python/spot.i b/wrap/python/spot.i index 514ad0441..20d674506 100644 --- a/wrap/python/spot.i +++ b/wrap/python/spot.i @@ -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). // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique // de Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -147,7 +147,9 @@ using namespace spot; %feature("new") spot::ltl_to_taa; %feature("new") spot::ltl_to_tgba_fm; %feature("new") spot::ltl_to_tgba_lacim; -%feature("new") spot::minimize; +%feature("new") spot::minimize_wdba; +%feature("new") spot::minimize_monitor; +%feature("new") spot::minimize_obligation; %feature("new") spot::reduc_tgba_sim; %feature("new") spot::scc_filter; %feature("new") spot::tgba_dupexp_bfs;