ltlcross3.test 8.07 KB
Newer Older
1 2
#!/bin/sh
# -*- coding: utf-8 -*-
3
# Copyright (C) 2012, 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche
4
# et Développement de l'Epita (LRDE).
5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23
#
# 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
# the Free Software Foundation; either version 3 of the License, or
# (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
# along with this program.  If not, see <http://www.gnu.org/licenses/>.

. ./defs
set -e

24 25 26 27 28 29 30 31 32 33
check_csv()
{
  # Make sure all lines in $1 have the same number of comas
  sed 's/[^,]//g' < "$1" |
  ( read first
  while read l; do
    test "x$first" = "x$l" || exit 1
  done)
}

34
ltl2tgba=ltl2tgba
35

36 37 38 39
# Make sure ltlcross quotes formulas correctly
cat >formula <<\EOF
G"a'-'>'b"
EOF
40
run 0 ltlcross -F formula --csv=out.csv \
41 42 43
                         "$ltl2tgba -s %f >%N" \
                         "$ltl2tgba --lenient -s %s >%N"

44
run 2 ltlcross "$ltl2tgba -s %f >%N" 'foo bar' 2>stderr -f a
45
grep 'ltlcross.*no input.*in.*foo bar' stderr
46 47

# Make sure non-zero exit codes are reported...
48
run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \
49 50 51 52 53 54 55 56
                         -f a --csv=out.csv 2>stderr
grep '"exit_status"' out.csv
grep '"exit_code"' out.csv
test `grep 'error:.*returned exit code 1' stderr | wc -l` -eq 2
test `grep '"exit code",1' out.csv | wc -l` -eq 2
check_csv out.csv

# ... unless --omit-missing is supplied.
57
run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \
58 59 60 61 62 63 64
                         -f a --csv=out.csv --omit-missing 2>stderr
grep '"exit_status"' out.csv && exit 1
grep '"exit_code"' out.csv && exit 1
test `grep 'error:.*returned exit code 1' stderr | wc -l` -eq 2
test `grep '"exit code",1' out.csv | wc -l` -eq 0
check_csv out.csv

65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97
# Additional columns should not be an issue
run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \
               -f a --csv=out.csv --strength 2>stderr
grep '"exit_status"' out.csv
grep '"exit_code"' out.csv
grep '"nonacc_scc","terminal_scc","weak_scc","strong_scc"' out.csv
grep '"terminal_aut","weak_aut","strong_aut"' out.csv
grep -v '"ambiguous_aut"' out.csv
test `grep 'error:.*returned exit code 1' stderr | wc -l` -eq 2
test `grep '"exit code",1' out.csv | wc -l` -eq 2
check_csv out.csv

run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \
               -f a --csv=out.csv --ambiguous 2>stderr
grep '"exit_status"' out.csv
grep '"exit_code"' out.csv
grep '"ambiguous_aut"' out.csv
grep -v '"terminal_aut"' out.csv
test `grep 'error:.*returned exit code 1' stderr | wc -l` -eq 2
test `grep '"exit code",1' out.csv | wc -l` -eq 2
check_csv out.csv

run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \
               -f a --csv=out.csv --ambiguous --strength 2>stderr
grep '"exit_status"' out.csv
grep '"exit_code"' out.csv
grep '"nonacc_scc","terminal_scc","weak_scc","strong_scc"' out.csv
grep '"terminal_aut","weak_aut","strong_aut"' out.csv
grep '"ambiguous_aut"' out.csv
test `grep 'error:.*returned exit code 1' stderr | wc -l` -eq 2
test `grep '"exit code",1' out.csv | wc -l` -eq 2
check_csv out.csv

98
# Likewise for timeouts
99
echo foo >bug
100
run 0 ltlcross 'sleep 5; false %f >%N' 'false %f >%N' \
101
                         --timeout 2 -f a --csv=out.csv \
102
                         --ignore-execution-failures \
103
                         --save-bogus=bug 2>stderr
104 105 106
grep '"exit_status"' out.csv
grep '"exit_code"' out.csv
test `grep 'warning:.*timeout' stderr | wc -l` -eq 2
107
test `grep 'warning:.*exit code 1' stderr | wc -l` -eq 2
108
test `grep '"timeout",-1' out.csv | wc -l` -eq 2
109
test `grep '"exit code",1' out.csv | wc -l` -eq 2
110 111 112 113

grep 'No major problem detected' stderr
grep '2 timeouts occurred' stderr
grep '2 non-zero exit statuses were ignored' stderr
114
check_csv out.csv
115 116 117
# 'bug' should exist but be empty
test -f bug
test -s bug && exit 1
118

119
run 0 ltlcross 'sleep 5; false %f >%N' \
120 121 122 123 124 125
                         --timeout 2 --omit-missing -f a --csv=out.csv 2>stderr
grep '"exit_status"' out.csv && exit 1
grep '"exit_code"' out.csv && exit 1
test `grep 'warning:.*timeout' stderr | wc -l` -eq 2
test `wc -l < out.csv` -eq 1
check_csv out.csv
126

127 128 129 130 131 132 133 134 135 136 137 138 139 140
run 1 ltlcross 'sleep 5; false %f >%N' --fail-on-timeout \
                  --timeout 2 -f a --csv=out.csv 2>stderr
test `grep 'error:.*timeout' stderr | wc -l` -eq 2
test `wc -l < out.csv` -eq 3
check_csv out.csv

run 1 ltlcross 'sleep 5; false %f >%N' --fail-on-timeout \
    --stop-on-error --timeout 2 -f a -f b --csv=out.csv \
    --save-bogus=bogous 2>stderr
test `grep 'error:.*timeout' stderr | wc -l` -eq 2
test `wc -l < out.csv` -eq 3
test `wc -l < bogous` -eq 1
check_csv out.csv

141
# Check with --products=5 --automata
142
run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \
143
      -f a --csv=out.csv --products=5 --automata 2>stderr
144 145 146 147 148
p=`sed 's/[^,]//g;q' out.csv | wc -c`
grep '"exit_status"' out.csv
grep '"exit_code"' out.csv
test `grep 'error:.*returned exit code 1' stderr | wc -l` -eq 2
test `grep '"exit code",1' out.csv | wc -l` -eq 2
149
test `grep '"HOA:.*--BODY--.*--END--"' out.csv | wc -l` -eq 2
150 151 152
check_csv out.csv

# ... unless --omit-missing is supplied.
153
run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \
154 155 156 157 158 159 160 161 162
      -f a --csv=out.csv --omit-missing --products=5  2>stderr
grep '"exit_status"' out.csv && exit 1
grep '"exit_code"' out.csv && exit 1
test `grep 'error:.*returned exit code 1' stderr | wc -l` -eq 2
test `grep '"exit code",1' out.csv | wc -l` -eq 0
check_csv out.csv


# Check with --products=+5
163
run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \
164
      -f a --csv=out.csv --products=+5 --automata 2>stderr
165 166 167 168 169
q=`sed 's/[^,]//g;q' out.csv | wc -c`
grep '"exit_status"' out.csv
grep '"exit_code"' out.csv
test `grep 'error:.*returned exit code 1' stderr | wc -l` -eq 2
test `grep '"exit code",1' out.csv | wc -l` -eq 2
170
test `grep '"HOA:.*--BODY--.*--END--"' out.csv | wc -l` -eq 2
171 172 173
check_csv out.csv

# ... unless --omit-missing is supplied.
174
run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \
175 176 177 178 179 180 181 182
      -f a --csv=out.csv --omit-missing --products=+5  2>stderr
grep '"exit_status"' out.csv && exit 1
grep '"exit_code"' out.csv && exit 1
test `grep 'error:.*returned exit code 1' stderr | wc -l` -eq 2
test `grep '"exit code",1' out.csv | wc -l` -eq 0
check_csv out.csv

test $q -eq `expr $p + 12`
183 184 185


# Check with Rabin/Streett output
186 187
first="should not be erased"
echo "$first" > bug.txt
188
run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%D' \
189
      -f 'X  a' --csv=out.csv --save-bogus='>>bug.txt' 2>stderr
190
q=`sed 's/[^,]//g;q' out.csv | wc -c`
191
test $q -eq `expr $p - 1`
192 193 194 195 196
grep '"exit_status"' out.csv
grep '"exit_code"' out.csv
test `grep 'error:.*returned exit code 1' stderr | wc -l` -eq 2
test `grep '"exit code",1' out.csv | wc -l` -eq 2
check_csv out.csv
197
grep 'X  a' bug.txt
198
test "`head -n 1 bug.txt`" = "$first"
199 200 201


# Support for --ABORT-- in HOA.
202
run 1 ltlcross 'echo HOA: --ABORT-- %f > %H' \
203 204 205 206 207
   -f a --csv=out.csv 2>stderr
grep '"exit_status"' out.csv
grep '"exit_code"' out.csv
test `grep 'error:.*aborted' stderr | wc -l` -eq 2
test `grep '"aborted",-1' out.csv | wc -l` -eq 2
208 209 210 211
test 3 = `wc -l < out.csv`
check_csv out.csv

# The header of CSV file is not output in append mode
212
run 1 ltlcross 'echo HOA: --ABORT-- %f > %H' \
213 214 215 216 217 218
   -f a --csv='>>out.csv' 2>stderr
grep '"exit_status"' out.csv
grep '"exit_code"' out.csv
test `grep 'error:.*aborted' stderr | wc -l` -eq 2
test `grep '"aborted",-1' out.csv | wc -l` -eq 4
test 5 = `wc -l < out.csv`
219
check_csv out.csv
220 221


222
# Diagnose empty automata, and make sure %% is correctly replaced by %
223
run 1 ltlcross ': %f >%O; echo %%>foo' -f a 2>stderr
224
test 2 = `grep -c ':.*empty input' stderr`
225 226 227 228 229
cat foo
cat >expected<<EOF
%
EOF
diff foo expected
230 231 232 233


# This command used to crash.  Report from František Blahoudek.
run 0 ltlcross --verbose --no-checks -f 'FGa' 'ltl2tgba'
234 235 236 237 238

# The CSV file should not talk about product if --products=0
ltlcross --products=0 ltl2tgba -f GFa -f FGa --csv=out.csv
grep product out.csv && exit 1
check_csv out.csv