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