diff --git a/bin/common_output.cc b/bin/common_output.cc
index 0c0d8625784b04f82297dee7ea7cbac3a96f93ba..2a6a920607ae447c2547d99540e5ac55b1e1f132 100644
--- a/bin/common_output.cc
+++ b/bin/common_output.cc
@@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche et
+// Copyright (C) 2012, 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@@ -172,92 +172,10 @@ namespace
virtual void
print(std::ostream& os, const char* opt) const override
{
- bool verbose = false;
- bool wide = false;
if (*opt == '[')
- do
- switch (*++opt)
- {
- case 'v':
- verbose = true;
- break;
- case 'w':
- wide = true;
- break;
- case ' ':
- case '\t':
- case '\n':
- case ',':
- case ']':
- break;
- }
- while (*opt != ']');
-
- std::string c(1, val_);
- if (wide)
- {
- switch (val_)
- {
- case 'B':
- c = "GSOPRT";
- break;
- case 'G':
- c = "GOPRT";
- break;
- case 'S':
- c = "SOPRT";
- break;
- case 'O':
- c = "OPRT";
- break;
- case 'P':
- c = "PT";
- break;
- case 'R':
- c = "RT";
- break;
- case 'T':
- break;
- }
- }
- if (!verbose)
- {
- os << c;
- return;
- }
-
- bool first = true;
- for (char ch: c)
- {
- if (first)
- first = false;
- else
- os << ' ';
- switch (ch)
- {
- case 'B':
- os << "guarantee safety";
- break;
- case 'G':
- os << "guarantee";
- break;
- case 'S':
- os << "safety";
- break;
- case 'O':
- os << "obligation";
- break;
- case 'P':
- os << "persistence";
- break;
- case 'R':
- os << "recurrence";
- break;
- case 'T':
- os << "reactivity";
- break;
- }
- }
+ os << spot::mp_class(val_, opt + 1);
+ else
+ os << val_;
}
};
diff --git a/python/ajax/spotcgi.in b/python/ajax/spotcgi.in
index 474d10edf64386c7fe5cc7767ab198cffa06a693..d0f9402085fb8fa8111b010774bd0256ffdd942a 100755
--- a/python/ajax/spotcgi.in
+++ b/python/ajax/spotcgi.in
@@ -505,24 +505,20 @@ if output_type == '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(automaton, f)
- if minimized != automaton:
- g = spot.is_terminal_automaton(minimized, None, True)
- s = spot.is_safety_automaton(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
+ mpc = spot.mp_class(f, 'w')
+ if 'S' in mpc:
+ unbufprint('safety')
+ if 'G' in mpc:
+ unbufprint('guarantee')
+ if 'O' in mpc:
+ unbufprint('obligation')
+ if 'R' in mpc:
+ unbufprint('recurrence')
+ if 'P' in mpc:
+ unbufprint('persistence')
+ if 'T' == mpc:
+ unbufprint('not a persistence nor a recurrence')
+
if not f.is_syntactic_stutter_invariant():
if spot.is_stutter_invariant(f):
unbufprint('stutter invariant')
diff --git a/python/spot/impl.i b/python/spot/impl.i
index cff9ca1c9e347537281cf2d11e3d432275da441b..8dfefa14ef1bd4ae825458c15b3b8555e470dd87 100644
--- a/python/spot/impl.i
+++ b/python/spot/impl.i
@@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016
+// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2017
// Laboratoire de Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique
// de Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -103,6 +103,7 @@
#include
#include
#include
+#include
#include
#include
@@ -448,6 +449,7 @@ namespace std {
%include
%include
%include
+%include
%include
%include
diff --git a/spot/tl/hierarchy.cc b/spot/tl/hierarchy.cc
index 53c5531e3121041913df1d279f559dc94051f7fc..e7967209f82664278396d1993ae48140f2709414 100644
--- a/spot/tl/hierarchy.cc
+++ b/spot/tl/hierarchy.cc
@@ -17,6 +17,7 @@
// You should have received a copy of the GNU General Public License
// along with this program. If not, see .
+#include
#include
#include
#include
@@ -85,4 +86,108 @@ namespace spot
return 'P';
return 'T';
}
+
+ std::string mp_class(formula f, const char* opt)
+ {
+ return mp_class(mp_class(f), opt);
+ }
+
+ std::string mp_class(char mpc, const char* opt)
+ {
+ bool verbose = false;
+ bool wide = false;
+ if (opt)
+ for (;;)
+ switch (int o = *opt++)
+ {
+ case 'v':
+ verbose = true;
+ break;
+ case 'w':
+ wide = true;
+ break;
+ case ' ':
+ case '\t':
+ case '\n':
+ case ',':
+ break;
+ case '\0':
+ case ']':
+ goto break2;
+ default:
+ {
+ std::ostringstream err;
+ err << "unknown option '" << o << "' for mp_class()";
+ throw std::runtime_error(err.str());
+ }
+ }
+ break2:
+ std::string c(1, mpc);
+ if (wide)
+ {
+ switch (mpc)
+ {
+ case 'B':
+ c = "GSOPRT";
+ break;
+ case 'G':
+ c = "GOPRT";
+ break;
+ case 'S':
+ c = "SOPRT";
+ break;
+ case 'O':
+ c = "OPRT";
+ break;
+ case 'P':
+ c = "PT";
+ break;
+ case 'R':
+ c = "RT";
+ break;
+ case 'T':
+ break;
+ default:
+ throw std::runtime_error("mp_class() called with unknown class");
+ }
+ }
+ if (!verbose)
+ return c;
+
+ std::ostringstream os;
+ bool first = true;
+ for (char ch: c)
+ {
+ if (first)
+ first = false;
+ else
+ os << ' ';
+ switch (ch)
+ {
+ case 'B':
+ os << "guarantee safety";
+ break;
+ case 'G':
+ os << "guarantee";
+ break;
+ case 'S':
+ os << "safety";
+ break;
+ case 'O':
+ os << "obligation";
+ break;
+ case 'P':
+ os << "persistence";
+ break;
+ case 'R':
+ os << "recurrence";
+ break;
+ case 'T':
+ os << "reactivity";
+ break;
+ }
+ }
+ return os.str();
+ }
+
}
diff --git a/spot/tl/hierarchy.hh b/spot/tl/hierarchy.hh
index 150ac91f878962d03557a6d3196efaeded213950..88def1831b9e846985a8f4caab9a0f5dce6eb79d 100644
--- a/spot/tl/hierarchy.hh
+++ b/spot/tl/hierarchy.hh
@@ -37,4 +37,34 @@ namespace spot
/// - 'T' (top) properties that are not persistence or recurrence
/// properties
SPOT_API char mp_class(formula f);
+
+
+ /// \brief Return the class of \a f in the temporal hierarchy of Manna
+ /// and Pnueli (PODC'90).
+ ///
+ /// The \a opt parameter should be a string specifying options
+ /// for expressing the class. If \a opt is empty, the
+ /// result is one character among B, G, S, O, P, R, T, specifying
+ /// the most precise class to which the formula belongs.
+ /// If \a opt contains 'w', then the string contains all the
+ /// characters corresponding to the classes that contain \a f.
+ /// If \a opt contains 'v', then the characters are replaced
+ /// by the name of each class. Space and commas are ignored.
+ /// Any ']' ends the processing of the options.
+ SPOT_API std::string mp_class(formula f, const char* opt);
+
+ /// \brief Expand a class in the temporal hierarchy of Manna
+ /// and Pnueli (PODC'90).
+ ///
+ /// \a mpc should be a character among B, G, S, O, P, R, T
+ /// specifying a class in the hierarchy.
+ ///
+ /// The \a opt parameter should be a string specifying options for
+ /// expressing the class. If \a opt is empty, the result is \a mpc.
+ /// If \a opt contains 'w', then the string contains all the
+ /// characters corresponding to the super-classes of \a mpc. If \a
+ /// opt contains 'v', then the characters are replaced by the name
+ /// of each class. Space and commas are ignored. Any ']' ends the
+ /// processing of the options.
+ SPOT_API std::string mp_class(char mpc, const char* opt);
}