Commit da5d23f0 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

simplify: GF(f)=GF(dnf(f)) FG(f)=FG(cnf(f))

These rules come from Delag's paper, and help some cases
in issue #385.

* spot/tl/simplify.cc: Implement the simplification.
* doc/tl/tl.tex, NEWS: Document it.
* tests/core/385.test: New file.
* tests/Makefile.am: Add it.
* tests/core/reduccmp.test: More tests.
* tests/core/ltl2tgba2.test: Adjust one improved case.
* tests/python/automata.ipynb, tests/python/twagraph-internals.ipynb:
Adjust expected output, as the cnf/dnf reorder some subformulas.
parent df326e03
......@@ -105,9 +105,11 @@ New in spot 2.7.5.dev (not yet released)
- The LTL simplifier learned the following optional rules:
F(G(a | Fb)) = FGa | GFb (if option "favor_event_univ")
G(F(a | Gb)) = GFa | FGb (if option "favor_event_univ")
G(F(a | Gb)) = GFa | FGb (if option "favor_event_univ")
F(G(a & Fb) = FGa & GFb (unless option "reduce_size_strictly")
G(F(a & Gb)) = GFa & FGb (unless option "reduce_size_strictly")
GF(f) = GF(dnf(f)) (unless option "reduce_size_strictly")
FG(f) = FG(cnf(f)) (unless option "reduce_size_strictly")
- cleanup_parity() and colorize_parity() were cleaned up a bit,
resulting in fewer colors used in some cases. In particular,
......
......@@ -116,7 +116,7 @@
\newcommand{\nsereMarked}[1]{\texttt{!+\{}#1\texttt{\}}}
\newcommand{\seren}[1]{\texttt{\{}#1\texttt{\}!}}
% rewriting rules that enlarge the formula
% rewriting rules that (may) enlarge the formula
\newcommand{\equiV}{\stackrel{\star}{\equiv}}
% rewriting rules that favors event/univ
\newcommand{\equivEU}{\stackrel{\blacktriangleup}{\equiv}}
......@@ -1463,15 +1463,19 @@ instead of $\equiv$, and they can be disabled by setting the
\label{sec:basic-simp-ltl}
The following are simplification rules for unary operators (applied
from left to right, as usual):
from left to right, as usual). The terms $\mathsf{dnf}(f)$ and
$\mathsf{cnf}(f)$ denote respectively the disjunctive and conjunctive
normal forms if $f$, handling non-Boolean sub-formulas as if they were
atomic propositions.
\begin{align*}
\X\F\G f & \equiv \F\G f & \F(f\U g) & \equiv \F g & \G(f \R g) & \equiv \G g \\
\X\G\F f & \equiv \G\F f & \F(f\M g) & \equiv \F (f\AND g) & \G(f \W g) & \equiv \G(f\OR g) \\
\F\X f & \equiv \X\F f & \F\G(f\AND \X g) & \equiv \F\G(f\AND g) & \G\F(f\OR \X g) & \equiv \G\F(f\OR g) \\
\G\X f & \equiv \X\G f & \F\G(f\AND \G g) & \equiv \F\G(f\AND g) & \G\F(f\OR \F g) & \equiv \G\F(f\OR g) \\
& & \F\G(f\OR\G g) & \equiv \F(\G f\OR\G g) & \G\F(f\AND\F g) & \equiv \G(\F f\AND\F g) \\
& & \F\G(f\AND\F g) & \equiV \F\G f\AND\G\F g & \G\F(f\AND\G g) & \equiV \G\F f\AND\F\G g \\
& & \F\G(f\OR\F g) & \equivEU \F\G f\OR\G\F g & \G\F(f\OR\G g) & \equivEU \G\F f\OR\F\G g
\X\F\G f & \equiv \F\G f & \F(f\U g) & \equiv \F g & \G(f \R g) & \equiv \G g \\
\X\G\F f & \equiv \G\F f & \F(f\M g) & \equiv \F (f\AND g) & \G(f \W g) & \equiv \G(f\OR g) \\
\F\X f & \equiv \X\F f & \F\G(f\AND \X g) & \equiv \F\G(f\AND g) & \G\F(f\OR \X g) & \equiv \G\F(f\OR g) \\
\G\X f & \equiv \X\G f & \F\G(f\AND \G g) & \equiv \F\G(f\AND g) & \G\F(f\OR \F g) & \equiv \G\F(f\OR g) \\
& & \F\G(f\OR\G g) & \equiv \F(\G f\OR\G g) & \G\F(f\AND\F g) & \equiv \G(\F f\AND\F g) \\
\G\F f & \equiV \G\F(\mathsf{dnf}(f)) & \F\G(f\AND\F g) & \equiV \F\G f\AND\G\F g & \G\F(f\AND\G g) & \equiV \G\F f\AND\F\G g \\
\F\G f & \equiV \F\G(\mathsf{cnf}(f)) & \F\G(f\OR\F g) & \equivEU \F\G f\OR\G\F g & \G\F(f\OR\G g) & \equivEU \G\F f\OR\F\G g
\end{align*}
\begin{align*}
\G(f_1\OR\ldots\OR f_n \OR \G\F(g_1)\OR\ldots\OR \G\F(g_m)) & \equiv \G(f_1\OR\ldots\OR f_n)\OR \G\F(g_1\OR\ldots\OR g_m)
......
......@@ -33,6 +33,7 @@
#include <spot/tl/snf.hh>
#include <spot/tl/length.hh>
#include <spot/twa/formula2bdd.hh>
#include <spot/misc/minato.hh>
#include <cassert>
#include <memory>
......@@ -45,6 +46,7 @@ namespace spot
{
typedef std::unordered_map<formula, formula> f2f_map;
typedef std::unordered_map<formula, bdd> f2b_map;
typedef std::map<int, formula> b2f_map;
typedef std::pair<formula, formula> pairf;
typedef std::map<pairf, bool> syntimpl_cache_t;
public:
......@@ -78,13 +80,18 @@ namespace spot
<< "syntactic implications: " << syntimpl_.size() << " entries\n"
<< "boolean to bdd: " << as_bdd_.size() << " entries\n"
<< "star normal form: " << snf_cache_.size() << " entries\n"
<< "boolean isop: " << bool_isop_.size() << " entries\n";
<< "boolean isop: " << bool_isop_.size() << " entries\n"
<< "as dnf: " << as_dnf_.size() << " entries\n"
<< "as cnf: " << as_cnf_.size() << " entries\n";
}
void
clear_as_bdd_cache()
{
as_bdd_.clear();
for (auto p: bdd_to_f_)
dict->unregister_variable(p.first, this);
bdd_to_f_.clear();
}
// Convert a Boolean formula into a BDD for easier comparison.
......@@ -136,7 +143,12 @@ namespace spot
break;
}
default:
SPOT_UNIMPLEMENTED();
{
unsigned var = dict->register_anonymous_variables(1, this);
bdd_to_f_[var] = f;
result = bdd_ithvar(var);
break;
}
}
// Cache the result before returning.
......@@ -144,6 +156,83 @@ namespace spot
return result;
}
formula as_xnf(formula f, bool cnf)
{
bdd in = as_bdd(f);
if (cnf)
in = !in;
minato_isop isop(in);
bdd cube;
vec clauses;
while ((cube = isop.next()) != bddfalse)
{
vec literals;
while (cube != bddtrue)
{
int var = bdd_var(cube);
const bdd_dict::bdd_info& i = dict->bdd_map[var];
formula res;
if (i.type == bdd_dict::var)
{
res = i.f;
}
else
{
res = bdd_to_f_[var];
assert(res);
}
bdd high = bdd_high(cube);
if (high == bddfalse)
{
if (!cnf)
res = formula::Not(res);
cube = bdd_low(cube);
}
else
{
if (cnf)
res = formula::Not(res);
// If bdd_low is not false, then cube was not a
// conjunction.
assert(bdd_low(cube) == bddfalse);
cube = high;
}
assert(cube != bddfalse);
literals.emplace_back(res);
}
if (cnf)
clauses.emplace_back(formula::Or(literals));
else
clauses.emplace_back(formula::And(literals));
}
if (cnf)
return formula::And(clauses);
else
return formula::Or(clauses);
}
formula as_dnf(formula f)
{
auto i = as_dnf_.find(f);
if (i != as_dnf_.end())
return i->second;
formula r = as_xnf(f, false);
as_dnf_[f] = r;
return r;
}
formula as_cnf(formula f)
{
auto i = as_cnf_.find(f);
if (i != as_cnf_.end())
return i->second;
formula r = as_xnf(f, true);
as_cnf_[f] = r;
return r;
}
formula
lookup_nenoform(formula f)
{
......@@ -303,7 +392,10 @@ namespace spot
private:
f2b_map as_bdd_;
b2f_map bdd_to_f_;
f2f_map simplified_;
f2f_map as_dnf_;
f2f_map as_cnf_;
f2f_map nenoform_;
syntimpl_cache_t syntimpl_;
snf_cache snf_cache_;
......@@ -987,22 +1079,32 @@ namespace spot
return recurse(res);
}
// FG(a & Xb) = FG(a & b)
// FG(a & Gb) = FG(a & b)
if (c.is({op::G, op::And}))
// FG(a) = FG(dnf(a)) if a is not Boolean
// and contains some | above non-Boolean subformulas.
if (c.is(op::G) && !c[0].is_boolean())
{
formula m = c[0];
if (!m.is_boolean())
{
formula out = m.map([](formula f)
{
if (f.is(op::X, op::G))
return f[0];
return f;
});
if (out != m)
return recurse(unop_unop(op::F, op::G, out));
}
bool want_cnf = m.is(op::And);
if (!want_cnf && m.is(op::Or))
for (auto cc : m)
if (cc.is(op::And))
{
want_cnf = true;
break;
}
if (want_cnf && !opt_.reduce_size_strictly)
m = c_->as_cnf(m);
// FG(a & Xb) = FG(a & b)
// FG(a & Gb) = FG(a & b)
if (m.is(op::And))
m = m.map([](formula f)
{
if (f.is(op::X, op::G))
return f[0];
return f;
});
if (c[0] != m)
return recurse(unop_unop(op::F, op::G, m));
}
}
// if Fa => a, keep a.
......@@ -1248,22 +1350,33 @@ namespace spot
return recurse(res);
}
// GF(a | Xb) = GF(a | b)
// GF(a | Fb) = GF(a | b)
if (c.is({op::F, op::Or}))
// GF(a) = GF(dnf(a)) if a is not Boolean
// and contains some | above non-Boolean subformulas.
if (c.is(op::F) && !c[0].is_boolean())
{
formula m = c[0];
if (!m.is_boolean())
{
formula out = m.map([](formula f)
{
if (f.is(op::X, op::F))
return f[0];
return f;
});
if (out != m)
return recurse(unop_unop(op::G, op::F, out));
}
bool want_dnf = m.is(op::Or);
if (!want_dnf && m.is(op::And))
for (auto cc : m)
if (cc.is(op::Or))
{
want_dnf = true;
break;
}
if (want_dnf && !opt_.reduce_size_strictly)
m = c_->as_dnf(m);
// GF(a | Xb) = GF(a | b)
// GF(a | Fb) = GF(a | b)
if (m.is(op::Or))
m = m.map([](formula f)
{
if (f.is(op::X, op::F))
return f[0];
return f;
});
if (c[0] != m)
return recurse(unop_unop(op::G, op::F, m));
}
// GF(f1 & f2 & eu1 & eu2) = G(F(f1 & f2) & eu1 & eu2
if (opt_.event_univ && c.is({op::F, op::And}))
......
......@@ -208,6 +208,7 @@ TESTS_misc = \
core/trival.test
TESTS_twa = \
core/385.test \
core/acc.test \
core/acc2.test \
core/bdddict.test \
......
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2019 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/>.
. ./defs
set -e
# Formulas from issue #385.
ltl2tgba -G --stats=%s,%f> out <<EOF
GFX((e & XXXa) -> (e & X!d))
G(Gc | Fa | F!G(c | Ge))
Ge | XGF(Ge & X(c & Fd))
G!GXXe -> GF(b & c & Gc)
G!(Gd & (c | Fb))
XF(F(Gc & Xb) -> a)
EOF
# Some of the following are still not optimal.
cat >expected <<EOF
1,GF(!a | !d | !e)
6,G(Gc | F(a | (!c & F!e)))
2,Ge | G(Fd & FGe & Fc)
1,F(G(Fb & FGc) | Ge)
4,G(F!d | (!c & G!b))
3,F(GF!c | G!b) | XFa
EOF
diff out expected
......@@ -369,7 +369,7 @@ diff output expected
cat >formulas <<EOF
GF((a & XXa) | (!a & XX!a)), 4,8, 4,8, 6,14, 7,14, 4,8
GF((a & XXXa) | (!a & XXX!a)), 7,14, 8,16, 8,18, 15,30, 8,16
GF(((a & Xb) | XXc) & Xd), 4,64, 4,64, 5,80, 5,80, 4,64
GF(((a & Xb) | XXc) & Xd), 3,58, 4,64, 3,58, 5,80, 4,64
GF((b | Fa) & (b R Xb)), 2,4, 2,4, 3,6, 3,12, 2,4
G(F(a & Xa) & F(a & X!a)), 2,4, 2,4, 4,8, 4,8, 3,6
G(!p0 & F(p1 & XG!p1)), 1,0, 1,0, 1,0, 1,0, 1,0
......
......@@ -346,6 +346,8 @@ F(G(a & Fb)), G(Fb & FGa)
G(F(a & Gb)), G(Fa & FGb)
Ge | XGF(Ge & X(c & Fd)), Ge | G(Fd & FGe & Fc)
G!GXXe -> GF(b & c & Gc), F(G(Fb & FGc) | Ge)
GFX((e & XXXa) -> (e & X!d)), GF(!a | !d | !e)
!GFX((e & XXXa) -> (e & X!d)), FG(a & d & e)
# Because reduccmp will translate the formula,
# this also check for an old bug in ltl2tgba_fm.
......
This diff is collapsed.
This diff is collapsed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment