alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

tl: implement suffix operator normal form

Browse source 
* 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
This commit is contained in:
Antoine Martin 2021-11-09 16:00:16 +01:00
parent c7201e4776
commit 0505ee9310
9 changed files with 348 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

4
NEWS
View file

@ -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

12
doc/spot.bib
View file

@ -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

3
python/spot/impl.i
View file

@ -94,6 +94,7 @@
#include <spot/tl/nenoform.hh>
#include <spot/tl/print.hh>
#include <spot/tl/simplify.hh>
#include <spot/tl/sonf.hh>
#include <spot/tl/unabbrev.hh>
#include <spot/tl/randomltl.hh>
#include <spot/tl/length.hh>
@ -517,6 +518,7 @@ namespace std {
%template(vectorbdd) vector<bdd>;
%template(aliasvector) vector<pair<string, bdd>>;
%template(vectorstring) vector<string>;
%template(pair_formula_vectorstring) pair<spot::formula, vector<string>>;
%template(atomic_prop_set) set<spot::formula>;
%template(relabeling_map) map<spot::formula, spot::formula>;
}
@ -577,6 +579,7 @@ namespace std {
%include <spot/tl/contain.hh>
%include <spot/tl/dot.hh>
%include <spot/tl/nenoform.hh>
%include <spot/tl/sonf.hh>
%include <spot/tl/print.hh>
%include <spot/tl/simplify.hh>
%include <spot/tl/unabbrev.hh>

2
spot/tl/Makefile.am
View file

@ -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

185
spot/tl/sonf.cc Normal file
View file

@ -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 <http://www.gnu.org/licenses/>.
#include "config.h"
#include <spot/tl/nenoform.hh>
#include <spot/tl/sonf.hh>
#include <string>
#include <unordered_set>
#include <utility>
#include <vector>
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<formula>&` 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<formula>& extracted,
/// auto&& extractor,
/// bool top_level,
/// bool in_top_level_and) -> formula
template<typename Ext>
static formula
extract(formula f, Ext extractor)
{
std::vector<formula> extracted;
formula new_f = extractor(f, extracted, extractor, true, false);
extracted.push_back(new_f);
return formula::And(extracted);
}
}
std::pair<formula, std::vector<std::string>>
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<std::string> used_aps;
std::vector<std::string> 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<formula>& 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<formula>& 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};
}
}

44
spot/tl/sonf.hh Normal file
View file

@ -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 <http://www.gnu.org/licenses/>.
#pragma once
#include <string>
#include <utility>
#include <vector>
#include <spot/tl/formula.hh>
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<formula, std::vector<std::string>>
suffix_operator_normal_form(formula f, const std::string prefix);
}

1
tests/Makefile.am
View file

@ -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 \

56
tests/python/formulas.ipynb
View file

@ -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": {

41
tests/python/sonf.py Normal file
View file

@ -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 <http://www.gnu.org/licenses/>.
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))