ltl2tgba.html: Display properties of formulas.

* src/ltlast/formula.hh, src/ltlast/formula.cc (list_formula_props):
New function.
* wrap/python/spot.i: Adjust to wrap list_formula_props.
* wrap/python/ajax/ltl2tgba.html: Add option to display properties.
* wrap/python/ajax/spot.in: Handle ff=p and display properties.
* wrap/python/ajax/protocol.txt: Adjust.

src/ltlast/formula.cc

@@ -1,7 +1,8 @@
-// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement
+// -*- encoding: utf-8 -*-
-// de l'Epita (LRDE).
+// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
-// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
@@ -62,6 +63,41 @@ namespace spot
       return false;
     }
 
+
+#define printprops							\
+      proprint(is_boolean, "B", "Boolean formula");			\
+      proprint(is_sugar_free_boolean, "&", "without Boolean sugar");	\
+      proprint(is_in_nenoform, "!", "in negative normal form");		\
+      proprint(is_X_free, "x", "without X operator");			\
+      proprint(is_sugar_free_ltl, "f", "without LTL sugar");		\
+      proprint(is_ltl_formula, "L", "LTL formula");			\
+      proprint(is_eltl_formula, "E", "ELTL formula");			\
+      proprint(is_psl_formula, "P", "PSL formula");			\
+      proprint(is_sere_formula, "S", "SERE formula");			\
+      proprint(is_finite, "F", "finite");				\
+      proprint(is_eventual, "e", "pure eventuality");			\
+      proprint(is_universal, "u", "purely universal");			\
+      proprint(is_syntactic_safety, "s", "syntactic safety");		\
+      proprint(is_syntactic_guarantee, "g", "syntactic guarantee");	\
+      proprint(is_syntactic_obligation, "o", "syntactic obligation");	\
+      proprint(is_syntactic_persistence, "p", "syntactic persistence");	\
+      proprint(is_syntactic_recurrence, "r", "syntactic recurrence");	\
+      proprint(is_marked, "+", "marked");				\
+      proprint(accepts_eword, "0", "accepts the empty word");
+
+
+    std::list<std::string>
+    list_formula_props(const formula* f)
+    {
+      std::list<std::string> res;
+#define proprint(m, a, l)			\
+      if (f->m())				\
+	res.push_back(std::string(l));
+      printprops;
+#undef proprint
+      return res;
+    }
+
     std::ostream&
     print_formula_props(std::ostream& out, const formula* f, bool abbr)
     {
@@ -74,26 +110,9 @@ namespace spot
 	  out << sep; out << (abbr ? a : l);	\
 	  sep = comma;				\
 	}
+      printprops;
+#undef proprint
 
-      proprint(is_boolean, "B", "Boolean formula");
-      proprint(is_sugar_free_boolean, "&", "without Boolean sugar");
-      proprint(is_in_nenoform, "!", "in negative normal form");
-      proprint(is_X_free, "x", "without X operator");
-      proprint(is_sugar_free_ltl, "f", "without LTL sugar");
-      proprint(is_ltl_formula, "L", "LTL formula");
-      proprint(is_eltl_formula, "E", "ELTL formula");
-      proprint(is_psl_formula, "P", "PSL formula");
-      proprint(is_sere_formula, "S", "SERE formula");
-      proprint(is_finite, "F", "finite");
-      proprint(is_eventual, "e", "pure eventuality");
-      proprint(is_universal, "u", "purely universal");
-      proprint(is_syntactic_safety, "s", "syntactic safety");
-      proprint(is_syntactic_guarantee, "g", "syntactic guarantee");
-      proprint(is_syntactic_obligation, "o", "syntactic obligation");
-      proprint(is_syntactic_persistence, "p", "syntactic persistence");
-      proprint(is_syntactic_recurrence, "r", "syntactic recurrence");
-      proprint(is_marked, "+", "marked");
-      proprint(accepts_eword, "0", "accepts the empty word");
       return out;
     }
   }

src/ltlast/formula.hh

@@ -1,5 +1,6 @@
-// Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et
+// -*- encoding: utf-8 -*-
-// Développement de l'Epita (LRDE).
+// Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche
+// et Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de
 //
 // This file is part of Spot, a model checking library.
@@ -27,6 +28,7 @@
 #include <string>
 #include <cassert>
 #include "predecl.hh"
+#include <list>
 
 namespace spot
 {
@@ -418,6 +420,8 @@ namespace spot
 				      const formula* f,
 				      bool abbreviated = false);
 
+    /// List the properties of formula \a f.
+    std::list<std::string> list_formula_props(const formula* f);
   }
 }
 

wrap/python/ajax/ltl2tgba.html

@@ -391,6 +391,10 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
 		  <INPUT type="radio" name="ff" value="g">
 		  a syntactic tree
 		</label><br>
+		<label class="rtip" title="Various properties of the formula.">
+		  <INPUT type="radio" name="ff" value="p">
+		  property information
+		</label><br>
 	      </div>
 	      <div id="tabs-om">
 		Translate the (simplified) formula as:<br>

wrap/python/ajax/protocol.txt

@@ -24,7 +24,8 @@ Type of formula output if o=f (pick one)
 
   ff=o    Spot syntax
   ff=i    Spin syntax
-  ff=g    graphviz
+  ff=g    graphviz output of the AST
+  ff=p    property dump
 
 Type of automaton if o=a (pick one)
 

wrap/python/ajax/spot.in

@@ -371,7 +371,7 @@ if dored:
 # Formula manipulation only.
 if output_type == 'f':
     formula_format = form.getfirst('ff', 'o')
-    # o = Spot, i = Spin, g = GraphViz
+    # o = Spot, i = Spin, g = GraphViz, p = properties
     if formula_format == 'o':
         unbufprint('<div class="formula spot-format">%s</div>' % f)
     elif formula_format == 'i':
@@ -379,6 +379,30 @@ if output_type == 'f':
                    + spot.to_spin_string(f) + '</div>')
     elif formula_format == 'g':
         render_formula(f)
+    elif formula_format == 'p':
+        unbufprint('Properties for <span class="formula spot-format">%s</span><ul>\n' % f)
+        for p in spot.list_formula_props(f):
+            unbufprint('<li>%s</li>\n' % p)
+
+        # Attempt to refine the hierarchy class using WDBA minimization
+        if not f.is_syntactic_safety() or not f.is_syntactic_guarantee():
+            dict = spot.bdd_dict()
+            automaton = spot.ltl_to_tgba_fm(f, dict, False, True)
+            minimized = spot.minimize_obligation_new(automaton, f)
+            if minimized:
+                g = spot.is_guarantee_automaton(minimized)
+                s = spot.is_safety_mwdba(minimized)
+                if s and not f.is_syntactic_safety():
+                    unbufprint('<li>pathologic safety</li>')
+                if g and not f.is_syntactic_guarantee():
+                    unbufprint('<li>pathologic guarantee</li>')
+                if not f.is_syntactic_obligation():
+                    unbufprint('<li>obligation (although not syntactically)</li>')
+            else:
+                unbufprint('<li>not an obligation</li>')
+            minimized = 0
+            automaton = 0
+        unbufprint('</ul>\n')
     finish()
 
 # Formula translation.

wrap/python/spot.i

@@ -33,6 +33,10 @@
 %include "std_string.i"
 %include "std_list.i"
 
+namespace std {
+   %template(liststr) list<string>;
+};
+
 %import "buddy.i"
 
 %{
@@ -98,6 +102,7 @@
 #include "tgbaalgos/neverclaim.hh"
 #include "tgbaalgos/rundotdec.hh"
 #include "tgbaalgos/save.hh"
+#include "tgbaalgos/safety.hh"
 #include "tgbaalgos/sccfilter.hh"
 #include "tgbaalgos/stats.hh"
 #include "tgbaalgos/simulation.hh"
@@ -226,6 +231,7 @@ using namespace spot;
 %include "tgbaalgos/neverclaim.hh"
 %include "tgbaalgos/rundotdec.hh"
 %include "tgbaalgos/save.hh"
+%include "tgbaalgos/safety.hh"
 %include "tgbaalgos/sccfilter.hh"
 %include "tgbaalgos/stats.hh"
 %include "tgbaalgos/simulation.hh"