From 5488cb75c6c83709e49958fd6c067634f61f45a7 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 9 Sep 2024 16:28:51 +0200 Subject: [PATCH] ltlsynt: overhaul CSV output Previous output was not very usable in presence of decomposed specifications. We now keep track of the number of parts, and also prefix the columns names with "max_" or "sum_" to indicate how their statistics are updated in presence of multiple part. Other missing statistics, like the size of the translated automaton, or maximal number of colors seen in a game, have been added. * spot/twaalgos/synthesis.hh (bench_var): Rename, augment, and document each statistsic. * spot/twaalgos/mealy_machine.cc, spot/twaalgos/synthesis.cc, bin/ltlsynt.cc: Adjust to the new naming scheme. * doc/org/ltlsynt.org: Show a CSV file, and document its columns. * tests/core/ltlsynt-pgame.test, tests/core/ltlsynt2.test, tests/core/ltlsynt.test: Adjust test cases. * NEWS: Mention the backward incompatible change. --- NEWS | 19 +++-- bin/ltlsynt.cc | 143 ++++++++++++++++++++++----------- doc/org/ltlsynt.org | 124 +++++++++++++++++++--------- spot/twaalgos/mealy_machine.cc | 20 +++-- spot/twaalgos/synthesis.cc | 96 +++++++++++++--------- spot/twaalgos/synthesis.hh | 81 +++++++++++++++---- tests/core/ltlsynt-pgame.test | 11 +-- tests/core/ltlsynt.test | 2 +- tests/core/ltlsynt2.test | 20 ++--- 9 files changed, 352 insertions(+), 164 deletions(-) diff --git a/NEWS b/NEWS index e8f01b7ca..89330adfb 100644 --- a/NEWS +++ b/NEWS @@ -5,13 +5,22 @@ New in spot 2.12.0.dev (not yet released) - ltlmix is a new tool that generates formulas by combining existing ones. See https://spot.lre.epita.fr/ltlmix.html for examples. - - ltlsynt --csv=FILENAME will now save the source filename for the - processed formulas as the first column of the CSV file. A new + - (BACKWARD INCOMPATIBILITY) ltlsynt's CSV output has been largely + overhauled, and the output columns have been both renamed (for + consistency) and augmented (with new statistics). The new CSV + output should more useful when the input specification was + decomposed, in particular, there is a column giving the number of + sub-specifications obained, and other statistics columns have name + starting with "max_" or "sum_" indicating how said statistics are + updated across sub-speciications. + + See https://spot.lre.epita.fr/ltlsynt.html#csv for an example. + + Additionally, --csv=FILENAME will now save the source filename for + the processed formulas as the first column of the CSV file. A new option --csv-without-formula=FILENAME can be used to save everything but the formula column (as it can be very large, and - can be found from the source filename). Several column names have - also been renamed for consistency, so any script reading these - file might require some adjustment. + can be found from the source filename). - ltlsynt learned a --part-file option, to specify the partition of input/output proposition from a *.part file, as used in several diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 7e1cfb5b2..0e846c386 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -298,18 +298,18 @@ ARGMATCH_VERIFY(simplify_args, simplify_values); static const char* const splittype_args[] = { + "auto", "expl", "semisym", "fullysym", - "auto", nullptr }; static spot::synthesis_info::splittype splittype_values[] = { + spot::synthesis_info::splittype::AUTO, spot::synthesis_info::splittype::EXPL, spot::synthesis_info::splittype::SEMISYM, spot::synthesis_info::splittype::FULLYSYM, - spot::synthesis_info::splittype::AUTO, }; ARGMATCH_VERIFY(splittype_args, splittype_values); @@ -363,25 +363,44 @@ namespace // (Even if that file was empty initially.) if (!outf.append()) { - out << "\"source\","; + out << "source"; if (opt_csv_with_formula) - out << "\"formula\","; - out << ("\"algo\",\"tot_time\",\"trans_time\"," - "\"split_time\",\"todpa_time\""); + out << ",formula"; + if (!was_game) + { + out << ",subspecs"; + out << ",algo"; + } + out << ",split,total_time"; + if (!was_game) + out << ",sum_trans_time"; + out << ",sum_split_time"; + if (!was_game) + out << ",sum_todpa_time"; if (!opt_print_pg && !opt_print_hoa) { - out << ",\"solve_time\""; + out << ",sum_solve_time"; if (!opt_real) - out << ",\"strat2aut_time\""; + out << ",sum_strat2aut_time"; if (opt_print_aiger) - out << ",\"aig_time\""; - out << ",\"realizable\""; //-1: Unknown, 0: Unreal, 1: Real + out << ",aig_time"; + out << ",realizable"; //-1: Unknown, 0: Unreal, 1: Real } - out << ",\"game_states\",\"game_states_env\""; + if (!was_game) + out << (",max_trans_states,max_trans_edges" + ",max_trans_colors,max_trans_ap"); + out << ",max_game_states,max_game_colors"; if (!opt_real) - out << ",\"strat_states\",\"strat_edges\""; + { + out << ",max_strat_states,max_strat_edges"; + if (!was_game) + out << ",sum_strat_states,sum_strat_edges"; + out << ",max_simpl_strat_states,max_simpl_strat_edges"; + if (!was_game) + out << ",sum_simpl_strat_states,sum_simpl_strat_edges"; + } if (opt_print_aiger) - out << ",\"aig_latches\",\"aig_gates\""; + out << ",aig_latches,aig_gates"; out << '\n'; } { @@ -404,28 +423,48 @@ namespace } } if (!was_game) - out << '"' << algo_names[(int) gi->s] << '"'; - out << ',' << bv->total_time - << ',' << bv->trans_time - << ',' << bv->split_time - << ',' << bv->paritize_time; + { + out << bv->sub_specs << ','; + out << algo_names[(int) gi->s] << ','; + } + out << splittype_args[(int) gi->sp] << ',' << bv->total_time; + if (!was_game) + out << ',' << bv->sum_trans_time; + out << ',' << bv->sum_split_time; + if (!was_game) + out << ',' << bv->sum_paritize_time; if (!opt_print_pg && !opt_print_hoa) { - out << ',' << bv->solve_time; + out << ',' << bv->sum_solve_time; if (!opt_real) - out << ',' << bv->strat2aut_time; + out << ',' << bv->sum_strat2aut_time; if (opt_print_aiger) out << ',' << bv->aig_time; out << ',' << bv->realizable; } - out << ',' << bv->nb_states_arena - << ',' << bv->nb_states_arena_env; + if (!was_game) + out << ',' << bv->max_trans_states + << ',' << bv->max_trans_edges + << ',' << bv->max_trans_colors + << ',' << bv->max_trans_ap; + out << ',' << bv->max_game_states + << ',' << bv->max_game_colors; if (!opt_real) - out << ',' << bv->nb_strat_states - << ',' << bv->nb_strat_edges; + { + out << ',' << bv->max_strat_states + << ',' << bv->max_strat_edges; + if (!was_game) + out << ',' << bv->sum_strat_states + << ',' << bv->sum_strat_edges; + out << ',' << bv->max_simpl_strat_states + << ',' << bv->max_simpl_strat_edges; + if (!was_game) + out << ',' << bv->sum_simpl_strat_states + << ',' << bv->sum_simpl_strat_edges; + } if (opt_print_aiger) - out << ',' << bv->nb_latches - << ',' << bv->nb_gates; + out << ',' << bv->aig_latches + << ',' << bv->aig_gates; out << '\n'; outf.close(opt_csv); } @@ -515,6 +554,8 @@ namespace } } + if (gi->bv) + gi->bv->sub_specs = sub_form.size(); std::vector> sub_outs_str; std::transform(sub_outs.begin(), sub_outs.end(), std::back_inserter(sub_outs_str), @@ -584,16 +625,23 @@ namespace case spot::mealy_like::realizability_code::UNKNOWN: { auto arena = spot::ltl_to_game(*sub_f, *sub_o, *gi); +#ifndef NDEBUG + auto spptr = + arena->get_named_prop>("state-player"); + assert(spptr); + assert((spptr->at(arena->get_init_state_number()) == false) + && "Env needs first turn"); +#endif if (gi->bv) { - gi->bv->nb_states_arena += arena->num_states(); - auto spptr = - arena->get_named_prop>("state-player"); - assert(spptr); - gi->bv->nb_states_arena_env += - std::count(spptr->cbegin(), spptr->cend(), false); - assert((spptr->at(arena->get_init_state_number()) == false) - && "Env needs first turn"); + unsigned ns = arena->num_states(); + unsigned nc = arena->num_sets(); + if (std::tie(gi->bv->max_game_states, gi->bv->max_game_colors) + < std::tie(ns, nc)) + { + gi->bv->max_game_states = ns; + gi->bv->max_game_colors = nc; + } } if (want_game()) { @@ -690,8 +738,8 @@ namespace if (gi->bv) { gi->bv->aig_time = sw2.stop(); - gi->bv->nb_latches = saig->num_latches(); - gi->bv->nb_gates = saig->num_gates(); + gi->bv->aig_latches = saig->num_latches(); + gi->bv->aig_gates = saig->num_gates(); } if (gi->verbose_stream) { @@ -828,7 +876,10 @@ namespace const std::string& location) { if (opt_csv) // reset benchmark data - gi->bv = spot::synthesis_info::bench_var(); + { + gi->bv = spot::synthesis_info::bench_var(); + gi->bv->sub_specs = 1; // We do not know how to split a game + } spot::stopwatch sw_global; spot::stopwatch sw_local; if (gi->bv) @@ -881,13 +932,9 @@ namespace } if (gi->bv) { - gi->bv->split_time += sw_local.stop(); - gi->bv->nb_states_arena += arena->num_states(); - auto spptr = - arena->get_named_prop>("state-player"); - assert(spptr); - gi->bv->nb_states_arena_env += - std::count(spptr->cbegin(), spptr->cend(), false); + gi->bv->sum_split_time += sw_local.stop(); + gi->bv->max_game_states = arena->num_states(); + gi->bv->max_game_colors = arena->num_sets(); } if (opt_print_pg || opt_print_hoa) { @@ -931,16 +978,16 @@ namespace if (gi->bv) { gi->bv->aig_time = sw_local.stop(); - gi->bv->nb_latches = saig->num_latches(); - gi->bv->nb_gates = saig->num_gates(); + gi->bv->aig_latches = saig->num_latches(); + gi->bv->aig_gates = saig->num_gates(); } if (gi->verbose_stream) { *gi->verbose_stream << "AIG circuit was created in " << gi->bv->aig_time - << " seconds and has " << saig->num_latches() + << " seconds and has " << gi->bv->aig_latches << " latches and " - << saig->num_gates() << " gates\n"; + << gi->bv->aig_gates << " gates\n"; } spot::print_aiger(std::cout, saig) << '\n'; } diff --git a/doc/org/ltlsynt.org b/doc/org/ltlsynt.org index 0230d0b11..82a3399c6 100644 --- a/doc/org/ltlsynt.org +++ b/doc/org/ltlsynt.org @@ -286,7 +286,10 @@ ltlsynt -f '(i1 & i2) <-> F(o1 & X(!o1))' --print-game-hoa --dot #+RESULTS: [[file:ltlsyntexgame.svg]] -** Saving statistics +** Saving statistics in CSV + :PROPERTIES: + :CUSTOM_ID: csv + :END: For benchmarking purpose, the =--csv= option can be used to record intermediate statistics about the resolution. The =--csv= option will @@ -301,7 +304,7 @@ Mealy's semantics.) #+BEGIN_SRC sh :results verbatim :exports code :epilogue true genltl --lily-patterns | - ltlsynt --algo=acd --realizability --csv-without-formula=bench.csv + ltlsynt --algo=acd -q --csv-without-formula=bench.csv #+END_SRC #+RESULTS: #+begin_example @@ -344,42 +347,91 @@ s/,/|/g ' bench.csv #+END_SRC +#+ATTR_HTML: :class csv-table #+RESULTS: -| source | algo | tot_time | trans_time | split_time | todpa_time | solve_time | realizable | game_states | game_states_env | -|--------+------+-------------+-------------+-------------+-------------+-------------+------------+-------------+-----------------| -| -:1 | acd | 0.000472663 | 0.00019603 | 2.0339e-05 | 2.0388e-05 | 1.4617e-05 | 0 | 3 | 2 | -| -:2 | acd | 0.00028595 | 0.000188466 | 1.4417e-05 | 2.0027e-05 | 5.861e-06 | 0 | 13 | 7 | -| -:3 | acd | 0.000741622 | 0.000591889 | 4.7229e-05 | 1.9516e-05 | 1.8014e-05 | 1 | 26 | 12 | -| -:4 | acd | 0.000917794 | 0.000725371 | 7.2026e-05 | 3.0328e-05 | 2.0349e-05 | 1 | 33 | 15 | -| -:5 | acd | 0.000878991 | 0.000612978 | 0.000102604 | 3.4155e-05 | 2.7913e-05 | 1 | 47 | 20 | -| -:6 | acd | 0.00100199 | 0.000761539 | 8.0191e-05 | 2.9817e-05 | 2.9075e-05 | 1 | 55 | 24 | -| -:7 | acd | 0.000587721 | 0.000425814 | 4.6268e-05 | 1.6261e-05 | 1.4106e-05 | 1 | 26 | 11 | -| -:8 | acd | 1.4046e-05 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | -| -:9 | acd | 0.000519242 | 0.000400918 | 2.2322e-05 | 2.9446e-05 | 1.3886e-05 | 1 | 16 | 6 | -| -:10 | acd | 6.0835e-05 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | -| -:11 | acd | 5.5245e-05 | 1.8335e-05 | 5.249e-06 | 4.007e-06 | 4.549e-06 | 0 | 3 | 2 | -| -:12 | acd | 1.6411e-05 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | -| -:13 | acd | 0.000192153 | 0.000134825 | 1.06e-05 | 8.506e-06 | 5.33e-06 | 1 | 5 | 2 | -| -:14 | acd | 0.000291931 | 0.000209857 | 1.0881e-05 | 1.4076e-05 | 6.182e-06 | 1 | 4 | 2 | -| -:15 | acd | 0.000690605 | 0.000480759 | 9.4349e-05 | 3.2541e-05 | 1.8675e-05 | 1 | 30 | 9 | -| -:16 | acd | 0.00232829 | 0.00173036 | 0.000348709 | 9.2966e-05 | 6.1276e-05 | 1 | 103 | 29 | -| -:17 | acd | 0.000554708 | 0.00038608 | 2.4887e-05 | 2.9205e-05 | 1.1902e-05 | 1 | 6 | 3 | -| -:18 | acd | 0.00114041 | 0.00088879 | 3.3784e-05 | 3.4585e-05 | 1.1602e-05 | 1 | 8 | 4 | -| -:19 | acd | 0.000761799 | 0.000517278 | 4.3132e-05 | 5.1968e-05 | 2.127e-05 | 1 | 11 | 4 | -| -:20 | acd | 0.0169891 | 0.0133503 | 0.00172203 | 0.00113707 | 0.000412299 | 1 | 1002 | 311 | -| -:21 | acd | 0.118002 | 0.115604 | 0.00165549 | 0.000149402 | 0.00024346 | 1 | 371 | 75 | -| -:22 | acd | 0.00316832 | 0.00240598 | 0.000305407 | 0.000103245 | 0.00010582 | 1 | 86 | 30 | -| -:23 | acd | 0.000824969 | 0.000632956 | 3.2161e-05 | 2.9766e-05 | 2.0299e-05 | 1 | 17 | 7 | +| source | subspecs | algo | split | total_time | sum_trans_time | sum_split_time | sum_todpa_time | sum_solve_time | sum_strat2aut_time | realizable | max_trans_states | max_trans_edges | max_trans_colors | max_trans_ap | max_game_states | max_game_colors | max_strat_states | max_strat_edges | sum_strat_states | sum_strat_edges | max_simpl_strat_states | max_simpl_strat_edges | sum_simpl_strat_states | sum_simpl_strat_edges | +|--------+----------+------+-------+-------------+----------------+----------------+----------------+----------------+--------------------+------------+------------------+-----------------+------------------+--------------+-----------------+-----------------+------------------+-----------------+------------------+-----------------+------------------------+-----------------------+------------------------+-----------------------| +| -:1 | 2 | acd | auto | 0.000327418 | 0.000135325 | 1.5128e-05 | 1.543e-05 | 6.171e-06 | 0 | 0 | 1 | 0 | 0 | 0 | 3 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | +| -:2 | 2 | acd | auto | 0.00020147 | 0.000117201 | 9.227e-06 | 1.2634e-05 | 3.607e-06 | 6.642e-06 | 0 | 5 | 8 | 0 | 1 | 10 | 0 | 2 | 2 | 2 | 2 | 2 | 2 | 2 | 2 | +| -:3 | 1 | acd | auto | 0.000487781 | 0.000360129 | 2.8053e-05 | 1.1211e-05 | 1.0851e-05 | 5.741e-06 | 1 | 12 | 46 | 1 | 3 | 26 | 1 | 5 | 5 | 5 | 5 | 2 | 4 | 2 | 4 | +| -:4 | 1 | acd | auto | 0.000491777 | 0.000356242 | 3.3032e-05 | 1.5269e-05 | 1.0379e-05 | 6.683e-06 | 1 | 15 | 62 | 1 | 3 | 33 | 1 | 6 | 6 | 6 | 6 | 3 | 7 | 3 | 7 | +| -:5 | 1 | acd | auto | 0.000476078 | 0.000314904 | 4.4103e-05 | 1.5029e-05 | 1.2133e-05 | 1.4237e-05 | 1 | 20 | 88 | 1 | 3 | 47 | 1 | 8 | 9 | 8 | 9 | 6 | 17 | 6 | 17 | +| -:6 | 1 | acd | auto | 0.000486699 | 0.000300587 | 4.4013e-05 | 1.6531e-05 | 1.3766e-05 | 1.57e-05 | 1 | 24 | 111 | 1 | 3 | 55 | 1 | 11 | 12 | 11 | 12 | 7 | 21 | 7 | 21 | +| -:7 | 1 | acd | auto | 0.000394895 | 0.00024404 | 2.7942e-05 | 9.317e-06 | 1.2443e-05 | 7.344e-06 | 1 | 11 | 38 | 1 | 3 | 26 | 1 | 7 | 8 | 7 | 8 | 6 | 14 | 6 | 14 | +| -:8 | 1 | acd | auto | 1.3125e-05 | 1.293e-06 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 1 | 1 | 1 | +| -:9 | 1 | acd | auto | 0.000309784 | 0.000223411 | 1.3456e-05 | 1.9046e-05 | 8.466e-06 | 3.968e-06 | 1 | 6 | 19 | 2 | 2 | 16 | 2 | 2 | 3 | 2 | 3 | 2 | 3 | 2 | 3 | +| -:10 | 1 | acd | auto | 1.4206e-05 | 6.81e-07 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 1 | 1 | 1 | +| -:11 | 1 | acd | auto | 2.8453e-05 | 9.968e-06 | 2.504e-06 | 2.114e-06 | 2.295e-06 | 0 | 0 | 1 | 0 | 0 | 0 | 3 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | +| -:12 | 1 | acd | auto | 1.3826e-05 | 8.81e-07 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 1 | 1 | 1 | +| -:13 | 1 | acd | auto | 0.000124284 | 7.6274e-05 | 6.192e-06 | 4.869e-06 | 3.066e-06 | 3.196e-06 | 1 | 2 | 3 | 1 | 2 | 5 | 1 | 2 | 2 | 2 | 2 | 1 | 2 | 1 | 2 | +| -:14 | 1 | acd | auto | 0.000184107 | 0.000122141 | 6.412e-06 | 8.275e-06 | 3.567e-06 | 2.725e-06 | 1 | 1 | 3 | 2 | 2 | 4 | 1 | 2 | 2 | 2 | 2 | 2 | 2 | 2 | 2 | +| -:15 | 1 | acd | auto | 0.00042922 | 0.000279297 | 3.7861e-05 | 1.9096e-05 | 1.057e-05 | 6.933e-06 | 1 | 8 | 40 | 2 | 4 | 30 | 1 | 7 | 12 | 7 | 12 | 5 | 13 | 5 | 13 | +| -:16 | 1 | acd | auto | 0.0015915 | 0.00103173 | 0.000202432 | 5.328e-05 | 3.6118e-05 | 1.8925e-05 | 1 | 22 | 225 | 3 | 6 | 103 | 1 | 22 | 40 | 22 | 40 | 17 | 71 | 17 | 71 | +| -:17 | 1 | acd | auto | 0.000271983 | 0.000184298 | 8.636e-06 | 9.919e-06 | 3.988e-06 | 3.046e-06 | 1 | 1 | 4 | 3 | 3 | 6 | 1 | 3 | 3 | 3 | 3 | 3 | 3 | 3 | 3 | +| -:18 | 1 | acd | auto | 0.000380097 | 0.000274818 | 1.1502e-05 | 1.1481e-05 | 4.098e-06 | 3.366e-06 | 1 | 1 | 5 | 4 | 4 | 8 | 1 | 4 | 4 | 4 | 4 | 4 | 4 | 4 | 4 | +| -:19 | 1 | acd | auto | 0.000263427 | 0.000170873 | 1.4458e-05 | 1.6912e-05 | 7.214e-06 | 2.835e-06 | 1 | 4 | 15 | 2 | 3 | 11 | 2 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | +| -:20 | 1 | acd | auto | 0.00668276 | 0.00504907 | 0.000916819 | 0.000353497 | 0.000170251 | 9.368e-06 | 1 | 311 | 3488 | 2 | 5 | 1002 | 2 | 10 | 10 | 10 | 10 | 6 | 12 | 6 | 12 | +| -:21 | 1 | acd | auto | 0.0414155 | 0.0392309 | 0.000744745 | 5.4213e-05 | 8.4029e-05 | 7.5533e-05 | 1 | 75 | 546 | 1 | 8 | 371 | 1 | 74 | 228 | 74 | 228 | 71 | 339 | 71 | 339 | +| -:22 | 1 | acd | auto | 0.00126613 | 0.000785011 | 0.000112663 | 3.5397e-05 | 3.5998e-05 | 1.7854e-05 | 1 | 30 | 161 | 2 | 4 | 86 | 1 | 22 | 25 | 22 | 25 | 15 | 67 | 15 | 67 | +| -:23 | 1 | acd | auto | 0.000305085 | 0.000213032 | 1.061e-05 | 1.0009e-05 | 6.752e-06 | 5.23e-06 | 1 | 7 | 16 | 1 | 2 | 17 | 1 | 5 | 6 | 5 | 6 | 3 | 6 | 3 | 6 | + +The names of the columns should be mostly self explanatory. The +decomposition of the specification into multiple sub-specifications +makes it slightly incoveniant to track statistics in a run. The +column =subspecs= indicates how many sub-specifications were found in +the original specification. Columns with names of the form =sum_*= +accumulate their statistics over all subspecifications. Columns with +names of the form =max_*= keep only the largest statistics. The following +statistics are gathered: + +- =source=: location of the specification in the form FILENAME:LINE + (FILENAME is =-= when reading from standard input as in the above + example). +- =formula= (if requested): the actual LTL formula used for the + specification +- =subspecs=: the number of sub-specifications resulting from the + decomposition +- =algo=: the name of the approach used to construct game, as + specified with the =--algo= option +- =split=: the name of the approach used to split the automaton into + input and output steps, as specified with the =--split= option +- =total_time=: total time measured by =ltlsynt= to solve the problem + once the problem has been loaded (parsing of the formula, conversion + from TSLF, or parsing of a parity game are all excluded) +- =sum_trans_time=: sum of the translation time needed to obtain an + automaton from each subspecification. +- =sum_split_time=: sum of the times needed to split the automata +- =sum_todpa_time=: sum of the times needed to paritize the automata +- =sum_solve_time=: sum of the times needed to solve the game for each + subspecification +- =sum_strat2aut_time= sum of the time needed to extract the + strategies +- =realizable=: whether the specification is realizable +- =max_trans_states,max_trans_edges,max_trans_colors,max_trans_ap=: + Size of the largest automaton constructed for a subspecification. + The largest size is actually the largest quadruple of the form + (states,edges,colors,ap), so those maximum values are not + independent. +- =max_game_states=: maximum number of state in any game constructed +- =max_game_colors=: maximum numbers of colors in any game constructed + (might not be the same game as for =max_game_states=) +- =max_strat_states,max_strat_edges=: size of the largest strategy + found. The largest size is the largest pair (states,edges), so + those two values are not indeendent. +- =sum_strat_states,sum_strat_edges=: sum of the states/edges in + strategies for all subspecifications +- =max_simpl_strat_states,max_simpl_strat_edges=: size of the largest + simplified strategy. +- =sum_simpl_strat_states,sum_simpl_strat_edges=: sum of the + states/edges in simplified strategies for all subspecifications +- =aig_gates,aig_latches=: Size of the AIG circuit, if requested. + + +In the table from the previous section some of the intermediate +processing times are listed as =0= (e.g., for input 8, 10, 12) because +the specifications can be found to be realizable trivially without +building any game. -A source of the form =-:N= designates the Nth line of the standard -input, as =ltlsynt= was reading from that. The various =*_time*= -columns refers to different steps in the processing pipeline. Note -that various bits and minor operations are not timed, so =tot_time= -(the total time) should be larger than the sum of times used for -translation, splitting, conversion to DPA, and game solving. Some of -these intermediate processing time are listed as =0= above because -(e.g., for input 8, 10, 12) because the specifications can be found to -be realizable trivially without building any game. ** Verifying the output diff --git a/spot/twaalgos/mealy_machine.cc b/spot/twaalgos/mealy_machine.cc index 5021f2a94..11a05d5cf 100644 --- a/spot/twaalgos/mealy_machine.cc +++ b/spot/twaalgos/mealy_machine.cc @@ -4353,9 +4353,10 @@ namespace spot if (si.verbose_stream) *si.verbose_stream << "simplification took " << sw.stop() << " seconds\n"; - si.bv->simplify_strat_time += sw.stop(); - auto n_s_env = 0u; - auto n_e_env = 0u; + si.bv->sum_simplify_strat_time += sw.stop(); + unsigned n_s_env = 0; + unsigned n_e_env = 0; + // If the strategy is split, count only the environment's states if (auto sp = m->get_named_prop("state-player")) { n_s_env = sp->size() - std::accumulate(sp->begin(), @@ -4365,15 +4366,22 @@ namespace spot [&n_e_env, &sp](const auto& e) { n_e_env += (*sp)[e.src]; - }); + }); } else { n_s_env = m->num_states(); n_e_env = m->num_edges(); } - si.bv->nb_simpl_strat_states += n_s_env; - si.bv->nb_simpl_strat_edges += n_e_env; + if (std::tie(si.bv->max_simpl_strat_states, + si.bv->max_simpl_strat_edges) + < std::tie(n_s_env, n_e_env)) + { + si.bv->max_simpl_strat_states = n_s_env; + si.bv->max_simpl_strat_edges = n_e_env; + } + si.bv->sum_simpl_strat_states += n_s_env; + si.bv->sum_simpl_strat_edges += n_e_env; } } } diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc index b2b54fcf3..5231f98ad 100644 --- a/spot/twaalgos/synthesis.cc +++ b/spot/twaalgos/synthesis.cc @@ -1574,11 +1574,11 @@ namespace spot // release the variables // Release the pairs for (auto pair_ptr : {replace_fwd, - replace_bkwd, - replace_in_fwd, - replace_in_bkwd, - replace_out_fwd, - replace_out_bkwd}) + replace_bkwd, + replace_in_fwd, + replace_in_bkwd, + replace_out_fwd, + replace_out_bkwd}) bdd_freepair(pair_ptr); aut->get_dict()->unregister_all_my_variables(&N); @@ -1602,17 +1602,17 @@ namespace spot : sp; switch (sp) - { - case (synthesis_info::splittype::EXPL): + { + case synthesis_info::splittype::EXPL: return split_2step_expl_impl(aut, output_bdd, complete_env); - case (synthesis_info::splittype::SEMISYM): + case synthesis_info::splittype::SEMISYM: return split_2step_sym_impl(aut, output_bdd, complete_env); - case (synthesis_info::splittype::FULLYSYM): + case synthesis_info::splittype::FULLYSYM: return split_2step_sym_impl(aut, output_bdd, complete_env); default: throw std::runtime_error("split_2step_(): " "Expected explicit splittype."); - } + } } } // End anonymous @@ -1826,13 +1826,29 @@ namespace spot sw.start(); auto aut = trans.run(f); if (bv) - bv->trans_time += sw.stop(); - + { + bv->sum_trans_time += sw.stop(); + unsigned ns = aut->num_states(); + unsigned ne = aut->num_edges(); + unsigned nc = aut->num_sets(); + unsigned na = aut->ap().size(); + if (std::tie(bv->max_trans_states, + bv->max_trans_edges, + bv->max_trans_colors, + bv->max_trans_ap) + < std::tie(ns, ne, nc, na)) + { + bv->max_trans_states = ns; + bv->max_trans_edges = ne; + bv->max_trans_colors = nc; + bv->max_trans_ap = na; + } + } if (vs) { assert(bv); *vs << "translating formula done in " - << bv->trans_time << " seconds\n"; + << bv->sum_trans_time << " seconds\n"; *vs << "automaton has " << aut->num_states() << " states and " << aut->num_sets() << " colors\n"; } @@ -1879,20 +1895,20 @@ namespace spot << tmp->num_sets() << " colors\n"; tmp->merge_states(); if (bv) - bv->paritize_time += sw.stop(); + bv->sum_paritize_time += sw.stop(); if (vs) *vs << "simplification done\nDPA has " << tmp->num_states() << " states\n" << "determinization and simplification took " - << bv->paritize_time << " seconds\n"; + << bv->sum_paritize_time << " seconds\n"; if (bv) sw.start(); dpa = set_split(tmp); if (bv) - bv->split_time += sw.stop(); + bv->sum_split_time += sw.stop(); if (vs) - *vs << "split inputs and outputs done in " << bv->split_time + *vs << "split inputs and outputs done in " << bv->sum_split_time << " seconds\nautomaton has " << tmp->num_states() << " states\n"; break; @@ -1903,18 +1919,18 @@ namespace spot sw.start(); aut->merge_states(); if (bv) - bv->paritize_time += sw.stop(); + bv->sum_paritize_time += sw.stop(); if (vs) - *vs << "simplification done in " << bv->paritize_time + *vs << "simplification done in " << bv->sum_paritize_time << " seconds\nDPA has " << aut->num_states() << " states\n"; if (bv) sw.start(); dpa = set_split(aut); if (bv) - bv->split_time += sw.stop(); + bv->sum_split_time += sw.stop(); if (vs) - *vs << "split inputs and outputs done in " << bv->split_time + *vs << "split inputs and outputs done in " << bv->sum_split_time << " seconds\nautomaton has " << dpa->num_states() << " states\n"; break; @@ -1924,9 +1940,9 @@ namespace spot sw.start(); auto split = set_split(aut); if (bv) - bv->split_time += sw.stop(); + bv->sum_split_time += sw.stop(); if (vs) - *vs << "split inputs and outputs done in " << bv->split_time + *vs << "split inputs and outputs done in " << bv->sum_split_time << " seconds\nautomaton has " << split->num_states() << " states\n"; if (bv) @@ -1942,12 +1958,12 @@ namespace spot // Merge states knows about players dpa->merge_states(); if (bv) - bv->paritize_time += sw.stop(); + bv->sum_paritize_time += sw.stop(); if (vs) *vs << "simplification done\nDPA has " << dpa->num_states() << " states\n" << "determinization and simplification took " - << bv->paritize_time << " seconds\n"; + << bv->sum_paritize_time << " seconds\n"; break; } case algo::ACD: @@ -1971,10 +1987,10 @@ namespace spot else dpa = acd_transform(aut); if (bv) - bv->paritize_time += sw.stop(); + bv->sum_paritize_time += sw.stop(); if (vs) *vs << (gi.s == algo::ACD ? "ACD" : "LAR") - << " construction done in " << bv->paritize_time + << " construction done in " << bv->sum_paritize_time << " seconds\nDPA has " << dpa->num_states() << " states, " << dpa->num_sets() << " colors\n"; @@ -1983,9 +1999,9 @@ namespace spot sw.start(); dpa = set_split(dpa); if (bv) - bv->split_time += sw.stop(); + bv->sum_split_time += sw.stop(); if (vs) - *vs << "split inputs and outputs done in " << bv->split_time + *vs << "split inputs and outputs done in " << bv->sum_split_time << " seconds\nautomaton has " << dpa->num_states() << " states\n"; break; @@ -2045,6 +2061,7 @@ namespace spot if (gi.bv) { + gi.bv->sum_strat2aut_time += sw.stop(); auto sp = get_state_players(m); auto n_s_env = sp.size() - std::accumulate(sp.begin(), sp.end(), @@ -2055,9 +2072,14 @@ namespace spot { n_e_env += sp[e.src]; }); - gi.bv->strat2aut_time += sw.stop(); - gi.bv->nb_strat_states += n_s_env; - gi.bv->nb_strat_edges += n_e_env; + if (std::tie(gi.bv->max_strat_states, gi.bv->max_strat_edges) + < std::tie(n_s_env, n_e_env)) + { + gi.bv->max_strat_states = n_s_env; + gi.bv->max_strat_edges = n_e_env; + } + gi.bv->sum_strat_states += n_s_env; + gi.bv->sum_strat_edges += n_e_env; } assert(is_mealy(m)); @@ -2383,7 +2405,7 @@ namespace spot if (bv) { auto delta = sw.stop(); - bv->trans_time += delta; + bv->sum_trans_time += delta; if (vs) *vs << "translating formula done in " << delta << " seconds...\n... but it gave a " @@ -2445,7 +2467,7 @@ namespace spot if (bv) { auto delta = sw.stop(); - bv->trans_time += delta; + bv->sum_trans_time += delta; if (vs) *vs << "translating formula done in " << delta << " seconds\n"; } @@ -2477,7 +2499,7 @@ namespace spot if (bv) { auto delta = sw.stop(); - bv->trans_time += delta; + bv->sum_trans_time += delta; if (vs) *vs << "translating formula done in " << delta << " seconds\n"; } @@ -2922,10 +2944,10 @@ namespace spot } bool res = solve_game(arena); if (gi.bv) - gi.bv->solve_time += sw.stop(); + gi.bv->sum_solve_time += sw.stop(); if (gi.verbose_stream) *(gi.verbose_stream) << "game solved in " - << gi.bv->solve_time << " seconds\n"; + << gi.bv->sum_solve_time << " seconds\n"; return res; } diff --git a/spot/twaalgos/synthesis.hh b/spot/twaalgos/synthesis.hh index 2c5bdff1b..34bd57ea0 100644 --- a/spot/twaalgos/synthesis.hh +++ b/spot/twaalgos/synthesis.hh @@ -32,7 +32,7 @@ namespace spot { enum class algo { - DET_SPLIT=0, + DET_SPLIT = 0, SPLIT_DET, DPA_SPLIT, LAR, @@ -42,30 +42,79 @@ namespace spot enum class splittype { - AUTO=0, // Uses a heuristic to choose + AUTO = 0, // Uses a heuristic to choose EXPL, // Explicit enumerations of inputs SEMISYM, // Works on one bdd per env state FULLYSYM // Works on a fully symbolic version of the automaton }; + // These statistics are recorded by various steps of the synthesis + // process. struct bench_var { + // Number of sub-spefications resulting from the decomposition. + // Updated by ltlsynt. + unsigned sub_specs = 0; + // Total time needed for the synthesis. Computed by ltlsynt. double total_time = 0.0; - double trans_time = 0.0; - double split_time = 0.0; - double paritize_time = 0.0; - double solve_time = 0.0; - double strat2aut_time = 0.0; - double simplify_strat_time = 0.0; + // Time needed to transform the LTL formula(s) into automata, summed + // over all subspecs. The type of automaton constructed depends on + // the "algo" parameter. + double sum_trans_time = 0.0; + // Time needed to split the automata into separate + // environment/controler steps. Summed over all subspecs. + // Splitting may occur before or after paritization depending on + // the "algo" parameter. + double sum_split_time = 0.0; + // Time needed to convert the automaton to deterministic parity + // automata. Summed over all subspecs. Paritization may occur + // before or after splitting depending on the "algo" parameter. + double sum_paritize_time = 0.0; + // Time needed to solve the game. Summed over all subspecs. + double sum_solve_time = 0.0; + // Time needed to convert the winning strategy into an + // automaton. Summed over all subspecs. + double sum_strat2aut_time = 0.0; + // Time needed to simplify the winning strategy. Summed over + // all subspecs. + double sum_simplify_strat_time = 0.0; + // Time needed to encode all the strategies into one AIG. double aig_time = 0.0; - unsigned nb_states_arena = 0; - unsigned nb_states_arena_env = 0; - unsigned nb_strat_states = 0; - unsigned nb_strat_edges = 0; - unsigned nb_simpl_strat_states = 0; - unsigned nb_simpl_strat_edges = 0; - unsigned nb_latches = 0; - unsigned nb_gates = 0; + // Size of the automaton resulting from the main translation. + // If multiple subspecifications are used, only the largest + // (states,edges,colors,aps) triplet is kept. + unsigned max_trans_states = 0; + unsigned max_trans_edges = 0; + unsigned max_trans_colors = 0; + unsigned max_trans_ap = 0; + // Size of the game that should be solved. If multiple + // subspecifications are used, only the maximum states and + // colors are kept (those are compared independently). + unsigned max_game_states = 0; + unsigned max_game_colors = 0; + // Size of the strategy extracted from the game. If multiple + // subspecifications are used, only the maximum pair (states, + // edges) is kept. + unsigned max_strat_states = 0; + unsigned max_strat_edges = 0; + // Size of the strategy extracted from the game, summed over all + // subspecifications. + unsigned sum_strat_states = 0; + unsigned sum_strat_edges = 0; + // Size of the strategy after simplification game. If multiple + // subspecifications are used, only the maximum pair (states, + // edges) is kept. + unsigned max_simpl_strat_states = 0; + unsigned max_simpl_strat_edges = 0; + // Size of the strategy after simplification, summed over all + // subspecifications. + unsigned sum_simpl_strat_states = 0; + unsigned sum_simpl_strat_edges = 0; + // Size of the AIG + unsigned aig_latches = 0; + unsigned aig_gates = 0; + // Whether the (global) specification is realizable. Updated by + // ltlsynt. bool realizable = false; }; diff --git a/tests/core/ltlsynt-pgame.test b/tests/core/ltlsynt-pgame.test index 0de7c9497..bdc117b77 100755 --- a/tests/core/ltlsynt-pgame.test +++ b/tests/core/ltlsynt-pgame.test @@ -145,11 +145,12 @@ ltlsynt --from-pgame starve.ehoa \ --from-pgame UnderapproxDemo2.ehoa \ --from-pgame aut7.hoa --csv-without-formula=out.csv >result || : test 4 = `wc -l < out.csv` -cut -d, -f 9,10,11,12,13 right +cut -d, -f 1,2,7,8,9,10,11,12,13 right +REST=strat_states,max_strat_edges,max_simpl_strat_states,max_simpl_strat_edges cat >expect < /->/g;' out > outx diff outx exp -genltl --lily-patterns | ltlsynt -q > out && exit 2 +genltl --lily-patterns | ltlsynt --realizability > out && exit 2 cat >expected <expected < Xo1),lar,1,3 formulas.ltl:2,F(i1 xor i2) <-> Fo1,lar,1,2 formulas.ltl:3,i1 <-> F(o1 xor o2),lar,1,3 @@ -72,7 +72,7 @@ ltlsynt --ins=i1,i2 -F input.csv/-2 --csv=out.csv -q && exit 2 test $? -eq 1 $PYTHON test.py cat >expected < Xo1),lar,1,3 input.csv:3,F(i1 xor i2) <-> Fo1,lar,1,2 input.csv:4,i1 <-> F(o1 xor o2),lar,1,3 @@ -85,7 +85,7 @@ grep -v 0,0 filtered.csv >input.csv ltlsynt -F input.csv/-2 --csv=out.csv -q $PYTHON test.py cat >expected < Xo1),lar,1,3 input.csv:3,F(i1 xor i2) <-> Fo1,lar,1,2 input.csv:4,i1 <-> F(o1 xor o2),lar,1,3 @@ -94,12 +94,12 @@ EOF diff filtered.csv expected ltlsynt -F input.csv/-2 --csv-without-formula=out.csv -q -cut out.csv -d, -f1,2 >filtered.csv +cut out.csv -d, -f1,2,3 >filtered.csv cat >expected <