diff --git a/doc/org/ltldo.org b/doc/org/ltldo.org index 785c3b5b5..775e7a9c9 100644 --- a/doc/org/ltldo.org +++ b/doc/org/ltldo.org @@ -574,8 +574,9 @@ dac-patterns:20,ltl2ba #+end_example Note that in case of equality, only the first translator is returned. -So when =ltl2ba= is output above, it could be the case that =ltl3ba= -or =ltl2tgba -s= are also producing automata of equal size. +So when =ltl2ba= is output above, it could be (and it probably is, see +below) the case that =ltl3ba= or =ltl2tgba -s= are also producing +automata of equal size. To understand the above pipeline, remove the =ltldo= invocation. The [[file:genltl.org][=genltl=]] command outputs this: @@ -607,6 +608,65 @@ formula through the three translator, pick the smallest automaton was used (=%T=) along with the portion of the CSV file that was before the input column (=%<=). + +If you are curious about the actually size of the automata produced by +=ltl2ba=, =ltl3ba=, and =ltl2tgba -s= in the above example, you can +quickly build a CSV file using the following pipeline where each +command append a new column. We wrap =ltl2ba= and =ltl3ba= with +=ltldo= so that they can process one column of the CSV that is input, +and output statistics in CSV as output. =ltl2tgba= does not need +that, as it already supports those features. In the resulting CSV +file, displayed as a table below, entries like =2s 4e 0d= represent an +automaton with 2 states, 4 edges, and that is not deterministic. . +(We have a [[file:csv.org][separate page]] with more examples of reading and writing CSV +files.) + +#+NAME: small-bench +#+BEGIN_SRC sh :exports code +echo input,ltl2ba,ltl3ba,ltl2tgba -s +genltl --dac=10..20 --format=%F:%L,%f | + ltldo -F-/2 ltl2ba --stats '%<,%f,%ss %ee %dd' | + ltldo -F-/2 ltl3ba --stats '%<,%f,%>,%ss %ee %dd' | + ltl2tgba -s -F-/2 --stats '%<,%>,%ss %ee %dd' +#+END_SRC + +#+BEGIN_SRC sh :results output raw :exports results :noweb yes +sed ' +$d +s/|/\\vert{}/g +s/--/@@html:--@@/g +s/^/| / +s/$/ |/ +s/,/|/g +s/"//g +1a\ +|-|\ +||||| +' <> +EOF +#+END_SRC + +#+ATTR_HTML: :class table-pre +#+RESULTS: +| input | ltl2ba | ltl3ba | ltl2tgba -s | +|-----------------+------------+------------+-------------| +| | | | | +| dac-patterns:10 | 2s 4e 0d | 2s 4e 1d | 2s 4e 1d | +| dac-patterns:11 | 5s 9e 1d | 5s 9e 1d | 5s 9e 1d | +| dac-patterns:12 | 8s 29e 0d | 8s 20e 0d | 7s 17e 1d | +| dac-patterns:13 | 8s 17e 0d | 8s 17e 0d | 6s 12e 1d | +| dac-patterns:14 | 16s 62e 0d | 11s 33e 0d | 7s 19e 1d | +| dac-patterns:15 | 10s 47e 0d | 10s 41e 0d | 6s 17e 1d | +| dac-patterns:16 | 1s 1e 1d | 1s 1e 1d | 1s 1e 1d | +| dac-patterns:17 | 4s 7e 0d | 4s 7e 0d | 3s 5e 1d | +| dac-patterns:18 | 2s 3e 0d | 2s 3e 1d | 2s 3e 1d | +| dac-patterns:19 | 4s 8e 0d | 3s 6e 0d | 3s 7e 1d | +| dac-patterns:20 | 2s 4e 0d | 2s 4e 1d | 2s 4e 1d | + +#+ATTR_HTML: :class table-pre +#+RESULTS: + * Controlling and measuring time The run time of each command can be restricted with the =-T NUM= diff --git a/doc/org/spot.css b/doc/org/spot.css index 78a03f19d..5602cc6c7 100644 --- a/doc/org/spot.css +++ b/doc/org/spot.css @@ -26,9 +26,9 @@ pre.src-C\+\+:before{content:'C++'} pre.src-hoa:before{content:'HOA';border-color:#d70079} img{max-width:100%} svg.org-svg{width:auto;max-width:100%} -table.csv-table {font-family:monospace, courier} -table.csv-table th {vertical-align:bottom} -table.csv-table th div {text-align:center} +table.csv-table,table.table-pre{font-family:monospace, courier} +table.csv-table th{vertical-align:bottom} +table.csv-table th div{text-align:center} table.csv-table th div span{text-align:left;writing-mode:vertical-lr;transform:rotate(180deg);display:inline-block;white-space:nowrap} @media screen{ #table-of-contents{position:fixed;right:0em;top:0em;max-width:50%;max-height:80%;overflow:auto;z-index:10}