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.
This commit is contained in:
Alexandre Duret-Lutz
parent
7262dff0d9
commit
062045eb45
3 changed files with 182 additions and 106 deletions
|
|
@ -1,3 +1,12 @@
|
||||||
|
2010-01-21 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
||||||
|
|
||||||
|
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 <adl@lrde.epita.fr>
|
2010-01-21 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
||||||
|
|
||||||
Move the last test from emptchk.test to emptchke.test.
|
Move the last test from emptchk.test to emptchke.test.
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,8 @@
|
||||||
// Copyright (C) 2004, 2006, 2007, 2008, 2009 Laboratoire
|
// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et Développement
|
||||||
// d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
|
// de l'Epita (LRDE).
|
||||||
// Coopératifs (SRC), Université Pierre et Marie Curie.
|
// 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.
|
// This file is part of Spot, a model checking library.
|
||||||
//
|
//
|
||||||
|
|
@ -20,8 +22,11 @@
|
||||||
// 02111-1307, USA.
|
// 02111-1307, USA.
|
||||||
|
|
||||||
#include <iostream>
|
#include <iostream>
|
||||||
|
#include <fstream>
|
||||||
#include <cassert>
|
#include <cassert>
|
||||||
#include <cstdlib>
|
#include <cstdlib>
|
||||||
|
#include <string>
|
||||||
|
#include <cstring>
|
||||||
#include "ltlparse/public.hh"
|
#include "ltlparse/public.hh"
|
||||||
#include "ltlvisit/lunabbrev.hh"
|
#include "ltlvisit/lunabbrev.hh"
|
||||||
#include "ltlvisit/tunabbrev.hh"
|
#include "ltlvisit/tunabbrev.hh"
|
||||||
|
|
@ -43,9 +48,28 @@ syntax(char* prog)
|
||||||
int
|
int
|
||||||
main(int argc, char** argv)
|
main(int argc, char** argv)
|
||||||
{
|
{
|
||||||
|
bool readfile = false;
|
||||||
|
bool hidereduc = false;
|
||||||
|
unsigned long sum_before = 0;
|
||||||
|
unsigned long sum_after = 0;
|
||||||
|
|
||||||
if (argc < 3)
|
if (argc < 3)
|
||||||
syntax(argv[0]);
|
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;
|
int o = spot::ltl::Reduce_None;
|
||||||
switch (atoi(argv[1]))
|
switch (atoi(argv[1]))
|
||||||
{
|
{
|
||||||
|
|
@ -109,105 +133,159 @@ main(int argc, char** argv)
|
||||||
return 2;
|
return 2;
|
||||||
}
|
}
|
||||||
|
|
||||||
spot::ltl::parse_error_list p1;
|
spot::ltl::formula* f1 = 0;
|
||||||
spot::ltl::formula* f1 = spot::ltl::parse(argv[2], p1);
|
|
||||||
spot::ltl::formula* f2 = 0;
|
spot::ltl::formula* f2 = 0;
|
||||||
|
|
||||||
if (spot::ltl::format_parse_errors(std::cerr, argv[2], p1))
|
std::ifstream* fin = 0;
|
||||||
return 2;
|
|
||||||
|
|
||||||
|
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 (argc == 4)
|
||||||
{
|
{
|
||||||
|
if (readfile)
|
||||||
|
{
|
||||||
|
std::cerr << "Cannot read from file and check result." << std::endl;
|
||||||
|
exit(2);
|
||||||
|
}
|
||||||
|
|
||||||
spot::ltl::parse_error_list p2;
|
spot::ltl::parse_error_list p2;
|
||||||
f2 = spot::ltl::parse(argv[3], p2);
|
f2 = spot::ltl::parse(argv[3], p2);
|
||||||
if (spot::ltl::format_parse_errors(std::cerr, argv[3], p2))
|
if (spot::ltl::format_parse_errors(std::cerr, argv[3], p2))
|
||||||
return 2;
|
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
|
spot::ltl::formula* ftmp1;
|
||||||
<< " '" << f1s_before << "' reduce to '" << f1s_after << "'"
|
spot::ltl::formula* ftmp2;
|
||||||
<< std::endl;
|
|
||||||
}
|
|
||||||
|
|
||||||
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)
|
std::cout << length_f1_before << " " << length_f1_after
|
||||||
{
|
<< " '" << f1s_before << "' reduce to '" << f1s_after << "'"
|
||||||
if (length_f1_after < length_f1_before)
|
<< std::endl;
|
||||||
std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after
|
}
|
||||||
<< " KOREDUC " << std::endl;
|
|
||||||
else
|
if (f2)
|
||||||
std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after
|
{
|
||||||
<< " KOIDEM " << std::endl;
|
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;
|
exit_code = 1;
|
||||||
}
|
}
|
||||||
else
|
|
||||||
{
|
f1->destroy();
|
||||||
if (f1s_before != f1s_after)
|
if (f2)
|
||||||
std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after
|
f2->destroy();
|
||||||
<< " OKREDUC " << std::endl;
|
|
||||||
else
|
if (fin)
|
||||||
std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after
|
goto next_line;
|
||||||
<< " OKIDEM" << std::endl;
|
}
|
||||||
exit_code = 0;
|
end:
|
||||||
}
|
|
||||||
}
|
if (fin)
|
||||||
else
|
|
||||||
{
|
{
|
||||||
if (length_f1_after < length_f1_before)
|
float before = sum_before;
|
||||||
exit_code = 0;
|
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::atomic_prop::instance_count() == 0);
|
||||||
assert(spot::ltl::unop::instance_count() == 0);
|
assert(spot::ltl::unop::instance_count() == 0);
|
||||||
assert(spot::ltl::binop::instance_count() == 0);
|
assert(spot::ltl::binop::instance_count() == 0);
|
||||||
|
|
|
||||||
|
|
@ -1,7 +1,9 @@
|
||||||
#! /bin/sh
|
#! /bin/sh
|
||||||
# Copyright (C) 2004, 2005, 2006, 2009 Laboratoire d'Informatique de
|
# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement de
|
||||||
# Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
# l'Epita (LRDE).
|
||||||
# Université Pierre et Marie Curie.
|
# 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.
|
# 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
|
run 0 ../randltl -u -s 100 -f $i a b c d e f -F 100 >> $FILE
|
||||||
done
|
done
|
||||||
|
|
||||||
for opt in 0 1 2 3 7 8 9; do
|
for opt in 0 1 2 3 7; do
|
||||||
rm -f result.data
|
run 0 ../reduc -f -h $opt "$FILE"
|
||||||
|
done
|
||||||
cat $FILE |
|
# Running the above through valgrind is quite slow already.
|
||||||
while read f; do
|
# Don't use valgrind for the next reductions (even slower).
|
||||||
../reduc $opt "$f" >> result.data
|
for opt in 8 9; do
|
||||||
done
|
../reduc -f -h $opt "$FILE"
|
||||||
|
|
||||||
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
|
|
||||||
|
|
||||||
done
|
done
|
||||||
|
|
||||||
rm -f result.data
|
|
||||||
rm -f $FILE
|
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue