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

simplifier: add two new rules

Browse source 
Fixes #354.

* spot/tl/simplify.cc: Implement the rules.
* doc/tl/tl.tex, NEWS: Document them.
* tests/core/reduccmp.test: Add tests.
* tests/core/det.test, tests/core/satmin.test: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2018-06-04 13:49:40 +02:00
parent 8e3b982985
commit ca1c67a73d
6 changed files with 51 additions and 29 deletions
Download patch file Download diff file Expand all files Collapse all files

7
NEWS
View file

@ -130,6 +130,13 @@ New in spot 2.5.3.dev (not yet released)
the resulting TGBA makes it more likely that simulation-based the resulting TGBA makes it more likely that simulation-based
reductions will reduce it. reductions will reduce it.
- The LTL simplification routine learned the following reductions,
where f is any formula, and q is a "suspendable" formula (a.k.a.
both a pure eventuality and purely universal).
q R Xf = X(q R f)
q U Xf = X(q U f)
Python: Python:
- New spot.jupyter package. This currently contains a function for - New spot.jupyter package. This currently contains a function for

20
doc/tl/tl.tex
View file

@ -1669,22 +1669,22 @@ notation to distinguish the class of subformulas:
\begin{center} \begin{center}
\begin{tabular}{rl} \begin{tabular}{rl}
\toprule \toprule
$f,\,f_i,\,g,\,g_i$ & any PSL formula \\ $f,\,f_i,\,g,\,g_i$ & any PSL formula \\
$e,\,e_i$ & a pure eventuality \\ $e,\,e_i$ & a pure eventuality \\
$u,\,u_i$ & a purely universal formula \\ $u,\,u_i$ & a purely universal formula \\
$q,\,q_i$ & a pure eventuality that is also purely universal \\ $q,\,q_i$ & a pure eventuality that is also purely universal \\
\bottomrule \bottomrule
\end{tabular} \end{tabular}
\end{center} \end{center}
\begin{align*} \begin{align*}
\F e & \equiv e & f \U e & \equiv e & e \M g & \equiv e\AND g & u_1 \M u_2 & \equiV (\F u_1) \AND u_2 \\ \F e & \equiv e & f \U e & \equiv e & e \M g & \equiv e\AND g & u_1 \M u_2 & \equiV (\F u_1) \AND u_2 \\
\F(u)\OR q & \equivEU \F(u\OR q) & f \U (g\OR e) & \equivEU (f \U g)\OR e & f\M (g\AND u) & \equivEU (f \M g)\AND u \\ \F(u)\OR q & \equivNeu \F(u\OR q) & f \U (g\OR e) & \equivEU (f \U g)\OR e & f\M (g\AND u) & \equivEU (f \M g)\AND u & q \U\X f & \equiv \X(q \U f) \\
& & f \U (g\AND q) & \equivEU (f \U g)\AND q & (f\AND q)\M g & \equivEU (f \M g)\AND q \\ & & f \U (g\AND q) & \equivEU (f \U g)\AND q & (f\AND q)\M g & \equivEU (f \M g)\AND q \\
\G u & \equiv u & u \W g & \equiv u\OR g & f \R u & \equiv u & e_1 \W e_2 & \equiV (\G e_1) \OR e_2 \\ \G u & \equiv u & u \W g & \equiv u\OR g & f \R u & \equiv u & e_1 \W e_2 & \equiV (\G e_1) \OR e_2 \\
\G(e)\AND q & \equiv \G(e\AND q) & f \W (g\OR e) & \equivEU (f \W g)\OR e & f\R (g\AND u) & \equivEU (f \R g)\AND u \\ \G(e)\AND q & \equiv \G(e\AND q) & f \W (g\OR e) & \equivEU (f \W g)\OR e & f\R (g\AND u) & \equivEU (f \R g)\AND u & q \R\X f & \equiv \X(q \R f) \\
\X q & \equiv q & q \AND \X f & \equivNeu \X(q \AND f) & q\OR \X f & \equivNeu \X(q \OR f) \\ \X q & \equiv q & q \AND \X f & \equivNeu \X(q \AND f) & q\OR \X f & \equivNeu \X(q \OR f) \\
& & \X(q \AND f) & \equivEU q \AND \X f & \X(q \OR f) & \equivEU q\OR \X f \\ & & \X(q \AND f) & \equivEU q \AND \X f & \X(q \OR f) & \equivEU q\OR \X f \\
\end{align*} \end{align*}
\begin{align*} \begin{align*}

11
spot/tl/simplify.cc
View file

@ -1682,8 +1682,19 @@ namespace spot
if (a.is_universal() && bo.is(op::W)) if (a.is_universal() && bo.is(op::W))
return recurse(formula::Or({a, b})); return recurse(formula::Or({a, b}));
// (q R Xf) = X(q R f)
// (q U Xf) = X(q U f)
if (a.is_eventual() && a.is_universal()
&& bo.is(op::R, op::U) && b.is(op::X))
return recurse(formula::X(formula::binop(o, a, b[0])));
// e₁ W e₂ = Ge₁ | e₂ // e₁ W e₂ = Ge₁ | e₂
// u₁ M u₂ = Fu₁ & u₂ // u₁ M u₂ = Fu₁ & u₂
//
// The above formulas are actually true if e₁ and u₁ are
// unconstrained, however there are many cases were such a
// more generic reduction rule will actually produce more
// states once the resulting formula is translated.
if (!opt_.reduce_size_strictly) if (!opt_.reduce_size_strictly)
{ {
if (bo.is(op::W) && a.is_eventual() && b.is_eventual()) if (bo.is(op::W) && a.is_eventual() && b.is_eventual())

2
tests/core/det.test
View file

@ -36,7 +36,7 @@ cat >formulas <<'EOF'
1,5,a M G(F!b | X!a) 1,5,a M G(F!b | X!a)
1,4,G!a R XFb 1,4,G!a R XFb
1,4,XF(!a | GFb) 1,4,XF(!a | GFb)
1,6,GF!a U Xa 1,5,X(GF!a U a)
1,5,(a | G(a M !b)) W Fc 1,5,(a | G(a M !b)) W Fc
1,6,Fa W Xb 1,6,Fa W Xb
1,9,X(a R ((!b & F!c) M X!a)) 1,9,X(a R ((!b & F!c) M X!a))

4
tests/core/reduccmp.test
View file

@ -192,7 +192,11 @@ GFa <=> GFb, F(G(Fa&Fb)|G(!a&!b))
FGa | (GFa & GFb), F(Ga | (G(Fa & Fb))) FGa | (GFa & GFb), F(Ga | (G(Fa & Fb)))
Gb W a, Gb|a Gb W a, Gb|a
a W Fb, a W Fb
Fb M Fa, Fa & Fb Fb M Fa, Fa & Fb
a M Gb, a M Gb
GFa R Xf, X(GFa R f)
GFa U Xf, X(GFa U f)
a U (b | G(a) | c), a W (b | c) a U (b | G(a) | c), a W (b | c)
a U (G(a)), Ga a U (G(a)), Ga

36
tests/core/satmin.test
View file

@ -1140,8 +1140,8 @@ cat >expected <<'EOF'
"!(X(F((!(p0)) | (G(F(p1))))))","15",3 "!(X(F((!(p0)) | (G(F(p1))))))","15",3
"!(X(F((!(p0)) | (G(F(p1))))))","16",3 "!(X(F((!(p0)) | (G(F(p1))))))","16",3
"!(X(F((!(p0)) | (G(F(p1))))))","17",3 "!(X(F((!(p0)) | (G(F(p1))))))","17",3
"(G((F(!(p0))) U (!(p0)))) U (X(p0))","1",6 "(G((F(!(p0))) U (!(p0)))) U (X(p0))","1",5
"(G((F(!(p0))) U (!(p0)))) U (X(p0))","2",6 "(G((F(!(p0))) U (!(p0)))) U (X(p0))","2",5
"(G((F(!(p0))) U (!(p0)))) U (X(p0))","3",5 "(G((F(!(p0))) U (!(p0)))) U (X(p0))","3",5
"(G((F(!(p0))) U (!(p0)))) U (X(p0))","4",5 "(G((F(!(p0))) U (!(p0)))) U (X(p0))","4",5
"(G((F(!(p0))) U (!(p0)))) U (X(p0))","6",5 "(G((F(!(p0))) U (!(p0)))) U (X(p0))","6",5
@ -1156,22 +1156,22 @@ cat >expected <<'EOF'
"(G((F(!(p0))) U (!(p0)))) U (X(p0))","15",5 "(G((F(!(p0))) U (!(p0)))) U (X(p0))","15",5
"(G((F(!(p0))) U (!(p0)))) U (X(p0))","16",5 "(G((F(!(p0))) U (!(p0)))) U (X(p0))","16",5
"(G((F(!(p0))) U (!(p0)))) U (X(p0))","17",5 "(G((F(!(p0))) U (!(p0)))) U (X(p0))","17",5
"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","1",5 "!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","1",4
"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","2",5 "!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","2",4
"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","3",5 "!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","3",4
"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","4",5 "!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","4",4
"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","6",5 "!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","6",4
"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","7",5 "!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","7",4
"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","8",5 "!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","8",4
"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","9",5 "!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","9",4
"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","10",5 "!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","10",4
"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","11",5 "!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","11",4
"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","12",5 "!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","12",4
"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","13",5 "!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","13",4
"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","14",5 "!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","14",4
"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","15",5 "!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","15",4
"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","16",5 "!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","16",4
"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","17",5 "!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","17",4
"((p0) | (G((p0) M (!(p1))))) W (F(p2))","1",4 "((p0) | (G((p0) M (!(p1))))) W (F(p2))","1",4
"((p0) | (G((p0) M (!(p1))))) W (F(p2))","2",5 "((p0) | (G((p0) M (!(p1))))) W (F(p2))","2",5
"((p0) | (G((p0) M (!(p1))))) W (F(p2))","3",4 "((p0) | (G((p0) M (!(p1))))) W (F(p2))","3",4