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

ltlsynt: Add more elements in csv

Browse source 
* bin/ltlsynt.cc: Add the number of states of the dpa
and of the parity game in the csv.
This commit is contained in:
Florian Renkin 2020-05-23 14:29:48 +02:00 • committed by Alexandre Duret-Lutz
parent 3fd5f38248
commit 494471a50b
1 changed files with 9 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

11
bin/ltlsynt.cc
View file

@ -135,6 +135,8 @@ static double paritize_time = 0.0;
static double bgame_time = 0.0; static double bgame_time = 0.0;
static double solve_time = 0.0; static double solve_time = 0.0;
static double strat2aut_time = 0.0; static double strat2aut_time = 0.0;
static unsigned nb_states_dpa = 0;
static unsigned nb_states_parity_game = 0;
enum solver enum solver
{ {
@ -318,7 +320,8 @@ namespace
out << ",\"strat2aut_time\""; out << ",\"strat2aut_time\"";
out << ",\"realizable\""; out << ",\"realizable\"";
} }
out << '\n'; out << ",\"dpa_num_states\",\"parity_game_num_states\""
<< '\n';
} }
std::ostringstream os; std::ostringstream os;
os << f; os << f;
@ -335,7 +338,9 @@ namespace
out << ',' << strat2aut_time; out << ',' << strat2aut_time;
out << ',' << realizable; out << ',' << realizable;
} }
out << '\n'; out << ',' << nb_states_dpa
<< ',' << nb_states_parity_game
<< '\n';
outf.close(opt_csv); outf.close(opt_csv);
} }
@ -532,6 +537,7 @@ namespace
break; break;
} }
} }
nb_states_dpa = dpa->num_states();
if (want_time) if (want_time)
sw.start(); sw.start();
auto owner = complete_env(dpa); auto owner = complete_env(dpa);
@ -557,6 +563,7 @@ namespace
solve_time = sw.stop(); solve_time = sw.stop();
if (verbose) if (verbose)
std::cerr << "parity game solved in " << solve_time << " seconds\n"; std::cerr << "parity game solved in " << solve_time << " seconds\n";
nb_states_parity_game = pg.num_states();
timer.stop(); timer.stop();
if (winning_region[1].count(pg.get_init_state_number())) if (winning_region[1].count(pg.get_init_state_number()))
{ {