alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

ltlsynt: have --csv exclude the formula column by default

Browse source 
* bin/ltlsynt.cc: Add the --csv-with-formula option.
* doc/org/ltlsynt.org, tests/core/ltlsynt2.test, NEWS: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2024-09-09 16:45:00 +02:00
parent 5488cb75c6
commit 950b205b63
4 changed files with 50 additions and 50 deletions
Download patch file Download diff file Expand all files Collapse all files

58
doc/org/ltlsynt.org
View file

@ -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