From d219e4a55644ae7be3689fdcfffddc71252e602a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 24 Nov 2017 16:57:15 +0100 Subject: [PATCH] tests: reduce the memory/time footprint of ltl2dstar.test * tests/core/ltl2dstar.test: Reduce the amount of tests performed on one formula that is problematic for ltl2dstar. --- tests/core/ltl2dstar.test | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/tests/core/ltl2dstar.test b/tests/core/ltl2dstar.test index d1a00d964..5a6272864 100755 --- a/tests/core/ltl2dstar.test +++ b/tests/core/ltl2dstar.test @@ -39,8 +39,7 @@ RAB=--automata=rabin STR=--automata=streett randltl -n 15 a b | ltlfilt --nnf --remove-wm | -ltlcross -F - -f 'GFa & GFb & GFc' -f '(GFa -> GFb) & (GFc -> GFd)' \ ---timeout=30 \ +ltlcross -F - -f 'GFa & GFb & GFc' --timeout=30 \ "ltl2tgba -s %f >%N" \ "ltl2dstar $RAB --output=nba --ltl2nba=spin:ltl2tgba@-s %L %T" \ "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" \ --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 # negative automaton. ltlcross -f 'GFa' --verbose \