alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* src/ltltest/equals.cc (main): Add option -E.

Browse source 
* src/ltltest/parseerr.test: Use `equals -E' instead of `readltl'
to check the parsing of erroneous strings without being sensible
to the ordering for formulae in memory.
This commit is contained in:
Alexandre Duret-Lutz 2004-11-28 20:17:06 +00:00
parent 896dc5afec
commit 13870bbaab
3 changed files with 28 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

28
src/ltltest/parseerr.test
View file

@ -52,25 +52,21 @@ check '+' ''
check '/2/3/4/5 a + b /6/7/8/' ''
# leading and trailing garbage are skipped
check 'a U b c' 'binop(U, AP(a), AP(b))'
check 'a &&& b' 'multop(And, constant(0), AP(b))'
run 0 ./equals -E 'a U b c' 'a U b'
run 0 ./equals -E 'a &&& b' '0 && b'
# (check multop merging while we are at it)
check 'a & b & c & d e' 'multop(And, AP(a), AP(b), AP(c), AP(d))'
check 'a & (b | c) & d should work' \
'multop(And, AP(a), multop(Or, AP(b), AP(c)), AP(d))'
run 0 ./equals -E 'a & b & c & d e' 'a & b & c & d'
run 0 ./equals -E 'a & (b | c) & d should work' 'a & (b | c) & d'
# Binop recovery
check 'a U' 'constant(0)'
check 'a U b V c R' 'constant(0)'
run 0 ./equals -E 'a U' 0
run 0 ./equals -E 'a U b V c R' 0
# Recovery inside parentheses
check 'a U (b c) U e R (f g <=> h)' \
'binop(R, binop(U, binop(U, AP(a), constant(0)), AP(e)), constant(0))'
check 'a U ((c) U e) R (<=> f g)' \
'binop(R, binop(U, AP(a), binop(U, AP(c), AP(e))), constant(0))'
run 0 ./equals -E 'a U (b c) U e R (f g <=> h)' 'a U (0) U e R (0)'
run 0 ./equals -E 'a U ((c) U e) R (<=> f g)' 'a U ((c) U e) R (0)'
# Missing parentheses
check 'a & (a + b' 'multop(And, AP(a), multop(Or, AP(a), AP(b)))'
check 'a & (a + b c' 'multop(And, constant(0), AP(a))'
check 'a & (+' 'multop(And, constant(0), AP(a))'
check 'a & (' 'multop(And, constant(0), AP(a))'
run 0 ./equals -E 'a & (a + b' 'a & (a + b)'
run 0 ./equals -E 'a & (a + b c' 'a & (0)'
run 0 ./equals -E 'a & (+' 'a & (0)'
run 0 ./equals -E 'a & (' 'a & (0)'