From 062045eb45de675535777f812da7b0d6b0130b07 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 21 Jan 2010 14:54:36 +0100 Subject: [PATCH] Speedup reduc.test by not spawning one process per formula. * src/ltltest/reduc.cc: Add an option -f to read a lost of formulae from a file. Running a process for each formula was too slow. Also add an option -h to hide reduced formulae. * src/ltltest/reduc.test: Simplify accordingly. --- ChangeLog | 9 ++ src/ltltest/reduc.cc | 244 +++++++++++++++++++++++++++-------------- src/ltltest/reduc.test | 35 ++---- 3 files changed, 182 insertions(+), 106 deletions(-) diff --git a/ChangeLog b/ChangeLog index 708596954..45b806060 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,12 @@ +2010-01-21 Alexandre Duret-Lutz + + Speedup reduc.test by not spawning one process per formula. + + * src/ltltest/reduc.cc: Add an option -f to read a lost of + formulae from a file. Running a process for each formula was + too slow. Also add an option -h to hide reduced formulae. + * src/ltltest/reduc.test: Simplify accordingly. + 2010-01-21 Alexandre Duret-Lutz Move the last test from emptchk.test to emptchke.test. diff --git a/src/ltltest/reduc.cc b/src/ltltest/reduc.cc index b0cd20da9..f022f5af0 100644 --- a/src/ltltest/reduc.cc +++ b/src/ltltest/reduc.cc @@ -1,6 +1,8 @@ -// Copyright (C) 2004, 2006, 2007, 2008, 2009 Laboratoire -// d'Informatique de Paris 6 (LIP6), département Systèmes Répartis -// Coopératifs (SRC), Université Pierre et Marie Curie. +// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). +// Copyright (C) 2004, 2006, 2007 Laboratoire d'Informatique de Paris +// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -20,8 +22,11 @@ // 02111-1307, USA. #include +#include #include #include +#include +#include #include "ltlparse/public.hh" #include "ltlvisit/lunabbrev.hh" #include "ltlvisit/tunabbrev.hh" @@ -43,9 +48,28 @@ syntax(char* prog) int main(int argc, char** argv) { + bool readfile = false; + bool hidereduc = false; + unsigned long sum_before = 0; + unsigned long sum_after = 0; + if (argc < 3) syntax(argv[0]); + if (!strncmp(argv[1], "-f", 3)) + { + readfile = true; + ++argv; + --argc; + } + + if (!strncmp(argv[1], "-h", 3)) + { + hidereduc = true; + ++argv; + --argc; + } + int o = spot::ltl::Reduce_None; switch (atoi(argv[1])) { @@ -109,105 +133,159 @@ main(int argc, char** argv) return 2; } - spot::ltl::parse_error_list p1; - spot::ltl::formula* f1 = spot::ltl::parse(argv[2], p1); + spot::ltl::formula* f1 = 0; spot::ltl::formula* f2 = 0; - if (spot::ltl::format_parse_errors(std::cerr, argv[2], p1)) - return 2; + std::ifstream* fin = 0; + if (readfile) + { + fin = new std::ifstream(argv[2]); + if (!*fin) + { + std::cerr << "Cannot open " << argv[2] << std::endl; + exit(2); + } + } + + int exit_code = 0; + + next_line: + + if (fin) + { + std::string input; + do + { + if (!std::getline(*fin, input)) + goto end; + } + while (input == ""); + + spot::ltl::parse_error_list p1; + f1 = spot::ltl::parse(input, p1); + if (spot::ltl::format_parse_errors(std::cerr, input, p1)) + return 2; + } + else + { + spot::ltl::parse_error_list p1; + f1 = spot::ltl::parse(argv[2], p1); + if (spot::ltl::format_parse_errors(std::cerr, argv[2], p1)) + return 2; + } if (argc == 4) { + if (readfile) + { + std::cerr << "Cannot read from file and check result." << std::endl; + exit(2); + } + spot::ltl::parse_error_list p2; f2 = spot::ltl::parse(argv[3], p2); if (spot::ltl::format_parse_errors(std::cerr, argv[3], p2)) return 2; } - int exit_code = 0; - - spot::ltl::formula* ftmp1; - spot::ltl::formula* ftmp2; - - ftmp1 = f1; - f1 = unabbreviate_logic(f1); - ftmp2 = f1; - f1 = negative_normal_form(f1); - ftmp1->destroy(); - ftmp2->destroy(); - - - int length_f1_before = spot::ltl::length(f1); - std::string f1s_before = spot::ltl::to_string(f1); - - ftmp1 = f1; - f1 = spot::ltl::reduce(f1, o); - ftmp2 = f1; - f1 = spot::ltl::unabbreviate_logic(f1); - ftmp1->destroy(); - ftmp2->destroy(); - - int length_f1_after = spot::ltl::length(f1); - std::string f1s_after = spot::ltl::to_string(f1); - - bool red = (length_f1_after < length_f1_before); - std::string f2s = ""; - if (f2) - { - ftmp1 = f2; - f2 = unabbreviate_logic(f2); - ftmp2 = f2; - f2 = negative_normal_form(f2); - ftmp1->destroy(); - ftmp2->destroy(); - ftmp1 = f2; - f2 = unabbreviate_logic(f2); - ftmp1->destroy(); - f2s = spot::ltl::to_string(f2); - } - - if ((red | !red) && !f2) { - std::cout << length_f1_before << " " << length_f1_after - << " '" << f1s_before << "' reduce to '" << f1s_after << "'" - << std::endl; - } + spot::ltl::formula* ftmp1; + spot::ltl::formula* ftmp2; - if (f2) + ftmp1 = f1; + f1 = unabbreviate_logic(f1); + ftmp2 = f1; + f1 = negative_normal_form(f1); + ftmp1->destroy(); + ftmp2->destroy(); + + + int length_f1_before = spot::ltl::length(f1); + std::string f1s_before = spot::ltl::to_string(f1); + + ftmp1 = f1; + f1 = spot::ltl::reduce(f1, o); + ftmp2 = f1; + f1 = spot::ltl::unabbreviate_logic(f1); + ftmp1->destroy(); + ftmp2->destroy(); + + int length_f1_after = spot::ltl::length(f1); + std::string f1s_after = spot::ltl::to_string(f1); + + std::string f2s = ""; + if (f2) + { + ftmp1 = f2; + f2 = unabbreviate_logic(f2); + ftmp2 = f2; + f2 = negative_normal_form(f2); + ftmp1->destroy(); + ftmp2->destroy(); + ftmp1 = f2; + f2 = unabbreviate_logic(f2); + ftmp1->destroy(); + f2s = spot::ltl::to_string(f2); + } + + sum_before += length_f1_before; + sum_after += length_f1_after; + + // If -h is set, we want to print only formulae that have become larger. + if (!f2 && (!hidereduc || (length_f1_after > length_f1_before))) { - if (f1 != f2) - { - if (length_f1_after < length_f1_before) - std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after - << " KOREDUC " << std::endl; - else - std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after - << " KOIDEM " << std::endl; + std::cout << length_f1_before << " " << length_f1_after + << " '" << f1s_before << "' reduce to '" << f1s_after << "'" + << std::endl; + } + + if (f2) + { + if (f1 != f2) + { + if (length_f1_after < length_f1_before) + std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after + << " KOREDUC " << std::endl; + else + std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after + << " KOIDEM " << std::endl; + exit_code = 1; + } + else + { + if (f1s_before != f1s_after) + std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after + << " OKREDUC " << std::endl; + else + std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after + << " OKIDEM" << std::endl; + exit_code = 0; + } + } + else + { + if (length_f1_after > length_f1_before) exit_code = 1; - } - else - { - if (f1s_before != f1s_after) - std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after - << " OKREDUC " << std::endl; - else - std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after - << " OKIDEM" << std::endl; - exit_code = 0; - } - } - else + } + + f1->destroy(); + if (f2) + f2->destroy(); + + if (fin) + goto next_line; + } + end: + + if (fin) { - if (length_f1_after < length_f1_before) - exit_code = 0; + float before = sum_before; + float after = sum_after; + std::cout << "gain: " + << (1 - (after / before)) * 100 << "%" << std::endl; } - f1->destroy(); - if (f2) - f2->destroy(); - - assert(spot::ltl::atomic_prop::instance_count() == 0); assert(spot::ltl::unop::instance_count() == 0); assert(spot::ltl::binop::instance_count() == 0); diff --git a/src/ltltest/reduc.test b/src/ltltest/reduc.test index 14b9f2fee..db356eaee 100755 --- a/src/ltltest/reduc.test +++ b/src/ltltest/reduc.test @@ -1,7 +1,9 @@ #! /bin/sh -# Copyright (C) 2004, 2005, 2006, 2009 Laboratoire d'Informatique de -# Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -# Université Pierre et Marie Curie. +# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement de +# l'Epita (LRDE). +# Copyright (C) 2004, 2005, 2006 Laboratoire d'Informatique de Paris 6 +# (LIP6), département Systèmes Répartis Coopératifs (SRC), Université +# Pierre et Marie Curie. # # This file is part of Spot, a model checking library. # @@ -34,24 +36,11 @@ for i in 10 12 14 16 18 20; do run 0 ../randltl -u -s 100 -f $i a b c d e f -F 100 >> $FILE done -for opt in 0 1 2 3 7 8 9; do - rm -f result.data - - cat $FILE | - while read f; do - ../reduc $opt "$f" >> result.data - done - - test $? = 0 || exit 1 - - perl -ne 'BEGIN { $sum1 = 0; $sum2 = 0; } -/^(\d+)\s+(\d+)/; -$sum1 += $1; -$sum2 += $2; -END { print 100 - ($sum2 * 100 / $sum1); print "\n"; } -' < result.data - +for opt in 0 1 2 3 7; do + run 0 ../reduc -f -h $opt "$FILE" +done +# Running the above through valgrind is quite slow already. +# Don't use valgrind for the next reductions (even slower). +for opt in 8 9; do + ../reduc -f -h $opt "$FILE" done - -rm -f result.data -rm -f $FILE