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

@@ -1,3 +1,27 @@
+2011-01-27  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	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  <adl@lrde.epita.fr>
 
 	* NEWS: Minor rewritings.

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.

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;

src/tgbaalgos/safety.cc

@@ -19,11 +19,13 @@
 // 02111-1307, USA.
 
 #include "safety.hh"
+#include "misc/hash.hh"
+#include <deque>
 
 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<const state*,
+			  state_ptr_hash, state_ptr_equal> seen_map;
+    seen_map seen;		   // States already seen.
+    std::deque<const state*> 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;
+  }
 
 
 

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
+  /// A weak deterministic TGBA represents a guarantee property if any
-  /// accepting state with only one transition that is a self-loop
+  /// accepting path ends on an accepting state with only one
-  /// labelled by true.  Note that this is only a sufficient
+  /// transition that is a self-loop labelled by true.
-  /// condition.  Some safety automata might not be recognized with
+  ///
-  /// this check because of some non-determinism in the automaton.
+  /// 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

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 \

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) ?
+	      if (minimized == 0)
-			    "is a safety automaton" :
+		{
-			    "may not be a safety automaton")
+		  std::cout << "this is not an obligation property";
-			<< std::endl;
+		}
+	      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");

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 <<EOF
+SA G(!p)
+SA Fr->(!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

src/tgbatest/safety.test

@@ -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 <<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 5 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