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

* src/misc/timer.hh, src/misc/timer.cc: New files.

Browse source 
* src/misc/Makefile.am (misc_HEADERS, libmisc_la_SOURCES): Add them.
* src/tgbatest/randtgba.cc: Use time_map to measure the algorithms.
Add the -R option.
* src/sanity/style.sh: Let me use `for (.*;;)'.
This commit is contained in:
Alexandre Duret-Lutz 2004-11-29 16:50:49 +00:00
parent 0531dfe6e5
commit 668666d246
6 changed files with 407 additions and 66 deletions
Download patch file Download diff file Expand all files Collapse all files

8
ChangeLog
View file

@ -1,3 +1,11 @@
2004-11-29 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/misc/timer.hh, src/misc/timer.cc: New files.
* src/misc/Makefile.am (misc_HEADERS, libmisc_la_SOURCES): Add them.
* src/tgbatest/randtgba.cc: Use time_map to measure the algorithms.
Add the -R option.
* src/sanity/style.sh: Let me use `for (.*;;)'.
2004-11-29 Denis Poitrenaud <Denis.Poitrenaud@lip6.fr>
* src/tgbaalgos/tau03opt.cc: Add a first version of the computation of

2
src/misc/Makefile.am
View file

@ -35,6 +35,7 @@ misc_HEADERS = \
minato.hh \
modgray.hh \
random.hh \
timer.hh \
version.hh
noinst_LTLIBRARIES = libmisc.la
@ -46,4 +47,5 @@ libmisc_la_SOURCES = \
minato.cc \
modgray.cc \
random.cc \
timer.cc \
version.cc

84
src/misc/timer.cc Normal file
View file

@ -0,0 +1,84 @@
// Copyright (C) 2004 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.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#include "timer.hh"
#include <iostream>
#include <iomanip>
namespace spot
{
std::ostream&
timer_map::print(std::ostream& os) const
{
time_info total;
for (tm_type::const_iterator i = tm.begin(); i != tm.end(); ++i)
{
total.utime += i->second.first.utime();
total.stime += i->second.first.stime();
}
clock_t grand_total = total.utime + total.stime;
os << std::setw(33) << ""
<< "| user time | sys. time | total |"
<< std::endl
<< std::setw(33) << "name "
<< "| ticks % | tics % | tics % | n"
<< std::endl
<< std::setw(79) << std::setfill('-') << "" << std::setfill(' ')
<< std::endl;
for (tm_type::const_iterator i = tm.begin(); i != tm.end(); ++i)
{
const spot::timer& t = i->second.first;
os << std::setw(32) << i->first << " |"
<< std::setw(6) << t.utime()
<< std::setw(5) << (total.utime ?
100.0 * t.utime() / total.utime : 0)
<< " |"
<< std::setw(6) << t.stime()
<< std::setw(5) << (total.stime ?
100.0 * t.stime() / total.stime : 0)
<< " |"
<< std::setw(6) << t.utime() + t.stime()
<< std::setw(5) << (grand_total ?
(100.0 * (t.utime() + t.stime()) /
grand_total) : 0)
<< " |"
<< std::setw(4) << i->second.second
<< std::endl;
}
os << std::setw(79) << std::setfill('-') << "" << std::setfill(' ')
<< std::endl
<< std::setw(32) << "TOTAL" << " |"
<< std::setw(6) << total.utime
<< std::setw(5) << 100
<< " |"
<< std::setw(6) << total.stime
<< std::setw(5) << 100
<< " |"
<< std::setw(6) << grand_total
<< std::setw(5) << 100
<< " |"
<< std::endl;
return os;
}
}

183
src/misc/timer.hh Normal file
View file

@ -0,0 +1,183 @@
// Copyright (C) 2004 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.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#ifndef SPOT_MISC_TIMER_HH
# define SPOT_MISC_TIMER_HH
# include <iosfwd>
# include <string>
# include <map>
# include <sys/times.h>
namespace spot
{
/// \addtogroup misc_tools
/// @{
/// A structure to record elapsed time in clock ticks.
struct time_info
{
time_info()
: utime(), stime(0)
{
}
clock_t utime;
clock_t stime;
};
/// A timekeeper that accumulate interval of time.
class timer
{
public:
/// Start a time interval.
void
start()
{
struct tms tmp;
times(&tmp);
start_.utime = tmp.tms_utime;
start_.stime = tmp.tms_stime;
}
/// Stop a time interval and update the sum of all intervals.
void
stop()
{
struct tms tmp;
times(&tmp);
total_.utime += tmp.tms_utime - start_.utime;
total_.stime += tmp.tms_stime - start_.stime;
}
/// \brief Return the user time of all accumulated interval.
///
/// Any time interval that has been start()ed but not stop()ed
/// will not be accounted for.
clock_t
utime() const
{
return total_.utime;
}
/// \brief Return the system time of all accumulated interval.
///
/// Any time interval that has been start()ed but not stop()ed
/// will not be accounted for.
clock_t
stime() const
{
return total_.stime;
}
protected:
time_info start_;
time_info total_;
};
/// \brief A map of timer, where each timer has a name.
///
/// Timer_map also keeps track of the number of measures each timer
/// has performed.
class timer_map
{
public:
/// \brief Start a timer with name \a name.
///
/// The timer is created if it did not exist already.
/// Once started, a timer should be either stop()ed or
/// cancel()ed.
void
start(const std::string& name)
{
item_type& it = tm[name];
it.first.start();
++it.second;
}
/// \brief Stop timer \a name.
///
/// The timer must have been previously started with start().
void
stop(const std::string& name)
{
tm[name].first.stop();
}
/// \brief Cancel timer \a name.
///
/// The timer must have been previously started with start().
///
/// This cancel only the current measure. (Previous measures
/// recorded by the timer are preserved.) When a timer that has
/// not done any measure is canceled, it is removed from the map.
void
cancel(const std::string& name)
{
tm_type::iterator i = tm.find(name);
assert(i != tm.end());
assert(0 < i->second.second);
if (0 == --i->second.second)
tm.erase(i);
}
/// Return the timer \a name.
const spot::timer&
timer(const std::string& name) const
{
tm_type::const_iterator i = tm.find(name);
assert(i != tm.end());
return i->second.first;
}
/// Return the timer \a name.
spot::timer&
timer(const std::string& name)
{
return tm[name].first;
}
/// \brief Whether there is no timer in the map.
///
/// If empty() return true, then either no timer where ever
/// started, or all started timers were canceled without
/// completing any measure.
bool
empty() const
{
return tm.empty();
}
/// Format information about all timers in a table.
std::ostream&
print(std::ostream& os) const;
protected:
typedef std::pair<spot::timer, int> item_type;
typedef std::map<std::string, item_type> tm_type;
tm_type tm;
};
/// @}
}
#endif // SPOT_MISC_ESCAPE_HH

2
src/sanity/style.test
View file

@ -110,7 +110,7 @@ for dir in "${INCDIR-..}" "${INCDIR-..}"/../iface; do
grep '[ ];' $tmp &&
diag 'No space before semicolon.'
grep -v 'for (;;)' $tmp | grep ';[^ ")]' &&
grep -v 'for (.*;;)' $tmp | grep ';[^ ")]' &&
diag 'Must have space or newline after semicolon.'
grep '}.*}' $tmp &&

194
src/tgbatest/randtgba.cc
View file

@ -33,6 +33,7 @@
#include "tgbaalgos/dotty.hh"
#include "misc/random.hh"
#include "tgba/tgbatba.hh"
#include "misc/timer.hh"
#include "tgbaalgos/emptiness.hh"
#include "tgbaalgos/emptiness_stats.hh"
@ -45,6 +46,65 @@
#include "tgbaalgos/tau03opt.hh"
#include "tgbaalgos/replayrun.hh"
spot::emptiness_check*
couvreur99_cons(const spot::tgba* a)
{
return new spot::couvreur99_check(a);
}
spot::emptiness_check*
couvreur99_shy_cons(const spot::tgba* a)
{
return new spot::couvreur99_check_shy(a);
}
spot::emptiness_check*
bsh_ms_cons(const spot::tgba* a)
{
return spot::bit_state_hashing_magic_search(a, 4096);
}
spot::emptiness_check*
bsh_se05_cons(const spot::tgba* a)
{
return spot::bit_state_hashing_se05_search(a, 4096);
}
struct ec_algo
{
const char* name;
spot::emptiness_check* (*construct)(const spot::tgba*);
unsigned int min_acc;
unsigned int max_acc;
bool safe;
};
ec_algo ec_algos[] =
{
{ "couvreur99", couvreur99_cons, 0, -1U, true },
{ "couvreur99_shy", couvreur99_shy_cons, 0, -1U, true },
{ "explicit_magic_search", spot::explicit_magic_search, 0, 1, true },
{ "bit_state_hashing_magic_search",
bsh_ms_cons, 0, 1, false },
{ "explicit_se05", spot::explicit_se05_search, 0, 1, true },
{ "bit_state_hashing_se05",
bsh_se05_cons, 0, 1, false },
{ "explicit_gv04", spot::explicit_gv04_check, 0, 1, true },
{ "explicit_tau03", spot::explicit_tau03_search, 1, -1U, true },
{ "explicit_tau03_opt", spot::explicit_tau03_opt_search, 0, -1U, true },
};
spot::emptiness_check*
cons_emptiness_check(int num, const spot::tgba* a,
const spot::tgba* degen, unsigned int n_acc)
{
if (n_acc < ec_algos[num].min_acc || n_acc > ec_algos[num].max_acc)
a = degen;
if (a)
return ec_algos[num].construct(a);
return 0;
}
void
syntax(char* prog)
{
@ -66,6 +126,8 @@ syntax(char* prog)
<< " -n N number of nodes of the graph [20]" << std::endl
<< " -r compute and replay acceptance runs (implies -e)"
<< std::endl
<< " -R N repeat each emptiness-check and accepting run "
<< "computation N times" << std::endl
<< " -s N seed for the random number generator" << std::endl
<< " -t F probability of the atomic propositions to be true"
<< " [0.5]" << std::endl
@ -275,6 +337,8 @@ main(int argc, char** argv)
bool opt_z = false;
bool opt_Z = false;
int opt_R = 0;
bool opt_dot = false;
int opt_ec = 0;
int opt_ec_seed = 0;
@ -341,6 +405,12 @@ main(int argc, char** argv)
if (!opt_ec)
opt_ec = 1;
}
else if (!strcmp(argv[argn], "-R"))
{
if (argc < argn + 2)
syntax(argv[0]);
opt_R = to_int(argv[++argn]);
}
else if (!strcmp(argv[argn], "-s"))
{
if (argc < argn + 2)
@ -371,7 +441,8 @@ main(int argc, char** argv)
spot::bdd_dict* dict = new spot::bdd_dict();
spot::timer_map tm_ec;
spot::timer_map tm_ar;
std::set<int> failed_seeds;
do
{
@ -397,69 +468,36 @@ main(int argc, char** argv)
if (opt_degen && opt_n_acc != 1)
degen = new spot::tgba_tba_proxy(a);
std::vector<spot::emptiness_check*> ec_obj;
std::vector<std::string> ec_name;
std::vector<bool> ec_safe;
ec_obj.push_back(new spot::couvreur99_check(a));
ec_name.push_back("couvreur99");
ec_safe.push_back(true);
ec_obj.push_back(new spot::couvreur99_check_shy(a));
ec_name.push_back("couvreur99_shy");
ec_safe.push_back(true);
if (opt_n_acc <= 1 || opt_degen)
{
spot::tgba* d = opt_n_acc > 1 ? degen : a;
ec_obj.push_back(spot::explicit_magic_search(d));
ec_name.push_back("explicit_magic_search");
ec_safe.push_back(true);
ec_obj.push_back(spot::bit_state_hashing_magic_search(d, 4096));
ec_name.push_back("bit_state_hashing_magic_search");
ec_safe.push_back(false);
ec_obj.push_back(spot::explicit_se05_search(d));
ec_name.push_back("explicit_se05");
ec_safe.push_back(true);
ec_obj.push_back(spot::bit_state_hashing_se05_search(d, 4096));
ec_name.push_back("bit_state_hashing_se05");
ec_safe.push_back(false);
ec_obj.push_back(spot::explicit_gv04_check(d));
ec_name.push_back("explicit_gv04");
ec_safe.push_back(true);
}
if (opt_n_acc >= 1 || opt_degen)
{
spot::tgba* d = opt_n_acc == 0 ? degen : a;
ec_obj.push_back(spot::explicit_tau03_search(d));
ec_name.push_back("explicit_tau03");
ec_safe.push_back(true);
}
ec_obj.push_back(spot::explicit_tau03_opt_search(a));
ec_name.push_back("explicit_tau03_opt");
ec_safe.push_back(true);
int n_ec = ec_obj.size();
int n_alg = sizeof(ec_algos) / sizeof(*ec_algos);
int n_ec = 0;
int n_empty = 0;
int n_non_empty = 0;
int n_maybe_empty = 0;
for (int i = 0; i < n_ec; ++i)
for (int i = 0; i < n_alg; ++i)
{
std::string algo = ec_name[i];
spot::emptiness_check* ec;
spot::emptiness_check_result* res;
ec = cons_emptiness_check(i, a, degen, opt_n_acc);
if (!ec)
continue;
++n_ec;
std::string algo = ec_algos[i].name;
std::cout.width(32);
std::cout << algo << ": ";
spot::emptiness_check_result* res = ec_obj[i]->check();
tm_ec.start(algo);
for (int count = opt_R;;)
{
res = ec->check();
if (count-- <= 0)
break;
delete res;
delete ec;
ec = cons_emptiness_check(i, a, degen, opt_n_acc);
}
tm_ec.stop(algo);
const spot::ec_statistics* ecs =
dynamic_cast<const spot::ec_statistics*>(ec_obj[i]);
dynamic_cast<const spot::ec_statistics*>(ec);
if (opt_z && ecs)
ec_stats[algo].count(ecs);
if (res)
@ -468,9 +506,23 @@ main(int argc, char** argv)
++n_non_empty;
if (opt_replay)
{
spot::tgba_run* run = res->accepting_run();
if (run)
spot::tgba_run* run;
tm_ar.start(algo);
for (int count = opt_R;;)
{
run = res->accepting_run();
if (count-- <= 0 || !run)
break;
delete run;
}
if (!run)
{
tm_ar.cancel(algo);
std::cout << " exists, not computed";
}
else
{
tm_ar.stop(algo);
std::ostringstream s;
if (!spot::replay_tgba_run(s, res->automaton(), run))
{
@ -515,17 +567,13 @@ main(int argc, char** argv)
}
delete run;
}
else
{
std::cout << " exists, not computed";
}
}
std::cout << std::endl;
delete res;
}
else
{
if (ec_safe[i])
if (ec_algos[i].safe)
{
std::cout << "empty language" << std::endl;
++n_empty;
@ -539,8 +587,8 @@ main(int argc, char** argv)
}
if (opt_Z)
ec_obj[i]->print_stats(std::cout);
delete ec_obj[i];
ec->print_stats(std::cout);
delete ec;
}
assert(n_empty + n_non_empty + n_maybe_empty == n_ec);
@ -632,6 +680,22 @@ main(int argc, char** argv)
print_ar_stats(mar_stats);
}
if (opt_z)
{
if (!tm_ec.empty())
{
std::cout << std::endl
<< "emptiness checks cumulated timings:" << std::endl;
tm_ec.print(std::cout);
}
if (!tm_ar.empty())
{
std::cout << std::endl
<< "accepting runs cumulated timings:" << std::endl;
tm_ar.print(std::cout);
}
}
if (!failed_seeds.empty())
{
exit_code = 1;