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

autcross: exercise %S, %L, and {name{nest}}

Browse source 
* tests/core/autcross.test, tests/core/autcross2.test: More tests.
This commit is contained in:
Alexandre Duret-Lutz 2018-05-21 15:17:18 +02:00
parent 3334a6a679
commit 6e8af75ee9
2 changed files with 11 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

13
tests/core/autcross.test
View file

@ -1,7 +1,7 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2017 Laboratoire de Recherche et Développement de # Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement
# l'Epita (LRDE). # de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
# #
@ -24,17 +24,20 @@ set -e
# Skip this test if ltl2dstar is not installed. # Skip this test if ltl2dstar is not installed.
(ltl2dstar --version) || exit 77 (ltl2dstar --version) || exit 77
# The {autfilt {complement}} name makes sure we can nest braces.
randaut -n10 2 | randaut -n10 2 |
autcross 'ltl2dstar --complement-input=yes' 'autfilt --complement' \ autcross 'ltl2dstar --complement-input=yes' \
'{autfilt {complement}} autfilt --complement' \
--csv=out.csv 2>stderr --csv=out.csv 2>stderr
# 5 lines per input automaton, and 1 "No problem detected" line. # 5 lines per input automaton, and 1 "No problem detected" line.
test 51 = `wc -l < stderr` test 51 = `wc -l < stderr`
grep -q 'sanity check' stderr grep -q 'sanity check' stderr
# --no-check still allows to build a CSV # --no-check still allows to build a CSV. Exercise %S.
randaut -n10 2 | randaut -n10 2 |
autcross 'ltl2dstar --complement-input=yes' 'autfilt --complement' \ autcross 'ltl2dstar --complement-input=yes' \
'{autfilt {complement}} autfilt --complement %S>%O' \
--csv=out2.csv --no-check 2>stderr --csv=out2.csv --no-check 2>stderr
test 51 = `wc -l < stderr` test 51 = `wc -l < stderr`
grep -q 'sanity check' stderr && exit 1 grep -q 'sanity check' stderr && exit 1

5
tests/core/autcross2.test
View file

@ -1,6 +1,6 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2017 Laboratoire de Recherche et Développement de # Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement de
# l'Epita (LRDE). # l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -21,8 +21,9 @@
. ./defs . ./defs
set -e set -e
# Exercise %L while we are at it.
randaut -n10 2 | tee input | randaut -n10 2 | tee input |
autcross --language-preserve 'autfilt' 'autfilt --complement' \ autcross --language-preserve 'autfilt %L>%O' 'autfilt --complement' \
--save-bogus=bogus.hoa 2>stderr && exit 1 --save-bogus=bogus.hoa 2>stderr && exit 1
cat stderr cat stderr
# We should have 4 counterexample per input automaton # We should have 4 counterexample per input automaton