diff --git a/ChangeLog b/ChangeLog index ebdb9002a..b08d1f8a2 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,13 @@ +2010-11-25 Alexandre Duret-Lutz + + Preliminary support for monitors. + + * src/tgbatest/ltl2tgba.cc (-M): New option for building + deterministic monitors. + * src/tgbaalgos/minimize.cc (minimize): Take a monitor + argument and adjust the code. + * src/tgbaalgos/minimize.hh (minimize): Document it. + 2010-11-25 Alexandre Duret-Lutz "ltl2tgba -Rm -X foo.tgba" would fail. diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc index b9b146eaa..92748de0e 100644 --- a/src/tgbaalgos/minimize.cc +++ b/src/tgbaalgos/minimize.cc @@ -135,14 +135,14 @@ namespace spot return res; } - tgba_explicit* minimize(const tgba* a) + tgba_explicit* minimize(const tgba* a, bool monitor) { // The list of accepting states of a. std::list acc_list; std::queue todo; // The list of equivalent states. std::list done; - tgba_explicit* det_a = tgba_powerset(a, &acc_list); + tgba_explicit* det_a = tgba_powerset(a, monitor ? 0 : &acc_list); hash_set* final = new hash_set; hash_set* non_final = new hash_set; hash_map state_set_map; diff --git a/src/tgbaalgos/minimize.hh b/src/tgbaalgos/minimize.hh index a646e47bf..185dfdeae 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 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -25,8 +25,74 @@ namespace spot { - tgba_explicit* minimize(const tgba* a); + // \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.) + tgba_explicit* minimize(const tgba* a, bool monitor = false); } - #endif /* !SPOT_TGBAALGOS_MINIMIZE_HH */ diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 3b4be7523..d57c46304 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -213,6 +213,11 @@ syntax(char* prog) << " -Rm attempt to minimize the automata" << std::endl << std::endl + << "Automaton conversion:" + << " -M convert into a deterministic minimal monitor " + << "(implies -R3 or R3b)" << std::endl + << std::endl + << "Options for performing emptiness checks:" << std::endl << " -e[ALGO] run emptiness check, expect and compute an " << "accepting run" << std::endl @@ -316,6 +321,7 @@ main(int argc, char** argv) bool graph_run_tgba_opt = false; bool opt_reduce = false; bool opt_minimize = false; + bool opt_monitor = false; bool containment = false; bool show_fc = false; bool spin_comments = false; @@ -632,6 +638,10 @@ main(int argc, char** argv) { opt_minimize = true; } + else if (!strcmp(argv[formula_index], "-M")) + { + opt_monitor = true; + } else if (!strcmp(argv[formula_index], "-s")) { dupexp = DFS; @@ -856,6 +866,14 @@ main(int argc, char** argv) to_free = a; } + if (opt_monitor && ((reduc_aut & spot::Reduce_Scc) == 0)) + { + if (dynamic_cast(a)) + symbolic_scc_pruning = true; + else + reduc_aut |= spot::Reduce_Scc; + } + if (symbolic_scc_pruning) { spot::tgba_bdd_concrete* bc = @@ -976,6 +994,13 @@ main(int argc, char** argv) tm.stop("WDBA-check"); } + if (opt_monitor) + { + tm.start("Monitor minimization"); + a = minimized = minimize(a, true); + tm.stop("Monitor minimization"); + } + spot::tgba_reduc* aut_red = 0; if (reduc_aut != spot::Reduce_None) {