From db124d02c02bd8810bf7f7cc3b58359966490979 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 27 Jan 2011 18:21:27 +0100 Subject: [PATCH] Rename is_safety_automaton() as is_guarantee_automaton() and implement is_safety_mwdba(). Note: I swapped the name of safety and guarantee when I implemented is_safety_automaton() on 2010-03-20. Fortunately, is_safety_automaton() was only used where is_guarantee_automaton() would have been correct. * src/tgbaalgos/safety.cc (is_guarantee_automaton): Rename as ... (is_guarantee_automaton): ... this. (is_safety_mwdba): New function. * src/tgbaalgos/safety.hh: Adjust and add documentation. * src/tgbaalgos/minimize.cc: Use is_guarantee_automaton() instead of is_safety_automaton(). * src/tgbatests/safety.test: Rename as ... * src/tgbatests/obligation.test: ... this, and augment the test. * src/tgbatest/Makefile.am: Adjust. * src/tgbatest/ltl2tgba.cc (-O): Display whether a formula represent a safety, guarantee, or obligation property. * NEWS: Adjust. --- ChangeLog | 24 ++++++++ NEWS | 5 +- src/tgbaalgos/minimize.cc | 8 +-- src/tgbaalgos/safety.cc | 58 +++++++++++++++++- src/tgbaalgos/safety.hh | 36 ++++++++--- src/tgbatest/Makefile.am | 2 +- src/tgbatest/ltl2tgba.cc | 32 ++++++++-- src/tgbatest/obligation.test | 116 +++++++++++++++++++++++++++++++++++ src/tgbatest/safety.test | 108 -------------------------------- 9 files changed, 260 insertions(+), 129 deletions(-) create mode 100755 src/tgbatest/obligation.test delete mode 100755 src/tgbatest/safety.test diff --git a/ChangeLog b/ChangeLog index b0632b066..97d9b9f49 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,27 @@ +2011-01-27 Alexandre Duret-Lutz + + Rename is_safety_automaton() as is_guarantee_automaton() and + implement is_safety_mwdba(). + + Note: I swapped the name of safety and guarantee when I + implemented is_safety_automaton() on 2010-03-20. Fortunately, + is_safety_automaton() was only used where is_guarantee_automaton() + would have been correct. + + * src/tgbaalgos/safety.cc (is_guarantee_automaton): Rename as ... + (is_guarantee_automaton): ... this. + (is_safety_mwdba): New function. + * src/tgbaalgos/safety.hh: Adjust and add documentation. + * src/tgbaalgos/minimize.cc: Use is_guarantee_automaton() instead + of is_safety_automaton(). + * src/tgbatests/safety.test: Rename as ... + * src/tgbatests/obligation.test: ... this, and augment the + test. + * src/tgbatest/Makefile.am: Adjust. + * src/tgbatest/ltl2tgba.cc (-O): Display whether a formula + represent a safety, guarantee, or obligation property. + * NEWS: Adjust. + 2011-01-27 Alexandre Duret-Lutz * NEWS: Minor rewritings. diff --git a/NEWS b/NEWS index fb45392ea..657ddf6a4 100644 --- a/NEWS +++ b/NEWS @@ -36,9 +36,10 @@ New in spot 0.6a: -ks: traverse the automaton to compute its number of states and transitions (this is faster than -k which will also count SCCs and paths). - -Rn: Minimize automata for obligation formulae. -M: Build a deterministic monitor. - -O: Tell whether an automaton is a safety automaton. + -O: Tell whether a formula represents a safety, guarantee, or + obligation property. + -Rm: Minimize automata representing obligation properties. * The on-line tool to translate LTL formulae into automata has been rewritten and is now at http://spot.lip6.fr/ltl2tgba.html It requires a javascript-enabled browser. diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc index 1cad49077..8d97dc8dd 100644 --- a/src/tgbaalgos/minimize.cc +++ b/src/tgbaalgos/minimize.cc @@ -610,9 +610,9 @@ namespace spot { tgba_explicit_number* min_aut_f = minimize_wdba(aut_f); - // If aut_f is a safety automaton, the WDBA minimization must be + // If aut_f is a guarantee automaton, the WDBA minimization must be // correct. - if (is_safety_automaton(aut_f)) + if (is_guarantee_automaton(aut_f)) { return min_aut_f; } @@ -640,9 +640,9 @@ namespace spot to_free = aut_neg_f = tmp; } - // If the negation is a safety automaton, then the + // If the negation is a guarantee automaton, then the // minimization is correct. - if (is_safety_automaton(aut_neg_f)) + if (is_guarantee_automaton(aut_neg_f)) { delete to_free; return min_aut_f; diff --git a/src/tgbaalgos/safety.cc b/src/tgbaalgos/safety.cc index ca4786f81..c04b65d1c 100644 --- a/src/tgbaalgos/safety.cc +++ b/src/tgbaalgos/safety.cc @@ -19,11 +19,13 @@ // 02111-1307, USA. #include "safety.hh" +#include "misc/hash.hh" +#include namespace spot { bool - is_safety_automaton(const tgba* aut, const scc_map* sm) + is_guarantee_automaton(const tgba* aut, const scc_map* sm) { // Create an scc_map of the user did not give one to us. bool need_sm = !sm; @@ -69,6 +71,60 @@ namespace spot return result; } + bool is_safety_mwdba(const tgba* aut) + { + typedef Sgi::hash_set seen_map; + seen_map seen; // States already seen. + std::deque todo; // A queue of states yet to explore. + + { + state* s = aut->get_init_state(); + todo.push_back(s); + seen.insert(s); + } + + bdd all_acc = aut->all_acceptance_conditions(); + + bool all_accepting = true; + while (all_accepting && !todo.empty()) + { + const state* s = todo.front(); + todo.pop_front(); + + tgba_succ_iterator* it = aut->succ_iter(s); + for (it->first(); !it->done(); it->next()) + { + bdd acc = it->current_acceptance_conditions(); + if (acc != all_acc) + { + all_accepting = false; + break; + } + state* d = it->current_state(); + if (seen.find(d) != seen.end()) + { + d->destroy(); + } + else + { + seen.insert(d); + todo.push_back(d); + } + } + delete it; + } + + seen_map::const_iterator it = seen.begin(); + while (it != seen.end()) + { + seen_map::const_iterator old = it; + ++it; + (*old)->destroy(); + } + + return all_accepting; + } diff --git a/src/tgbaalgos/safety.hh b/src/tgbaalgos/safety.hh index ac55e6c12..c7e02a4d6 100644 --- a/src/tgbaalgos/safety.hh +++ b/src/tgbaalgos/safety.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2010 Laboratoire de Recherche et Développement de +// Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement de // l'Epita (LRDE) // // This file is part of Spot, a model checking library. @@ -25,20 +25,40 @@ namespace spot { - /// \brief Whether an automaton is a safety property. + /// \brief Whether an automaton represents a guarantee property. /// - /// An automaton is an safety if any accepting path ends on an - /// accepting state with only one transition that is a self-loop - /// labelled by true. Note that this is only a sufficient - /// condition. Some safety automata might not be recognized with - /// this check because of some non-determinism in the automaton. + /// A weak deterministic TGBA represents a guarantee property if any + /// accepting path ends on an accepting state with only one + /// transition that is a self-loop labelled by true. + /// + /// Note that in the general case, this is only a sufficient + /// condition : some guarantee automata might not be recognized with + /// this check e.g. because of some non-determinism in the + /// automaton. In that case, you should interpret a \c false return + /// value as "I don't know". + /// + /// If you apply this function on a weak deterministic TGBA + /// (e.g. after a successful minimization with + /// minimize_obligation()), then the result leaves no doubt: false + /// really means that the automaton is not a guarantee property. /// /// \param aut the automaton to check /// /// \param sm an scc_map of the automaton if available (it will be /// built otherwise. If you supply an scc_map you should call /// build_map() before passing it to this function. - bool is_safety_automaton(const tgba* aut, const scc_map* sm = 0); + bool is_guarantee_automaton(const tgba* aut, const scc_map* sm = 0); + + /// \brief Whether a minimized WDBA represents a safety property. + /// + /// A minimized WDBA (as returned by a successful run of + /// minimize_obligation()) represent safety property if it contains + /// only accepting transitions. + /// + /// \param aut the automaton to check + bool is_safety_mwdba(const tgba* aut); + + } #endif // SPOT_TGBAALGOS_SAFETY_HH diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 59fe4a5f0..9597f7356 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -90,7 +90,7 @@ TESTS = \ reduccmp.test \ reductgba.test \ scc.test \ - safety.test \ + obligation.test \ wdba.test \ randtgba.test \ emptchk.test \ diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 35e42353a..50a127da9 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -266,7 +266,8 @@ syntax(char* prog) << std::endl << " -NN output the never clain for Spin, with commented states" << " (implies -D)" << std::endl - << " -O tell whether the automaton is a safety automaton" + << " -O tell if a formula represents a safety, guarantee, " + << "or obligation property" << std::endl << " -t output automaton in LBTT's format" << std::endl << std::endl @@ -534,6 +535,7 @@ main(int argc, char** argv) else if (!strcmp(argv[formula_index], "-O")) { output = 13; + opt_minimize = true; } else if (!strcmp(argv[formula_index], "-p")) { @@ -1144,10 +1146,30 @@ main(int argc, char** argv) stats_reachable(a).dump(std::cout); break; case 13: - std::cout << (is_safety_automaton(a) ? - "is a safety automaton" : - "may not be a safety automaton") - << std::endl; + if (minimized == 0) + { + std::cout << "this is not an obligation property"; + } + else + { + if (is_guarantee_automaton(minimized)) + { + std::cout << "this is a guarantee property (hence, " + << "an obligation property)"; + } + else if (is_safety_mwdba(minimized)) + { + std::cout << "this is a safety property (hence, " + << "an obligation property)"; + } + else + { + std::cout << "this is an obligation property that is " + << "neither a safety nor a guarantee"; + } + } + std::cout << std::endl; + break; default: assert(!"unknown output option"); diff --git a/src/tgbatest/obligation.test b/src/tgbatest/obligation.test new file mode 100755 index 000000000..882385a4d --- /dev/null +++ b/src/tgbatest/obligation.test @@ -0,0 +1,116 @@ +#!/bin/sh +# Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 2 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with Spot; see the file COPYING. If not, write to the Free +# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +# 02111-1307, USA. + +. ./defs + +set +x +set -e + +cat >formulas.txt <(!p U r) +SA G(q->G(!p)) +SA G((q&!r&Fr)->(!p U r)) +SA G(q&!r->((!p U r)|G!p )) +SA (!r U (p&!r))|(G!r) +SA G(q&!r->((!r U (p&!r))|G!r)) +SA (!p U ((p U ((!p U ((p U G!p)|Gp))|G!p))|Gp))|G!p +SA Fr->((!p&!r)U(r|((p&!r)U(r|((!p&!r)U(r|((p&!r)U(r|(!p U r))))))))) +SA Fq->(!q U (q&((!p U ((p U ((!p U ((p U G!p)|Gp))|G!p))|Gp))|G!p))) +SA G((q&Fr)->((!p&!r)U(r|((p&!r)U(r|((!p&!r)U(r|((p&!r)U(r|(!p U r)))))))))) +SA G(q->((!p&!r)U(r|((p&!r)U(r|((!p&!r)U(r|((p&!r)U(r|((!p U r)|G!p)|Gp))))))))) +SA G(p) +SA Fr->(p U r) +SA G(q->G(p)) +SA G((p&!r&Fr)->(p U r)) +SA G(q&!r->((p U r)|Gp)) +SA Fr->(!p U (s|r)) +SA G((q&!r&Fr)->(!p U (s|r))) +SA G(q&!r->((!p U (s|r))|G!p)) +SA Fr->(p->(!r U (s&!r))) U r +SA G((q&!r&Fr)->(p->(!r U (s&!r))) U r) +SA Fp->(!p U (s&!p&X(!p U t))) +SA Fr->(!p U (r|(s&!p&X(!p U t)))) +SA (G!q)|(!q U (q&Fp->(!p U (s&!p&X(!p U t))))) +SA G((q&Fr)->(!p U (r|(s&!p&X(!p U t))))) +SA G(q->(Fp->(!p U (r|(s&!p&X(!p U t)))))) +SA (F(s&XFt))->((!s) U p) +SA Fr->((!(s&(!r)&X(!r U (t&!r))))U(r|p)) +SA (G!q)|((!q)U(q&((F(s&XFt))->((!s) U p)))) +SA G((q&Fr)->((!(s&(!r)&X(!r U (t&!r))))U(r|p))) +SA Fr->(p->(!r U (s&!r&X(!r U t)))) U r +SA G((q&Fr)->(p->(!r U (s&!r&X(!r U t)))) U r) +SA Fr->(p->(!r U (s&!r&!z&X((!r&!z) U t)))) U r +SA G((q&Fr)->(p->(!r U (s&!r&!z&X((!r&!z) U t)))) U r) +GU Fp +OB G(!q)|F(q&Fp) +OB (!p U s)|Gp +SA G(q->(!(s&(!r)&X(!r U (t&!r)))U(r|p)|G(!(s&XFt)))) +OB Fr->(s&X(!r U t)->X(!r U (t&Fp))) U r +NO G(q&!r->(!r U (p&!r))) +NO G!q|F(q&((!p U s)|G!p)) +NO G(p->Fs) +NO G(q->G(p->Fs)) +NO G(q&!r->(((p->(!r U (s&!r))) U r)|G(p->(!r U (s&!r))))) +NO G(s&XFt->X(F(t&Fp))) +NO G(q->G(s&XFt->X(!t U (t&Fp)))) +NO G((q&Fr)->(s&X(!r U t)->X(!r U (t&Fp))) U r) +NO G(q->(s&X(!r U t)->X(!r U (t&Fp)))U(r|G(s&X(!r U t)->X(!r U (t&Fp))))) +NO G(p->F(s&XFt)) +NO G(q->G(p->(s&XFt))) +NO G(q->(p->(!r U (s&!r&X(!r U t))))U(r|G(p->(s&XFt)))) +NO G(p->F(s&!z&X(!z U t))) +NO G(q->G(p->(s&!z&X(!z U t)))) +NO G(q->(p->(!r U (s&!r&!z&X((!r&!z) U t))))U(r|G(p->(s&!z&X(!z U t))))) +EOF + +grok() +{ + case $1 in + "this is a safety property"*) echo SA;; + "this is a guarantee property"*) echo GU;; + "this is an obligation property"*) echo OB;; + "this is not an obligation property"*) echo NO;; + *) echo XX;; + esac +} + +success=: +while read exp f; do + x=`../ltl2tgba -O "$f"` + y=`../ltl2tgba -O "!($f)"` + resx=`grok "$x"` + resy=`grok "$y"` + echo "$resx $f" + if test "$resx" != "$exp"; then + echo "Expected $exp, got $resx"; exit 1 + fi + echo "$resy !($f)" + case $resx,$resy in + SA,GU);; + GU,SA);; + OB,OB);; + NO,NO);; + *) echo "Incompatible results: $resx,$resy"; exit 1;; + esac +done < formulas.txt + +exit 0 diff --git a/src/tgbatest/safety.test b/src/tgbatest/safety.test deleted file mode 100755 index 964ed3847..000000000 --- a/src/tgbatest/safety.test +++ /dev/null @@ -1,108 +0,0 @@ -#!/bin/sh -# Copyright (C) 2010 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). -# -# This file is part of Spot, a model checking library. -# -# Spot is free software; you can redistribute it and/or modify it -# under the terms of the GNU General Public License as published by -# the Free Software Foundation; either version 2 of the License, or -# (at your option) any later version. -# -# Spot is distributed in the hope that it will be useful, but WITHOUT -# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -# License for more details. -# -# You should have received a copy of the GNU General Public License -# along with Spot; see the file COPYING. If not, write to the Free -# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA -# 02111-1307, USA. - -. ./defs - -set -e - -cat >safety.txt <(!p U r) -G(q->G(!p)) -G((q&!r&Fr)->(!p U r)) -G(q&!r->((!p U r)|G!p )) -(!r U (p&!r))|(G!r) -G(q&!r->((!r U (p&!r))|G!r)) -(!p U ((p U ((!p U ((p U G!p)|Gp))|G!p))|Gp))|G!p -Fr->((!p&!r)U(r|((p&!r)U(r|((!p&!r)U(r|((p&!r)U(r|(!p U r))))))))) -Fq->(!q U (q&((!p U ((p U ((!p U ((p U G!p)|Gp))|G!p))|Gp))|G!p))) -G((q&Fr)->((!p&!r)U(r|((p&!r)U(r|((!p&!r)U(r|((p&!r)U(r|(!p U r)))))))))) -G(q->((!p&!r)U(r|((p&!r)U(r|((!p&!r)U(r|((p&!r)U(r|((!p U r)|G!p)|Gp))))))))) -G(p) -Fr->(p U r) -G(q->G(p)) -G((p&!r&Fr)->(p U r)) -G(q&!r->((p U r)|Gp)) -Fr->(!p U (s|r)) -G((q&!r&Fr)->(!p U (s|r))) -G(q&!r->((!p U (s|r))|G!p)) -Fr->(p->(!r U (s&!r))) U r -G((q&!r&Fr)->(p->(!r U (s&!r))) U r) -Fp->(!p U (s&!p&X(!p U t))) -Fr->(!p U (r|(s&!p&X(!p U t)))) -(G!q)|(!q U (q&Fp->(!p U (s&!p&X(!p U t))))) -G((q&Fr)->(!p U (r|(s&!p&X(!p U t))))) -G(q->(Fp->(!p U (r|(s&!p&X(!p U t)))))) -(F(s&XFt))->((!s) U p) -Fr->((!(s&(!r)&X(!r U (t&!r))))U(r|p)) -(G!q)|((!q)U(q&((F(s&XFt))->((!s) U p)))) -G((q&Fr)->((!(s&(!r)&X(!r U (t&!r))))U(r|p))) -Fr->(p->(!r U (s&!r&X(!r U t)))) U r -G((q&Fr)->(p->(!r U (s&!r&X(!r U t)))) U r) -Fr->(p->(!r U (s&!r&!z&X((!r&!z) U t)))) U r -G((q&Fr)->(p->(!r U (s&!r&!z&X((!r&!z) U t)))) U r) -EOF - -# The negation of the first 5 formulae are not safety properties, but they -# are obligation properties. -cat >non-safety.txt <(!(s&(!r)&X(!r U (t&!r)))U(r|p)|G(!(s&XFt)))) -Fr->(s&X(!r U t)->X(!r U (t&Fp))) U r -G(q&!r->(!r U (p&!r))) -G!q|F(q&((!p U s)|G!p)) -G(p->Fs) -G(q->G(p->Fs)) -G(q&!r->(((p->(!r U (s&!r))) U r)|G(p->(!r U (s&!r))))) -G(s&XFt->X(F(t&Fp))) -G(q->G(s&XFt->X(!t U (t&Fp)))) -G((q&Fr)->(s&X(!r U t)->X(!r U (t&Fp))) U r) -G(q->(s&X(!r U t)->X(!r U (t&Fp)))U(r|G(s&X(!r U t)->X(!r U (t&Fp))))) -G(p->F(s&XFt)) -G(q->G(p->(s&XFt))) -G(q->(p->(!r U (s&!r&X(!r U t))))U(r|G(p->(s&XFt)))) -G(p->F(s&!z&X(!z U t))) -G(q->G(p->(s&!z&X(!z U t)))) -G(q->(p->(!r U (s&!r&!z&X((!r&!z) U t))))U(r|G(p->(s&!z&X(!z U t))))) -EOF - -success=: -while read f; do - x=`../ltl2tgba -f -R3f -O "!($f)"` - case $x in - *may*) echo "MNO !($f)"; success=false;; - *) echo "OBL !($f)";; - esac -done < safety.txt - -echo ==== - -while read f; do - x=`../ltl2tgba -f -R3f -O "!($f)"` - case $x in - *may*) echo "MNO !($f)";; - *) echo "OBL !($f)"; success=false;; - esac -done < non-safety.txt - -$success