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

tl: implement to_delta2()

Browse source 
* 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.
This commit is contained in:
Alexandre Duret-Lutz 2024-07-25 10:42:58 +02:00
parent 5bc4d12bba
commit 41abe3f831
7 changed files with 559 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

4
NEWS
View file

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

2
python/spot/impl.i
View file

@ -90,6 +90,7 @@
#include <spot/tl/nenoform.hh>
#include <spot/tl/print.hh>
#include <spot/tl/simplify.hh>
#include <spot/tl/delta2.hh>
#include <spot/tl/sonf.hh>
#include <spot/tl/unabbrev.hh>
#include <spot/tl/randomltl.hh>
@ -632,6 +633,7 @@ namespace std {
%include <spot/tl/sonf.hh>
%include <spot/tl/print.hh>
%include <spot/tl/simplify.hh>
%include <spot/tl/delta2.hh>
%include <spot/tl/unabbrev.hh>
%include <spot/tl/randomltl.hh>
%include <spot/tl/length.hh>

2
spot/tl/Makefile.am
View file

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

451
spot/tl/delta2.cc Normal file
View file

@ -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 <http://www.gnu.org/licenses/>.
#include "config.h"
#include <spot/tl/delta2.hh>
#include <iostream>
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<typename Fun>
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>, 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;
}
}

42
spot/tl/delta2.hh Normal file
View file

@ -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 <http://www.gnu.org/licenses/>.
#pragma once
#include <spot/tl/formula.hh>
#include <spot/tl/simplify.hh>
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);
}

1
tests/Makefile.am
View file

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

57
tests/python/delta2.py Executable file
View file

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