Skip to content
GitLab
Commit 82a152c3 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

unabbreviate: add new rules based on eventual/universal arguments 

Based on a report by Simon Jantsch.  Fixes #362.

* NEWS, doc/tl/tl.tex: Mention the new rules.
* spot/tl/unabbrev.cc: Implement them.
* tests/core/unabbrevwm.test: Test them.
* tests/python/randltl.ipynb: Adjust.
parent 0de334d7
Pipeline #3960 failed with stages
in 264 minutes and 11 seconds
Hide whitespace changes
Inline Side-by-side
NEWS
View file @ 82a152c3
......@@ -37,6 +37,16 @@ New in spot 2.6.2.dev (not yet released)
formula::F(unsigned, unsigned, formula)
formula::G(unsigned, unsigned, formula)
- spot::unabbreviate(), used to rewrite away operators such as M or
W, learned to use some shorter rewritings when an argument (e) is
a pure eventuality or (u) is purely universal:
Fe = e
Gu = u
f R u = u
f M e = F(f & e)
f W u = G(f | u)
- The twa_graph class has a new dump_storage_as_dot() method
to show its data structure. This is more conveniently used
as aut.show_storage() in a Jupyter notebook. See
......
doc/tl/tl.tex
View file @ 82a152c3
......@@ -1272,18 +1272,23 @@ instance passing the string \texttt{"\^{}ei"} will rewrite all
occurrences of $\XOR$, $\EQUIV$ and $\IMPLIES$.
\[
\begin{array}{l@{\qquad}r@{\;}c@{\;}l}
\begin{array}{l@{\qquad}r@{\;}c@{\;}ll}
``\texttt{i}" & f\IMPLIES g &\equiv& (\NOT f)\OR g\\
``\texttt{e}" & f\EQUIV g &\equiv& (f\AND g)\OR ((\NOT g)\AND(\NOT f))\\
``\texttt{\^{}e}" & f\XOR g &\equiv& (f\AND\NOT g)\OR (g\AND\NOT f)\\
``\texttt{\^{}}"\text{~without~}``\texttt{e}" & f\XOR g &\equiv& \NOT(f\EQUIV g)\\
``\texttt{F}" & \F e&\equiv& e & \text{when $e$ is a pure eventuality}\\
``\texttt{F}" & \F f&\equiv& \1\U f\\
``\texttt{G}" & \G u&\equiv& u & \text{when $u$ is purely universal}\\
``\texttt{G}"\text{~without~}``\texttt{R}" & \G f&\equiv& \0\R f \\
``\texttt{GR}"\text{~without~}``\texttt{W}" & \G f&\equiv& f \W \0 \\
``\texttt{GRW}" & \G f&\equiv& \NOT\F\NOT f \\
``\texttt{M}" & f \M e&\equiv& \F(f\AND e) & \text{when $e$ is a pure eventuality} \\
``\texttt{M}" & f \M g&\equiv& g \U (g \AND f) \\
``\texttt{R}" & f \R u&\equiv& u & \text{when $u$ is purely universal} \\
``\texttt{R}"\text{~without~}``\texttt{W}" & f \R g&\equiv& g\W (f \AND g)\\
``\texttt{RW}" & f \R g&\equiv& g\U ((f \AND g) \OR \G g) \\
``\texttt{W}" & f \W u&\equiv& \G(f \OR u) & \text{when $u$ is purely universal} \\
``\texttt{W}"\text{~without~}``\texttt{R}" & f \W g&\equiv& g \R (g \OR f)\\
``\texttt{WR}" & f \W g&\equiv& f \U (g \OR \G f)\\
\end{array}
......
spot/tl/unabbrev.cc
View file @ 82a152c3
......@@ -115,18 +115,30 @@ namespace spot
case op::FStar:
break;
case op::F:
// F e = e if e eventual
// F f = true U f
if (!re_f_)
break;
if (out[0].is_eventual())
{
out = out[0];
break;
}
out = formula::U(formula::tt(), out[0]);
break;
case op::G:
// G u = u if u universal
// G f = false R f
// G f = f W false
// G f = !F!f
// G f = !(true U !f)
if (!re_g_)
break;
if (out[0].is_universal())
{
out = out[0];
break;
}
if (!re_r_)
{
out = formula::R(formula::ff(), out[0]);
......@@ -188,6 +200,7 @@ namespace spot
break;
}
case op::R:
// f1 R u = u if u universal
// f1 R f2 = f2 W (f1 & f2)
// f1 R f2 = f2 U ((f1 & f2) | Gf2)
// f1 R f2 = f2 U ((f1 & f2) | !F!f2)
......@@ -195,8 +208,13 @@ namespace spot
if (!re_r_)
break;
{
auto f1 = out[0];
auto f2 = out[1];
if (f2.is_universal())
{
out = f2;
break;
}
auto f1 = out[0];
auto f12 = formula::And({f1, f2});
if (!re_w_)
{
......@@ -210,6 +228,7 @@ namespace spot
break;
}
case op::W:
// f1 W u = G(f1 | u) if u universal
// f1 W f2 = f2 R (f2 | f1)
// f1 W f2 = f1 U (f2 | G f1)
// f1 W f2 = f1 U (f2 | !F !f1)
......@@ -219,9 +238,15 @@ namespace spot
{
auto f1 = out[0];
auto f2 = out[1];
if (f2.is_universal())
{
auto g = formula::G(formula::Or({f1, f2}));
out = re_g_ ? run(g) : g;
break;
}
if (!re_r_)
{
out = formula::R(f2, formula::Or({f2, f1}));
out = formula::R(f2, formula::Or({f1, f2}));
break;
}
auto gf1 = formula::G(f1);
......@@ -231,12 +256,21 @@ namespace spot
break;
}
case op::M:
// f1 M e = F(f1 & e) if e eventual
// f1 M f2 = f2 U (g2 & f1)
if (!re_m_)
break;
{
auto f1 = out[0];
auto f2 = out[1];
out = formula::U(f2, formula::And({f2, out[0]}));
auto andf = formula::And({f1, f2});
if (f2.is_eventual())
{
auto f = formula::F(andf);
out = re_f_ ? run(f) : f;
break;
}
out = formula::U(f2, andf);
break;
}
}
......
tests/core/unabbrevwm.test
View file @ 82a152c3
#! /bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2012, 2015, 2017 Laboratoire de Recherche et Développement
# Copyright (C) 2012, 2015, 2017, 2018 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
......@@ -26,16 +26,33 @@
set -e
# Removing W,M in this formula caused a segfault at some point.
run 0 ltlfilt --remove-wm >out <<EOF
run 0 ltlfilt --remove-wm <<EOF | uniq >out
(!((G(p0)) U ((F(p0)) M ((F(X(p1))) & ((p2) W (G(p2))))))) M (F(p0))
(Fp0 U(Fp0&!(Gp0 U((FXp1 &(Gp2 R(p2|Gp2))) U(Fp0&FXp1&(Gp2 R(p2|Gp2)))))))
F(Fp0 & !(Gp0 U ((FXp1 & G(p2 | Gp2)) U (Fp0 & FXp1 & G(p2 | Gp2)))))
EOF
# The first formula will be simplified to the second, so after uniq
# the output should have one line.
test `uniq out | wc -l` = 1
test `wc -l <out` = 1
for i in 'GFa' 'a R b' 'a W b' 'a M b'; do
f='(Fp0 U(Fp0&!(Gp0 U((FXp1 &(Gp2 R(p2|Gp2))) U(Fp0&FXp1&(Gp2 R(p2|Gp2)))))))'
test `ltlfilt -c --equivalent-to="$f" out` = 1
# From issue #362.
simon='!p0 W (p0 W (!p0 W (p0 W G!p0)))'
ltlfilt --unabbrev=WRMF -f "$simon" -f 'FGFa' -f 'a M Fb' -f 'a R Gb' >out
cat out
cat >expected <<EOF
G(!p0 | G(p0 | G(!p0 | G(p0 | G!p0))))
G(1 U a)
1 U (a & (1 U b))
Gb
EOF
diff out expected
for i in 'GFa' 'a R b' 'a W b' 'a M b' "$simon"; do
for fg in '' F G GF; do
for rwm in '' R W M RW RM WM RWM; do
ltlfilt -f "$i" --unabbrev=$fg$rwm --equivalent-to "$i" >out
......
tests/python/randltl.ipynb
View file @ 82a152c3
%% Cell type:markdown id: tags:
# Documentation for spot's randltl python binding
# Documentation for Spot's randltl Python binding
%% Cell type:code id: tags:
``` python
import spot
```
%% Cell type:markdown id: tags:
## Basic usage
%% Cell type:markdown id: tags:
Generate random formulas from specified atomic propositions:
%% Cell type:code id: tags:
``` python
f = spot.randltl(['a', 'b', 'c'])
for i in range(3):
print(next(f))
```
%% Output
0
0 R b
F(XG(F!b M Fb) W (b R a))
%% Cell type:markdown id: tags:
Generate random formulas using 3 atomic propositions:
%% Cell type:code id: tags:
``` python
f = spot.randltl(3)
for i in range(3):
print(next(f))
```
%% Output
0
0 R p1
F(XG(F!p1 M Fp1) W (p1 R p0))
%% Cell type:markdown id: tags:
By default, there is no limit to the number of formulas generated.<br/>
To specify a number of formulas:
%% Cell type:code id: tags:
``` python
f = spot.randltl(3, 4)
for formula in f:
print(formula)
```
%% Output
0
0 R p1
F(XG(F!p1 M Fp1) W (p1 R p0))
F(p0 R !p2)
%% Cell type:markdown id: tags:
## Keyword arguments
%% Cell type:markdown id: tags:
## seed
%% Cell type:markdown id: tags:
Seed for the pseudo random number generator (default: 0).
%% Cell type:code id: tags:
``` python
f = spot.randltl(3, seed=11)
print(next(f))
```
%% Output
G(p1 U Gp0)
%% Cell type:markdown id: tags:
### output
%% Cell type:markdown id: tags:
Type of formulas to output: 'ltl', 'psl', 'bool' or 'sere' (default: 'ltl').
%% Cell type:code id: tags:
``` python
f = spot.randltl(3, output='psl', seed=332)
print(next(f))
```
%% Output
{{p0 && p2}[*]}<>-> (Fp2 & Fp0)
%% Cell type:markdown id: tags:
### allow_dups
%% Cell type:markdown id: tags:
Allow duplicate formulas (default: False).
%% Cell type:code id: tags:
``` python
f = spot.randltl(1, allow_dups=True)
print(next(f))
print(next(f))
print(next(f))
```
%% Output
0
0
Fp0
%% Cell type:markdown id: tags:
### tree_size
%% Cell type:markdown id: tags:
Tree size of the formulas generated, before mandatory simplifications (default: 15).
%% Cell type:code id: tags:
``` python
f = spot.randltl(3, tree_size=30, seed=11)
print(next(f))
```
%% Output
G(((p0 U !Xp1) M Gp1) U Gp0)
%% Cell type:markdown id: tags:
A range can be specified as a tuple:
%% Cell type:code id: tags:
``` python
f = spot.randltl(3, tree_size=(1, 40))
print(next(f))
print(next(f))
```
%% Output
X!(Gp1 M p2) R (!p2 M Xp1)
F(G(F(Gp0 R (1 U Fp2)) M (p2 -> Gp0)) M F((p0 | Fp0) W Gp2))
%% Cell type:markdown id: tags:
### boolean_priorities, ltl_priorities, sere_priorities, dump_priorities
%% Cell type:code id: tags:
``` python
f = spot.randltl(3, output='bool', boolean_priorities='and=10,or=0')
for i in range(5):
print(next(f))
```
%% Output
0
!p2 & (p1 <-> p2)
p2
p0 & ((p1 & p2) <-> !(!p0 & p1 & p2))
1
%% Cell type:markdown id: tags:
To see which operators are available along with their default priorities:
%% Cell type:code id: tags:
``` python
spot.randltl(3, output='psl', dump_priorities=True)
```
%% Output
Use argument ltl_priorities=STRING to set the following LTL priorities:
ap 3
false 1
true 1
not 1
F 1
G 1
X 1
Closure 1
equiv 1
implies 1
xor 1
R 1
U 1
W 1
M 1
and 1
or 1
EConcat 1
UConcat 1
Use argument sere_priorities=STRING to set the following SERE priorities:
ap 3
false 1
true 1
not 1
F 1
G 1
X 1
Closure 1
equiv 1
implies 1
xor 1
R 1
U 1
W 1
M 1
and 1
or 1
EConcat 1
UConcat 1
eword 1
boolform 1
star 1
star_b 1
fstar 1
fstar_b 1
and 1
andNLM 1
or 1
concat 1
fusion 1
Use argument boolean_priorities=STRING to set the following Boolean formula priorities:
ap 3
false 1
true 1
not 1
F 1
G 1
X 1
Closure 1
equiv 1
implies 1
xor 1
R 1
U 1
W 1
M 1
and 1
or 1
EConcat 1
UConcat 1
eword 1
boolform 1
star 1
star_b 1
fstar 1
fstar_b 1
and 1
andNLM 1
or 1
concat 1
fusion 1
ap 3
false 1
true 1
not 1
equiv 1
implies 1
xor 1
and 1
or 1
%% Cell type:markdown id: tags:
### simplify
%% Cell type:markdown id: tags:
0 No rewriting<br/>
1 basic rewritings and eventual/universal rules<br/>
2 additional syntactic implication rules<br/>
3 better implications using containment<br/>
default: 3
%% Cell type:code id: tags:
``` python
f = spot.randltl(3, simplify=0, seed=5)
print(next(f))
f = spot.randltl(3, simplify=3, seed=5)
print(next(f))
```
%% Output
G!(!p1 & (Xp2 | F(p0 R Xp2)))
G(p1 | (X!p2 & G(!p0 U X!p2)))
%% Cell type:markdown id: tags:
## Filters and maps
%% Cell type:markdown id: tags:
most boolean functions found in the class formula can be used to filter the random formula generator like this:
%% Cell type:code id: tags:
``` python
f = spot.randltl(3, 20).is_syntactic_stutter_invariant()
for formula in f:
print(formula)
```
%% Output
0
0 R p2
F(p0 R !p1)
G(p0 | Fp2) W (FGp2 R !p2)
(p2 R G!p1) | G(p2 U !p0)
(p2 W p0) U p2
F!G(!Gp1 W p1)
G!p1 & (!((p2 & Fp1) M p1) U p1)
%% Cell type:markdown id: tags:
likewise, functions from formula to formula can be applied to map the iterator:
%% Cell type:code id: tags:
``` python
f = spot.randltl(2, 6).remove_x()
for formula in f:
print(formula)
```
%% Output
0
!(F!p1 M 1)
(Gp0 | Fp1) M 1
F!(!p1 <-> FGp1)
Gp1 U (p1 U GFp1)
(!p1 U p1) U ((p0 & (p0 U (!p0 & (!p0 -> Fp1))) & ((!p1 U !p0) | (p1 U !p0))) | (!p0 & (!p0 U (p0 & (!p0 -> Fp1))) & ((!p1 U p0) | (p1 U p0))) | (p1 & (p1 U (!p1 & (!p0 -> Fp1))) & ((!p0 U !p1) | (p0 U !p1))) | (!p1 & (!p1 U (p1 & (!p0 -> Fp1))) & ((!p0 U p1) | (p0 U p1))) | ((!p0 -> Fp1) & (Gp0 | G!p0) & (Gp1 | G!p1)))
%% Cell type:markdown id: tags:
Since the boolean filters and mapping functions return an iterator of the same type, these operations can be chained like this:
%% Cell type:code id: tags:
``` python
f = spot.randltl(3, 20).is_syntactic_stutter_invariant().relabel(spot.Abc).simplify()
for formula in f:
print(formula)
```
%% Output
0
Ga
F(a R !b)
G(a | Fb) | (FGb R !b)
G!b | G(a U !c)
b U a
0
0
%% Cell type:code id: tags:
``` python
for formula in spot.randltl(3, 10).simplify().unabbreviate("WMGFR"): print(formula)
```
%% Output
0
!(1 U !p1)
1 U ((p0 U ((p0 & p1) | !(1 U !p0))) | !(1 U !((1 U !p1) & (1 U p1))))
1 U (!p2 U ((p0 & !p2) | !(1 U p2)))
(!p1 U ((!p1 & (1 U !(1 U !p1))) | !(1 U p1))) | !(1 U !(p0 | (1 U p1)))
X(p2 & X(p2 U (!p0 | !(1 U !p2))))
(1 U p2) | (X(!p2 | !(1 U !p2)) U ((1 U p2) U (!p1 & (1 U p2))))
(1 U p2) | (X(!p2 | !(1 U !p2)) U (1 U (!p1 & (1 U p2))))
XX!(1 U !((X!p1 U (!p2 U (!p0 & !p2))) | X!(1 U !p0)))
XX(1 U (p1 U ((p0 & p1) | !(1 U !p1))))
p2 & Xp0
%% Cell type:code id: tags:
``` python
```
......
Supports Markdown
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