ltl2tgba.test 6.5 KB
Newer Older
1
#!/bin/sh
2
# -*- coding: utf-8 -*-
3
# Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche et
4
# Développement de l'Epita (LRDE).
Guillaume Sadegh's avatar
Guillaume Sadegh committed
5
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
6
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
7
8
9
10
11
12
# et Marie Curie.
#
# 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
13
# the Free Software Foundation; either version 3 of the License, or
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
14
15
16
17
18
19
20
21
# (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
22
# along with this program.  If not, see <http://www.gnu.org/licenses/>.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
23

24
25
26
27
28

. ./defs

set -e

29
30
31
32
33
34
35
36
37
38
39
40
cat >check.txt <<\EOF
a
a U b
X a
a & b & c
a | b | (c U (d & (g U (h ^ i))))
Xa & (b U !a) & (b U !a)
Fa & Xb & GFc & Gd
Fa & Xa & GFc & Gc
Fc & X(a | Xb) & GF(a | Xb) & Gc
a R (b R c)
(a U b) U (c U d)
41

42
((Xp2)U(X(1)))&(p1 R(p2 R p0))
43

44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
{a*;c}<>->GFb
{((a*;b;c)*)&((b*;a;c)*)}<>->x
{(g;y;r)*}<>->x
G({(g;y;r)*}<>->x)
G({(a;b)*}<>->x)&G({(c;d)*}<>->y)
# try sub-braces
G({{a;b}*}[]->x)&G({{c;d}*}[]->y)
{([*0] + a):c*:([*0] + b)}<>->d
{a;e;f:(g*);h}<>->d
{(a:b)* & (c*:d)}<>->e
{(a:b)*}
G{(a:b)*}
{a;b}
{(a;b)*}
G{(a;b)*}
{a*}[]->{b*}
{a*}[]=>{b*}
{a*&b}
{a*&b*}
{((!c;b*) & d);e}
{(a* & (c;b*) & d);e}
{[*2];a[*2..4]}|->b
{a[*2..5] && b[*..3]}|->c
{{[+];a;[+]} && {[+];b;[+]}}<>->c
{(a[->3]) & {[+];b}}<>->c
69
70
# This formula (built by a random formula generator), exhibited an
# infinite recursion in the translation:
71
{(a|[*0])[*];1}
72
73
# Example from "Beyond Hardware Verification" by Glazberg, Moulin, Orni,
# Ruah, Zarpas (2007).
74
{[*];req;ack}|=>{start;busy[*];done}
75
76
# Examples from "Property-by-Example Guide: a Handbook of PSL Examples"
# by Ben David and Orni (2005)/
77
78
79
80
81
82
# - 2.27.A
{end[=3]}(false)
# - 3.5.A
{[*]; {read[=3]} && {write[=2]}} |=> {(!read && !write)[*]; ready}
# - 2.33  (abridged to fit in 80 cols)
{[*];st&&comp_d_en;!comp_d_en&&good_c;{st_v[->]}&&{stop[=0];true}}|->{!d_out}
83

84
85
# Some tricky cases that require the rational automaton to be pruned
# before it is used in the translation.
86
87
{{b[*];c} | {{a && !a}}[=2]}
{((a&!b);((!a&!b)*))&&(!b*;(!a&b))}
88
89
90
# When translating this formula, we expect the translator to ignore
# `a;(f&!f)[=2];c' on one side because it as already seen it on the
# other side.
91
{c;a;(f&!f)[=2];c}|{b;a;(!f&f)[=2];c}
92
93

# these were mis-translated in Spot 0.9
94
95
96
97
98
99
G!{(b;1)*;a}
(G!{(b;1)*;a} && ({1;1[*3]*}[]->{(b&!a)[*2];!b&!a}))
EOF

run 0 ../checkpsl check.txt

100
101
102
103
104
# In particular, Spot 0.9 would incorrectly reject the sequence:
# (a̅b;a̅b;a̅b̅);(a̅b;a̅b;a̅b̅);(a̅b;a̅b;a̅b̅);... in 'G!{(b;1)*;a}'
# This means the following automaton was incorrectly empty in Spot 0.9.
run 0 ../ltl2tgba -e -R3 '(G!{(b;1)*;a} && ({1;1[*3]*}[]->{(b&!a)[*2];!b&!a}))'

105
106
# Make sure 'a U (b U c)' has 3 states and 6 transitions,
# before and after degeneralization.
107
for opt in '' -DT -DS; do
108
  ../ltl2tgba -ks -f -R3 $opt 'a U (b U c)' > stdout
109
110
111
  grep 'transitions: 6$' stdout
  grep 'states: 3$' stdout
done
112
113
114

# Make sure '!(Ga U b)' has 3 states and 6 transitions,
# before and after degeneralization.
115
for opt in '' -DT -DS; do
116
117
  ../ltl2tgba -kt -f -R3 $opt '!(Ga U b)' > stdout
  grep 'sub trans.: 11$' stdout
118
119
120
121
122
123
  grep 'transitions: 6$' stdout
  grep 'states: 3$' stdout
done

# Make sure 'Ga U b' has 4 states and 6 transitions,
# before and after degeneralization.
124
for opt in '' -DT -DS; do
125
126
  ../ltl2tgba -kt -f -R3 $opt 'Ga U b' > stdout
  grep 'sub trans.: 12$' stdout
127
128
129
  grep 'transitions: 6$' stdout
  grep 'states: 4$' stdout
done
130
131
132
133

# Make sure '(G (p -> F q)) && ((X (p) U q) || ! X (p U (p && q)))'
# has 6 states and 15 transitions, before and after degeneralization.
f='(G (p -> F q)) && ((X (p) U q) || ! X (p U (p && q)))'
134
for opt in '' -DT -DS; do
135
  ../ltl2tgba -ks -f -R3 $opt "$f" > stdout
136
137
  grep 'transitions: 15$' stdout
  grep 'states: 6$' stdout
138
139
140
  ../ltl2tgba -ks -f -R3f $opt "$f" > stdout
  grep 'transitions: 15$' stdout
  grep 'states: 6$' stdout
141
done
142
143
144
145

# Make sure 'GFa & GFb & GFc & GFd & GFe & GFf'
# has 7 states and 34 transitions after degeneralization.
f='GFa & GFb & GFc & GFd & GFe & GFg'
146
../ltl2tgba -ks -DS -x -f "$f" > stdout
147
148
grep 'transitions: 34$' stdout
grep 'states: 7$' stdout
149
150
151
152
153
154
155
156
157

# Make sure 'Ga & XXXX!a' is minimized to one state.
f='Ga & XXXX!a'
../ltl2tgba -ks -f "$f" > stdout
grep 'transitions: 4$' stdout
grep 'states: 5$' stdout
../ltl2tgba -ks -Rm -f "$f" > stdout
grep 'transitions: 0$' stdout
grep 'states: 1$' stdout
158
159

# Make sure a monitor for F(a & F(b)) accepts everything.
160
run 0 ../ltl2tgba -M -f "F(a & F(b))" | grep ' ->' > stdout
161
162
163
164
165
cat >expected <<EOF
  0 -> 1
  1 -> 1 [label="1\n"]
EOF
cmp stdout expected
166
167
168
169
170
171
172
173
174
175

# This formula caused a segfault with Spot 0.7.
run 0 ../ltl2tgba -Rm -ks -f "Gq|Gr|(G(q|FGp)&G(r|FG!p))" >stdout
grep 'transitions: 5$' stdout
grep 'states: 3$' stdout

# Adding -R3 used to make it work...
run 0 ../ltl2tgba -R3 -Rm -ks -f "Gq|Gr|(G(q|FGp)&G(r|FG!p))" >stdout
grep 'transitions: 5$' stdout
grep 'states: 3$' stdout
176
177
178
179
180
181
182
183
184
185

# Make sure FGa|GFb has the same number of states/transitions when
# output as a never claim or are a degeneralized BA in Spot's textual
# format.  The option -R1q -R1t used to cause two degeneralizations to
# occur.
run 0 ../ltl2tgba -R1q -R1t -N 'FGa|FGb' > out.never
run 0 ../ltl2tgba -XN -kt out.never > count.never
run 0 ../ltl2tgba -R1q -R1t -DS -b 'FGa|FGb' > out.spot
run 0 ../ltl2tgba -X -kt out.spot > count.spot
cmp count.never count.spot
186
187
188
189
190

# The following automaton should have only 4 states.
run 0 ../ltl2tgba -R3 -ks -f '(p&XF!p)|(!p&XFp)|X(Fp&F!p)' >stdout
grep 'transitions: 7$' stdout
grep 'states: 4$' stdout
191
192
193
194
195

# A bug in the translation of !{xxx} when xxx reduces to false caused
# the following formula to be considered equivalent to anything...
../../bin/ltlfilt -f '!{[*2] && [*0..1]}' --equivalent-to 'false' && exit 1
../../bin/ltlfilt -f '!{[*2] && [*0..1]}' --equivalent-to 'true'
196
197
198
199
200
201
202
203

# Test some equivalences fixed in Spot 1.1.4
../../bin/ltlfilt    -f '{{a;b}[*]}'  --equivalent-to 'a & Xb'
../../bin/ltlfilt -r -f '{{a;b}[*]}'  --equivalent-to 'a & Xb'
../../bin/ltlfilt    -f '!{{a;b}[*]}' --equivalent-to '!a | X!b'
../../bin/ltlfilt -r -f '!{{a;b}[*]}' --equivalent-to '!a | X!b'
../../bin/ltlfilt    -f '{a[*];b[*]}' --equivalent-to 'a | b'
../../bin/ltlfilt -r -f '{a[*];b[*]}' --equivalent-to 'a | b'