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

@@ -1,3 +1,15 @@
+2010-03-20  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	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  <abecassis@lrde.epita.fr>
 
 	* src/tgbaalgos/minimize.cc: Now use register_anonymous_variables.

src/tgbaalgos/Makefile.am

@@ -1,7 +1,8 @@
-## Copyright (C) 2003, 2004, 2005, 2008, 2009 Laboratoire
+## Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et
-## d'Informatique de Paris 6 (LIP6),
+## Développement de l'Epita (LRDE).
-## département Systèmes Répartis Coopératifs (SRC), Université Pierre
+## Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris
-## et Marie Curie.
+## 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 \

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<const state*>& 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;
+  }
+
+
+
+
+}

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

src/tgbaalgos/scc.hh

@@ -1,5 +1,5 @@
-// Copyright (C) 2008, 2009  Laboratoire de Recherche et Developpement de
+// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et
-// l'Epita.
+// 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;
 

src/tgbatest/Makefile.am

@@ -92,6 +92,7 @@ TESTS = \
   reduccmp.test \
   reductgba.test \
   scc.test \
+  safety.test \
   randtgba.test \
   emptchk.test \
   emptchke.test \

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");
 	    }

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 <<EOF
+G(!p)
+Fr->(!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 <<EOF
+Fp
+G(!q)|F(q&Fp)
+(!p U s)|Gp
+G(q->(!(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