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

tests: reduce the memory/time footprint of ltl2dstar.test

Browse source 
* tests/core/ltl2dstar.test: Reduce the amount of tests performed on
one formula that is problematic for ltl2dstar.
This commit is contained in:
Alexandre Duret-Lutz 2017-11-24 16:57:15 +01:00
parent a9a375ccd8
commit d219e4a556
1 changed files with 14 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

16
tests/core/ltl2dstar.test
View file

@ -39,8 +39,7 @@ RAB=--automata=rabin
STR=--automata=streett STR=--automata=streett
randltl -n 15 a b | ltlfilt --nnf --remove-wm | randltl -n 15 a b | ltlfilt --nnf --remove-wm |
ltlcross -F - -f 'GFa & GFb & GFc' -f '(GFa -> GFb) & (GFc -> GFd)' \ ltlcross -F - -f 'GFa & GFb & GFc' --timeout=30 \
--timeout=30 \
"ltl2tgba -s %f >%N" \ "ltl2tgba -s %f >%N" \
"ltl2dstar $RAB --output=nba --ltl2nba=spin:ltl2tgba@-s %L %T" \ "ltl2dstar $RAB --output=nba --ltl2nba=spin:ltl2tgba@-s %L %T" \
"ltl2dstar $RAB --ltl2nba=spin:ltl2tgba@-s %L %D" \ "ltl2dstar $RAB --ltl2nba=spin:ltl2tgba@-s %L %D" \
@ -50,6 +49,19 @@ ltlcross -F - -f 'GFa & GFb & GFc' -f '(GFa -> GFb) & (GFc -> GFd)' \
"ltl2dstar $STR --ltl2nba=spin:ltl2tgba@-s %L - | dstar2tgba --low -s >%N" \ "ltl2dstar $STR --ltl2nba=spin:ltl2tgba@-s %L - | dstar2tgba --low -s >%N" \
--csv=out.csv --csv=out.csv
# We used to include the following formula in the above test, but the
# --output=nba option of ltl2dstar is too memory-hungry on this
# formula, and this is causing issues in our builds. We also reduce
# the size of the products, as they would be too huge.
ltlcross -f '(GFa -> GFb) & (GFc -> GFd)' --verbose --states=100 --timeout=30 \
"ltl2tgba -s %f >%N" \
"ltl2dstar $RAB --output=nba --ltl2nba=spin:ltl2tgba@-s %L %T" \
"ltl2dstar $RAB --ltl2nba=spin:ltl2tgba@-s %L %D" \
"ltl2dstar $RAB --ltl2nba=spin:ltl2tgba@-s %L - | dstar2tgba --low -s >%N" \
"ltl2dstar $STR --ltl2nba=spin:ltl2tgba@-s %L %D" \
"ltl2dstar $STR --ltl2nba=spin:ltl2tgba@-s %L - | dstar2tgba --low -s >%N" \
--csv='>>out.csv'
# A bug in ltlcross <=1.2.5 caused it to not use the complement of the # A bug in ltlcross <=1.2.5 caused it to not use the complement of the
# negative automaton. # negative automaton.
ltlcross -f 'GFa' --verbose \ ltlcross -f 'GFa' --verbose \