From 0505ee93106cfa29e99c1e5464114961b0849061 Mon Sep 17 00:00:00 2001 From: Antoine Martin Date: Tue, 9 Nov 2021 16:00:16 +0100 Subject: [PATCH] tl: implement suffix operator normal form * spot/tl/Makefile.am: New sonf files * spot/tl/sonf.cc,spot/tl/sonf.hh: Here. * python/spot/impl.i: include sonf.hh header * doc/spot.bib: add entry for the SONF paper * tests/python/formulas.ipynb: show sample usage * tests/python/spot.py: test automata equivalence before/after SONF * NEWS: mention the change --- NEWS | 4 + doc/spot.bib | 12 +++ python/spot/impl.i | 3 + spot/tl/Makefile.am | 2 + spot/tl/sonf.cc | 185 ++++++++++++++++++++++++++++++++++++ spot/tl/sonf.hh | 44 +++++++++ tests/Makefile.am | 1 + tests/python/formulas.ipynb | 56 +++++++++++ tests/python/sonf.py | 41 ++++++++ 9 files changed, 348 insertions(+) create mode 100644 spot/tl/sonf.cc create mode 100644 spot/tl/sonf.hh create mode 100644 tests/python/sonf.py diff --git a/NEWS b/NEWS index 928a25da2..cc0fe35a6 100644 --- a/NEWS +++ b/NEWS @@ -11,6 +11,10 @@ New in spot 2.10.4.dev (net yet released) Library: + - The new function suffix_operator_normal_form() implements + transformation of formulas to Suffix Operator Normal Form, + described in [cimatti.06.fmcad]. + - "original-classes" is a new named property similar to "original-states". It maps an each state to an unsigned integer such that if two classes are in the same class, they are expected diff --git a/doc/spot.bib b/doc/spot.bib index 9f18ad2a9..9d5d6b235 100644 --- a/doc/spot.bib +++ b/doc/spot.bib @@ -214,6 +214,18 @@ doi = {10.1109/DepCoS-RELCOMEX.2009.31} } +@InProceedings{ cimatti.06.fmcad, + author = {Cimatti, Alessandro and Roveri, Marco and Semprini, Simone and + Tonetta, Stefano}, + title = {From {PSL} to {NBA}: a Modular Symbolic Encoding}, + booktitle = {Proceedings of the 6th conference on Formal Methods in Computer + Aided Design (FMCAD'06)}, + pages = {125--133}, + year = {2006}, + publisher = {IEEE Computer Society}, + doi = {10.1109/FMCAD.2006.19} +} + @Article{ cimatti.08.tcad, author = {Alessandro Cimatti and Marco Roveri and Stefano Tonetta}, journal = {IEEE Transactions on Computer Aided Design of Integrated diff --git a/python/spot/impl.i b/python/spot/impl.i index 90a38a55a..7132a5cc6 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -94,6 +94,7 @@ #include #include #include +#include #include #include #include @@ -517,6 +518,7 @@ namespace std { %template(vectorbdd) vector; %template(aliasvector) vector>; %template(vectorstring) vector; + %template(pair_formula_vectorstring) pair>; %template(atomic_prop_set) set; %template(relabeling_map) map; } @@ -577,6 +579,7 @@ namespace std { %include %include %include +%include %include %include %include diff --git a/spot/tl/Makefile.am b/spot/tl/Makefile.am index b7362ae99..cdedddffd 100644 --- a/spot/tl/Makefile.am +++ b/spot/tl/Makefile.am @@ -44,6 +44,7 @@ tl_HEADERS = \ remove_x.hh \ simplify.hh \ snf.hh \ + sonf.hh \ unabbrev.hh noinst_LTLIBRARIES = libtl.la @@ -68,4 +69,5 @@ libtl_la_SOURCES = \ remove_x.cc \ simplify.cc \ snf.cc \ + sonf.cc \ unabbrev.cc diff --git a/spot/tl/sonf.cc b/spot/tl/sonf.cc new file mode 100644 index 000000000..29a319039 --- /dev/null +++ b/spot/tl/sonf.cc @@ -0,0 +1,185 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2021 Laboratoire de Recherche et Developpement 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 "config.h" +#include +#include + +#include +#include +#include +#include + +namespace spot +{ + namespace + { + /// Uses `extractor` to extract some parts of the formula and replace them + /// with atomic propositions. + /// + /// Returns (f & g1 & g2 & .. & gn) with g1..gn the extracted subformulas. + /// + /// `extractor` should be a lambda taking the following parameters as input: + /// + /// - `formula` the formula to process + /// - `std::vector&` the vector that stores extracted subformulas + /// - `auto&&` itself, in case it needs to call itself recursively + /// (formula::map for example) + /// - `bool` a boolean indicating whether the lambda is currently being + /// called at the formula's "root" + /// - `bool` a boolean indicating whether the lambda is currently being + /// called inside a toplevel `and` construct. + /// + /// Note that the last 2 boolean arguments can be used as you see fit in + /// your recursive calls, the first one being set to true in the original + /// call, and the second one to false. + /// + /// `extractor` should return the new rewritten formula. + /// + /// auto sample_extractor = [](formula f, + /// std::vector& extracted, + /// auto&& extractor, + /// bool top_level, + /// bool in_top_level_and) -> formula + template + static formula + extract(formula f, Ext extractor) + { + std::vector extracted; + formula new_f = extractor(f, extracted, extractor, true, false); + extracted.push_back(new_f); + return formula::And(extracted); + } + } + + std::pair> + suffix_operator_normal_form(formula f, const std::string prefix) + { + // SONF can only be applied to formulas in negative normal form + f = negative_normal_form(f); + + std::unordered_set used_aps; + std::vector added_aps; + size_t count = 0; + + // identify all used ap names to avoid them when generating new ones + auto ap_indexer = [&used_aps](formula f) noexcept { + if (f.is(op::ap)) + { + used_aps.insert(f.ap_name()); + return true; + } + + return false; + }; + + f.traverse(ap_indexer); + + auto new_ap_name = + [&used_aps, &added_aps, &prefix, &count]() noexcept -> std::string + { + std::string new_name = prefix + std::to_string(count++); + while (used_aps.find(new_name) != used_aps.end()) + new_name = prefix + std::to_string(count++); + used_aps.insert(new_name); + added_aps.push_back(new_name); + return new_name; + }; + + // extracts the SERE part and replaces it with an atomic proposition, + // storing the extracted formula in `extracted` and returning the rewritten + // original formula + auto sonf_extract = [&](formula f, + std::vector& extracted, + auto&& extractor, + bool top_level, + bool in_top_level_and) noexcept -> formula + { + const auto kind = f.kind(); + + switch (kind) + { + case op::G: + { + // skip if shape is G(!ap | (regex []-> formula)) and at top level + if ((top_level || in_top_level_and) + && f[0].is(op::Or) // G(_ | _) + && f[0][0].is(op::Not) // G(!_ | _) + && f[0][0][0].is(op::ap) // G(!ap | _) + && f[0][1].is(op::EConcat, op::UConcat)) // G(!ap | (_ []-> _)) + return f; + else + return f.map(extractor, extracted, extractor, false, false); + } + case op::EConcat: + case op::UConcat: + { + // recurse into rhs first (_ []-> rhs) + formula rhs = + f[1].map(extractor, extracted, extractor, false, false); + f = formula::binop(kind, f[0], rhs); + + formula ap = formula::ap(new_ap_name()); + extracted.push_back(formula::G(formula::Or({formula::Not(ap), f}))); + return ap; + } + default: + // tracking if we're in a op::And at the formula root + in_top_level_and = top_level && f.is(op::And); + return f.map(extractor, extracted, extractor, + false, in_top_level_and); + } + }; + + f = extract(f, sonf_extract); + + auto ltl_extract = [&](formula f, + std::vector& extracted, + auto&& extractor, + [[maybe_unused]] + bool top_level, + [[maybe_unused]] + bool in_top_level_and) noexcept -> formula + { + switch (f.kind()) + { + case op::EConcat: + case op::UConcat: + { + formula rhs = f[1]; + + if (rhs.is(op::ap)) + return f; + + formula ap = formula::ap(new_ap_name()); + extracted.push_back( + formula::G(formula::Or({formula::Not(ap), rhs}))); + + return formula::binop(f.kind(), f[0], ap); + } + default: + return f.map(extractor, extracted, extractor, false, false); + } + }; + + f = extract(f, ltl_extract); + + return {f, added_aps}; + } +} diff --git a/spot/tl/sonf.hh b/spot/tl/sonf.hh new file mode 100644 index 000000000..37ef5d05d --- /dev/null +++ b/spot/tl/sonf.hh @@ -0,0 +1,44 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2021 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 +#include +#include + +#include + +namespace spot +{ + /// \ingroup tl_rewriting + /// \brief Helper to rewrite a PSL formula in Suffix Operator Normal Form. + /// + /// SONF is described in section 4 of \cite cimatti.06.fmcad + /// + /// The formula output by this function is guaranteed to be in Negative Normal + /// Form. + /// + /// \param f the PSL formula to rewrite + /// \param prefix the prefix to use to name newly introduced aps + /// \return a pair with the rewritten formula, and a vector containing the + /// names of newly introduced aps + SPOT_API std::pair> + suffix_operator_normal_form(formula f, const std::string prefix); +} diff --git a/tests/Makefile.am b/tests/Makefile.am index 1b5d63fee..a6f4ab56c 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -445,6 +445,7 @@ TESTS_python = \ python/setxor.py \ python/simplacc.py \ python/simstate.py \ + python/sonf.py \ python/split.py \ python/streett_totgba.py \ python/streett_totgba2.py \ diff --git a/tests/python/formulas.ipynb b/tests/python/formulas.ipynb index 95241be9d..7075cf653 100644 --- a/tests/python/formulas.ipynb +++ b/tests/python/formulas.ipynb @@ -976,6 +976,62 @@ "print(ap) # print as a string\n", "display(ap) # LaTeX-style, for notebooks" ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Converting to Suffix Operator Normal Form:" + ] + }, + { + "cell_type": "code", + "execution_count": 27, + "metadata": {}, + "outputs": [ + { + "data": { + "text/latex": [ + "$\\mathsf{G} (\\{x^{\\star}\\}\\mathrel{\\Box\\kern-1.7pt\\raise.4pt\\hbox{$\\mathord{\\rightarrow}$}} \\mathsf{F} a)$" + ], + "text/plain": [ + "spot.formula(\"G({x[*]}[]-> Fa)\")" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/latex": [ + "$\\mathsf{G} \\mathit{sonf\\_}_{0} \\land \\mathsf{G} (\\lnot \\mathit{sonf\\_}_{1} \\lor \\mathsf{F} a) \\land \\mathsf{G} (\\lnot \\mathit{sonf\\_}_{0} \\lor (\\{x^{\\star}\\}\\mathrel{\\Box\\kern-1.7pt\\raise.4pt\\hbox{$\\mathord{\\rightarrow}$}} \\mathit{sonf\\_}_{1}))$" + ], + "text/plain": [ + "spot.formula(\"Gsonf_0 & G(!sonf_1 | Fa) & G(!sonf_0 | ({x[*]}[]-> sonf_1))\")" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/plain": [ + "('sonf_0', 'sonf_1')" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "f = spot.formula('G({x*} []-> Fa)')\n", + "display(f)\n", + "\n", + "# In addition to the formula, returns a list of newly introduced APs\n", + "f, aps = spot.suffix_operator_normal_form(f, 'sonf_')\n", + "display(f)\n", + "display(aps)" + ] } ], "metadata": { diff --git a/tests/python/sonf.py b/tests/python/sonf.py new file mode 100644 index 000000000..558f90c63 --- /dev/null +++ b/tests/python/sonf.py @@ -0,0 +1,41 @@ +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2020 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 . + +import spot + +formulas = """\ +{x[*]}[]-> F({y[*]}<>-> GFz) +<>(({{p12}[*0..3]}[]-> ((p9) || (!(p17)))) V ((true) U (p17))) +{{true} || {[*0]}}[]-> (false) +{{p14} & {{p0}[*]}}[]-> (p11) +{{{!{p6}} -> {!{p3}}}[*]}[]-> ((p3)V((p3) || ((X((false))) && ((p2)V(p18))))) +""" + +for f1 in formulas.splitlines(): + f1 = spot.formula(f1) + a1 = spot.translate(f1) + + f2, aps = spot.suffix_operator_normal_form(f1, 'sonf_') + a2 = spot.translate(f2) + rm = spot.remove_ap() + for ap in aps: + rm.add_ap(ap) + a2 = rm.strip(a2) + + assert(spot.are_equivalent(a1, a2))