neverclaimread.test 7.36 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, 2015 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
  rankdir=LR
137 138 139 140 141 142
  I [label="", style=invis, width=0]
  I -> 0
  0 [label="0", peripheries=2]
  0 -> 1 [label="p1"]
  1 [label="1", peripheries=2]
  1 -> 1 [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 --name=%F --dot=nsc <input >stdout 2>stderr && exit 1
326 327
cat >expected <<EOF
digraph G {
328
  rankdir=LR
329 330
  label="-"
  labelloc="t"
331
  node [shape="circle"]
332 333
  I [label="", style=invis, width=0]
  I -> 0
334
  subgraph cluster_0 {
335
  color=green
336
  label=""
337 338 339
  1 [label="1", peripheries=2]
  }
  subgraph cluster_1 {
340
  color=red
341
  label=""
342
  0 [label="0"]
343
  }
344 345 346
  0 -> 1 [label="b"]
  0 -> 0 [label="0"]
  1 -> 1 [label="1"]
347 348 349
}
EOF
diff stdout expected
350 351 352 353 354 355 356 357 358
# 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
359 360


361 362
cat >formulae<<EOF
a
363
FG a
364
X false
365
(G a) U X b
366
(a U b) U (c U d)
367
true
368 369 370
(Ga && XXXX!a)
"a > b" U "process@foo"
GF("(a + b) == 42" U "process@foo")
371 372 373
EOF
while read f
do
374 375 376 377 378 379 380 381 382 383
    run 0 ../../bin/ltl2tgba -H "!($f)" > f.hoa
    run 0 ../../bin/ltl2tgba -s -f "$f" > f.spot
    # 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
    # In case we cannot run spin or ltl2ba, use the spot output
    cp f.spot f.spin
    cp f.spot f.ltl2ba

384
    sf=`../../bin/ltlfilt -sf "$f"`
385

386
    if test -n "$SPIN"; then
387
        # Old spin versions cannot parse formulas such as ((a + b) == 42).
388
	$SPIN -f "$sf" > f.spin.tmp && mv f.spin.tmp f.spin
389
    fi
390 391 392 393 394 395 396
    case $f in
      *\"*);;
      *)
      if test -n "$LTL2BA"; then
	  $LTL2BA -f "$sf" > f.ltl2ba
      fi
    esac
397 398 399 400

    run 0 ../../bin/autfilt --count -v --intersect=f.hoa \
	                    f.spot f.spin f.ltl2ba >out
    test 3 = `cat out`
401
done  <formulae