diff --git a/src/ltlast/formula.cc b/src/ltlast/formula.cc index 8e906f977..aa9e91b86 100644 --- a/src/ltlast/formula.cc +++ b/src/ltlast/formula.cc @@ -1,7 +1,8 @@ -// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- encoding: utf-8 -*- +// 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 + list_formula_props(const formula* f) + { + std::list 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; } } diff --git a/src/ltlast/formula.hh b/src/ltlast/formula.hh index 92ec764c9..5773f2a8b 100644 --- a/src/ltlast/formula.hh +++ b/src/ltlast/formula.hh @@ -1,5 +1,6 @@ -// Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// -*- encoding: utf-8 -*- +// 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 #include #include "predecl.hh" +#include namespace spot { @@ -418,6 +420,8 @@ namespace spot const formula* f, bool abbreviated = false); + /// List the properties of formula \a f. + std::list list_formula_props(const formula* f); } } diff --git a/wrap/python/ajax/ltl2tgba.html b/wrap/python/ajax/ltl2tgba.html index 5d51945c1..a767847eb 100644 --- a/wrap/python/ajax/ltl2tgba.html +++ b/wrap/python/ajax/ltl2tgba.html @@ -391,6 +391,10 @@ an identifier: aUb is an atomic proposition, unlike a syntactic tree
+
Translate the (simplified) formula as:
diff --git a/wrap/python/ajax/protocol.txt b/wrap/python/ajax/protocol.txt index 94c2d80e2..e56c28457 100644 --- a/wrap/python/ajax/protocol.txt +++ b/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) diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in index 580e9c1a8..2c98dbb58 100755 --- a/wrap/python/ajax/spot.in +++ b/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('
%s
' % f) elif formula_format == 'i': @@ -379,6 +379,30 @@ if output_type == 'f': + spot.to_spin_string(f) + '
') elif formula_format == 'g': render_formula(f) + elif formula_format == 'p': + unbufprint('Properties for %s
    \n' % f) + for p in spot.list_formula_props(f): + unbufprint('
  • %s
    • \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('
  • pathologic safety
    • ') + if g and not f.is_syntactic_guarantee(): + unbufprint('
  • pathologic guarantee
    • ') + if not f.is_syntactic_obligation(): + unbufprint('
  • obligation (although not syntactically)
    • ') + else: + unbufprint('
  • not an obligation
    • ') + minimized = 0 + automaton = 0 + unbufprint('
\n') finish() # Formula translation. diff --git a/wrap/python/spot.i b/wrap/python/spot.i index 1167a9393..c6cd9c18c 100644 --- a/wrap/python/spot.i +++ b/wrap/python/spot.i @@ -33,6 +33,10 @@ %include "std_string.i" %include "std_list.i" +namespace std { + %template(liststr) list; +}; + %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"