diff --git a/NEWS b/NEWS index 012ca6f32..e8f01b7ca 100644 --- a/NEWS +++ b/NEWS @@ -9,7 +9,9 @@ New in spot 2.12.0.dev (not yet released) 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). + 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. - 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 ee985b4be..7e1cfb5b2 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -349,8 +349,8 @@ namespace { auto& vs = gi->verbose_stream; auto& bv = gi->bv; - if (not bv) - error(2, 0, "no information available for csv (please send bug report)"); + if (!bv) + error(2, 0, "no information available for csv (please report bug)"); if (vs) *vs << "writing CSV to " << opt_csv << '\n'; @@ -377,10 +377,11 @@ namespace out << ",\"aig_time\""; out << ",\"realizable\""; //-1: Unknown, 0: Unreal, 1: Real } - out << ",\"dpa_num_states\",\"dpa_num_states_env\"" - << ",\"strat_num_states\",\"strat_num_edges\""; + out << ",\"game_states\",\"game_states_env\""; + if (!opt_real) + out << ",\"strat_states\",\"strat_edges\""; if (opt_print_aiger) - out << ",\"nb latches\",\"nb gates\""; + out << ",\"aig_latches\",\"aig_gates\""; out << '\n'; } { @@ -418,15 +419,13 @@ namespace out << ',' << bv->realizable; } out << ',' << bv->nb_states_arena - << ',' << bv->nb_states_arena_env - << ',' << bv->nb_strat_states - << ',' << bv->nb_strat_edges; - + << ',' << bv->nb_states_arena_env; + if (!opt_real) + out << ',' << bv->nb_strat_states + << ',' << bv->nb_strat_edges; if (opt_print_aiger) - { out << ',' << bv->nb_latches << ',' << bv->nb_gates; - } out << '\n'; outf.close(opt_csv); } @@ -608,8 +607,6 @@ namespace safe_tot_time(); return 1; } - if (gi->bv) - gi->bv->realizable = true; // Create the (partial) strategy // only if we need it if (!opt_real) @@ -654,6 +651,8 @@ namespace "(please send bug report)"); } } + if (gi->bv) + gi->bv->realizable = true; // If we only wanted to print the game we are done if (want_game()) diff --git a/doc/org/ltlsynt.org b/doc/org/ltlsynt.org index 93c92e29b..0230d0b11 100644 --- a/doc/org/ltlsynt.org +++ b/doc/org/ltlsynt.org @@ -268,6 +268,8 @@ be tried by separating them using commas. For instance * Other useful options +** Printing games + You can also ask =ltlsynt= to print to obtained parity game into [[https://github.com/tcsprojects/pgsolver][PGSolver]] format, with the flag =--print-pg=, or in the HOA format, using =--print-game-hoa=. These flags deactivate the resolution of the @@ -284,8 +286,102 @@ ltlsynt -f '(i1 & i2) <-> F(o1 & X(!o1))' --print-game-hoa --dot #+RESULTS: [[file:ltlsyntexgame.svg]] +** Saving statistics + For benchmarking purpose, the =--csv= option can be used to record -intermediate statistics about the resolution. +intermediate statistics about the resolution. The =--csv= option will +also save the formula into the CSV file, which can therefore become +very large. The variant =--csv-without-formula= is usually enough. + +For instance the following command tests the realizability of the 23 +demonstration specifications from [[http://www.ist.tugraz.at/staff/jobstmann/lily/][Lily 1.0.2]] while saving some +statistics in =bench.csv=. (If you compare our results with theirs, +keep in mind that Lily uses Moore's semantics, while =ltlsynt= uses +Mealy's semantics.) + +#+BEGIN_SRC sh :results verbatim :exports code :epilogue true + genltl --lily-patterns | + ltlsynt --algo=acd --realizability --csv-without-formula=bench.csv +#+END_SRC +#+RESULTS: +#+begin_example +UNREALIZABLE +UNREALIZABLE +REALIZABLE +REALIZABLE +REALIZABLE +REALIZABLE +REALIZABLE +REALIZABLE +REALIZABLE +REALIZABLE +UNREALIZABLE +REALIZABLE +REALIZABLE +REALIZABLE +REALIZABLE +REALIZABLE +REALIZABLE +REALIZABLE +REALIZABLE +REALIZABLE +REALIZABLE +REALIZABLE +REALIZABLE +#+end_example + +After execution, =bench.csv= contains a table like the following: + +#+BEGIN_SRC sh :results output raw :exports results +sed 's/"//g +s/|/\\vert{}/g +s/--/@@html:--@@/g +1a\ +|-| +s/^/| / +s/$/ |/ +s/,/|/g +' bench.csv +#+END_SRC + +#+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 | + +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 The =--verify= option requests that the produced strategy or aiger circuit are compatible with the specification. This is done by diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc index 6b5fa7af9..b2b54fcf3 100644 --- a/spot/twaalgos/synthesis.cc +++ b/spot/twaalgos/synthesis.cc @@ -2215,17 +2215,6 @@ namespace spot (twa_graph_ptr strat) { dict->unregister_all_my_variables(&tmp); - if (vs) - { - *vs << "direct strategy was found.\n"; - if (want_strategy) - { - *vs << "direct strat has " << strat->num_states() - << " states, " << strat->num_edges() - << " edges and " << strat->num_sets() << " colors\n"; - - } - } if (strat) { strat->merge_edges(); @@ -2238,6 +2227,13 @@ namespace spot set_synthesis_outputs(strat, outputs); } + if (vs) + { + *vs << "direct strategy was found.\n"; + if (strat && want_strategy) + *vs << "direct strategy has " << strat->num_states() + << " states and " << strat->num_edges() << " edges\n"; + } return mealy_like{ mealy_like::realizability_code::REALIZABLE_REGULAR, strat, @@ -2383,15 +2379,19 @@ namespace spot auto res = trans.run(f_left); if (!is_deterministic(res)) - return ret_sol_maybe(); + { + if (bv) + { + auto delta = sw.stop(); + bv->trans_time += delta; + if (vs) + *vs << "translating formula done in " << delta + << " seconds...\n... but it gave a " + << "non-deterministic automaton (rejected)\n"; + } + return ret_sol_maybe(); + } - if (bv) - { - auto delta = sw.stop(); - bv->trans_time += delta; - if (vs) - *vs << "translating formula done in " << delta << " seconds\n"; - } res->prop_complete(trival::maybe()); bdd output_bdd = bddtrue; @@ -2442,12 +2442,23 @@ namespace spot res->prop_terminal(trival::maybe()); res->set_named_prop("synthesis-outputs", new bdd(output_bdd)); + if (bv) + { + auto delta = sw.stop(); + bv->trans_time += delta; + if (vs) + *vs << "translating formula done in " << delta << " seconds\n"; + } return ret_sol_exists(res); } else if (f_other.is_tt()) { if (!want_strategy) return ret_sol_exists(nullptr); + stopwatch sw; + if (bv) + sw.start(); + auto res = make_twa_graph(dict); res->prop_weak(true); @@ -2463,6 +2474,13 @@ namespace spot bdd g_bdd = formula_to_bdd(f_g, dict, res); res->new_state(); res->new_edge(0, 0, g_bdd); + if (bv) + { + auto delta = sw.stop(); + bv->trans_time += delta; + if (vs) + *vs << "translating formula done in " << delta << " seconds\n"; + } return ret_sol_exists(res); } return ret_sol_maybe(); diff --git a/tests/core/ltlsynt-pgame.test b/tests/core/ltlsynt-pgame.test index 900e90120..0de7c9497 100755 --- a/tests/core/ltlsynt-pgame.test +++ b/tests/core/ltlsynt-pgame.test @@ -143,12 +143,11 @@ test 4 = `wc -l < out.csv` ltlsynt --from-pgame starve.ehoa \ --from-pgame UnderapproxDemo2.ehoa \ - --from-pgame aut7.hoa --csv=out.csv >result || : + --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 -end='"strat_num_states","strat_num_edges"' cat >expect < GFb translating formula done in X seconds direct strategy was found. -direct strat has 1 states, 2 edges and 0 colors +direct strategy has 1 states and 1 edges simplification took X seconds EOF ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --verbose --algo=ps 2> out @@ -660,7 +660,7 @@ there are 1 subformulas trying to create strategy directly for GFa <-> GFb translating formula done in X seconds direct strategy was found. -direct strat has 1 states, 2 edges and 0 colors +direct strategy has 1 states and 1 edges simplification took X seconds EOF ltlsynt -f '(GFa <-> GFb) && (G(c <-> d))' --outs=b,c --verbose 2> out @@ -676,7 +676,7 @@ do trying to create strategy directly for $f translating formula done in X seconds direct strategy was found. -direct strat has 1 states, 2 edges and 0 colors +direct strategy has 1 states and 1 edges simplification took X seconds EOF ltlsynt -f "$f" --outs=b,c --verbose --decompose=0 \ @@ -705,7 +705,7 @@ cat >exp < GFa) & G((a & c) | (!a & !c)) translating formula done in X seconds direct strategy was found. -direct strat has 1 states, 2 edges and 0 colors +direct strategy has 1 states and 1 edges simplification took X seconds EOF ltlsynt -f '(GFb <-> GFa) && (G((a&c)|(!a&!c)))' --outs=b,c --verbose\ @@ -719,7 +719,7 @@ cat >exp < FGb translating formula done in X seconds direct strategy was found. -direct strat has 2 states, 3 edges and 0 colors +direct strategy has 2 states and 3 edges simplification took X seconds EOF ltlsynt -f "Fa <-> FGb" --outs=b,c --verbose --decompose=0 --verify 2> out @@ -789,8 +789,9 @@ new formula: x & y new formula: 1 there are 1 subformulas trying to create strategy directly for 1 +translating formula done in X seconds direct strategy was found. -direct strat has 1 states, 1 edges and 0 colors +direct strategy has 1 states and 1 edges simplification took X seconds AIG circuit was created in X seconds and has 0 latches and 0 gates EOF @@ -804,13 +805,15 @@ cat >exp < GFo1 translating formula done in X seconds direct strategy was found. -direct strat has 1 states, 2 edges and 0 colors +direct strategy has 1 states and 1 edges simplification took X seconds EOF ltlsynt -f "G(o1|o2) & (GFi <-> GFo1)" --outs="o1,o2" --verbose\ @@ -1255,8 +1258,9 @@ new formula: G(o1 | !o2) & G(!o1 | o2) o2 := o1 new formula: G(o1 | !o1) trying to create strategy directly for G(o1 | !o1) +translating formula done in X seconds direct strategy was found. -direct strat has 1 states, 1 edges and 0 colors +direct strategy has 1 states and 1 edges simplification took X seconds working on subformula G(!i1 -> (o3 | !o4)) & G(!i2 -> (!o3 | o4)) the following signals can be temporarily removed: @@ -1266,8 +1270,9 @@ new formula: G(o3 | !o4) & G(!o3 | o4) o4 := o3 new formula: G(o3 | !o3) trying to create strategy directly for G(o3 | !o3) +translating formula done in X seconds direct strategy was found. -direct strat has 1 states, 1 edges and 0 colors +direct strategy has 1 states and 1 edges simplification took X seconds REALIZABLE HOA: v1 @@ -1298,13 +1303,15 @@ new formula: G(i1->(o1 | !o2)) & G(!i1->(o3 | !o4)) & $gg there are 2 subformulas working on subformula G(i1->(o1 | !o2)) & G(i2->(!o1 | o2)) trying to create strategy directly for G(i1->(o1 | !o2)) & G(i2->(!o1 | o2)) +translating formula done in X seconds direct strategy was found. -direct strat has 1 states, 1 edges and 0 colors +direct strategy has 1 states and 1 edges simplification took X seconds working on subformula G(!i1->(o3 | !o4)) & G(!i2->(!o3 | o4)) trying to create strategy directly for G(!i1->(o3 | !o4)) & G(!i2->(!o3 | o4)) +translating formula done in X seconds direct strategy was found. -direct strat has 1 states, 1 edges and 0 colors +direct strategy has 1 states and 1 edges simplification took X seconds REALIZABLE HOA: v1 diff --git a/tests/core/ltlsynt2.test b/tests/core/ltlsynt2.test index 108cb5f94..c43f928c5 100755 --- a/tests/core/ltlsynt2.test +++ b/tests/core/ltlsynt2.test @@ -48,7 +48,7 @@ except ImportError: x = pandas.read_csv("out.csv") x.to_csv('filtered.csv', columns=('source', 'formula', 'algo', - 'realizable', 'strat_num_states'), + 'realizable', 'strat_states'), index=False) EOF @@ -56,7 +56,7 @@ EOF $PYTHON test.py cat >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