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

ltlcross: count SCCs of various strenghts

Browse source 
* src/bin/ltlcross.cc: Implement the counters.
* doc/org/ltlcross.org: Update the documentation.
* bench/ltl2tgba/sum.py: Do not assume a fixed column for the time.
* NEWS: Update.
This commit is contained in:
Alexandre Duret-Lutz 2013-04-27 20:33:51 +02:00
parent cb7cd868a5
commit fec939c1a6
4 changed files with 133 additions and 79 deletions
Download patch file Download diff file Expand all files Collapse all files

4
NEWS
View file

@ -82,6 +82,10 @@ New in spot 1.0.2a (not released):
are required to make the format usable for other benchmarks (not are required to make the format usable for other benchmarks (not
just ltlcross). just ltlcross).
- ltlcross will now count the number of non-accepting, terminal,
weak, and strong SCCs, as well as the number of terminal, weak,
and strong automata produced by each tool.
* Documentation: * Documentation:
- org-mode files used to generate the documentation about - org-mode files used to generate the documentation about

4
bench/ltl2tgba/sum.py
View file

@ -65,6 +65,8 @@ def process_file(filename):
name = name[name.rfind('/', 0, name.find(' ')) + 1:] name = name[name.rfind('/', 0, name.find(' ')) + 1:]
data["tool"][i] = latex_escape(name[0:name.find('%')]) data["tool"][i] = latex_escape(name[0:name.find('%')])
timecol = fields['time']
print(r''' print(r'''
\section*{\texttt{%s}} \section*{\texttt{%s}}
\subsection*{Cumulative summary}''' % latex_escape(filename)) \subsection*{Cumulative summary}''' % latex_escape(filename))
@ -74,7 +76,7 @@ def process_file(filename):
"\\\\") "\\\\")
for i in range(0, ntools): for i in range(0, ntools):
# Compute sums over each column. # Compute sums over each column.
sums = [("%6.2f" if j == 9 else "%6d") % sums = [("%6.2f" if j == timecol else "%6d") %
(sum([x[j] for x in results[i].values()])) (sum([x[j] for x in results[i].values()]))
for j in datacols] for j in datacols]
print("\\texttt{%-18s} & %3d & " print("\\texttt{%-18s} & %3d & "

158
doc/org/ltlcross.org
View file

@ -10,16 +10,20 @@ same sanity checks.
The main motivations for rewriting this tool were: The main motivations for rewriting this tool were:
- support for PSL formulas in addition to LTL - support for PSL formulas in addition to LTL
- more statistics (like counting the number of logical transitions - more statistics, especially:
represented by each physical edge), output in a format that - the number of logical transitions represented by each physical edge,
can be more easily be post-processed, - the number of deterministic states and automata
- the number of SCCs with their various strengths (nonaccepting, terminal, weak, strong)
- the number of terminal, weak, and strong automata
- output in a format that can be more easily be post-processed,
- more precise time measurement (LBTT was only precise to - more precise time measurement (LBTT was only precise to
1/100 of a second, reporting most times as "0.00s"). 1/100 of a second, reporting most times as "0.00s").
Although =ltlcross= performs the same sanity checks as LBTT, it does Although =ltlcross= performs the same sanity checks as LBTT, it does
not implement any of the interactive features of LBTT. Essentially not implement any of the interactive features of LBTT. In our almost
=ltlcross= will report problems, but you will be on your own to 10-year usage of LBTT, we never had to use its interactive features to
investigate and fix them. understand bugs in our translation. Therefore =ltlcross= will report
problems, but you will be on your own to investigate and fix them.
The core of =ltlcross= is a loop that does the following steps: The core of =ltlcross= is a loop that does the following steps:
- Input a formula - Input a formula
@ -106,8 +110,8 @@ product of that resulting automaton with the random state-space, can
be obtained using the =--csv=FILE= or =--json=FILE= option. be obtained using the =--csv=FILE= or =--json=FILE= option.
The following compare =ltl2tgba=, =spin=, and =lbt= on three random The following compare =ltl2tgba=, =spin=, and =lbt= on three random
formula (where =W= and =M= operators have been removed because they formula (where =W= and =M= operators have been rewritten away because
are not supported by =spin= and =lbt=). they are not supported by =spin= and =lbt=).
#+BEGIN_SRC sh :results verbatim :exports code #+BEGIN_SRC sh :results verbatim :exports code
randltl -n 2 a b | randltl -n 2 a b |
@ -128,25 +132,25 @@ ltlcross --csv=results.csv --json=results.json \
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:
#+begin_example #+begin_example
-:1: (G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1))))))) -:1: (G((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) R ((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) | (X(p1)))))
Running [P0]: ltl2tgba -s '(G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1)))))))' >'lck-o0-eGEYaZ' Running [P0]: ltl2tgba -s '(G((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) R ((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) | (X(p1)))))' >'lck-o0-HcRzrd'
Running [P1]: spin -f '([](((p0) U ((p0) && ([](p1)))) V (([](p1)) || ((p0) U ((p0) && ([](p1)))))))' >'lck-o1-nYpFBX' Running [P1]: spin -f '([]((((p0) && (<>(p1))) U ((p1) U ((p1) && ((!(p2)) V (p0))))) V ((((p0) && (<>(p1))) U ((p1) U ((p1) && ((!(p2)) V (p0))))) || (X(p1)))))' >'lck-o1-Sir9YC'
Running [P2]: lbt < 'lck-i0-fGdZQ0' >'lck-o2-CPs23V' Running [P2]: lbt < 'lck-i0-W7LdjO' >'lck-o2-ZACV3b'
Running [N0]: ltl2tgba -s '(!(G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1))))))))' >'lck-o0-kXiZZS' Running [N0]: ltl2tgba -s '(!(G((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) R ((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) | (X(p1))))))' >'lck-o0-KoveKk'
Running [N1]: spin -f '(!([](((p0) U ((p0) && ([](p1)))) V (([](p1)) || ((p0) U ((p0) && ([](p1))))))))' >'lck-o1-7ILLzR' Running [N1]: spin -f '(!([]((((p0) && (<>(p1))) U ((p1) U ((p1) && ((!(p2)) V (p0))))) V ((((p0) && (<>(p1))) U ((p1) U ((p1) && ((!(p2)) V (p0))))) || (X(p1))))))' >'lck-o1-xxXdfU'
Running [N2]: lbt < 'lck-i0-9KG0wU' >'lck-o2-CcMCaQ' Running [N2]: lbt < 'lck-i0-tcO4oL' >'lck-o2-QQUs0t'
Performing sanity checks and gathering statistics... Performing sanity checks and gathering statistics...
-:2: (!((G(F(p0))) -> (F(p1)))) -:2: (!(((!(G((p0) | (F(p1))))) <-> ((p0) | (X(p1)))) -> (!(p1))))
Running [P0]: ltl2tgba -s '(!((G(F(p0))) -> (F(p1))))' >'lck-o0-IOckzW' Running [P0]: ltl2tgba -s '(!(((!(G((p0) | (F(p1))))) <-> ((p0) | (X(p1)))) -> (!(p1))))' >'lck-o0-qlcvic'
Running [P1]: spin -f '(!((<>(p1)) || (!([](<>(p0))))))' >'lck-o1-tsT3RZ' Running [P1]: spin -f '(!((!(p1)) || (!(((!([]((p0) || (<>(p1))))) && ((p0) || (X(p1)))) || (([]((p0) || (<>(p1)))) && (!((p0) || (X(p1)))))))))' >'lck-o1-fEBqz3'
Running [P2]: lbt < 'lck-i1-5TJXmT' >'lck-o2-5E9jb3' Running [P2]: lbt < 'lck-i1-sint9k' >'lck-o2-6oY4RU'
Running [N0]: ltl2tgba -s '(G(F(p0))) -> (F(p1))' >'lck-o0-M3XRO9' Running [N0]: ltl2tgba -s '((!(G((p0) | (F(p1))))) <-> ((p0) | (X(p1)))) -> (!(p1))' >'lck-o0-6PQGuD'
Running [N1]: spin -f '(<>(p1)) || (!([](<>(p0))))' >'lck-o1-6nxqfd' Running [N1]: spin -f '(!(p1)) || (!(((!([]((p0) || (<>(p1))))) && ((p0) || (X(p1)))) || (([]((p0) || (<>(p1)))) && (!((p0) || (X(p1)))))))' >'lck-o1-1l4NVu'
Running [N2]: lbt < 'lck-i1-4hS5u6' >'lck-o2-vNItGg' Running [N2]: lbt < 'lck-i1-iEEnbM' >'lck-o2-a2Toum'
Performing sanity checks and gathering statistics... Performing sanity checks and gathering statistics...
no problem detected No problem detected.
#+end_example #+end_example
After this execution, the file =results.csv= contains the following: After this execution, the file =results.csv= contains the following:
@ -156,19 +160,19 @@ cat results.csv
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:
#+begin_example #+begin_example
"formula", "tool", "states", "edges", "transitions", "acc", "scc", "nondetstates", "nondeterministic", "time", "product_states", "product_transitions", "product_scc" "formula", "tool", "states", "edges", "transitions", "acc", "scc", "nonacc_scc", "terminal_scc", "weak_scc", "strong_scc", "nondetstates", "nondeterministic", "terminal_aut", "weak_aut", "strong_aut", "time", "product_states", "product_transitions", "product_scc"
"(G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1)))))))", "ltl2tgba -s %f >%N", 3, 5, 9, 1, 3, 2, 1, 0.0453898, 401, 5136, 3 "(G((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) R ((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) | (X(p1)))))", "ltl2tgba -s %f >%N", 7, 27, 42, 1, 1, 0, 0, 0, 1, 5, 1, 0, 0, 1, 0.162927, 1333, 20565, 3
"(G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1)))))))", "spin -f %s >%N", 6, 13, 18, 1, 3, 6, 1, 0.0108596, 995, 14384, 5 "(G((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) R ((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) | (X(p1)))))", "spin -f %s >%N", 55, 957, 1723, 1, 1, 0, 0, 0, 1, 55, 1, 0, 0, 1, 3.83261, 10791, 866615, 37
"(G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1)))))))", "lbt < %L >%T", 8, 41, 51, 1, 3, 8, 1, 0.00343479, 1389, 42998, 5 "(G((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) R ((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) | (X(p1)))))", "lbt < %L >%T", 167, 5656, 10744, 3, 2, 1, 0, 0, 1, 167, 1, 0, 0, 1, 0.0365079, 32258, 5318535, 96
"(!(G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1))))))))", "ltl2tgba -s %f >%N", 4, 10, 16, 1, 3, 0, 0, 0.0437875, 797, 16340, 3 "(!(G((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) R ((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) | (X(p1))))))", "ltl2tgba -s %f >%N", 11, 28, 72, 1, 10, 6, 1, 2, 1, 1, 1, 0, 0, 1, 0.0628941, 2163, 36722, 594
"(!(G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1))))))))", "spin -f %s >%N", 7, 24, 63, 1, 4, 6, 1, 0.0061535, 1400, 64668, 4 "(!(G((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) R ((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) | (X(p1))))))", "spin -f %s >%N", 23, 113, 331, 1, 14, 9, 1, 1, 3, 20, 1, 0, 0, 1, 0.101343, 4567, 171114, 1193
"(!(G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1))))))))", "lbt < %L >%T", 39, 286, 614, 3, 28, 33, 1, 0.00384434, 7592, 602204, 4400 "(!(G((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) R ((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) | (X(p1))))))", "lbt < %L >%T", 157, 2414, 5957, 3, 109, 103, 1, 1, 4, 133, 1, 0, 0, 1, 0.0197828, 30811, 3020266, 19147
"(!((G(F(p0))) -> (F(p1))))", "ltl2tgba -s %f >%N", 2, 4, 4, 1, 1, 0, 0, 0.0416853, 398, 4198, 1 "(!(((!(G((p0) | (F(p1))))) <-> ((p0) | (X(p1)))) -> (!(p1))))", "ltl2tgba -s %f >%N", 6, 12, 21, 1, 5, 3, 0, 1, 1, 1, 1, 0, 0, 1, 0.0509422, 806, 15638, 9
"(!((G(F(p0))) -> (F(p1))))", "spin -f %s >%N", 2, 3, 5, 1, 1, 1, 1, 0.00325558, 398, 5227, 1 "(!(((!(G((p0) | (F(p1))))) <-> ((p0) | (X(p1)))) -> (!(p1))))", "spin -f %s >%N", 11, 21, 47, 1, 8, 6, 0, 1, 1, 7, 1, 0, 0, 1, 0.0102468, 1217, 36416, 20
"(!((G(F(p0))) -> (F(p1))))", "lbt < %L >%T", 5, 10, 15, 1, 4, 5, 1, 0.00299424, 409, 6401, 12 "(!(((!(G((p0) | (F(p1))))) <-> ((p0) | (X(p1)))) -> (!(p1))))", "lbt < %L >%T", 17, 45, 100, 2, 13, 11, 0, 1, 1, 14, 1, 0, 0, 1, 0.00346881, 1744, 57783, 347
"(G(F(p0))) -> (F(p1))", "ltl2tgba -s %f >%N", 3, 5, 11, 1, 3, 1, 1, 0.0422192, 600, 11663, 3 "((!(G((p0) | (F(p1))))) <-> ((p0) | (X(p1)))) -> (!(p1))", "ltl2tgba -s %f >%N", 7, 14, 28, 1, 6, 3, 1, 1, 1, 2, 1, 0, 0, 1, 0.0503676, 1006, 19822, 10
"(G(F(p0))) -> (F(p1))", "spin -f %s >%N", 3, 5, 14, 1, 3, 1, 1, 0.00293655, 600, 14840, 3 "((!(G((p0) | (F(p1))))) <-> ((p0) | (X(p1)))) -> (!(p1))", "spin -f %s >%N", 17, 43, 102, 1, 13, 10, 1, 1, 1, 12, 1, 0, 0, 1, 0.0474604, 2449, 70190, 256
"(G(F(p0))) -> (F(p1))", "lbt < %L >%T", 11, 18, 54, 2, 11, 5, 1, 0.0030133, 1253, 26891, 457 "((!(G((p0) | (F(p1))))) <-> ((p0) | (X(p1)))) -> (!(p1))", "lbt < %L >%T", 23, 68, 154, 2, 19, 16, 1, 1, 1, 18, 1, 0, 0, 1, 0.0037305, 2236, 73111, 640
#+end_example #+end_example
This can be loaded in any spreadsheet application. Although we only This can be loaded in any spreadsheet application. Although we only
@ -185,47 +189,52 @@ cat results.json
#+RESULTS: #+RESULTS:
#+begin_example #+begin_example
{ {
"tools": [ "tool": [
"ltl2tgba -s %f >%N", "ltl2tgba -s %f >%N",
"spin -f %s >%N", "spin -f %s >%N",
"lbt < %L >%T" "lbt < %L >%T"
], ],
"inputs": [ "formula": [
"(G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1)))))))", "(G((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) R ((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) | (X(p1)))))",
"(!(G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1))))))))", "(!(G((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) R ((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) | (X(p1))))))",
"(!((G(F(p0))) -> (F(p1))))", "(!(((!(G((p0) | (F(p1))))) <-> ((p0) | (X(p1)))) -> (!(p1))))",
"(G(F(p0))) -> (F(p1))" "((!(G((p0) | (F(p1))))) <-> ((p0) | (X(p1)))) -> (!(p1))"
], ],
"fields": [ "fields": [
"input", "tool", "states", "edges", "transitions", "acc", "scc", "nondetstates", "nondeterministic", "time", "product_states", "product_transitions", "product_scc" "formula", "tool", "states", "edges", "transitions", "acc", "scc", "nonacc_scc", "terminal_scc", "weak_scc", "strong_scc", "nondetstates", "nondeterministic", "terminal_aut", "weak_aut", "strong_aut", "time", "product_states", "product_transitions", "product_scc"
], ],
"inputs": [ 0, 1 ],
"results": [ "results": [
[ 0, 0, 3, 5, 9, 1, 3, 2, 1, 0.0431589, 401, 5136, 3 ], [ 0, 0, 7, 27, 42, 1, 1, 0, 0, 0, 1, 5, 1, 0, 0, 1, 0.162927, 1333, 20565, 3 ],
[ 0, 1, 6, 13, 18, 1, 3, 6, 1, 0.0104812, 995, 14384, 5 ], [ 0, 1, 55, 957, 1723, 1, 1, 0, 0, 0, 1, 55, 1, 0, 0, 1, 3.83261, 10791, 866615, 37 ],
[ 0, 2, 8, 41, 51, 1, 3, 8, 1, 0.00321619, 1389, 42998, 5 ], [ 0, 2, 167, 5656, 10744, 3, 2, 1, 0, 0, 1, 167, 1, 0, 0, 1, 0.0365079, 32258, 5318535, 96 ],
[ 1, 0, 4, 10, 16, 1, 3, 0, 0, 0.0443761, 797, 16340, 3 ], [ 1, 0, 11, 28, 72, 1, 10, 6, 1, 2, 1, 1, 1, 0, 0, 1, 0.0628941, 2163, 36722, 594 ],
[ 1, 1, 7, 24, 63, 1, 4, 6, 1, 0.00623927, 1400, 64668, 4 ], [ 1, 1, 23, 113, 331, 1, 14, 9, 1, 1, 3, 20, 1, 0, 0, 1, 0.101343, 4567, 171114, 1193 ],
[ 1, 2, 39, 286, 614, 3, 28, 33, 1, 0.00386306, 7592, 602204, 4400 ], [ 1, 2, 157, 2414, 5957, 3, 109, 103, 1, 1, 4, 133, 1, 0, 0, 1, 0.0197828, 30811, 3020266, 19147 ],
[ 2, 0, 2, 4, 4, 1, 1, 0, 0, 0.0414639, 398, 4198, 1 ], [ 2, 0, 6, 12, 21, 1, 5, 3, 0, 1, 1, 1, 1, 0, 0, 1, 0.0509422, 806, 15638, 9 ],
[ 2, 1, 2, 3, 5, 1, 1, 1, 1, 0.00327304, 398, 5227, 1 ], [ 2, 1, 11, 21, 47, 1, 8, 6, 0, 1, 1, 7, 1, 0, 0, 1, 0.0102468, 1217, 36416, 20 ],
[ 2, 2, 5, 10, 15, 1, 4, 5, 1, 0.00322862, 409, 6401, 12 ], [ 2, 2, 17, 45, 100, 2, 13, 11, 0, 1, 1, 14, 1, 0, 0, 1, 0.00346881, 1744, 57783, 347 ],
[ 3, 0, 3, 5, 11, 1, 3, 1, 1, 0.0432979, 600, 11663, 3 ], [ 3, 0, 7, 14, 28, 1, 6, 3, 1, 1, 1, 2, 1, 0, 0, 1, 0.0503676, 1006, 19822, 10 ],
[ 3, 1, 3, 5, 14, 1, 3, 1, 1, 0.00296043, 600, 14840, 3 ], [ 3, 1, 17, 43, 102, 1, 13, 10, 1, 1, 1, 12, 1, 0, 0, 1, 0.0474604, 2449, 70190, 256 ],
[ 3, 2, 11, 18, 54, 2, 11, 5, 1, 0.00295457, 1253, 26891, 457 ] [ 3, 2, 23, 68, 154, 2, 19, 16, 1, 1, 1, 18, 1, 0, 0, 1, 0.0037305, 2236, 73111, 640 ]
] ]
} }
#+end_example #+end_example
Here the =fields= table describes the columns of the =results= table, Here the =fields= table describes the columns of the =results= table.
and the =input= and =tool= columns contains indices relative to the The =inputs= tables lists the columns that are considered as inputs
=inputs= and =tools= table. This format is more compact when dealing for the experiments. The values in the columns corresponding to the
with lots of translators and formulas, because they don't have to be fields =formula= and =tool= contains indices relative to the =formula=
repeated on each line as in the CSV version. and =tool= tables. This format is more compact when dealing with lots
of translators and formulas, because they don't have to be repeated on
each line as in the CSV version.
JSON data can be easily processed in any language. For instance the JSON data can be easily processed in any language. For instance the
following Python3 script averages each column for each tool, following Python3 script averages each column for each tool, and
and presents the results in a form that can almost be copied into a presents the results in a form that can almost be copied into a LaTeX
LaTeX table (the =%= in the tool names have to be taken care of). table (the =%= in the tool names have to be taken care of). Note that
for simplicity we assume that the first two columns are inputs,
instead of reading the =inputs= field.
#+BEGIN_SRC python :results output :exports both #+BEGIN_SRC python :results output :exports both
#!/usr/bin/python3 #!/usr/bin/python3
@ -233,24 +242,23 @@ import json
data = json.load(open('results.json')) data = json.load(open('results.json'))
datacols = range(2, len(data["fields"])) datacols = range(2, len(data["fields"]))
# Index results by tool # Index results by tool
results = { t:[] for t in range(0, len(data["tools"])) } results = { t:[] for t in range(0, len(data["tool"])) }
for l in data["results"]: for l in data["results"]:
results[l[1]].append(l) results[l[1]].append(l)
# Average columns for each tools, and display them as a table # Average columns for each tool, and display them as a table
print("%-18s &" % "tool", "count &", print("%-18s & count & %s \\\\" % ("tool", " & ".join(data["fields"][2:])))
" & ".join(data["fields"][2:]), "\\\\") for i in range(0, len(data["tool"])):
for i in range(0, len(data["tools"])):
c = len(results[i]) c = len(results[i])
sums = ["%6.2f" % (sum([x[j] for x in results[i]])/c) sums = ["%6.1f" % (sum([x[j] for x in results[i]])/c)
for j in datacols] for j in datacols]
print("%-18s & %3d & " % (data["tools"][i], c), print("%-18s & %3d & %s \\\\" % (data["tool"][i], c,
" & ".join(sums), "\\\\") " & ".join(sums)))
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:
: tool & count & states & edges & transitions & acc & scc & nondetstates & nondeterministic & time & product_states & product_transitions & product_scc \\ : tool & count & states & edges & transitions & acc & scc & nonacc_scc & terminal_scc & weak_scc & strong_scc & nondetstates & nondeterministic & terminal_aut & weak_aut & strong_aut & time & product_states & product_transitions & product_scc \\
: ltl2tgba -s %f >%N & 4 & 3.00 & 6.00 & 10.00 & 1.00 & 2.50 & 0.75 & 0.50 & 0.04 & 549.00 & 9334.25 & 2.50 \\ : ltl2tgba -s %f >%N & 4 & 7.0 & 20.0 & 40.0 & 1.0 & 5.0 & 3.0 & 0.0 & 1.0 & 1.0 & 2.0 & 1.0 & 0.0 & 0.0 & 1.0 & 0.1 & 1327.0 & 23186.0 & 154.0 \\
: spin -f %s >%N & 4 & 4.50 & 11.25 & 25.00 & 1.00 & 2.75 & 3.50 & 1.00 & 0.01 & 848.25 & 24779.75 & 3.25 \\ : spin -f %s >%N & 4 & 26.0 & 283.0 & 550.0 & 1.0 & 9.0 & 6.0 & 0.0 & 0.0 & 1.0 & 23.0 & 1.0 & 0.0 & 0.0 & 1.0 & 1.0 & 4756.0 & 286083.0 & 376.0 \\
: lbt < %L >%T & 4 & 15.75 & 88.75 & 183.50 & 1.75 & 11.50 & 12.75 & 1.00 & 0.00 & 2660.75 & 169623.50 & 1218.50 \\ : lbt < %L >%T & 4 & 91.0 & 2045.0 & 4238.0 & 2.0 & 35.0 & 32.0 & 0.0 & 0.0 & 1.0 & 83.0 & 1.0 & 0.0 & 0.0 & 1.0 & 0.0 & 16762.0 & 2117423.0 & 5057.0 \\
The script =bench/ltl2tgba/sum.py= is a more evolved version of the The script =bench/ltl2tgba/sum.py= is a more evolved version of the
above script that generates two kinds of LaTeX tables. above script that generates two kinds of LaTeX tables.

44
src/bin/ltlcross.cc
View file

@ -48,6 +48,7 @@
#include "tgbaalgos/randomgraph.hh" #include "tgbaalgos/randomgraph.hh"
#include "tgbaalgos/scc.hh" #include "tgbaalgos/scc.hh"
#include "tgbaalgos/dotty.hh" #include "tgbaalgos/dotty.hh"
#include "tgbaalgos/isweakscc.hh"
#include "misc/formater.hh" #include "misc/formater.hh"
#include "tgbaalgos/stats.hh" #include "tgbaalgos/stats.hh"
#include "tgbaalgos/isdet.hh" #include "tgbaalgos/isdet.hh"
@ -167,8 +168,15 @@ struct statistics
unsigned transitions; unsigned transitions;
unsigned acc; unsigned acc;
unsigned scc; unsigned scc;
unsigned nonacc_scc;
unsigned terminal_scc;
unsigned weak_scc;
unsigned strong_scc;
unsigned nondetstates; unsigned nondetstates;
bool nondeterministic; bool nondeterministic;
bool terminal_aut;
bool weak_aut;
bool strong_aut;
double time; double time;
unsigned product_states; unsigned product_states;
unsigned product_transitions; unsigned product_transitions;
@ -182,8 +190,15 @@ struct statistics
" \"transitions\"," " \"transitions\","
" \"acc\"," " \"acc\","
" \"scc\"," " \"scc\","
" \"nondetstates\"," " \"nonacc_scc\","
" \"nondeterministic\"," " \"terminal_scc\","
" \"weak_scc\","
" \"strong_scc\","
" \"nondet_states\","
" \"nondet_aut\","
" \"terminal_aut\","
" \"weak_aut\","
" \"strong_aut\","
" \"time\"," " \"time\","
" \"product_states\"," " \"product_states\","
" \"product_transitions\"," " \"product_transitions\","
@ -198,8 +213,15 @@ struct statistics
<< transitions << ", " << transitions << ", "
<< acc << ", " << acc << ", "
<< scc << ", " << scc << ", "
<< nonacc_scc << ", "
<< terminal_scc << ", "
<< weak_scc << ", "
<< strong_scc << ", "
<< nondetstates << ", " << nondetstates << ", "
<< nondeterministic << ", " << nondeterministic << ", "
<< terminal_aut << ", "
<< weak_aut << ", "
<< strong_aut << ", "
<< time << ", " << time << ", "
<< product_states << ", " << product_states << ", "
<< product_transitions << ", " << product_transitions << ", "
@ -658,9 +680,27 @@ namespace
st->acc = res->number_of_acceptance_conditions(); st->acc = res->number_of_acceptance_conditions();
spot::scc_map m(res); spot::scc_map m(res);
m.build_map(); m.build_map();
unsigned c = m.scc_count();
st->scc = m.scc_count(); st->scc = m.scc_count();
st->nondetstates = spot::count_nondet_states(res); st->nondetstates = spot::count_nondet_states(res);
st->nondeterministic = st->nondetstates != 0; st->nondeterministic = st->nondetstates != 0;
for (unsigned n = 0; n < c; ++n)
{
if (!m.accepting(n))
++st->nonacc_scc;
else if (is_terminal_scc(m, n))
++st->terminal_scc;
else if (is_weak_scc(m, n))
++st->weak_scc;
else
++st->strong_scc;
}
if (st->strong_scc)
st->strong_aut = true;
else if (st->weak_scc)
st->weak_aut = true;
else
st->terminal_aut = true;
double prec = XTIME_PRECISION; double prec = XTIME_PRECISION;
st->time = (after - before) / prec; st->time = (after - before) / prec;
} }