From 7d9ce0d6fcd44ef012cfc774647186274b3cce7c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 10 Jan 2017 21:34:56 +0100 Subject: [PATCH] tl: mp_class() and --format=%[vw]h Tools for deciding the class of a formula. * spot/tl/hierarchy.cc, spot/tl/hierarchy.hh: New files. * spot/tl/Makefile.am: Add them. * bin/common_output.cc, bin/common_output.hh: Implement --format=%h. * tests/core/hierarchy.test: More tests. * NEWS: Update. --- NEWS | 8 +++ bin/common_output.cc | 108 ++++++++++++++++++++++++++++++++++++++ bin/common_output.hh | 22 ++++---- spot/tl/Makefile.am | 6 ++- spot/tl/hierarchy.cc | 85 ++++++++++++++++++++++++++++++ spot/tl/hierarchy.hh | 40 ++++++++++++++ tests/core/hierarchy.test | 18 +++++++ 7 files changed, 276 insertions(+), 11 deletions(-) create mode 100644 spot/tl/hierarchy.cc create mode 100644 spot/tl/hierarchy.hh diff --git a/NEWS b/NEWS index 18a4a8c11..db6a9bb9b 100644 --- a/NEWS +++ b/NEWS @@ -45,6 +45,11 @@ New in spot 2.2.2.dev (Not yet released) --syntactic-recurrence and --syntactic-persistence, the new checks are automata-based and will also match pathological formulas. + * The --format option of ltlfilt/genltl/randltl/ltlgrind learned to + print the class of a formula in the temporal hierachy of Manna & + Pnueli using %h. Try to classify the Dwyer & al. patterns with: + genltl --dac --format='%[vw]h' | sort | uniq -c + Library: * A twa is required to have at least one state, the initial state. @@ -122,6 +127,9 @@ New in spot 2.2.2.dev (Not yet released) competition will be generated. This requires the use of an exteral SAT solver, setup with "SPOT_SATSOLVER". See spot-x(7). + * The new function mp_class(f) returns the class of the formula + f in the temporal hierarchy of Manna & Pnueli. + New in spot 2.2.2 (2016-12-16) Build: diff --git a/bin/common_output.cc b/bin/common_output.cc index f0a162a87..0c0d86257 100644 --- a/bin/common_output.cc +++ b/bin/common_output.cc @@ -24,6 +24,7 @@ #include #include #include +#include #include #include #include "common_cout.hh" @@ -157,6 +158,109 @@ namespace const char* suffix; }; + class printable_formula_class final: + public spot::printable_value + { + public: + printable_formula_class& + operator=(char new_val) + { + val_ = new_val; + return *this; + } + + 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; + } + } + } + }; + class printable_formula final: public spot::printable_value { @@ -187,6 +291,7 @@ namespace declare('F', &filename_); declare('L', &line_); declare('s', &size_); + declare('h', &class_); declare('<', &prefix_); declare('>', &suffix_); set_output(os); @@ -212,6 +317,8 @@ namespace bool_size_ = spot::length_boolone(f); if (has('s')) size_ = spot::length(f); + if (has('h')) + class_ = spot::mp_class(f); return format(format_); } @@ -223,6 +330,7 @@ namespace spot::printable_value prefix_; spot::printable_value suffix_; spot::printable_value size_; + printable_formula_class class_; spot::printable_value bool_size_; spot::printable_value ap_num_; }; diff --git a/bin/common_output.hh b/bin/common_output.hh index fac994bbb..8e61811cf 100644 --- a/bin/common_output.hh +++ b/bin/common_output.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche +// 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. @@ -36,14 +36,18 @@ extern output_format_t output_format; extern bool full_parenth; extern bool escape_csv; -#define COMMON_LTL_OUTPUT_SPECS \ - { "%a", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, \ - "number of atomic propositions used in the formula", 0 }, \ - { "%s", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, \ - "the length (or size) of the formula", 0 }, \ - { "%b", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, \ - "the Boolean-length of the formula (i.e., all Boolean " \ - "subformulas count as 1)", 0 } +#define COMMON_LTL_OUTPUT_SPECS \ + { "%a", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, \ + "number of atomic propositions used in the formula", 0 }, \ + { "%s", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, \ + "the length (or size) of the formula", 0 }, \ + { "%b", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, \ + "the Boolean-length of the formula (i.e., all Boolean " \ + "subformulas count as 1)", 0 }, \ + { "%h, %[vw]h", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, \ + "the class of the formula is the Manna-Pnueli hierarchy " \ + "([v] replaces abbreviations by class names, [w] for all " \ + "compatible classes)", 0 } extern const struct argp output_argp; diff --git a/spot/tl/Makefile.am b/spot/tl/Makefile.am index 5ab305edf..e997811b5 100644 --- a/spot/tl/Makefile.am +++ b/spot/tl/Makefile.am @@ -1,6 +1,6 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de -## l'Epita (LRDE). +## Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et +## Développement de l'Epita (LRDE). ## ## This file is part of Spot, a model checking library. ## @@ -31,6 +31,7 @@ tl_HEADERS = \ environment.hh \ exclusive.hh \ formula.hh \ + hierarchy.hh \ length.hh \ ltlf.hh \ mutation.hh \ @@ -53,6 +54,7 @@ libtl_la_SOURCES = \ dot.cc \ exclusive.cc \ formula.cc \ + hierarchy.cc \ length.cc \ ltlf.cc \ mark.cc \ diff --git a/spot/tl/hierarchy.cc b/spot/tl/hierarchy.cc new file mode 100644 index 000000000..122665b5d --- /dev/null +++ b/spot/tl/hierarchy.cc @@ -0,0 +1,85 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2017 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 3 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 this program. If not, see . + +#include +#include +#include +#include +#include +#include +#include +#include + + +namespace spot +{ + namespace + { + static bool is_recurrence(formula f, const twa_graph_ptr& aut) + { + if (f.is_syntactic_recurrence() || is_deterministic(aut)) + return true; + // If aut is a non-deterministic TGBA, we do + // TGBA->DPA->DRA->(D?)BA. The conversion from DRA to + // BA will preserve determinism if possible. + spot::postprocessor p; + p.set_type(spot::postprocessor::Generic); + p.set_pref(spot::postprocessor::Deterministic + | spot::postprocessor::SBAcc); + p.set_level(spot::postprocessor::Low); + auto dra = p.run(aut); + if (dra->acc().is_generalized_buchi()) + { + return true; + } + else + { + auto ba = rabin_to_buchi_maybe(to_generalized_rabin(dra)); + assert(ba); + return is_deterministic(ba); + } + } + } + + char mp_class(formula f) + { + if (f.is_syntactic_safety() && f.is_syntactic_guarantee()) + return 'B'; + auto dict = make_bdd_dict(); + auto aut = ltl_to_tgba_fm(f, dict, true); + auto min = minimize_obligation(aut, f); + if (aut != min) // An obligation. + { + bool g = is_terminal_automaton(min); + bool s = is_safety_mwdba(min); + if (g) + return s ? 'B' : 'G'; + else + return s ? 'S' : 'O'; + } + // Not an obligation. Could by 'P', 'R', or 'T'. + if (is_recurrence(f, aut)) + return 'R'; + f = formula::Not(f); + aut = ltl_to_tgba_fm(f, dict, true); + if (is_recurrence(f, aut)) + return 'P'; + return 'T'; + } +} diff --git a/spot/tl/hierarchy.hh b/spot/tl/hierarchy.hh new file mode 100644 index 000000000..150ac91f8 --- /dev/null +++ b/spot/tl/hierarchy.hh @@ -0,0 +1,40 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2017 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 3 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 this program. If not, see . + +#pragma once + +#include + +namespace spot +{ + /// \brief Return the class of \a f in the temporal hierarchy of Manna + /// and Pnueli (PODC'90). + /// + /// The class is indicated using a character among: + /// - 'B' (bottom) safety properties that are also guarantee properties + /// - 'G' guarantee properties that are not also safety properties + /// - 'S' safety properties that are not also guarantee properties + /// - 'O' obligation properties that are not safety or guarantee + /// properties + /// - 'P' persistence properties that are not obligations + /// - 'R' recurrence properties that are not obligations + /// - 'T' (top) properties that are not persistence or recurrence + /// properties + SPOT_API char mp_class(formula f); +} diff --git a/tests/core/hierarchy.test b/tests/core/hierarchy.test index 57b78d551..9515d9011 100755 --- a/tests/core/hierarchy.test +++ b/tests/core/hierarchy.test @@ -44,3 +44,21 @@ test 3 -eq `genltl --dac | ltlfilt --recurrence -v -c` test 3 -eq `genltl --dac | ltl2tgba -G -D -S | autfilt --generalized-rabin | dstar2tgba | autfilt --is-deterministic -v -c` + +test "$(echo $(genltl --dac --format='%h') | sed 's/ //g')" = \ + SSSSSGSOSRSSSSSSSSSSSSPSSRSRSRSSSSSSSSSSRORRRRSRSTRSRST + + +# Implementations of uniq differ in the number of leading spaces, so +# we remove them all. +genltl --dac --format='%[vw]h' | sort | uniq -c | + sed 's/^ *\([0-9]\+\) \+/\1 /g' >out +cat >expected <