Commit 646c5170 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

simplify: some new simplification rules

For #263, reported by Mikuláš Klokočka.

G(a & Xe1 & F(b & e2)) = G(a & e1 & Fb & e2)
F(a | Xu1 | G(b | u2)) = F(a | u1 | Gb | u2)

* spot/tl/simplify.cc: Implement the rules.
* doc/tl/tl.tex, NEWS: Document them.
* tests/core/reduccmp.test, tests/core/eventuniv.test: Add test cases.
* tests/core/det.test, tests/core/ltl2tgba2.test: Adjust to expect
smaller automata.
* THANKS: Add Mikuláš.
parent cd6f1c2c
......@@ -173,6 +173,10 @@ New in spot 2.3.5.dev (not yet released)
more (this threshold can be changed, see -x relabel-bool=N in
the spot-x(7) man page).
- The LTL simplification routines learned that an LTL formula like
G(a & XF(b & XFc & Fd) can be simplified to G(a & Fb & Fc & Fd),
and dually F(a | XG(b | XGc | Gd)) = F(a | Gb | Gc | Gd).
- The new function spot::to_weak_alternating() is able to take an
input automaton with generalized Büchi/co-Büchi acceptance and
convert it to a weak alternating automaton.
......
......@@ -26,6 +26,7 @@ Martin Dieguez Lodeiro
Matthias Heizmann
Michael Tautschnig
Michael Weber
Mikuláš Klokočka
Ming-Hsien Tsai
Nikos Gorogiannis
Reuben Rowe
......
......@@ -1682,6 +1682,10 @@ $q,\,q_i$ & a pure eventuality that is also purely universal \\
\end{align*}
\begin{align*}
\G(f_1\AND\ldots\AND f_n \AND \X e_1 \AND \ldots \AND \X e_p)&\equiv \G(f_1\AND\ldots\AND f_n \AND e_1 \AND \ldots \AND e_p) \\
\G(f_1\AND\ldots\AND f_n \AND \F (g_1 \AND \ldots \AND g_p \AND \X e_1 \AND \X e_m))&\equiv \G(f_1\AND\ldots\AND f_n \AND \F(g_1 \AND \ldots \AND g_p) \AND e_1 \AND \ldots \AND e_m) \\
\F(f_1\OR\ldots\OR f_n \OR \X u_1 \OR \ldots \OR \X u_p)&\equiv \F(f_1\OR\ldots\OR f_n \OR u_1 \OR \ldots \AND u_p) \\
\F(f_1\OR\ldots\OR f_n \OR \G (g_1 \OR \ldots \OR g_p \OR \X u_1 \OR \X u_m))&\equiv \F(f_1\OR\ldots\AND f_n \OR \G(g_1 \OR \ldots \OR g_p) \OR u_1 \OR \ldots \OR u_m) \\
\G(f_1\OR\ldots\OR f_n \OR q_1 \OR \ldots \OR q_p)&\equiv \G(f_1\OR\ldots\OR f_n)\OR q_1 \OR \ldots \OR q_p \\
\F(f_1\AND\ldots\AND f_n \AND q_1 \AND \ldots \AND q_p)&\equivEU \F(f_1\AND\ldots\AND f_n)\AND q_1 \AND \ldots \AND q_p \\
\G(f_1\AND\ldots\AND f_n \AND q_1 \AND \ldots \AND q_p)&\equivEU \G(f_1\AND\ldots\AND f_n)\AND q_1 \AND \ldots \AND q_p \\
......
......@@ -995,28 +995,52 @@ namespace spot
return recurse(res);
}
// If u3 and u4 are universal formulae and h is not:
// F(f1 | f2 | Fu3 | u4 | FGg | Fh)
// = F(f1 | f2 | u3 | u4 | Gg | h)
// F(f1 | f2 | Fu3 | u4 | FGg | Fh | Xu5 | G(f6 | Xu7 | u8))
// = F(f1 | f2 | u3 | u4 | Gg | h | u5 | Gf6 | u7 | u8)
// or
// F(f1 | f2 | Fu3 | u4 | FGg | Fh)
// = F(f1 | f2 | h) | F(u3 | u4 | Gg)
// F(f1 | f2 | Fu3 | u4 | FGg | Fh | Xu5)
// = F(f1 | f2 | h) | F(u3 | u4 | Gg | u5 | Gf6 | u7 | u8)
// depending on whether favor_event_univ is set.
if (c.is(op::Or))
{
int w = mospliter::Strip_F;
int w = mospliter::Strip_F
| mospliter::Strip_X | mospliter::Split_G;
if (opt_.favor_event_univ)
w |= mospliter::Split_Univ;
mospliter s(w, c, c_);
s.res_other->insert(s.res_other->end(),
s.res_F->begin(), s.res_F->end());
for (formula f: *s.res_X)
if (f.is_universal())
s.res_other->push_back(f);
else
s.res_other->push_back(formula::X(f));
std::vector<formula>* to = opt_.favor_event_univ ?
s.res_Univ.get() : s.res_other.get();
for (formula g: *s.res_G)
if (g[0].is(op::Or))
{
mospliter s2(mospliter::Split_Univ, g[0], c_);
for (formula u: *s2.res_Univ)
to->push_back(u.is(op::X) ? u[0] : u);
to->push_back(unop_multop(op::G, op::Or,
std::move(*s2.res_other)));
}
else
{
to->push_back(g);
}
formula res = unop_multop(op::F, op::Or,
std::move(*s.res_other));
if (s.res_Univ)
{
// Strip any F.
std::vector<formula> toadd;
for (auto& g: *s.res_Univ)
if (g.is(op::F))
// Strip any F or X
if (g.is(op::F, op::X))
g = g[0];
s.res_Univ->insert(s.res_Univ->end(),
toadd.begin(), toadd.end());
formula fu = unop_multop(op::F, op::Or,
std::move(*s.res_Univ));
res = formula::Or({res, fu});
......@@ -1071,29 +1095,55 @@ namespace spot
return recurse(res);
}
// If e3 and e4 are eventual formulae and h is not:
// G(f1 & f2 & Ge3 & e4 & GFg & Gh)
// = G(f1 & f2 & e3 & e4 & Fg & h)
// G(f1 & f2 & Ge3 & e4 & GFg & Gh & Xe5 & F(f6 & Xe7 & e8))
// = G(f1 & f2 & e3 & e4 & Fg & h & e5 & Ff6 & e7 & e8)
// or
// G(f1 & f2 & Ge3 & e4 & GFg & Gh)
// = G(f1 & f2 & h) & G(e3 & e4 & Fg)
// G(f1 & f2 & Ge3 & e4 & GFg & Gh & Xe5 & F(f6 & Xe7 & e8))
// = G(f1 & f2 & h) & G(e3 & e4 & Fg & e5 & Ff6 & e7 & e8)
// depending on whether favor_event_univ is set.
else if (c.is(op::And))
{
int w = mospliter::Strip_G;
int w = mospliter::Strip_G |
mospliter::Strip_X | mospliter::Split_F;
if (opt_.favor_event_univ)
w |= mospliter::Split_Event;
mospliter s(w, c, c_);
s.res_other->insert(s.res_other->end(),
s.res_G->begin(), s.res_G->end());
for (formula f: *s.res_X)
if (f.is_eventual())
s.res_other->push_back(f);
else
s.res_other->push_back(formula::X(f));
std::vector<formula>* to = opt_.favor_event_univ ?
s.res_Event.get() : s.res_other.get();
for (formula f: *s.res_F)
if (f[0].is(op::And))
{
mospliter s2(mospliter::Split_Event, f[0], c_);
for (formula e: *s2.res_Event)
to->push_back(e.is(op::X) ? e[0] : e);
to->push_back
(unop_multop(op::F, op::And,
std::move(*s2.res_other)));
}
else
{
to->push_back(f);
}
formula res = unop_multop(op::G, op::And,
std::move(*s.res_other));
if (s.res_Event)
{
// Strip any G.
std::vector<formula> toadd;
// Strip any G or X
for (auto& g: *s.res_Event)
if (g.is(op::G))
g = g[0];
if (g.is(op::G, op::X))
{
g = g[0];
}
s.res_Event->insert(s.res_Event->end(),
toadd.begin(), toadd.end());
formula ge =
unop_multop(op::G, op::And,
std::move(*s.res_Event));
......
......@@ -51,7 +51,7 @@ cat >formulas <<'EOF'
1,2,Ga R Fb
1,3,G(a U (b | X((!a & !c) | (a & c))))
1,5,XG((G!a & F!b) | (Fa & (a | Gb)))
1,10,(a U X!a) | XG(!b & XFc)
1,9,(a U X!a) | XG(!b & Fc)
1,4,X(G!a | GFa)
1,4,G(G!a | F!c | G!b)
EOF
......
#! /bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
# Copyright (C) 2012, 2013, 2014, 2017 Laboratoire de Recherche et
# Developpement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
......@@ -41,6 +41,11 @@ G(Ga & GXFb & c & FGd & FGe & Fc), G(Fb & FG(d & e)) & G(a & c)
Ga & Gb & GFd & FGe & FGf, G(Fd & FG(e & f)) & G(a & b)
G(Ga & Gb & GFd & FGe) & FGf, G(Fd & FG(e & f)) & G(a & b)
G(a & XFb), Ga & GFb
G(a & XF(b & XFc & Fd)), Ga & G(Fb & Fc & Fd)
F(a | XGb), Fa | FGb
F(a | XG(b | XGc | Gd)), Fa | F(Gb | Gc | Gd)
a U (b | Fc), (a U b) | Fc
a W (b | Fc), (a W b) | Fc
a U (b & GFc), (a U b) & GFc
......
......@@ -100,7 +100,7 @@ eh-patterns,5, 4,32, 4,32, 4,32, 4,32
eh-patterns,6, 3,24, 3,24, 3,24, 3,24
eh-patterns,7, 3,14, 3,14, 4,18, 4,18
eh-patterns,8, 2,13, 2,13, 2,13, 2,13
eh-patterns,9, 5,58, 5,58, 8,80, 8,80
eh-patterns,9, 1,8, 1,8, 4,32, 4,32
eh-patterns,10, 1,32, 1,32, 6,192, 6,192
eh-patterns,11, 2,15, 2,15, 2,15, 2,15
eh-patterns,12, 4,60, 4,60, 4,60, 4,60
......@@ -264,7 +264,7 @@ p-patterns,20, 1,8, 1,8, 3,24, 3,24
!eh-patterns,6, 2,12, 2,12, 2,12, 2,12
!eh-patterns,7, 2,7, 2,7, 3,9, 3,9
!eh-patterns,8, 3,21, 3,21, 3,21, 3,21
!eh-patterns,9, 5,80, 5,80, 5,80, 5,80
!eh-patterns,9, 5,68, 5,68, 5,68, 5,68
!eh-patterns,10, 6,192, 6,192, 6,192, 6,192
!eh-patterns,11, 2,9, 2,9, 2,9, 2,9
!eh-patterns,12, 6,103, 6,103, 8,135, 8,135
......
......@@ -300,6 +300,11 @@ a W ((a&b) W c), a W c
Fa M b, Fa & b
GFa M b, GFa & b
G(a & XFb), G(a & Fb)
G(a & XF(b & XFc & Fd)), G(a & Fb & Fc & Fd)
F(a | XGb), F(a | Gb)
F(a | XG(b | XGc | Gd)), F(a | Gb | Gc | Gd)
Fa|Xb|GFc, Fa | X(b|GFc)
Fa|GFc, F(a|GFc)
FGa|GFc, F(Ga|GFc)
......
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