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

* src/bin/ltlcheck.cc: Cleanup temporary files on ^C.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2012-10-19 16:17:53 +02:00
parent e426c63550
commit 0bdfd9c72c
1 changed files with 25 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

40
src/bin/ltlcheck.cc
View file

@ -133,7 +133,6 @@ const struct argp_child children[] =
{ 0, 0, 0, 0 } { 0, 0, 0, 0 }
}; };
spot::bdd_dict dict;
unsigned states = 200; unsigned states = 200;
float density = 0.1; float density = 0.1;
unsigned timeout = 0; unsigned timeout = 0;
@ -206,6 +205,17 @@ typedef std::vector<statistics_formula> statistics_vector;
statistics_vector vstats; statistics_vector vstats;
std::vector<std::string> formulas; std::vector<std::string> formulas;
// Cleanup temporary files.
std::list<std::string> toclean;
void
cleanup()
{
for (std::list<std::string>::const_iterator i = toclean.begin();
i != toclean.end(); ++i)
unlink(i->c_str());
toclean.clear();
}
static int static int
to_int(const char* s) to_int(const char* s)
{ {
@ -303,6 +313,7 @@ create_tmpfile(char c, unsigned int n, std::string& name)
static volatile bool timed_out = false; static volatile bool timed_out = false;
#if ENABLE_TIMEOUT #if ENABLE_TIMEOUT
static volatile int alarm_on = 0; static volatile int alarm_on = 0;
static int child_pid = -1; static int child_pid = -1;
@ -334,6 +345,8 @@ sig_handler(int sig)
{ {
// forward signal // forward signal
kill(-child_pid, sig); kill(-child_pid, sig);
// cleanup files
cleanup();
// and die verbosely // and die verbosely
error(2, 0, "received signal %d", sig); error(2, 0, "received signal %d", sig);
} }
@ -439,6 +452,7 @@ namespace
class translator_runner: protected spot::formater class translator_runner: protected spot::formater
{ {
private: private:
spot::bdd_dict& dict;
// Round-specific variables // Round-specific variables
quoted_string string_ltl_spot; quoted_string string_ltl_spot;
quoted_string string_ltl_spin; quoted_string string_ltl_spin;
@ -446,13 +460,13 @@ namespace
quoted_string filename_ltl_spot; quoted_string filename_ltl_spot;
quoted_string filename_ltl_spin; quoted_string filename_ltl_spin;
quoted_string filename_ltl_lbt; quoted_string filename_ltl_lbt;
std::list<std::string> toclean;
// Run-specific variables // Run-specific variables
printable_result_filename output; printable_result_filename output;
public: public:
using spot::formater::has; using spot::formater::has;
translator_runner() translator_runner(spot::bdd_dict& dict)
: dict(dict)
{ {
declare('f', &string_ltl_spot); declare('f', &string_ltl_spot);
declare('s', &string_ltl_spin); declare('s', &string_ltl_spin);
@ -470,16 +484,6 @@ namespace
} }
// Cleanup temporary files.
void
round_cleanup()
{
for (std::list<std::string>::const_iterator i = toclean.begin();
i != toclean.end(); ++i)
unlink(i->c_str());
toclean.clear();
}
void void
string_to_tmp(std::string& str, unsigned n, std::string& tmpname) string_to_tmp(std::string& str, unsigned n, std::string& tmpname)
{ {
@ -589,7 +593,7 @@ namespace
{ {
res = spot::lbtt_parse(f, error, &dict); res = spot::lbtt_parse(f, error, &dict);
if (!res) if (!res)
global_error() << ("Failed error to parse output in " global_error() << ("error: failed to parse output in "
"LBTT format: ") "LBTT format: ")
<< error << std::endl; << error << std::endl;
} }
@ -729,9 +733,15 @@ namespace
class processor: public job_processor class processor: public job_processor
{ {
spot::bdd_dict dict;
translator_runner runner; translator_runner runner;
fset_t unique_set; fset_t unique_set;
public: public:
processor()
: runner(dict)
{
}
~processor() ~processor()
{ {
fset_t::iterator i = unique_set.begin(); fset_t::iterator i = unique_set.begin();
@ -837,7 +847,7 @@ namespace
} }
f->destroy(); f->destroy();
runner.round_cleanup(); cleanup();
++round; ++round;
if (!no_checks) if (!no_checks)