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 <