From fec939c1a68cf666c962c383515868cbfa3400bb Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 27 Apr 2013 20:33:51 +0200 Subject: [PATCH] ltlcross: count SCCs of various strenghts * 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. --- NEWS | 4 ++ bench/ltl2tgba/sum.py | 4 +- doc/org/ltlcross.org | 160 ++++++++++++++++++++++-------------------- src/bin/ltlcross.cc | 44 +++++++++++- 4 files changed, 133 insertions(+), 79 deletions(-) diff --git a/NEWS b/NEWS index 9b3744699..7064685b9 100644 --- a/NEWS +++ b/NEWS @@ -82,6 +82,10 @@ New in spot 1.0.2a (not released): are required to make the format usable for other benchmarks (not 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: - org-mode files used to generate the documentation about diff --git a/bench/ltl2tgba/sum.py b/bench/ltl2tgba/sum.py index 32b8bdb54..a3c0275dd 100755 --- a/bench/ltl2tgba/sum.py +++ b/bench/ltl2tgba/sum.py @@ -65,6 +65,8 @@ def process_file(filename): name = name[name.rfind('/', 0, name.find(' ')) + 1:] data["tool"][i] = latex_escape(name[0:name.find('%')]) + timecol = fields['time'] + print(r''' \section*{\texttt{%s}} \subsection*{Cumulative summary}''' % latex_escape(filename)) @@ -74,7 +76,7 @@ def process_file(filename): "\\\\") for i in range(0, ntools): # 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()])) for j in datacols] print("\\texttt{%-18s} & %3d & " diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index 5af5e53bd..d3f76dd3d 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -10,16 +10,20 @@ same sanity checks. The main motivations for rewriting this tool were: - support for PSL formulas in addition to LTL - - more statistics (like counting the number of logical transitions - represented by each physical edge), output in a format that - can be more easily be post-processed, + - more statistics, especially: + - the number of logical transitions represented by each physical edge, + - 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 1/100 of a second, reporting most times as "0.00s"). Although =ltlcross= performs the same sanity checks as LBTT, it does -not implement any of the interactive features of LBTT. Essentially -=ltlcross= will report problems, but you will be on your own to -investigate and fix them. +not implement any of the interactive features of LBTT. In our almost +10-year usage of LBTT, we never had to use its interactive features to +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: - 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. The following compare =ltl2tgba=, =spin=, and =lbt= on three random -formula (where =W= and =M= operators have been removed because they -are not supported by =spin= and =lbt=). +formula (where =W= and =M= operators have been rewritten away because +they are not supported by =spin= and =lbt=). #+BEGIN_SRC sh :results verbatim :exports code randltl -n 2 a b | @@ -128,25 +132,25 @@ ltlcross --csv=results.csv --json=results.json \ #+END_SRC #+RESULTS: #+begin_example --:1: (G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1))))))) -Running [P0]: ltl2tgba -s '(G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1)))))))' >'lck-o0-eGEYaZ' -Running [P1]: spin -f '([](((p0) U ((p0) && ([](p1)))) V (([](p1)) || ((p0) U ((p0) && ([](p1)))))))' >'lck-o1-nYpFBX' -Running [P2]: lbt < 'lck-i0-fGdZQ0' >'lck-o2-CPs23V' -Running [N0]: ltl2tgba -s '(!(G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1))))))))' >'lck-o0-kXiZZS' -Running [N1]: spin -f '(!([](((p0) U ((p0) && ([](p1)))) V (([](p1)) || ((p0) U ((p0) && ([](p1))))))))' >'lck-o1-7ILLzR' -Running [N2]: lbt < 'lck-i0-9KG0wU' >'lck-o2-CcMCaQ' +-: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) & (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) && (<>(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-W7LdjO' >'lck-o2-ZACV3b' +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) && (<>(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-tcO4oL' >'lck-o2-QQUs0t' Performing sanity checks and gathering statistics... --:2: (!((G(F(p0))) -> (F(p1)))) -Running [P0]: ltl2tgba -s '(!((G(F(p0))) -> (F(p1))))' >'lck-o0-IOckzW' -Running [P1]: spin -f '(!((<>(p1)) || (!([](<>(p0))))))' >'lck-o1-tsT3RZ' -Running [P2]: lbt < 'lck-i1-5TJXmT' >'lck-o2-5E9jb3' -Running [N0]: ltl2tgba -s '(G(F(p0))) -> (F(p1))' >'lck-o0-M3XRO9' -Running [N1]: spin -f '(<>(p1)) || (!([](<>(p0))))' >'lck-o1-6nxqfd' -Running [N2]: lbt < 'lck-i1-4hS5u6' >'lck-o2-vNItGg' +-:2: (!(((!(G((p0) | (F(p1))))) <-> ((p0) | (X(p1)))) -> (!(p1)))) +Running [P0]: ltl2tgba -s '(!(((!(G((p0) | (F(p1))))) <-> ((p0) | (X(p1)))) -> (!(p1))))' >'lck-o0-qlcvic' +Running [P1]: spin -f '(!((!(p1)) || (!(((!([]((p0) || (<>(p1))))) && ((p0) || (X(p1)))) || (([]((p0) || (<>(p1)))) && (!((p0) || (X(p1)))))))))' >'lck-o1-fEBqz3' +Running [P2]: lbt < 'lck-i1-sint9k' >'lck-o2-6oY4RU' +Running [N0]: ltl2tgba -s '((!(G((p0) | (F(p1))))) <-> ((p0) | (X(p1)))) -> (!(p1))' >'lck-o0-6PQGuD' +Running [N1]: spin -f '(!(p1)) || (!(((!([]((p0) || (<>(p1))))) && ((p0) || (X(p1)))) || (([]((p0) || (<>(p1)))) && (!((p0) || (X(p1)))))))' >'lck-o1-1l4NVu' +Running [N2]: lbt < 'lck-i1-iEEnbM' >'lck-o2-a2Toum' Performing sanity checks and gathering statistics... -no problem detected +No problem detected. #+end_example After this execution, the file =results.csv= contains the following: @@ -156,19 +160,19 @@ cat results.csv #+END_SRC #+RESULTS: #+begin_example -"formula", "tool", "states", "edges", "transitions", "acc", "scc", "nondetstates", "nondeterministic", "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) 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) 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) 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) 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) 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(F(p0))) -> (F(p1))))", "ltl2tgba -s %f >%N", 2, 4, 4, 1, 1, 0, 0, 0.0416853, 398, 4198, 1 -"(!((G(F(p0))) -> (F(p1))))", "spin -f %s >%N", 2, 3, 5, 1, 1, 1, 1, 0.00325558, 398, 5227, 1 -"(!((G(F(p0))) -> (F(p1))))", "lbt < %L >%T", 5, 10, 15, 1, 4, 5, 1, 0.00299424, 409, 6401, 12 -"(G(F(p0))) -> (F(p1))", "ltl2tgba -s %f >%N", 3, 5, 11, 1, 3, 1, 1, 0.0422192, 600, 11663, 3 -"(G(F(p0))) -> (F(p1))", "spin -f %s >%N", 3, 5, 14, 1, 3, 1, 1, 0.00293655, 600, 14840, 3 -"(G(F(p0))) -> (F(p1))", "lbt < %L >%T", 11, 18, 54, 2, 11, 5, 1, 0.0030133, 1253, 26891, 457 +"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) & (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) & (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) & (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) & (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) & (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) & (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((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((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((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((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((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((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 This can be loaded in any spreadsheet application. Although we only @@ -185,47 +189,52 @@ cat results.json #+RESULTS: #+begin_example { - "tools": [ + "tool": [ "ltl2tgba -s %f >%N", "spin -f %s >%N", "lbt < %L >%T" ], - "inputs": [ - "(G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1)))))))", - "(!(G(((p0) U ((p0) & (G(p1)))) R ((G(p1)) | ((p0) U ((p0) & (G(p1))))))))", - "(!((G(F(p0))) -> (F(p1))))", - "(G(F(p0))) -> (F(p1))" + "formula": [ + "(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) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) R ((((p0) & (F(p1))) U ((p1) U ((p1) & ((!(p2)) R (p0))))) | (X(p1))))))", + "(!(((!(G((p0) | (F(p1))))) <-> ((p0) | (X(p1)))) -> (!(p1))))", + "((!(G((p0) | (F(p1))))) <-> ((p0) | (X(p1)))) -> (!(p1))" ], - "fields": [ - "input", "tool", "states", "edges", "transitions", "acc", "scc", "nondetstates", "nondeterministic", "time", "product_states", "product_transitions", "product_scc" + "fields": [ + "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": [ - [ 0, 0, 3, 5, 9, 1, 3, 2, 1, 0.0431589, 401, 5136, 3 ], - [ 0, 1, 6, 13, 18, 1, 3, 6, 1, 0.0104812, 995, 14384, 5 ], - [ 0, 2, 8, 41, 51, 1, 3, 8, 1, 0.00321619, 1389, 42998, 5 ], - [ 1, 0, 4, 10, 16, 1, 3, 0, 0, 0.0443761, 797, 16340, 3 ], - [ 1, 1, 7, 24, 63, 1, 4, 6, 1, 0.00623927, 1400, 64668, 4 ], - [ 1, 2, 39, 286, 614, 3, 28, 33, 1, 0.00386306, 7592, 602204, 4400 ], - [ 2, 0, 2, 4, 4, 1, 1, 0, 0, 0.0414639, 398, 4198, 1 ], - [ 2, 1, 2, 3, 5, 1, 1, 1, 1, 0.00327304, 398, 5227, 1 ], - [ 2, 2, 5, 10, 15, 1, 4, 5, 1, 0.00322862, 409, 6401, 12 ], - [ 3, 0, 3, 5, 11, 1, 3, 1, 1, 0.0432979, 600, 11663, 3 ], - [ 3, 1, 3, 5, 14, 1, 3, 1, 1, 0.00296043, 600, 14840, 3 ], - [ 3, 2, 11, 18, 54, 2, 11, 5, 1, 0.00295457, 1253, 26891, 457 ] + [ 0, 0, 7, 27, 42, 1, 1, 0, 0, 0, 1, 5, 1, 0, 0, 1, 0.162927, 1333, 20565, 3 ], + [ 0, 1, 55, 957, 1723, 1, 1, 0, 0, 0, 1, 55, 1, 0, 0, 1, 3.83261, 10791, 866615, 37 ], + [ 0, 2, 167, 5656, 10744, 3, 2, 1, 0, 0, 1, 167, 1, 0, 0, 1, 0.0365079, 32258, 5318535, 96 ], + [ 1, 0, 11, 28, 72, 1, 10, 6, 1, 2, 1, 1, 1, 0, 0, 1, 0.0628941, 2163, 36722, 594 ], + [ 1, 1, 23, 113, 331, 1, 14, 9, 1, 1, 3, 20, 1, 0, 0, 1, 0.101343, 4567, 171114, 1193 ], + [ 1, 2, 157, 2414, 5957, 3, 109, 103, 1, 1, 4, 133, 1, 0, 0, 1, 0.0197828, 30811, 3020266, 19147 ], + [ 2, 0, 6, 12, 21, 1, 5, 3, 0, 1, 1, 1, 1, 0, 0, 1, 0.0509422, 806, 15638, 9 ], + [ 2, 1, 11, 21, 47, 1, 8, 6, 0, 1, 1, 7, 1, 0, 0, 1, 0.0102468, 1217, 36416, 20 ], + [ 2, 2, 17, 45, 100, 2, 13, 11, 0, 1, 1, 14, 1, 0, 0, 1, 0.00346881, 1744, 57783, 347 ], + [ 3, 0, 7, 14, 28, 1, 6, 3, 1, 1, 1, 2, 1, 0, 0, 1, 0.0503676, 1006, 19822, 10 ], + [ 3, 1, 17, 43, 102, 1, 13, 10, 1, 1, 1, 12, 1, 0, 0, 1, 0.0474604, 2449, 70190, 256 ], + [ 3, 2, 23, 68, 154, 2, 19, 16, 1, 1, 1, 18, 1, 0, 0, 1, 0.0037305, 2236, 73111, 640 ] ] } #+end_example -Here the =fields= table describes the columns of the =results= table, -and the =input= and =tool= columns contains indices relative to the -=inputs= and =tools= table. 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. +Here the =fields= table describes the columns of the =results= table. +The =inputs= tables lists the columns that are considered as inputs +for the experiments. The values in the columns corresponding to the +fields =formula= and =tool= contains indices relative to the =formula= +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 -following Python3 script averages each column for each tool, -and presents the results in a form that can almost be copied into a -LaTeX table (the =%= in the tool names have to be taken care of). +following Python3 script averages each column for each tool, and +presents the results in a form that can almost be copied into a LaTeX +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 #!/usr/bin/python3 @@ -233,24 +242,23 @@ import json data = json.load(open('results.json')) datacols = range(2, len(data["fields"])) # 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"]: results[l[1]].append(l) -# Average columns for each tools, and display them as a table -print("%-18s &" % "tool", "count &", - " & ".join(data["fields"][2:]), "\\\\") -for i in range(0, len(data["tools"])): +# Average columns for each tool, and display them as a table +print("%-18s & count & %s \\\\" % ("tool", " & ".join(data["fields"][2:]))) +for i in range(0, len(data["tool"])): 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] - print("%-18s & %3d & " % (data["tools"][i], c), - " & ".join(sums), "\\\\") + print("%-18s & %3d & %s \\\\" % (data["tool"][i], c, + " & ".join(sums))) #+END_SRC #+RESULTS: -: tool & count & states & edges & transitions & acc & scc & nondetstates & nondeterministic & 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 \\ -: 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 \\ -: 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 \\ +: 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 & 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 & 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 & 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 above script that generates two kinds of LaTeX tables. diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index be7934f5c..0adb98711 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -48,6 +48,7 @@ #include "tgbaalgos/randomgraph.hh" #include "tgbaalgos/scc.hh" #include "tgbaalgos/dotty.hh" +#include "tgbaalgos/isweakscc.hh" #include "misc/formater.hh" #include "tgbaalgos/stats.hh" #include "tgbaalgos/isdet.hh" @@ -167,8 +168,15 @@ struct statistics unsigned transitions; unsigned acc; unsigned scc; + unsigned nonacc_scc; + unsigned terminal_scc; + unsigned weak_scc; + unsigned strong_scc; unsigned nondetstates; bool nondeterministic; + bool terminal_aut; + bool weak_aut; + bool strong_aut; double time; unsigned product_states; unsigned product_transitions; @@ -182,8 +190,15 @@ struct statistics " \"transitions\"," " \"acc\"," " \"scc\"," - " \"nondetstates\"," - " \"nondeterministic\"," + " \"nonacc_scc\"," + " \"terminal_scc\"," + " \"weak_scc\"," + " \"strong_scc\"," + " \"nondet_states\"," + " \"nondet_aut\"," + " \"terminal_aut\"," + " \"weak_aut\"," + " \"strong_aut\"," " \"time\"," " \"product_states\"," " \"product_transitions\"," @@ -198,8 +213,15 @@ struct statistics << transitions << ", " << acc << ", " << scc << ", " + << nonacc_scc << ", " + << terminal_scc << ", " + << weak_scc << ", " + << strong_scc << ", " << nondetstates << ", " << nondeterministic << ", " + << terminal_aut << ", " + << weak_aut << ", " + << strong_aut << ", " << time << ", " << product_states << ", " << product_transitions << ", " @@ -658,9 +680,27 @@ namespace st->acc = res->number_of_acceptance_conditions(); spot::scc_map m(res); m.build_map(); + unsigned c = m.scc_count(); st->scc = m.scc_count(); st->nondetstates = spot::count_nondet_states(res); 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; st->time = (after - before) / prec; }