From 950b205b6379135b469a2ecb7bcab33e5298c8e5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 9 Sep 2024 16:45:00 +0200 Subject: [PATCH] ltlsynt: have --csv exclude the formula column by default * bin/ltlsynt.cc: Add the --csv-with-formula option. * doc/org/ltlsynt.org, tests/core/ltlsynt2.test, NEWS: Adjust. --- NEWS | 16 +++++------ bin/ltlsynt.cc | 17 ++++++------ doc/org/ltlsynt.org | 58 +++++++++++++++++++--------------------- tests/core/ltlsynt2.test | 9 ++++--- 4 files changed, 50 insertions(+), 50 deletions(-) diff --git a/NEWS b/NEWS index 89330adfb..91c1979cb 100644 --- a/NEWS +++ b/NEWS @@ -8,19 +8,19 @@ New in spot 2.12.0.dev (not yet released) - (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 + output should be more useful when the input specification is 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. + sub-specifications obained, and other statistics columns have + names starting with "max_" or "sum_" indicating how said + statistics are updated across sub-specifications. 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). + the processed formulas as the first column of the CSV file, and + the "formula" column is no longer output by default to save space. + This "formula" column can be added back with the new option + --csv-with-formula=FILENAME if really needed. - 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 0e846c386..4522e4a88 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -49,8 +49,8 @@ enum { OPT_ALGO = 256, OPT_BYPASS, - OPT_CSV, - OPT_CSV_NO_FORMULA, + OPT_CSV_WITH_FORMULA, + OPT_CSV_WITHOUT_FORMULA, OPT_DECOMPOSE, OPT_DOT, OPT_FROM_PGAME, @@ -150,13 +150,14 @@ static const argp_option options[] = "For games and strategies, standard automata rendering " "options are supported (e.g., see ltl2tgba --dot). For AIG circuit, " "use (h) for horizontal and (v) for vertical layouts.", 0 }, - { "csv", OPT_CSV, "[>>]FILENAME", OPTION_ARG_OPTIONAL, + { "csv", OPT_CSV_WITHOUT_FORMULA, "[>>]FILENAME", OPTION_ARG_OPTIONAL, "output statistics as CSV in FILENAME or on standard output " "(if '>>' is used to request append mode, the header line is " "not output)", 0 }, - { "csv-without-formula", OPT_CSV_NO_FORMULA, "[>>]FILENAME", - OPTION_ARG_OPTIONAL, "like --csv, but without 'fomula' column", 0 }, - { "csv-no-formula", 0, nullptr, OPTION_ALIAS, nullptr, 0 }, + { "csv-without-formula", 0, nullptr, OPTION_ALIAS, nullptr, 0 }, + { "csv-with-formula", OPT_CSV_WITH_FORMULA, "[>>]FILENAME", + OPTION_ARG_OPTIONAL, + "like --csv, but with an additional 'fomula' column", 0 }, { "hide-status", OPT_HIDE, nullptr, 0, "Hide the REALIZABLE or UNREALIZABLE line. (Hint: exit status " "is enough of an indication.)", 0 }, @@ -1051,11 +1052,11 @@ parse_opt(int key, char *arg, struct argp_state *) case OPT_BYPASS: opt_bypass = XARGMATCH("--bypass", arg, bypass_args, bypass_values); break; - case OPT_CSV: + case OPT_CSV_WITH_FORMULA: opt_csv = arg ? arg : "-"; opt_csv_with_formula = true; break; - case OPT_CSV_NO_FORMULA: + case OPT_CSV_WITHOUT_FORMULA: opt_csv = arg ? arg : "-"; opt_csv_with_formula = false; break; diff --git a/doc/org/ltlsynt.org b/doc/org/ltlsynt.org index 82a3399c6..f9d5554d0 100644 --- a/doc/org/ltlsynt.org +++ b/doc/org/ltlsynt.org @@ -292,9 +292,7 @@ ltlsynt -f '(i1 & i2) <-> F(o1 & X(!o1))' --print-game-hoa --dot :END: For benchmarking purpose, the =--csv= option can be used to record -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. +intermediate statistics about the resolution. 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 @@ -303,8 +301,7 @@ 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 -q --csv-without-formula=bench.csv + genltl --lily-patterns | ltlsynt --algo=acd -q --csv=bench.csv #+END_SRC #+RESULTS: #+begin_example @@ -351,29 +348,29 @@ s/,/|/g #+RESULTS: | 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 | +| -:1 | 2 | acd | auto | 0.000645823 | 0.000271534 | 2.6961e-05 | 2.8614e-05 | 1.0931e-05 | 0 | 0 | 1 | 0 | 0 | 0 | 3 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | +| -:2 | 2 | acd | auto | 0.000560151 | 0.000345114 | 2.4457e-05 | 3.6228e-05 | 9.639e-06 | 1.1773e-05 | 0 | 5 | 8 | 0 | 1 | 10 | 0 | 2 | 2 | 2 | 2 | 2 | 2 | 2 | 2 | +| -:3 | 1 | acd | auto | 0.0013147 | 0.000951121 | 8.1794e-05 | 3.2291e-05 | 2.9255e-05 | 1.5389e-05 | 1 | 12 | 46 | 1 | 3 | 26 | 1 | 5 | 5 | 5 | 5 | 2 | 4 | 2 | 4 | +| -:4 | 1 | acd | auto | 0.00131727 | 0.000944167 | 9.2395e-05 | 3.6679e-05 | 3.0989e-05 | 1.8685e-05 | 1 | 15 | 62 | 1 | 3 | 33 | 1 | 6 | 6 | 6 | 6 | 3 | 7 | 3 | 7 | +| -:5 | 1 | acd | auto | 0.00137646 | 0.000919601 | 0.000126099 | 4.3342e-05 | 3.4295e-05 | 4.1769e-05 | 1 | 20 | 88 | 1 | 3 | 47 | 1 | 8 | 9 | 8 | 9 | 6 | 17 | 6 | 17 | +| -:6 | 1 | acd | auto | 0.00140189 | 0.000877561 | 0.000128823 | 4.8351e-05 | 3.9455e-05 | 4.5746e-05 | 1 | 24 | 111 | 1 | 3 | 55 | 1 | 11 | 12 | 11 | 12 | 7 | 21 | 7 | 21 | +| -:7 | 1 | acd | auto | 0.00109549 | 0.000722327 | 7.5212e-05 | 2.8033e-05 | 2.3525e-05 | 1.6241e-05 | 1 | 11 | 38 | 1 | 3 | 26 | 1 | 7 | 8 | 7 | 8 | 6 | 14 | 6 | 14 | +| -:8 | 1 | acd | auto | 3.4956e-05 | 2.364e-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.000963203 | 0.00068121 | 4.9574e-05 | 5.1888e-05 | 2.8173e-05 | 1.1412e-05 | 1 | 6 | 19 | 2 | 2 | 16 | 2 | 2 | 3 | 2 | 3 | 2 | 3 | 2 | 3 | +| -:10 | 1 | acd | auto | 5.5886e-05 | 4.098e-06 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 1 | 1 | 1 | +| -:11 | 1 | acd | auto | 0.000113636 | 3.7351e-05 | 1.5379e-05 | 1.1382e-05 | 6.893e-06 | 0 | 0 | 1 | 0 | 0 | 0 | 3 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | +| -:12 | 1 | acd | auto | 4.6338e-05 | 2.535e-06 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 1 | 1 | 1 | +| -:13 | 1 | acd | auto | 0.000361985 | 0.000218364 | 1.7153e-05 | 1.3826e-05 | 8.587e-06 | 8.576e-06 | 1 | 2 | 3 | 1 | 2 | 5 | 1 | 2 | 2 | 2 | 2 | 1 | 2 | 1 | 2 | +| -:14 | 1 | acd | auto | 0.000529893 | 0.000350774 | 1.8105e-05 | 2.3745e-05 | 1.0009e-05 | 7.585e-06 | 1 | 1 | 3 | 2 | 2 | 4 | 1 | 2 | 2 | 2 | 2 | 2 | 2 | 2 | 2 | +| -:15 | 1 | acd | auto | 0.0011819 | 0.000769016 | 0.000107514 | 5.5094e-05 | 3.1399e-05 | 1.9367e-05 | 1 | 8 | 40 | 2 | 4 | 30 | 1 | 7 | 12 | 7 | 12 | 5 | 13 | 5 | 13 | +| -:16 | 1 | acd | auto | 0.00427915 | 0.00279572 | 0.000574768 | 0.000156947 | 0.000103396 | 5.4894e-05 | 1 | 22 | 225 | 3 | 6 | 103 | 1 | 22 | 40 | 22 | 40 | 17 | 71 | 17 | 71 | +| -:17 | 1 | acd | auto | 0.000811907 | 0.000552656 | 2.4486e-05 | 2.9295e-05 | 1.1221e-05 | 8.436e-06 | 1 | 1 | 4 | 3 | 3 | 6 | 1 | 3 | 3 | 3 | 3 | 3 | 3 | 3 | 3 | +| -:18 | 1 | acd | auto | 0.00109892 | 0.000793111 | 3.2972e-05 | 3.3543e-05 | 1.1472e-05 | 9.668e-06 | 1 | 1 | 5 | 4 | 4 | 8 | 1 | 4 | 4 | 4 | 4 | 4 | 4 | 4 | 4 | +| -:19 | 1 | acd | auto | 0.000800405 | 0.00051217 | 4.2461e-05 | 5.0525e-05 | 2.4046e-05 | 1.2293e-05 | 1 | 4 | 15 | 2 | 3 | 11 | 2 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | +| -:20 | 1 | acd | auto | 0.0196147 | 0.0149021 | 0.00268845 | 0.00104262 | 0.000504074 | 2.5819e-05 | 1 | 311 | 3488 | 2 | 5 | 1002 | 2 | 10 | 10 | 10 | 10 | 6 | 12 | 6 | 12 | +| -:21 | 1 | acd | auto | 0.119126 | 0.113659 | 0.00162097 | 0.000147229 | 0.000243901 | 0.000215418 | 1 | 75 | 546 | 1 | 8 | 371 | 1 | 74 | 228 | 74 | 228 | 71 | 339 | 71 | 339 | +| -:22 | 1 | acd | auto | 0.00351029 | 0.00222552 | 0.000303284 | 0.00010043 | 0.000104838 | 5.3962e-05 | 1 | 30 | 161 | 2 | 4 | 86 | 1 | 22 | 25 | 22 | 25 | 15 | 67 | 15 | 67 | +| -:23 | 1 | acd | auto | 0.000890897 | 0.000617519 | 3.165e-05 | 2.9737e-05 | 2.0017e-05 | 1.5259e-05 | 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 @@ -387,8 +384,9 @@ 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 +- =formula= (if requested with option =--csv-with-formula=): is the + actual LTL formula used for the specification, is usually makes the + CSV file very large - =subspecs=: the number of sub-specifications resulting from the decomposition - =algo=: the name of the approach used to construct game, as diff --git a/tests/core/ltlsynt2.test b/tests/core/ltlsynt2.test index 18a2c9ab3..7fe4e86e3 100755 --- a/tests/core/ltlsynt2.test +++ b/tests/core/ltlsynt2.test @@ -31,7 +31,8 @@ i1 <-> F(o1 xor o2) F(i1) <-> G(o2) EOF -ltlsynt --ins=i1,i2 -F formulas.ltl -f 'o1 & F(i1 <-> o2)' -q --csv=out.csv &&\ +ltlsynt --ins=i1,i2 -F formulas.ltl -f 'o1 & F(i1 <-> o2)' -q \ + --csv-with-formula=out.csv &&\ exit 2 test $? -eq 1 || exit 2 @@ -68,7 +69,7 @@ diff filtered.csv expected # ltlfilt should be able to read the second column mv filtered.csv input.csv -ltlsynt --ins=i1,i2 -F input.csv/-2 --csv=out.csv -q && exit 2 +ltlsynt --ins=i1,i2 -F input.csv/-2 --csv-with-formula=out.csv -q && exit 2 test $? -eq 1 $PYTHON test.py cat >expected <input.csv -ltlsynt -F input.csv/-2 --csv=out.csv -q +ltlsynt -F input.csv/-2 --csv-with-formula=out.csv -q $PYTHON test.py cat >expected < o2),lar,1,2 EOF diff filtered.csv expected -ltlsynt -F input.csv/-2 --csv-without-formula=out.csv -q +ltlsynt -F input.csv/-2 --csv=out.csv -q cut out.csv -d, -f1,2,3 >filtered.csv cat >expected <