neverclaimread.test 7.07 KB
Newer Older
Felix Abecassis's avatar
Felix Abecassis committed
1
#!/bin/sh
2
# -*- coding: utf-8 -*-
3
4
# Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche
# et Développement de l'Epita (LRDE).
Felix Abecassis's avatar
Felix Abecassis committed
5
6
7
8
9
#
# 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
10
# the Free Software Foundation; either version 3 of the License, or
Felix Abecassis's avatar
Felix Abecassis committed
11
12
13
14
15
16
17
18
# (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
19
# along with this program.  If not, see <http://www.gnu.org/licenses/>.
Felix Abecassis's avatar
Felix Abecassis committed
20
21
22
23
24
25
26
27
28
29
30
31
32
33


. ./defs

set -e

cat >input <<EOF
never {
T2_init:
if
:: (1) -> goto T2_init
:: (p1 && p0) -> goto T1
fi;
T1:
34
T1b: /* alias */
Felix Abecassis's avatar
Felix Abecassis committed
35
if
36
37
:: (p1 && (! p0)) -> goto alias2
:: !(p1) -> goto T1b
38
:: ! (p1) -> goto T2_init
Felix Abecassis's avatar
Felix Abecassis committed
39
fi;
40
alias1:
Felix Abecassis's avatar
Felix Abecassis committed
41
accept_all:
42
alias2:
Felix Abecassis's avatar
Felix Abecassis committed
43
44
45
46
skip
}
EOF

47
run 0 ../ltl2tgba -XN -H input > stdout
Felix Abecassis's avatar
Felix Abecassis committed
48
49

cat >expected <<EOF
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
HOA: v1
States: 3
Start: 0
AP: 2 "p0" "p1"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc
--BODY--
State: 0
[t] 0
[0&1] 1
State: 1
[!1] 0
[!1] 1
[!0&1] 2
State: 2 {0}
[t] 2
--END--
Felix Abecassis's avatar
Felix Abecassis committed
68
69
EOF

70
run 0 ../../bin/autfilt -F stdout --isomorph expected
Felix Abecassis's avatar
Felix Abecassis committed
71
72

rm input stdout expected
73
74


75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
# Same test, but with the newer syntax output since Spin 6.24
cat >input <<EOF
never {
T2_init:
do
:: (1) -> goto T2_init
:: (p1 && p0) -> goto T1
od;
T1:
do
:: atomic { (p1 && (! p0)) -> assert(!(p1 && (! p0))) }
:: !(p1) -> goto T1
:: ! (p1) -> goto T2_init
od;
}
EOF

92
run 0 ../ltl2tgba -XN -H input > stdout
93
94

cat >expected <<EOF
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
HOA: v1
States: 3
Start: 0
AP: 2 "p0" "p1"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc
--BODY--
State: 0
[t] 0
[0&1] 1
State: 1
[!1] 0
[!1] 1
[!0&1] 2
State: 2 {0}
[t] 2
--END--
113
114
EOF

115
run 0 ../../bin/autfilt -F stdout --isomorph expected
116
117
118
119

rm input stdout expected


120
121
122
123
124
# Unparenthesed disjunction
cat >input <<EOF
never { /* p0 || p1  */
accept_init:
        if
125
126
        :: (p1) && (p0) -> goto accept_all
        :: (p1) && !(p0) -> goto accept_all
127
128
129
130
131
132
133
134
135
        fi;
accept_all:
        skip
}
EOF
run 0 ../ltl2tgba -XN input > stdout

cat >expected <<EOF
digraph G {
136
137
  rankdir=LR
  0 [label="", style=invis, width=0]
138
  0 -> 1
139
  1 [label="0", peripheries=2]
140
  1 -> 2 [label="p1"]
141
  2 [label="1", peripheries=2]
142
  2 -> 2 [label="1"]
143
144
145
146
147
148
149
}
EOF

diff stdout expected

rm input stdout expected

150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
# Test broken guards in input
cat >input <<EOF
never {
T2_init:
if
:: (1) -> goto T2_init
:: (p1 && ) -> goto T1
fi;
T1:
if
:: (p1 && ! p0)) -> goto accept_all
:: (p1) -> goto T1
fi;
accept_all:
skip
}
EOF

168
169
170
171
172
173
# We used to catch the following error:
#   input:5.11: syntax error, unexpected closing parenthesis
#   input:5.8-9: missing right operand for "and operator"
# but since the guard parser is more lenient, we just assume
# that "p1 && " is an atomic property.

174
run 2 ../ltl2tgba -XN input > stdout 2>stderr
175
cat >expected <<\EOF
176
input:9.16: syntax error, unexpected ')', expecting fi or ':'
177
EOF
178
grep input: stderr > stderrfilt
179
180
diff stderrfilt expected

181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214

# This output from MoDeLLa was not property parsed by Spot because of
# the missing parentheses around p0.  Report from František Blahoudek.
cat >input <<EOF
never{
T0_init:
	if
	:: true -> goto T1
	:: p0 -> goto T2
	fi;
T1:
	if
	:: true -> goto T1
	:: p0 -> goto accept_T3
	fi;
T2:
	if
	:: p0 -> goto accept_T3
	fi;
accept_T3:
	if
	:: p0 -> goto T2
	fi;
}
EOF
cat >expected<<EOF
transitions: 6
states: 4
EOF

run 0 ../ltl2tgba -ks -XN input > output
diff output expected


215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
# Test duplicated labels.  The following neverclaim was produced by
# ltl2ba 1.1 for '[](<>[]p1 U X[]<>Xp0)', but is rejected by Spin
# because of a duplicate label (accept_S10).  We should
# complain as well.  This was reported by Joachim Klein.

cat >input <<\EOF
never { /* [](<>[]p1 U X[]<>Xp0) */
T0_init:
	if
	:: (1) -> goto accept_S2
	:: (1) -> goto T1_S3
	:: (p1) -> goto T2_S4
	fi;
accept_S2:
	if
	:: (1) -> goto accept_S39
	:: (1) -> goto T1_S24
	:: (p1) -> goto accept_S10
	fi;
accept_S39:
	if
	:: (p0) -> goto accept_S39
	:: (1) -> goto T0_S39
	:: (1) -> goto T0_S24
	:: (p1) -> goto T0_S10
	fi;
T0_S39:
	if
	:: (p0) -> goto accept_S39
	:: (1) -> goto T0_S39
	:: (1) -> goto T0_S24
	:: (p1) -> goto T0_S10
	fi;
T0_S24:
	if
	:: (1) -> goto T0_S24
	:: (p1) -> goto T0_S10
	fi;
T0_S10:
	if
	:: (p0 && p1) -> goto accept_S10
	:: (p1) -> goto T0_S10
	fi;
accept_S10:
	if
	:: (p0 && p1) -> goto accept_S10
	:: (p1) -> goto T0_S10
	fi;
T1_S24:
	if
	:: (1) -> goto T1_S24
	:: (p1) -> goto accept_S10
	fi;
accept_S10:
	if
	:: (p1) -> goto accept_S10
	fi;
T1_S3:
	if
	:: (1) -> goto T1_S3
	:: (1) -> goto T1_S24
	:: (p1) -> goto T2_S4
	:: (p1) -> goto accept_S10
	fi;
T2_S4:
	if
	:: (p1) -> goto T2_S4
	:: (p1) -> goto accept_S10
	fi;
}
EOF

run 2 ../ltl2tgba -ks -XN input > stdout 2>stderr
cat stderr
cat >expected-err <<\EOF
input:48.1-10: redefinition of accept_S10...
input:38.1-10: ... accept_S10 previously defined here
EOF
grep input: stderr > stderrfilt
diff stderrfilt expected-err

296
# DOS-style new lines should have the same output.
297
perl -pi -e 's/$/\r/' input
298
299
300
301
302
run 2 ../ltl2tgba -ks -XN input > stdout 2>stderr
cat stderr
grep input: stderr > stderrfilt
diff stderrfilt expected-err

303
304
305
306
307
308
309
310
311
312
313
314

# Empty guards should be diagnosed at the correct location
cat >input <<EOF
never { /* a U b */
T0_init:
  if
  :: ((b)) -> goto accept_all
  :: ( ) -> goto T0_init
  fi;
accept_all:
  skip
}
315
316
317
318
319
320
321
322
323
never { /* a U b */
T0_init:
  if
  :: ((b)) -> goto accept_all
  :: ((b) -> goto T0_init
  fi;
accept_all:
  skip
}
324
EOF
325
../../bin/autfilt --dot <input >stdout 2>stderr && exit 1
326
327
cat >expected <<EOF
digraph G {
328
329
  rankdir=LR
  0 [label="", style=invis, width=0]
330
331
332
333
334
  0 -> 1
  1 [label="0"]
  1 -> 2 [label="b"]
  1 -> 1 [label="0"]
  2 [label="1", peripheries=2]
335
  2 -> 2 [label="1"]
336
337
338
}
EOF
diff stdout expected
339
340
341
342
343
344
345
346
347
# FIXME: the "ignoring trailing garbage" is unwanted
cat >expected.err <<EOF
5.6-8: unexpected empty block
5.6-8: ignoring trailing garbage
14.6-19.1: missing closing parenthese
19.1: syntax error, unexpected end of file, expecting fi or ':'
autfilt: failed to read automaton from -
EOF
diff stderr expected.err
348
349


350
351
cat >formulae<<EOF
a
352
FG a
353
X false
354
(G a) U X b
355
(a U b) U (c U d)
356
true
357
358
359
(Ga && XXXX!a)
"a > b" U "process@foo"
GF("(a + b) == 42" U "process@foo")
360
361
362
363
EOF
while read f
do
    run 0 ../ltl2tgba -b -f "!($f)" > f.tgba
364
    sf=`../../bin/ltlfilt -sf "$f"`
365
    if test -n "$SPIN"; then
366
367
368
369
        # Old spin versions cannot parse formulas such as ((a + b) == 42).
	if $SPIN -f "$sf" > f.spin; then
	  run 0 ../ltl2tgba -E -Pf.tgba -XN f.spin
        fi
370
    fi
371
372
373
374
375
376
377
378
    case $f in
      *\"*);;
      *)
      if test -n "$LTL2BA"; then
	  $LTL2BA -f "$sf" > f.ltl2ba
	  run 0 ../ltl2tgba -E -Pf.tgba -XN f.ltl2ba
      fi
    esac
379
    run 0 ../ltl2tgba -DS -NN -f "$f" > f.spot
380
381
382
383
    # Make sure there is no `!x' occurring in the
    # output.  Because `x' is usually #define'd, we
    # should use `!(x)' in guards.
    grep '![^(].*->' f.spot && exit 1
384
    run 0 ../ltl2tgba -E -Pf.tgba -XN f.spot
385
done  <formulae