hierarchy: expose mp_class to python
* bin/common_output.cc: Move some of the printing code... * spot/tl/hierarchy.cc, spot/tl/hierarchy.hh: ... here, as new variants of mp_class... * python/spot/impl.i: ... that we can now call from Python. * python/ajax/spotcgi.in: Use those to simplify and extend the code printing class membership.
This commit is contained in:
Alexandre Duret-Lutz
parent
a0891fde18
commit
ebdb198b64
5 changed files with 156 additions and 105 deletions
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- 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).
|
// Développement de l'Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
@ -172,92 +172,10 @@ namespace
|
||||||
virtual void
|
virtual void
|
||||||
print(std::ostream& os, const char* opt) const override
|
print(std::ostream& os, const char* opt) const override
|
||||||
{
|
{
|
||||||
bool verbose = false;
|
|
||||||
bool wide = false;
|
|
||||||
if (*opt == '[')
|
if (*opt == '[')
|
||||||
do
|
os << spot::mp_class(val_, opt + 1);
|
||||||
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
|
else
|
||||||
os << ' ';
|
os << val_;
|
||||||
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;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -505,24 +505,20 @@ if output_type == 'f':
|
||||||
for p in spot.list_formula_props(f):
|
for p in spot.list_formula_props(f):
|
||||||
unbufprint('<li>%s</li>\n' % p)
|
unbufprint('<li>%s</li>\n' % p)
|
||||||
|
|
||||||
# Attempt to refine the hierarchy class using WDBA minimization
|
mpc = spot.mp_class(f, 'w')
|
||||||
if not f.is_syntactic_safety() or not f.is_syntactic_guarantee():
|
if 'S' in mpc:
|
||||||
dict = spot.bdd_dict()
|
unbufprint('<li>safety</li>')
|
||||||
automaton = spot.ltl_to_tgba_fm(f, dict, False, True)
|
if 'G' in mpc:
|
||||||
minimized = spot.minimize_obligation(automaton, f)
|
unbufprint('<li>guarantee</li>')
|
||||||
if minimized != automaton:
|
if 'O' in mpc:
|
||||||
g = spot.is_terminal_automaton(minimized, None, True)
|
unbufprint('<li>obligation</li>')
|
||||||
s = spot.is_safety_automaton(minimized)
|
if 'R' in mpc:
|
||||||
if s and not f.is_syntactic_safety():
|
unbufprint('<li>recurrence</li>')
|
||||||
unbufprint('<li>pathologic safety</li>')
|
if 'P' in mpc:
|
||||||
if g and not f.is_syntactic_guarantee():
|
unbufprint('<li>persistence</li>')
|
||||||
unbufprint('<li>pathologic guarantee</li>')
|
if 'T' == mpc:
|
||||||
if not f.is_syntactic_obligation():
|
unbufprint('<li>not a persistence nor a recurrence</li>')
|
||||||
unbufprint('<li>obligation (although not syntactically)</li>')
|
|
||||||
else:
|
|
||||||
unbufprint('<li>not an obligation</li>')
|
|
||||||
minimized = 0
|
|
||||||
automaton = 0
|
|
||||||
if not f.is_syntactic_stutter_invariant():
|
if not f.is_syntactic_stutter_invariant():
|
||||||
if spot.is_stutter_invariant(f):
|
if spot.is_stutter_invariant(f):
|
||||||
unbufprint('<li>stutter invariant</li>')
|
unbufprint('<li>stutter invariant</li>')
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- 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).
|
// Laboratoire de Recherche et Développement de l'Epita (LRDE).
|
||||||
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique
|
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique
|
||||||
// de Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
// de Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
||||||
|
|
@ -103,6 +103,7 @@
|
||||||
#include <spot/tl/randomltl.hh>
|
#include <spot/tl/randomltl.hh>
|
||||||
#include <spot/tl/length.hh>
|
#include <spot/tl/length.hh>
|
||||||
#include <spot/tl/ltlf.hh>
|
#include <spot/tl/ltlf.hh>
|
||||||
|
#include <spot/tl/hierarchy.hh>
|
||||||
#include <spot/tl/remove_x.hh>
|
#include <spot/tl/remove_x.hh>
|
||||||
#include <spot/tl/relabel.hh>
|
#include <spot/tl/relabel.hh>
|
||||||
|
|
||||||
|
|
@ -448,6 +449,7 @@ namespace std {
|
||||||
%include <spot/tl/randomltl.hh>
|
%include <spot/tl/randomltl.hh>
|
||||||
%include <spot/tl/length.hh>
|
%include <spot/tl/length.hh>
|
||||||
%include <spot/tl/ltlf.hh>
|
%include <spot/tl/ltlf.hh>
|
||||||
|
%include <spot/tl/hierarchy.hh>
|
||||||
%include <spot/tl/remove_x.hh>
|
%include <spot/tl/remove_x.hh>
|
||||||
%include <spot/tl/relabel.hh>
|
%include <spot/tl/relabel.hh>
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -17,6 +17,7 @@
|
||||||
// You should have received a copy of the GNU General Public License
|
// You should have received a copy of the GNU General Public License
|
||||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||||
|
|
||||||
|
#include <sstream>
|
||||||
#include <spot/tl/hierarchy.hh>
|
#include <spot/tl/hierarchy.hh>
|
||||||
#include <spot/twaalgos/isdet.hh>
|
#include <spot/twaalgos/isdet.hh>
|
||||||
#include <spot/twaalgos/ltl2tgba_fm.hh>
|
#include <spot/twaalgos/ltl2tgba_fm.hh>
|
||||||
|
|
@ -85,4 +86,108 @@ namespace spot
|
||||||
return 'P';
|
return 'P';
|
||||||
return 'T';
|
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();
|
||||||
|
}
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -37,4 +37,34 @@ namespace spot
|
||||||
/// - 'T' (top) properties that are not persistence or recurrence
|
/// - 'T' (top) properties that are not persistence or recurrence
|
||||||
/// properties
|
/// properties
|
||||||
SPOT_API char mp_class(formula f);
|
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);
|
||||||
}
|
}
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue