From 0af8d032614102f6c20f6584d8d7730227c7920c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 20 Mar 2010 12:57:36 +0100 Subject: [PATCH] Implement is_safety_automaton(). * src/tgbaalgos/safety.hh, src/tgbaalgos/safety.cc: New files. * src/tgbaalgos/Makefile.am: Add them. * src/tgbatests/ltl2tgba.cc: Add option "-O". * src/tgbaalgos/scc.hh: Update documentation. * src/tgbatest/Makefile.am (TESTS): Add safety.test. * src/tgbatest/safety.test: New file. --- ChangeLog | 12 +++++ src/tgbaalgos/Makefile.am | 11 ++-- src/tgbaalgos/safety.cc | 75 ++++++++++++++++++++++++++ src/tgbaalgos/safety.hh | 44 ++++++++++++++++ src/tgbaalgos/scc.hh | 6 ++- src/tgbatest/Makefile.am | 1 + src/tgbatest/ltl2tgba.cc | 13 +++++ src/tgbatest/safety.test | 108 ++++++++++++++++++++++++++++++++++++++ 8 files changed, 264 insertions(+), 6 deletions(-) create mode 100644 src/tgbaalgos/safety.cc create mode 100644 src/tgbaalgos/safety.hh create mode 100755 src/tgbatest/safety.test diff --git a/ChangeLog b/ChangeLog index a9d0d0448..51bf97332 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,15 @@ +2010-03-20 Alexandre Duret-Lutz + + Implement is_safety_automaton(). + + * src/tgbaalgos/safety.hh, src/tgbaalgos/safety.cc: New + files. + * src/tgbaalgos/Makefile.am: Add them. + * src/tgbatests/ltl2tgba.cc: Add option "-O". + * src/tgbaalgos/scc.hh: Update documentation. + * src/tgbatest/Makefile.am (TESTS): Add safety.test. + * src/tgbatest/safety.test: New file. + 2010-03-26 Felix Abecassis * src/tgbaalgos/minimize.cc: Now use register_anonymous_variables. diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index dc9bd7546..dc56b1cda 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -1,7 +1,8 @@ -## Copyright (C) 2003, 2004, 2005, 2008, 2009 Laboratoire -## d'Informatique de Paris 6 (LIP6), -## département Systèmes Répartis Coopératifs (SRC), Université Pierre -## et Marie Curie. +## Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et +## Développement de l'Epita (LRDE). +## Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris +## 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +## Université Pierre et Marie Curie. ## ## This file is part of Spot, a model checking library. ## @@ -51,6 +52,7 @@ tgbaalgos_HEADERS = \ reducerun.hh \ replayrun.hh \ rundotdec.hh \ + safety.hh \ save.hh \ scc.hh \ sccfilter.hh \ @@ -86,6 +88,7 @@ libtgbaalgos_la_SOURCES = \ reducerun.cc \ replayrun.cc \ rundotdec.cc \ + safety.cc \ save.cc \ scc.cc \ sccfilter.cc \ diff --git a/src/tgbaalgos/safety.cc b/src/tgbaalgos/safety.cc new file mode 100644 index 000000000..42d86d15e --- /dev/null +++ b/src/tgbaalgos/safety.cc @@ -0,0 +1,75 @@ +// 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. + +#include "safety.hh" + +namespace spot +{ + bool + is_safety_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; + if (need_sm) + { + scc_map* x = new scc_map(aut); + x->build_map(); + sm = x; + } + + bool result = true; + + unsigned scc_count = sm->scc_count(); + for (unsigned scc = 0; (scc < scc_count) && result; ++scc) + { + if (!sm->accepting(scc)) + continue; + // Accepting SCCs should have only one state. + const std::list& st = sm->states_of(scc); + if (st.size() != 1) + { + result = false; + break; + } + // The state should have only one transition that is a + // self-loop labelled by true. + const state* s = *st.begin(); + tgba_succ_iterator* it = aut->succ_iter(s); + it->first(); + assert(!it->done()); + state* dest = it->current_state(); + bdd cond = it->current_condition(); + it->next(); + result = (!dest->compare(s)) && it->done() && (cond == bddtrue); + delete dest; + delete it; + } + + // Free the scc_map if we created it. + if (need_sm) + delete sm; + + return result; + } + + + + +} diff --git a/src/tgbaalgos/safety.hh b/src/tgbaalgos/safety.hh new file mode 100644 index 000000000..ac55e6c12 --- /dev/null +++ b/src/tgbaalgos/safety.hh @@ -0,0 +1,44 @@ +// 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. + +#ifndef SPOT_TGBAALGOS_SAFETY_HH +# define SPOT_TGBAALGOS_SAFETY_HH + +#include "scc.hh" + +namespace spot +{ + /// \brief Whether an automaton is a safety 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. + /// + /// \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); +} + +#endif // SPOT_TGBAALGOS_SAFETY_HH diff --git a/src/tgbaalgos/scc.hh b/src/tgbaalgos/scc.hh index 998f6c4bd..920cc0bd6 100644 --- a/src/tgbaalgos/scc.hh +++ b/src/tgbaalgos/scc.hh @@ -1,5 +1,5 @@ -// Copyright (C) 2008, 2009 Laboratoire de Recherche et Developpement de -// l'Epita. +// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et +// Developpement de l'Epita. // // This file is part of Spot, a model checking library. // @@ -90,6 +90,8 @@ namespace spot /// \brief Get the number of SCC in the automaton. /// + /// SCCs are labelled from 0 to scc_count()-1. + /// /// \pre This should only be called once build_map() has run. unsigned scc_count() const; diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index f3867f054..154a99005 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -92,6 +92,7 @@ TESTS = \ reduccmp.test \ reductgba.test \ scc.test \ + safety.test \ randtgba.test \ emptchk.test \ emptchke.test \ diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 9eaa05204..4e0e7c877 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -53,6 +53,7 @@ #include "tgbaalgos/replayrun.hh" #include "tgbaalgos/rundotdec.hh" #include "tgbaalgos/sccfilter.hh" +#include "tgbaalgos/safety.hh" #include "tgbaalgos/eltl2tgba_lacim.hh" #include "eltlparse/public.hh" #include "misc/timer.hh" @@ -256,6 +257,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" + << std::endl << " -t output automaton in LBTT's format" << std::endl << std::endl @@ -522,6 +525,10 @@ main(int argc, char** argv) output = 8; spin_comments = true; } + else if (!strcmp(argv[formula_index], "-O")) + { + output = 13; + } else if (!strcmp(argv[formula_index], "-p")) { post_branching = true; @@ -1087,6 +1094,12 @@ main(int argc, char** argv) case 12: 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; + break; default: assert(!"unknown output option"); } diff --git a/src/tgbatest/safety.test b/src/tgbatest/safety.test new file mode 100755 index 000000000..cd7712921 --- /dev/null +++ b/src/tgbatest/safety.test @@ -0,0 +1,108 @@ +#!/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 4 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