From 41abe3f831eba9cdfa72f6b8685aba26accbce59 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 25 Jul 2024 10:42:58 +0200 Subject: [PATCH] tl: implement to_delta2() * spot/tl/delta2.cc, spot/tl/delta2.hh: New files. * spot/tl/Makefile.am: Add them. * python/spot/impl.i: Include delta2.hh. * tests/python/delta2.py: New file. * tests/Makefile.am: Add it. * NEWS: Mention the change. --- NEWS | 4 + python/spot/impl.i | 2 + spot/tl/Makefile.am | 2 + spot/tl/delta2.cc | 451 +++++++++++++++++++++++++++++++++++++++++ spot/tl/delta2.hh | 42 ++++ tests/Makefile.am | 1 + tests/python/delta2.py | 57 ++++++ 7 files changed, 559 insertions(+) create mode 100644 spot/tl/delta2.cc create mode 100644 spot/tl/delta2.hh create mode 100755 tests/python/delta2.py diff --git a/NEWS b/NEWS index 5f09664f9..a4670f5d8 100644 --- a/NEWS +++ b/NEWS @@ -26,6 +26,10 @@ New in spot 2.12.0.dev (not yet released) formula::is_delta1(), formula::is_sigma2(), formula::is_pi2(), formula::is_delta2(). See doc/tl/tl.pdf from more discussion. + - spot::to_delta2() implements Δ₂-normalization for LTL formulas, + following "Efficient Normalization of Linear Temporal Logic" by + Esparza et al. (J. ACM, 2024). + New in spot 2.12 (2024-05-16) Build: diff --git a/python/spot/impl.i b/python/spot/impl.i index 6fa3e9f07..6d91144d8 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -90,6 +90,7 @@ #include #include #include +#include #include #include #include @@ -632,6 +633,7 @@ namespace std { %include %include %include +%include %include %include %include diff --git a/spot/tl/Makefile.am b/spot/tl/Makefile.am index a1f0ce104..6c7650875 100644 --- a/spot/tl/Makefile.am +++ b/spot/tl/Makefile.am @@ -27,6 +27,7 @@ tl_HEADERS = \ contain.hh \ declenv.hh \ defaultenv.hh \ + delta2.hh \ dot.hh \ environment.hh \ exclusive.hh \ @@ -52,6 +53,7 @@ libtl_la_SOURCES = \ contain.cc \ declenv.cc \ defaultenv.cc \ + delta2.cc \ dot.cc \ exclusive.cc \ formula.cc \ diff --git a/spot/tl/delta2.cc b/spot/tl/delta2.cc new file mode 100644 index 000000000..e2d2e66d4 --- /dev/null +++ b/spot/tl/delta2.cc @@ -0,0 +1,451 @@ +// -*- coding: utf-8 -*- +// Copyright (C) by the Spot authors, see the AUTHORS file for details. +// +// 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 + +namespace spot +{ + namespace + { + static formula + is_F(formula f) + { + if (f.is(op::F)) + return f[0]; + if (f.is(op::U) && f[0].is_tt()) + return f[1]; + if (f.is(op::M) && f[1].is_tt()) + return f[0]; + return nullptr; + } + + static formula + is_G(formula f) + { + if (f.is(op::G)) + return f[0]; + if (f.is(op::R) && f[0].is_ff()) + return f[1]; + if (f.is(op::W) && f[1].is_ff()) + return f[0]; + return nullptr; + } + + static formula + is_FG(formula x) + { + if (formula f = is_F(x); f) + return is_G(f); + return nullptr; + } + + static formula + is_GF(formula x) + { + if (formula f = is_G(x); f) + return is_F(f); + return nullptr; + } + + + static formula + rewrite_strong_under_weak(formula f) + { + // FIXME: Can we replace is_FG/is_GF by is_suspendable? This + // isn't straightforward, because stage3 is only looking for + // FG/GF. + if (f.is_delta1() || is_FG(f) || is_GF(f)) + return f; + if (f.is(op::W) || f.is(op::G)) + { + formula f0 = f[0]; + formula f1 = f.is(op::W) ? f[1] : formula::ff(); + // If φ₁ contains a strong operator (i.e., is not a safety) + // we have φ₀ W φ₁ = (φ₀ U φ₁) | G(φ₀) + if (!f1.is_syntactic_safety()) + { + formula left = formula::U(f0, f1); + formula right = formula::G(f0); + return rewrite_strong_under_weak(formula::Or({left, right})); + } + // x[φ₀Uφ₁] W φ₂ = + // (GFφ₁ & (x[φ₀Wφ₁] W φ₂)) | x[φ₀Uφ₁] U (φ₂|G(x[false])) + // x[Fφ₀] W φ₂= (GFφ₀ & (x[true] W φ₂)) | x[Fφ₀] U (φ₂ | G(x[false])) + // x[φ₀Mφ₁] W φ₂ = + // (GFφ₀ & (x[φ₀Rφ₁] R φ₂)) | x[φ₀Mφ₁] U (φ₂|G(x[false])) + formula match = nullptr; // (φ₀ U φ₁) once matched + formula prefix = nullptr; // GF(φ₁) + auto find_u = [&](formula node, auto&& self) { + if (!match || match == node) + { + if (is_FG(node) || is_GF(node)) + return node; + if (node.is(op::U)) + { + if (!match) + { + match = node; + prefix = formula::G(formula::F(match[1])); + } + return formula::W(node[0], node[1]); + } + else if (node.is(op::M)) + { + if (!match) + { + match = node; + prefix = formula::G(formula::F(match[0])); + } + return formula::R(node[0], node[1]); + } + else if (node.is(op::F)) // like tt U φ₀ + { + if (!match) + { + match = node; + prefix = formula::G(formula::F(match[0])); + } + return formula::tt(); + } + } + return node.map(self, self); + }; + formula g = find_u(f0, find_u); + if (!match) + return f; + assert(!match.is_syntactic_safety()); + auto match_to_false = [&](formula node, auto&& self) { + if (node == match) + return formula::ff(); + if (node.is_syntactic_safety()) + return node; + return node.map(self, self); + }; + formula ww = rewrite_strong_under_weak(formula::W(g, f1)); + prefix = formula::And({prefix, ww}); + formula gx_false = formula::G(match_to_false(f0, match_to_false)); + formula u_right = formula::U(f0, formula::Or({f1, gx_false})); + return formula::Or({prefix, rewrite_strong_under_weak(u_right)}); + } + if (f.is(op::R)) + { + formula f0 = f[0]; + formula f1 = f[1]; + // If φ₀ contains a strong operator (i.e., is not a safety) + // we have φ₀ R φ₁ = (φ₀ M φ₁) | G(φ₁) + if (!f0.is_syntactic_safety()) + { + formula left = formula::M(f0, f1); + formula right = formula::G(f1); + return rewrite_strong_under_weak(formula::Or({left, right})); + } + // φ₀ R x[φ₁Uφ₂] = + // (GFφ₂ & (φ₀ R x[φ₁Wφ₂])) | ((φ₀|G(x[false])) M x[φ₁Uφ₂]) + // φ₀ R x[Fφ₁] = (GFφ₁ & (φ₀ R x[true])) | ((φ₀|G(x[false])) M x[Fφ₁]) + // φ₀ R x[φ₁Mφ₂] = + // (GFφ₀ & (φ₀ R x[φ₁Rφ₂])) | ((φ₀|G(x[false])) M x[φ₁Mφ₂]) + formula match = nullptr; // (φ₀ U φ₁) once matched + formula prefix = nullptr; // GF(φ₁) + auto find_u = [&](formula node, auto&& self) { + if (!match || match == node) + { + if (is_FG(node) || is_GF(node)) + return node; + if (node.is(op::U)) + { + if (!match) + { + match = node; + prefix = formula::G(formula::F(match[1])); + } + return formula::W(node[0], node[1]); + } + else if (node.is(op::M)) + { + if (!match) + { + match = node; + prefix = formula::G(formula::F(match[0])); + } + return formula::R(node[0], node[1]); + } + else if (node.is(op::F)) // like tt U φ₀ + { + if (!match) + { + match = node; + prefix = formula::G(formula::F(match[0])); + } + return formula::tt(); + } + } + return node.map(self, self); + }; + formula g = find_u(f1, find_u); + if (!match) + return f; + // φ₀ R x[φ₁Uφ₂] = + // (GFφ₂ & (φ₀ R x[φ₁Wφ₂])) | ((φ₀|G(x[false])) M x[φ₁Uφ₂]) + // φ₀ R x[Fφ₁] = (GFφ₁ & (φ₀ R x[true])) | ((φ₀|G(x[false])) M x[Fφ₁]) + // φ₀ R x[φ₁Mφ₂] = + // (GFφ₀ & (φ₀ R x[φ₁Rφ₂])) | ((φ₀|G(x[false])) M x[φ₁Mφ₂]) + assert(!match.is_syntactic_safety()); + auto match_to_false = [&](formula node, auto&& self) { + if (node == match) + return formula::ff(); + if (node.is_syntactic_safety()) + return node; + return node.map(self, self); + }; + formula rw = rewrite_strong_under_weak(formula::R(f0, g)); + prefix = formula::And({prefix, rw}); + formula gx_false = formula::G(match_to_false(f1, match_to_false)); + formula m_right = formula::M(formula::Or({f0, gx_false}), f1); + return formula::Or({prefix, rewrite_strong_under_weak(m_right)}); + } + return f.map(rewrite_strong_under_weak); + } + + // c[susp] = (susp & c[true]) || c[false] + formula + fish_inner_suspendable(formula f) + { + if (f.is_delta1() || is_FG(f) || is_GF(f)) + return f; + formula match = nullptr; + // return c[true], and set match to susp. + auto find_inner_susp = [&](formula node, auto self) + { + if (node.is_delta1()) + { + return node; + } + else if (node.is_eventual() && node.is_universal()) + { + if (!match) + { + // Try to find a deeper suspendable node if it + // exist, we want to start from the bottom. + node = node.map(self, self); + if (!match) + match = node; + } + if (node == match) + return formula::tt(); + } + return node.map(self, self); + }; + formula c_true = f.map(find_inner_susp, find_inner_susp); + if (!match) + return c_true; // == f. + + auto match_to_false = [&](formula node, auto&& self) { + if (node.is_delta1()) + return node; + if (node == match) + return formula::ff(); + return node.map(self, self); + }; + formula c_false = f.map(match_to_false, match_to_false); + match = fish_inner_suspendable(match); + c_true = fish_inner_suspendable(c_true); + c_false = fish_inner_suspendable(c_false); + return formula::Or({formula::And({match, c_true}), c_false}); + } + + static formula + normalize_inside_suspendable(formula f) + { + if (f.is_delta1()) + return f; + if (formula inner = is_GF(f)) + { + // GF(x[φ₀ W φ₁]) = GF(x[φ₀ U φ₁]) | (FG(φ₀) & GF(x[true]) + // GF(x[φ₀ R φ₁]) = GF(x[φ₀ M φ₁]) | (FG(φ₁) & GF(x[true]) + // GF(x[Gφ₀]) = GF(x[false]) | (FG(φ₀) & GF(x[true]) + formula match = nullptr; // (φ₀ W φ₁) once matched + formula suffix = nullptr; // FG(φ₀) + auto find_w = [&](formula node, auto&& self) { + if (!match || match == node) + { + if (node.is(op::W)) + { + if (!match) + { + match = node; + suffix = formula::F(formula::G(match[0])); + } + return formula::U(node[0], node[1]); + } + else if (node.is(op::R)) + { + if (!match) + { + match = node; + suffix = formula::F(formula::G(match[1])); + } + return formula::M(node[0], node[1]); + } + else if (node.is(op::G)) // like 0 R φ₀ + { + if (!match) + { + match = node; + suffix = formula::F(formula::G(match[0])); + } + return formula::ff(); + } + } + return node.map(self, self); + }; + formula res = find_w(inner, find_w); + if (!match) + return f; + // append GF(x[true]) to suffix + assert(!match.is_syntactic_guarantee()); + auto match_to_true = [&](formula node, auto&& self) { + if (node == match) + return formula::tt(); + if (node.is_syntactic_guarantee()) + return node; + return node.map(self, self); + }; + suffix = formula::And({suffix, + f.map(match_to_true, match_to_true)}); + res = formula::Or({formula::G(formula::F(res)), suffix}); + return normalize_inside_suspendable(res); + } + else if (formula inner = is_FG(f)) + { + // FG(x[φ₀ U φ₁]) = (GF(φ₁) & FG(x[φ₀ W φ₁])) | FG(x[false]) + // FG(x[φ₀ M φ₁]) = (GF(φ₀) & FG(x[φ₀ R φ₁])) | FG(x[false]) + // FG(x[Fφ₀]) = (GF(φ₀) & FG(x[true])) | FG(x[false]) + formula match = nullptr; // (φ₀ U φ₁) once matched + formula prefix = nullptr; // GF(φ₁) + auto find_u = [&](formula node, auto&& self) { + if (!match || match == node) + { + if (node.is(op::U)) + { + if (!match) + { + match = node; + prefix = formula::G(formula::F(match[1])); + } + return formula::W(node[0], node[1]); + } + else if (node.is(op::M)) + { + if (!match) + { + match = node; + prefix = formula::G(formula::F(match[0])); + } + return formula::R(node[0], node[1]); + } + else if (node.is(op::F)) // like tt U φ₀ + { + if (!match) + { + match = node; + prefix = formula::G(formula::F(match[0])); + } + return formula::tt(); + } + } + return node.map(self, self); + }; + formula res = find_u(inner, find_u); + if (!match) + return f; + res = formula::And({formula::F(formula::G(res)), prefix}); + // append FG(x[false]) + assert(!match.is_syntactic_safety()); + auto match_to_false = [&](formula node, auto&& self) { + if (node == match) + return formula::ff(); + if (node.is_syntactic_safety()) + return node; + return node.map(self, self); + }; + res = formula::Or({res, f.map(match_to_false, match_to_false)}); + return normalize_inside_suspendable(res); + } + return f.map(normalize_inside_suspendable); + } + + + // Dispatch Fun on top-level temporal operators that aren't + // already in Δ₂ form. + template + static formula + dispatch(formula f, Fun&& fun) + { + if (f.is_delta2()) + return f; + switch (auto k = f.kind()) + { + case op::F: + case op::G: + case op::U: + case op::R: + case op::W: + case op::M: + return fun(f); + case op::EConcat: + case op::EConcatMarked: + case op::UConcat: + // not yet supported + return formula::binop(k, f[0], dispatch(f[1], fun)); + default: + break; + } + return f.map(dispatch, fun); + } + } + + formula to_delta2(formula f, tl_simplifier* tls) + { + if (f.is_delta2()) + return f; + bool own_tls = !tls; + if (own_tls) + { + tl_simplifier_options opt(false, false, false, + false, false, false, + false, false, false, + true); + tls = new tl_simplifier(opt); + } + // This will ensure the formula is in NNF, except + // maybe for the top level operator. + f = tls->simplify(f); + // stage 1 + f = dispatch(f, rewrite_strong_under_weak); + // stage 2 + f = dispatch(f, fish_inner_suspendable); + // stage 3 + f = dispatch(f, normalize_inside_suspendable); + // f = tls->simplify(f); + if (own_tls) + delete tls; + return f; + } +} diff --git a/spot/tl/delta2.hh b/spot/tl/delta2.hh new file mode 100644 index 000000000..766a8ffc1 --- /dev/null +++ b/spot/tl/delta2.hh @@ -0,0 +1,42 @@ +// -*- coding: utf-8 -*- +// Copyright (C) by the Spot authors, see the AUTHORS file for details. +// +// 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 + +namespace spot +{ + /// \ingroup tl_rewriting + /// \brief Convert an LTL formula to Δ₂ + /// + /// This implement LTL rewriting rules as given by + /// \cite esparza.24.acm + /// + /// Only LTL operators are supported, PSL operators + /// will be left untouched. + /// + /// If \a tls is given, it will be used to simplify formulas and + /// puts formulas in negative normal form. If \a tls is not + /// given, a temporary simplifier will be created. + /// + /// No transformation is attempted if the input is already Δ₂. + SPOT_API formula + to_delta2(formula f, tl_simplifier* tls = nullptr); +} diff --git a/tests/Makefile.am b/tests/Makefile.am index cfe6a033a..08dfbf377 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -415,6 +415,7 @@ TESTS_python = \ python/declenv.py \ python/decompose_scc.py \ python/deadends.py \ + python/delta2.py \ python/det.py \ python/dualize.py \ python/ecfalse.py \ diff --git a/tests/python/delta2.py b/tests/python/delta2.py new file mode 100755 index 000000000..a60f60456 --- /dev/null +++ b/tests/python/delta2.py @@ -0,0 +1,57 @@ +#!/usr/bin/python3 +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) by the Spot authors, see the AUTHORS file for details. +# +# 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 +from unittest import TestCase +tc = TestCase() + +def generate_formulas(): + for i in ['{} {} ({} {} {})', '({} {} {}) {} {}']: + for k in "MWUR": + for l in "MWUR": + for a in ['a', 'false', 'true']: + for b in ['b', 'false', 'true']: + for c in ['c', 'false', 'true']: + inner = i.format(a,k,b,l,c); + for j in ['GF({})', 'FG({})', + '({}) W d', '({}) U d', + 'd W ({})', 'd U ({})', + '({}) R d', '({}) M d', + 'd R ({})', 'd M ({})']: + yield j.format(inner) + + for j1 in ['G(F({}){}F(e {} f))', + 'F(G({}){}G(e {} f))']: + for j2 in "&|": + for j3 in "MWUR": + yield j1.format(inner,j2,j3) + +seen = set() +for f in generate_formulas(): + ltl_in = spot.formula(f) + if ltl_in in seen: + continue + seen.add(ltl_in) + ltl_out = spot.to_delta2(ltl_in) + ok = spot.are_equivalent(ltl_in, ltl_out) + din = ltl_in.is_delta2() + dout = ltl_out.is_delta2() + print(f"{ok:1} {din:1}{dout:1} {ltl_in::30} {ltl_out::30}") + tc.assertTrue(ok) + tc.assertTrue(dout)