diff --git a/README b/README index cd954d297..37344b5f5 100644 --- a/README +++ b/README @@ -192,6 +192,7 @@ bench/ Benchmarks for ... ltlclasses/ ... translation of more classes of LTL formulae, scc-stats/ ... SCC statistics after translation of LTL formulae, split-product/ ... parallelizing gain after splitting LTL automata, + spin13/ ... compositional suspension and other improvements, wdba/ ... WDBA minimization (for obligation properties). wrap/ Wrappers for other languages. python/ Python bindings for Spot and BuDDy diff --git a/bench/Makefile.am b/bench/Makefile.am index 06810b65a..9afdd3188 100644 --- a/bench/Makefile.am +++ b/bench/Makefile.am @@ -1,5 +1,5 @@ -## Copyright (C) 2008, 2009, 2010, 2012 Laboratoire de Recherche et -## Développement de l'Epita (LRDE). +## Copyright (C) 2008, 2009, 2010, 2012, 2013 Laboratoire de Recherche +## et Développement de l'Epita (LRDE). ## Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre ## et Marie Curie. @@ -20,4 +20,4 @@ ## along with this program. If not, see . SUBDIRS = emptchk ltl2tgba scc-stats split-product ltlcounter \ - ltlclasses wdba + ltlclasses wdba spin13 diff --git a/bench/ltl2tgba/sum.py b/bench/ltl2tgba/sum.py index 9d4a4eeba..32b8bdb54 100755 --- a/bench/ltl2tgba/sum.py +++ b/bench/ltl2tgba/sum.py @@ -51,7 +51,7 @@ def process_file(filename): fields = { name:index for index,name in enumerate(data["fields"]) } toolcol = fields['tool'] inputcol = fields['formula'] - + inputs = data["inputs"] # Index results by tool, then input @@ -67,9 +67,9 @@ def process_file(filename): print(r''' \section*{\texttt{%s}} -\subsection*{Cumulative summary}''' % filename) +\subsection*{Cumulative summary}''' % latex_escape(filename)) - print('\\begin{tabular}{l' + ('r' * (ncols - 1)) + '}\n', + print('\\noindent\\begin{tabular}{l' + ('r' * (ncols - 1)) + '}\n', " & ".join(rot(latex_escape(["tool", "count"] + data["fields"][2:]))), "\\\\") for i in range(0, ntools): @@ -89,7 +89,7 @@ states and more transitions. ''') - header = '\\begin{tabular}{l' + header = '\\noindent{\\small\\begin{tabular}{l' for i in data["tool"]: header += 'c' header += '}' @@ -114,7 +114,7 @@ states and more transitions. x += 1 print("&", x, end=' ') print(r"\\") - print(r'\end{tabular}') + print(r'\end{tabular}}') def main(): @@ -129,7 +129,7 @@ def main(): args = p.parse_args() print(r'''\documentclass{article} -\usepackage[a4paper,landscape,margin=2cm]{geometry} +\usepackage[a4paper,landscape,margin=1cm]{geometry} \usepackage{adjustbox} \usepackage{array} @@ -138,7 +138,7 @@ def main(): l% <{\egroup}% } -\newcommand*\rot{\multicolumn{1}{R{45}{1em}}}% no optional argument here, please! +\newcommand*\rot{\multicolumn{1}{R{90}{0em}}}% no optional argument here, please! \begin{document} ''') diff --git a/bench/spin13/Makefile.am b/bench/spin13/Makefile.am new file mode 100644 index 000000000..bccddb174 --- /dev/null +++ b/bench/spin13/Makefile.am @@ -0,0 +1,22 @@ +## Copyright (C) 2013 Laboratoire de Recherche et Développement de +## l'Epita (LRDE). +## +## This file is part of Spot, a model checking library. +## +## Spot is free software; you can redistribute it and/or modify it +## under the terms of the GNU General Public License as published by +## the Free Software Foundation; either version 3 of the License, or +## (at your option) any later version. +## +## Spot is distributed in the hope that it will be useful, but WITHOUT +## ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +## or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +## License for more details. +## +## You should have received a copy of the GNU General Public License +## along with this program. If not, see . + +EXTRA_DIST = big_2-fair_2.ltl big_2-fair_3-3.ltl big_2-strong_1.ltl \ + big_2-strong_2.ltl big_2.ltl html.bottom html.top \ + known.ltl new-fair2.ltl new-strong1.ltl new-strong2.ltl \ + new-weak3.ltl new.ltl run.sh README diff --git a/bench/spin13/README b/bench/spin13/README new file mode 100644 index 000000000..86a0e6e8a --- /dev/null +++ b/bench/spin13/README @@ -0,0 +1,78 @@ +This contains most of the a benchmark used for the paper + + "Compositional Approach to Suspension and Other Improvements to LTL + Translation", Tomáš Babiak, Thomas Badie, Alexandre Duret-Lutz, + Mojmír KÅ™etínský, and Jan StrejÄek. + +To appear in the proceedings of Spin'13. + +By "most" we means that some lines of the table we actually be missing +because we cannot compute them with the current version of Spot. The +missing lines are those with a small "a", that use the old SCC-based +simplification, and not the new one which is presented in section 4.1 +of the paper. + +If you have any interest in reproducing the data from the paper, using +exactly the same versions (yes, that's a plural), please head over to + http://www.lrde.epita.fr/~adl/spin13/ + +Keep in mind that as Spot is evolving, the results from this benchmark +may evolve (hopefully for the best!) with time. + + +Running instructions +==================== + +To run the benchmark: + + 1) Now configure and compile the current tarball with + ./configure --disable-shared --disable-devel + make + but to not install it. + 2) Go to directory bench/spin13/ and run the script "run.sh", + this will just build "run.mk" + 3) Run "make -f run.mk -j4", adjusting "-j8" to the number of + cores that your computer have. + +The run.mk makefile will launch several instances of ltlcross in +parallel (depending on the -j argument). There are 22 of them +to run in total. Once that is done, the different data are +collated into a LaTeX file (using the ../ltl2tgba/sum.py script) +which is then compiled to PDF (using latexmk). Finally, all +data are compacted into a tarball named with the date. + + +Results +======= + +The results are more detailed that Table 1 in the Spin'13 paper. + +ba-sum.pdf and tgba-sum.pdf show the main results over several sets +of formulae: + - known.ltl is the set described in the paper; + - new-fair3.ltl.pos is what we call fair3.ltl in the paper; + - new-strong2.ltl.pos is what we call strong2.ltl in the paper. +The extra sets are: + - new-ltl.pos: the set of random \varphi_i formula used to build + new-fair3.ltl.pos and new-strong2.ltl.pos; + - new-fair2.ltl.pos: the above formulae combined with weak + fairness hypothesis of the form (FG(a)->GF(b)); + - new-strong1.ltl.pos: simimular to strong2 but using only + one strong fairness hypothesis of the form + (GF(a)->GF(b)). + +Additionally, for all *.ltl.pos files, we have an *.ltl.neg file that +contains the negated formulas. + +These 11 sets are translated to TGBA or BA using different +translation configurations. Many of the configurations should be +recognized from the name in the paper. The "Early" lines describe +an extra experiement (not discussed in the paper), where +composition of the suspended subformula starts on the transition +that enters an accepting SCC (not in the SCC itself). + +In addition to the summaries in ba-sum.pdf and tgba-sum.pdf, detailled +results are provided as CSV files, slightly better formated JSON +files, and in HTML pages that can be used to explore the results +interactively. (It probably does not work with Internet Explorer. If +you have problems, install FireFox or Chrome.) diff --git a/bench/spin13/big_2-fair_2.ltl b/bench/spin13/big_2-fair_2.ltl new file mode 100644 index 000000000..37f9e140f --- /dev/null +++ b/bench/spin13/big_2-fair_2.ltl @@ -0,0 +1,100 @@ +((X ((p1 V <> ! p0) U p2) U [] ! <> ! X p4)) /\ (<>[]p10 -> []<>p11) +(((p0 U (! <> <> p4 U <> X ! p5)) U [] (X p0 U X p0))) /\ (<>[]p10 -> []<>p11) +([] ((<> p3 U p1) U ((((p1 U p5) \/ p5) U ! [] p0) /\ p1))) /\ (<>[]p10 -> []<>p11) +(! ((<> <> <> (p6 U p5) U <> X p1) /\ ! <> p2)) /\ (<>[]p10 -> []<>p11) +(((<> p6 -> X X X p1) U (([] p3 \/ p6) V [] p3))) /\ (<>[]p10 -> []<>p11) +((X p4 -> ([] <> (X (X (p4 U ! p7) U <> p4) U [] p2) U p0))) /\ (<>[]p10 -> []<>p11) +((((p6 /\ <> false) V (! (<> p4 V p3) V [] p0)) V [] (p0 -> p5))) /\ (<>[]p10 -> []<>p11) +(! ((! p1 U p4) U (<> p7 U ((p0 -> ! p4) V [] p0)))) /\ (<>[]p10 -> []<>p11) +(X (<> p0 /\ (! ! ((p0 U [] p6) U ! (p3 U p1)) V (p5 \/ <> p2)))) /\ (<>[]p10 -> []<>p11) +(((! p4 /\ ((p2 U p0) U (! p6 -> (<> p2 \/ p6)))) -> X (p2 -> p1))) /\ (<>[]p10 -> []<>p11) +(((<> (p4 U <> p3) \/ [] [] (p2 U [] [] p1)) /\ ! ! (p5 U <> p3))) /\ (<>[]p10 -> []<>p11) +(([] <> (<> ! ! (p2 V p1) -> [] (p7 -> X p2)) -> <> ! X p2)) /\ (<>[]p10 -> []<>p11) +(! (X (p1 /\ X X [] ! [] <> (p6 /\ X p1)) \/ (p5 -> p7))) /\ (<>[]p10 -> []<>p11) +(([] <> (<> ([] p3 -> [] X p3) V <> p3) U X X X p7)) /\ (<>[]p10 -> []<>p11) +(<> ((p6 \/ p6) V ((<> [] X X X ! p1 U p1) -> <> p1))) /\ (<>[]p10 -> []<>p11) +(<> X <> X <> (X [] p2 -> (<> (true -> [] p2) /\ X p2))) /\ (<>[]p10 -> []<>p11) +((([] ! [] (p7 U p5) V X p0) -> (p5 -> [] X p5))) /\ (<>[]p10 -> []<>p11) +(([] [] (p2 \/ p1) -> (([] p3 U true) U X (X p6 U (p5 /\ <> p5))))) /\ (<>[]p10 -> []<>p11) +([] ([] p1 /\ (<> p7 -> ((! p0 U p0) U <> <> p4)))) /\ (<>[]p10 -> []<>p11) +(((p2 V p3) U ! ((<> p4 \/ p5) -> (! (p5 \/ p4) V p7)))) /\ (<>[]p10 -> []<>p11) +((([] (<> (<> X p4 /\ [] p1) U p1) V [] <> X [] p5) U p1)) /\ (<>[]p10 -> []<>p11) +(X [] X ! ((p4 U (p2 -> p1)) \/ ! (<> p5 \/ p4))) /\ (<>[]p10 -> []<>p11) +((((<> p7 U (p6 U p7)) -> (p4 -> p6)) -> <> X (p0 -> <> (<> p6 -> p0)))) /\ (<>[]p10 -> []<>p11) +((p6 \/ ([] (p1 /\ p7) U <> (p4 U ((p2 \/ p7) -> [] (p3 U p7)))))) /\ (<>[]p10 -> []<>p11) +(((<> (p0 U p0) /\ [] p4) V ! <> (p2 /\ <> <> (p7 -> [] p7)))) /\ (<>[]p10 -> []<>p11) +((<> X <> <> <> (p3 -> ([] ! p6 -> p5)) \/ (p5 \/ ! [] (p4 /\ p4)))) /\ (<>[]p10 -> []<>p11) +(((X <> <> true U ! p1) V ((! ! p7 V p3) U ! (p1 /\ p5)))) /\ (<>[]p10 -> []<>p11) +((<> [] (((p6 -> p1) V (p5 U p5)) U ! p2) /\ (<> (p2 U p5) /\ ! p4))) /\ (<>[]p10 -> []<>p11) +(([] (X ((p4 V (p5 /\ p7)) \/ (p1 U p5)) U ! p5) U (p2 U p6))) /\ (<>[]p10 -> []<>p11) +((! [] p5 /\ ((! (! p2 -> p6) \/ [] (p1 V p7)) U (<> p4 V [] p6)))) /\ (<>[]p10 -> []<>p11) +((<> p7 U <> ((p1 U <> p4) U X ! X [] [] p3))) /\ (<>[]p10 -> []<>p11) +(<> ([] X ((p3 /\ p2) -> ! X <> p4) U ((p0 /\ <> p6) -> [] p2))) /\ (<>[]p10 -> []<>p11) +(<> [] [] (p4 /\ <> ((X p7 U p3) U <> (p5 U ([] p4 V p2))))) /\ (<>[]p10 -> []<>p11) +(X ([] ((p5 /\ ! [] p2) U p6) U (! p6 V (p6 \/ p7)))) /\ (<>[]p10 -> []<>p11) +(((((p2 -> (p5 U p3)) U (p6 U p0)) V p3) -> [] [] p7)) /\ (<>[]p10 -> []<>p11) +((([] p4 \/ X <> (X p6 U X p7)) /\ (p1 /\ ((p7 /\ X p2) \/ p1)))) /\ (<>[]p10 -> []<>p11) +((! ((! [] p3 \/ ! p7) /\ p5) U (X ! (X p2 -> p0) \/ X [] p5))) /\ (<>[]p10 -> []<>p11) +(((! p5 -> ! p4) U ((p3 V X X p2) U (<> p7 U X p2)))) /\ (<>[]p10 -> []<>p11) +(<> (X (<> X ((p3 U (p0 \/ p4)) U p6) U p1) V <> ! <> X ! p4)) /\ (<>[]p10 -> []<>p11) +(! (<> p4 /\ <> (([] (p0 -> p4) /\ X p1) /\ X p0))) /\ (<>[]p10 -> []<>p11) +(<> ((((p2 /\ p7) -> X p4) U true) U X (p5 \/ ! false))) /\ (<>[]p10 -> []<>p11) +((X ((p2 /\ [] [] ! p1) U <> p5) \/ <> ! X [] (<> X p2 U p5))) /\ (<>[]p10 -> []<>p11) +((! (p1 -> [] ! ([] p3 U [] [] p6)) /\ (p3 U p2))) /\ (<>[]p10 -> []<>p11) +((p4 U <> (X ((<> ([] p1 V p5) U X p6) U <> p4) \/ (false \/ p1)))) /\ (<>[]p10 -> []<>p11) +(<> (p6 U ! [] X <> (! (p3 U (X p6 U true)) -> (X X p5 V p4)))) /\ (<>[]p10 -> []<>p11) +((([] p1 V ! p5) V <> ! ([] ! [] p2 U [] p4))) /\ (<>[]p10 -> []<>p11) +(((((<> p0 -> p1) U (p3 -> p7)) \/ (<> p7 V (p0 U p0))) -> ! p6)) /\ (<>[]p10 -> []<>p11) +(((X p4 U <> ([] p2 -> (p1 V p3))) \/ (! p6 U <> p4))) /\ (<>[]p10 -> []<>p11) +(X ([] [] p2 U (X (X [] p7 U <> [] p2) -> (p4 /\ X p2)))) /\ (<>[]p10 -> []<>p11) +((p5 -> (<> p2 U (((! ! p5 U (p2 -> ! p2)) U <> p1) V p5)))) /\ (<>[]p10 -> []<>p11) +(X ((! (p4 /\ p1) \/ p6) U [] (<> (p6 U ! p6) V p4))) /\ (<>[]p10 -> []<>p11) +((<> (p1 \/ ([] (p7 /\ p0) -> p5)) \/ (p4 U (p5 /\ p1)))) /\ (<>[]p10 -> []<>p11) +((([] <> p0 -> ([] <> <> <> p2 V ((X p4 /\ X p5) U p6))) /\ ! p6)) /\ (<>[]p10 -> []<>p11) +(([] ! (p5 V p7) V ((p0 V ! p2) U [] (p7 \/ ! [] [] p3)))) /\ (<>[]p10 -> []<>p11) +((! [] p1 -> ((p4 U p0) V (! (p5 V p4) U ! [] (p7 V p5))))) /\ (<>[]p10 -> []<>p11) +((<> X [] [] p2 \/ <> X <> ((p0 U p0) U (p1 /\ (p4 -> p3))))) /\ (<>[]p10 -> []<>p11) +(! ((((p4 \/ p7) V p0) U (p2 U p4)) V (! p7 U ! p2))) /\ (<>[]p10 -> []<>p11) +((! p3 U ((((! p7 \/ p6) -> ! p5) U (p2 V p1)) /\ ! ! p0))) /\ (<>[]p10 -> []<>p11) +(((p3 U p2) U (<> (X (p4 /\ ! (p0 V X p6)) V <> p1) -> p3))) /\ (<>[]p10 -> []<>p11) +((((p4 U (<> p0 V <> p1)) U p1) -> (((X p3 U (false /\ p6)) U false) U p5))) /\ (<>[]p10 -> []<>p11) +(! [] (([] p4 -> (p7 V ! true)) \/ (! p3 V ! ! p2))) /\ (<>[]p10 -> []<>p11) +(((p2 \/ p7) U ! (p6 \/ X ((p6 -> [] p1) V [] ! ((p3 U p7) U p5))))) /\ (<>[]p10 -> []<>p11) +(<> (X ((! (p7 U true) U (p6 V p7)) V X p5) \/ X p4)) /\ (<>[]p10 -> []<>p11) +(X <> <> ! ((! (p6 V true) -> X p3) V X ! (! p0 U p0))) /\ (<>[]p10 -> []<>p11) +((((X (p5 U ! p1) U ! p1) U <> p0) U ! ((true -> p6) V [] [] true))) /\ (<>[]p10 -> []<>p11) +(((<> p6 U X ((p1 /\ p7) U (X p1 \/ p6))) -> (<> [] p6 U <> p2))) /\ (<>[]p10 -> []<>p11) +((((p5 U p7) U (p3 U <> p4)) -> (! p4 U X ! <> p3))) /\ (<>[]p10 -> []<>p11) +((X (<> ([] p0 V X [] p0) U [] p5) U [] (<> p2 U [] p6))) /\ (<>[]p10 -> []<>p11) +(<> ((((X p3 V X p7) U [] p5) U ((X p2 -> p1) U <> p2)) -> [] p5)) /\ (<>[]p10 -> []<>p11) +((! p3 \/ (<> (p4 U (p4 U p3)) U ([] p6 -> <> p0)))) /\ (<>[]p10 -> []<>p11) +(([] X ([] <> p4 U p6) -> [] ((p0 \/ X p0) -> ! <> (p3 U p6)))) /\ (<>[]p10 -> []<>p11) +([] <> (<> ((p7 V (p7 \/ p6)) U p0) /\ X (X p1 -> ! ! p1))) /\ (<>[]p10 -> []<>p11) +((<> (<> ((p4 U p6) \/ ! p3) U p3) -> [] (false \/ ([] p2 /\ p3)))) /\ (<>[]p10 -> []<>p11) +(((p0 U p5) /\ [] (<> (p2 V ! p0) /\ <> [] ([] p2 V ! X p1)))) /\ (<>[]p10 -> []<>p11) +((<> p2 -> (! p0 \/ <> ((! <> p4 -> ! p5) U p4)))) /\ (<>[]p10 -> []<>p11) +((((p4 \/ X p5) U (p1 V p3)) V (<> <> (X p4 /\ p2) -> (p3 U p0)))) /\ (<>[]p10 -> []<>p11) +(([] (p5 -> <> (p0 /\ p4)) U X <> (p5 U (! false -> p4)))) /\ (<>[]p10 -> []<>p11) +((! ((p5 \/ <> X p2) U p3) V (<> (true U <> p0) \/ p1))) /\ (<>[]p10 -> []<>p11) +((((! p1 U (p2 -> [] [] p3)) -> [] <> (p5 -> <> p3)) /\ [] X p4)) /\ (<>[]p10 -> []<>p11) +(<> ((p1 U X p3) \/ <> X (([] p4 U (true U p3)) V ! (p4 U X p1)))) /\ (<>[]p10 -> []<>p11) +((<> [] (! X p5 /\ <> (X p6 -> (p5 V p7))) U p5)) /\ (<>[]p10 -> []<>p11) +((((p5 /\ p1) -> [] (<> (p1 U X p6) U (p5 U p5))) -> (X X p4 U p0))) /\ (<>[]p10 -> []<>p11) +(([] <> p6 V (((p5 \/ p7) -> X X ! (p7 U p4)) U p0))) /\ (<>[]p10 -> []<>p11) +((<> <> [] ((p6 \/ p6) V ! [] p5) \/ (X ! p6 U p0))) /\ (<>[]p10 -> []<>p11) +(((p5 \/ (p3 U [] ! p7)) U <> X ((p0 \/ X p3) /\ ! ! p5))) /\ (<>[]p10 -> []<>p11) +(<> ! <> [] ! (<> (p6 U p3) /\ [] ((<> [] p6 \/ p4) V p7))) /\ (<>[]p10 -> []<>p11) +(((((p2 /\ (p1 \/ p2)) /\ p2) U X (p6 V p1)) U ((p7 -> ! p6) U p6))) /\ (<>[]p10 -> []<>p11) +(((! p1 /\ p3) V [] <> ! <> (<> (p0 U p4) U X p7))) /\ (<>[]p10 -> []<>p11) +(! (([] ((p2 U ! p1) U (p6 V p7)) \/ (<> p0 U p0)) -> (p3 U p0))) /\ (<>[]p10 -> []<>p11) +(((! ! ((p1 \/ ((p2 V p0) V ! p1)) -> X p1) V ! p4) \/ p2)) /\ (<>[]p10 -> []<>p11) +(((<> p0 U ! <> p7) \/ X (X ! [] X [] p5 U p4))) /\ (<>[]p10 -> []<>p11) +((X (((p1 U p1) U p4) -> [] X ! p5) U (! p7 -> ! p5))) /\ (<>[]p10 -> []<>p11) +((<> [] p0 V X ! (! p6 U (p3 V ! X ([] <> p1 \/ p1))))) /\ (<>[]p10 -> []<>p11) +(([] (false U <> <> X p5) U (X p7 V [] (<> X p4 \/ (<> p2 -> p5))))) /\ (<>[]p10 -> []<>p11) +((X [] p3 U <> ([] <> <> (p0 U false) \/ (! p5 \/ (! ! p2 -> p0))))) /\ (<>[]p10 -> []<>p11) +((X p1 \/ ((X (! [] p0 U p7) U ! p0) U ! p2))) /\ (<>[]p10 -> []<>p11) +(X ([] true U (X (p3 V [] p2) \/ (! p4 \/ <> p2)))) /\ (<>[]p10 -> []<>p11) +([] (<> <> <> X ((p2 V ([] p3 /\ p2)) /\ ! <> [] p3) \/ p3)) /\ (<>[]p10 -> []<>p11) +(X [] [] ((! p1 \/ p6) U <> X (! p2 U <> p1))) /\ (<>[]p10 -> []<>p11) +(((true /\ [] p6) U X <> (<> ((p3 U p5) V [] (p6 -> p6)) U ! ! p3))) /\ (<>[]p10 -> []<>p11) diff --git a/bench/spin13/big_2-fair_3-3.ltl b/bench/spin13/big_2-fair_3-3.ltl new file mode 100644 index 000000000..a4122d22a --- /dev/null +++ b/bench/spin13/big_2-fair_3-3.ltl @@ -0,0 +1,100 @@ +((X ((p1 V <> ! p0) U p2) U [] ! <> ! X p4)) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(((p0 U (! <> <> p4 U <> X ! p5)) U [] (X p0 U X p0))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +([] ((<> p3 U p1) U ((((p1 U p5) \/ p5) U ! [] p0) /\ p1))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(! ((<> <> <> (p6 U p5) U <> X p1) /\ ! <> p2)) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(((<> p6 -> X X X p1) U (([] p3 \/ p6) V [] p3))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((X p4 -> ([] <> (X (X (p4 U ! p7) U <> p4) U [] p2) U p0))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((((p6 /\ <> false) V (! (<> p4 V p3) V [] p0)) V [] (p0 -> p5))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(! ((! p1 U p4) U (<> p7 U ((p0 -> ! p4) V [] p0)))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(X (<> p0 /\ (! ! ((p0 U [] p6) U ! (p3 U p1)) V (p5 \/ <> p2)))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(((! p4 /\ ((p2 U p0) U (! p6 -> (<> p2 \/ p6)))) -> X (p2 -> p1))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(((<> (p4 U <> p3) \/ [] [] (p2 U [] [] p1)) /\ ! ! (p5 U <> p3))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(([] <> (<> ! ! (p2 V p1) -> [] (p7 -> X p2)) -> <> ! X p2)) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(! (X (p1 /\ X X [] ! [] <> (p6 /\ X p1)) \/ (p5 -> p7))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(([] <> (<> ([] p3 -> [] X p3) V <> p3) U X X X p7)) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(<> ((p6 \/ p6) V ((<> [] X X X ! p1 U p1) -> <> p1))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(<> X <> X <> (X [] p2 -> (<> (true -> [] p2) /\ X p2))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((([] ! [] (p7 U p5) V X p0) -> (p5 -> [] X p5))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(([] [] (p2 \/ p1) -> (([] p3 U true) U X (X p6 U (p5 /\ <> p5))))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +([] ([] p1 /\ (<> p7 -> ((! p0 U p0) U <> <> p4)))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(((p2 V p3) U ! ((<> p4 \/ p5) -> (! (p5 \/ p4) V p7)))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((([] (<> (<> X p4 /\ [] p1) U p1) V [] <> X [] p5) U p1)) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(X [] X ! ((p4 U (p2 -> p1)) \/ ! (<> p5 \/ p4))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((((<> p7 U (p6 U p7)) -> (p4 -> p6)) -> <> X (p0 -> <> (<> p6 -> p0)))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((p6 \/ ([] (p1 /\ p7) U <> (p4 U ((p2 \/ p7) -> [] (p3 U p7)))))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(((<> (p0 U p0) /\ [] p4) V ! <> (p2 /\ <> <> (p7 -> [] p7)))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((<> X <> <> <> (p3 -> ([] ! p6 -> p5)) \/ (p5 \/ ! [] (p4 /\ p4)))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(((X <> <> true U ! p1) V ((! ! p7 V p3) U ! (p1 /\ p5)))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((<> [] (((p6 -> p1) V (p5 U p5)) U ! p2) /\ (<> (p2 U p5) /\ ! p4))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(([] (X ((p4 V (p5 /\ p7)) \/ (p1 U p5)) U ! p5) U (p2 U p6))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((! [] p5 /\ ((! (! p2 -> p6) \/ [] (p1 V p7)) U (<> p4 V [] p6)))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((<> p7 U <> ((p1 U <> p4) U X ! X [] [] p3))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(<> ([] X ((p3 /\ p2) -> ! X <> p4) U ((p0 /\ <> p6) -> [] p2))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(<> [] [] (p4 /\ <> ((X p7 U p3) U <> (p5 U ([] p4 V p2))))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(X ([] ((p5 /\ ! [] p2) U p6) U (! p6 V (p6 \/ p7)))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(((((p2 -> (p5 U p3)) U (p6 U p0)) V p3) -> [] [] p7)) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((([] p4 \/ X <> (X p6 U X p7)) /\ (p1 /\ ((p7 /\ X p2) \/ p1)))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((! ((! [] p3 \/ ! p7) /\ p5) U (X ! (X p2 -> p0) \/ X [] p5))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(((! p5 -> ! p4) U ((p3 V X X p2) U (<> p7 U X p2)))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(<> (X (<> X ((p3 U (p0 \/ p4)) U p6) U p1) V <> ! <> X ! p4)) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(! (<> p4 /\ <> (([] (p0 -> p4) /\ X p1) /\ X p0))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(<> ((((p2 /\ p7) -> X p4) U true) U X (p5 \/ ! false))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((X ((p2 /\ [] [] ! p1) U <> p5) \/ <> ! X [] (<> X p2 U p5))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((! (p1 -> [] ! ([] p3 U [] [] p6)) /\ (p3 U p2))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((p4 U <> (X ((<> ([] p1 V p5) U X p6) U <> p4) \/ (false \/ p1)))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(<> (p6 U ! [] X <> (! (p3 U (X p6 U true)) -> (X X p5 V p4)))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((([] p1 V ! p5) V <> ! ([] ! [] p2 U [] p4))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(((((<> p0 -> p1) U (p3 -> p7)) \/ (<> p7 V (p0 U p0))) -> ! p6)) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(((X p4 U <> ([] p2 -> (p1 V p3))) \/ (! p6 U <> p4))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(X ([] [] p2 U (X (X [] p7 U <> [] p2) -> (p4 /\ X p2)))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((p5 -> (<> p2 U (((! ! p5 U (p2 -> ! p2)) U <> p1) V p5)))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(X ((! (p4 /\ p1) \/ p6) U [] (<> (p6 U ! p6) V p4))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((<> (p1 \/ ([] (p7 /\ p0) -> p5)) \/ (p4 U (p5 /\ p1)))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((([] <> p0 -> ([] <> <> <> p2 V ((X p4 /\ X p5) U p6))) /\ ! p6)) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(([] ! (p5 V p7) V ((p0 V ! p2) U [] (p7 \/ ! [] [] p3)))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((! [] p1 -> ((p4 U p0) V (! (p5 V p4) U ! [] (p7 V p5))))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((<> X [] [] p2 \/ <> X <> ((p0 U p0) U (p1 /\ (p4 -> p3))))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(! ((((p4 \/ p7) V p0) U (p2 U p4)) V (! p7 U ! p2))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((! p3 U ((((! p7 \/ p6) -> ! p5) U (p2 V p1)) /\ ! ! p0))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(((p3 U p2) U (<> (X (p4 /\ ! (p0 V X p6)) V <> p1) -> p3))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((((p4 U (<> p0 V <> p1)) U p1) -> (((X p3 U (false /\ p6)) U false) U p5))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(! [] (([] p4 -> (p7 V ! true)) \/ (! p3 V ! ! p2))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(((p2 \/ p7) U ! (p6 \/ X ((p6 -> [] p1) V [] ! ((p3 U p7) U p5))))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(<> (X ((! (p7 U true) U (p6 V p7)) V X p5) \/ X p4)) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(X <> <> ! ((! (p6 V true) -> X p3) V X ! (! p0 U p0))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((((X (p5 U ! p1) U ! p1) U <> p0) U ! ((true -> p6) V [] [] true))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(((<> p6 U X ((p1 /\ p7) U (X p1 \/ p6))) -> (<> [] p6 U <> p2))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((((p5 U p7) U (p3 U <> p4)) -> (! p4 U X ! <> p3))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((X (<> ([] p0 V X [] p0) U [] p5) U [] (<> p2 U [] p6))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(<> ((((X p3 V X p7) U [] p5) U ((X p2 -> p1) U <> p2)) -> [] p5)) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((! p3 \/ (<> (p4 U (p4 U p3)) U ([] p6 -> <> p0)))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(([] X ([] <> p4 U p6) -> [] ((p0 \/ X p0) -> ! <> (p3 U p6)))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +([] <> (<> ((p7 V (p7 \/ p6)) U p0) /\ X (X p1 -> ! ! p1))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((<> (<> ((p4 U p6) \/ ! p3) U p3) -> [] (false \/ ([] p2 /\ p3)))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(((p0 U p5) /\ [] (<> (p2 V ! p0) /\ <> [] ([] p2 V ! X p1)))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((<> p2 -> (! p0 \/ <> ((! <> p4 -> ! p5) U p4)))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((((p4 \/ X p5) U (p1 V p3)) V (<> <> (X p4 /\ p2) -> (p3 U p0)))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(([] (p5 -> <> (p0 /\ p4)) U X <> (p5 U (! false -> p4)))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((! ((p5 \/ <> X p2) U p3) V (<> (true U <> p0) \/ p1))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((((! p1 U (p2 -> [] [] p3)) -> [] <> (p5 -> <> p3)) /\ [] X p4)) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(<> ((p1 U X p3) \/ <> X (([] p4 U (true U p3)) V ! (p4 U X p1)))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((<> [] (! X p5 /\ <> (X p6 -> (p5 V p7))) U p5)) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((((p5 /\ p1) -> [] (<> (p1 U X p6) U (p5 U p5))) -> (X X p4 U p0))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(([] <> p6 V (((p5 \/ p7) -> X X ! (p7 U p4)) U p0))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((<> <> [] ((p6 \/ p6) V ! [] p5) \/ (X ! p6 U p0))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(((p5 \/ (p3 U [] ! p7)) U <> X ((p0 \/ X p3) /\ ! ! p5))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(<> ! <> [] ! (<> (p6 U p3) /\ [] ((<> [] p6 \/ p4) V p7))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(((((p2 /\ (p1 \/ p2)) /\ p2) U X (p6 V p1)) U ((p7 -> ! p6) U p6))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(((! p1 /\ p3) V [] <> ! <> (<> (p0 U p4) U X p7))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(! (([] ((p2 U ! p1) U (p6 V p7)) \/ (<> p0 U p0)) -> (p3 U p0))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(((! ! ((p1 \/ ((p2 V p0) V ! p1)) -> X p1) V ! p4) \/ p2)) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(((<> p0 U ! <> p7) \/ X (X ! [] X [] p5 U p4))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((X (((p1 U p1) U p4) -> [] X ! p5) U (! p7 -> ! p5))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((<> [] p0 V X ! (! p6 U (p3 V ! X ([] <> p1 \/ p1))))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(([] (false U <> <> X p5) U (X p7 V [] (<> X p4 \/ (<> p2 -> p5))))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((X [] p3 U <> ([] <> <> (p0 U false) \/ (! p5 \/ (! ! p2 -> p0))))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +((X p1 \/ ((X (! [] p0 U p7) U ! p0) U ! p2))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(X ([] true U (X (p3 V [] p2) \/ (! p4 \/ <> p2)))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +([] (<> <> <> X ((p2 V ([] p3 /\ p2)) /\ ! <> [] p3) \/ p3)) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(X [] [] ((! p1 \/ p6) U <> X (! p2 U <> p1))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) +(((true /\ [] p6) U X <> (<> ((p3 U p5) V [] (p6 -> p6)) U ! ! p3))) /\ ([]<>p10 /\ []<>p11 /\ []<>p12) diff --git a/bench/spin13/big_2-strong_1.ltl b/bench/spin13/big_2-strong_1.ltl new file mode 100644 index 000000000..71b2f1904 --- /dev/null +++ b/bench/spin13/big_2-strong_1.ltl @@ -0,0 +1,100 @@ +((X ((p1 V <> ! p0) U p2) U [] ! <> ! X p4)) /\ (G(F(p10)) -> G(F(p11))) +(((p0 U (! <> <> p4 U <> X ! p5)) U [] (X p0 U X p0))) /\ (G(F(p10)) -> G(F(p11))) +([] ((<> p3 U p1) U ((((p1 U p5) \/ p5) U ! [] p0) /\ p1))) /\ (G(F(p10)) -> G(F(p11))) +(! ((<> <> <> (p6 U p5) U <> X p1) /\ ! <> p2)) /\ (G(F(p10)) -> G(F(p11))) +(((<> p6 -> X X X p1) U (([] p3 \/ p6) V [] p3))) /\ (G(F(p10)) -> G(F(p11))) +((X p4 -> ([] <> (X (X (p4 U ! p7) U <> p4) U [] p2) U p0))) /\ (G(F(p10)) -> G(F(p11))) +((((p6 /\ <> false) V (! (<> p4 V p3) V [] p0)) V [] (p0 -> p5))) /\ (G(F(p10)) -> G(F(p11))) +(! ((! p1 U p4) U (<> p7 U ((p0 -> ! p4) V [] p0)))) /\ (G(F(p10)) -> G(F(p11))) +(X (<> p0 /\ (! ! ((p0 U [] p6) U ! (p3 U p1)) V (p5 \/ <> p2)))) /\ (G(F(p10)) -> G(F(p11))) +(((! p4 /\ ((p2 U p0) U (! p6 -> (<> p2 \/ p6)))) -> X (p2 -> p1))) /\ (G(F(p10)) -> G(F(p11))) +(((<> (p4 U <> p3) \/ [] [] (p2 U [] [] p1)) /\ ! ! (p5 U <> p3))) /\ (G(F(p10)) -> G(F(p11))) +(([] <> (<> ! ! (p2 V p1) -> [] (p7 -> X p2)) -> <> ! X p2)) /\ (G(F(p10)) -> G(F(p11))) +(! (X (p1 /\ X X [] ! [] <> (p6 /\ X p1)) \/ (p5 -> p7))) /\ (G(F(p10)) -> G(F(p11))) +(([] <> (<> ([] p3 -> [] X p3) V <> p3) U X X X p7)) /\ (G(F(p10)) -> G(F(p11))) +(<> ((p6 \/ p6) V ((<> [] X X X ! p1 U p1) -> <> p1))) /\ (G(F(p10)) -> G(F(p11))) +(<> X <> X <> (X [] p2 -> (<> (true -> [] p2) /\ X p2))) /\ (G(F(p10)) -> G(F(p11))) +((([] ! [] (p7 U p5) V X p0) -> (p5 -> [] X p5))) /\ (G(F(p10)) -> G(F(p11))) +(([] [] (p2 \/ p1) -> (([] p3 U true) U X (X p6 U (p5 /\ <> p5))))) /\ (G(F(p10)) -> G(F(p11))) +([] ([] p1 /\ (<> p7 -> ((! p0 U p0) U <> <> p4)))) /\ (G(F(p10)) -> G(F(p11))) +(((p2 V p3) U ! ((<> p4 \/ p5) -> (! (p5 \/ p4) V p7)))) /\ (G(F(p10)) -> G(F(p11))) +((([] (<> (<> X p4 /\ [] p1) U p1) V [] <> X [] p5) U p1)) /\ (G(F(p10)) -> G(F(p11))) +(X [] X ! ((p4 U (p2 -> p1)) \/ ! (<> p5 \/ p4))) /\ (G(F(p10)) -> G(F(p11))) +((((<> p7 U (p6 U p7)) -> (p4 -> p6)) -> <> X (p0 -> <> (<> p6 -> p0)))) /\ (G(F(p10)) -> G(F(p11))) +((p6 \/ ([] (p1 /\ p7) U <> (p4 U ((p2 \/ p7) -> [] (p3 U p7)))))) /\ (G(F(p10)) -> G(F(p11))) +(((<> (p0 U p0) /\ [] p4) V ! <> (p2 /\ <> <> (p7 -> [] p7)))) /\ (G(F(p10)) -> G(F(p11))) +((<> X <> <> <> (p3 -> ([] ! p6 -> p5)) \/ (p5 \/ ! [] (p4 /\ p4)))) /\ (G(F(p10)) -> G(F(p11))) +(((X <> <> true U ! p1) V ((! ! p7 V p3) U ! (p1 /\ p5)))) /\ (G(F(p10)) -> G(F(p11))) +((<> [] (((p6 -> p1) V (p5 U p5)) U ! p2) /\ (<> (p2 U p5) /\ ! p4))) /\ (G(F(p10)) -> G(F(p11))) +(([] (X ((p4 V (p5 /\ p7)) \/ (p1 U p5)) U ! p5) U (p2 U p6))) /\ (G(F(p10)) -> G(F(p11))) +((! [] p5 /\ ((! (! p2 -> p6) \/ [] (p1 V p7)) U (<> p4 V [] p6)))) /\ (G(F(p10)) -> G(F(p11))) +((<> p7 U <> ((p1 U <> p4) U X ! X [] [] p3))) /\ (G(F(p10)) -> G(F(p11))) +(<> ([] X ((p3 /\ p2) -> ! X <> p4) U ((p0 /\ <> p6) -> [] p2))) /\ (G(F(p10)) -> G(F(p11))) +(<> [] [] (p4 /\ <> ((X p7 U p3) U <> (p5 U ([] p4 V p2))))) /\ (G(F(p10)) -> G(F(p11))) +(X ([] ((p5 /\ ! [] p2) U p6) U (! p6 V (p6 \/ p7)))) /\ (G(F(p10)) -> G(F(p11))) +(((((p2 -> (p5 U p3)) U (p6 U p0)) V p3) -> [] [] p7)) /\ (G(F(p10)) -> G(F(p11))) +((([] p4 \/ X <> (X p6 U X p7)) /\ (p1 /\ ((p7 /\ X p2) \/ p1)))) /\ (G(F(p10)) -> G(F(p11))) +((! ((! [] p3 \/ ! p7) /\ p5) U (X ! (X p2 -> p0) \/ X [] p5))) /\ (G(F(p10)) -> G(F(p11))) +(((! p5 -> ! p4) U ((p3 V X X p2) U (<> p7 U X p2)))) /\ (G(F(p10)) -> G(F(p11))) +(<> (X (<> X ((p3 U (p0 \/ p4)) U p6) U p1) V <> ! <> X ! p4)) /\ (G(F(p10)) -> G(F(p11))) +(! (<> p4 /\ <> (([] (p0 -> p4) /\ X p1) /\ X p0))) /\ (G(F(p10)) -> G(F(p11))) +(<> ((((p2 /\ p7) -> X p4) U true) U X (p5 \/ ! false))) /\ (G(F(p10)) -> G(F(p11))) +((X ((p2 /\ [] [] ! p1) U <> p5) \/ <> ! X [] (<> X p2 U p5))) /\ (G(F(p10)) -> G(F(p11))) +((! (p1 -> [] ! ([] p3 U [] [] p6)) /\ (p3 U p2))) /\ (G(F(p10)) -> G(F(p11))) +((p4 U <> (X ((<> ([] p1 V p5) U X p6) U <> p4) \/ (false \/ p1)))) /\ (G(F(p10)) -> G(F(p11))) +(<> (p6 U ! [] X <> (! (p3 U (X p6 U true)) -> (X X p5 V p4)))) /\ (G(F(p10)) -> G(F(p11))) +((([] p1 V ! p5) V <> ! ([] ! [] p2 U [] p4))) /\ (G(F(p10)) -> G(F(p11))) +(((((<> p0 -> p1) U (p3 -> p7)) \/ (<> p7 V (p0 U p0))) -> ! p6)) /\ (G(F(p10)) -> G(F(p11))) +(((X p4 U <> ([] p2 -> (p1 V p3))) \/ (! p6 U <> p4))) /\ (G(F(p10)) -> G(F(p11))) +(X ([] [] p2 U (X (X [] p7 U <> [] p2) -> (p4 /\ X p2)))) /\ (G(F(p10)) -> G(F(p11))) +((p5 -> (<> p2 U (((! ! p5 U (p2 -> ! p2)) U <> p1) V p5)))) /\ (G(F(p10)) -> G(F(p11))) +(X ((! (p4 /\ p1) \/ p6) U [] (<> (p6 U ! p6) V p4))) /\ (G(F(p10)) -> G(F(p11))) +((<> (p1 \/ ([] (p7 /\ p0) -> p5)) \/ (p4 U (p5 /\ p1)))) /\ (G(F(p10)) -> G(F(p11))) +((([] <> p0 -> ([] <> <> <> p2 V ((X p4 /\ X p5) U p6))) /\ ! p6)) /\ (G(F(p10)) -> G(F(p11))) +(([] ! (p5 V p7) V ((p0 V ! p2) U [] (p7 \/ ! [] [] p3)))) /\ (G(F(p10)) -> G(F(p11))) +((! [] p1 -> ((p4 U p0) V (! (p5 V p4) U ! [] (p7 V p5))))) /\ (G(F(p10)) -> G(F(p11))) +((<> X [] [] p2 \/ <> X <> ((p0 U p0) U (p1 /\ (p4 -> p3))))) /\ (G(F(p10)) -> G(F(p11))) +(! ((((p4 \/ p7) V p0) U (p2 U p4)) V (! p7 U ! p2))) /\ (G(F(p10)) -> G(F(p11))) +((! p3 U ((((! p7 \/ p6) -> ! p5) U (p2 V p1)) /\ ! ! p0))) /\ (G(F(p10)) -> G(F(p11))) +(((p3 U p2) U (<> (X (p4 /\ ! (p0 V X p6)) V <> p1) -> p3))) /\ (G(F(p10)) -> G(F(p11))) +((((p4 U (<> p0 V <> p1)) U p1) -> (((X p3 U (false /\ p6)) U false) U p5))) /\ (G(F(p10)) -> G(F(p11))) +(! [] (([] p4 -> (p7 V ! true)) \/ (! p3 V ! ! p2))) /\ (G(F(p10)) -> G(F(p11))) +(((p2 \/ p7) U ! (p6 \/ X ((p6 -> [] p1) V [] ! ((p3 U p7) U p5))))) /\ (G(F(p10)) -> G(F(p11))) +(<> (X ((! (p7 U true) U (p6 V p7)) V X p5) \/ X p4)) /\ (G(F(p10)) -> G(F(p11))) +(X <> <> ! ((! (p6 V true) -> X p3) V X ! (! p0 U p0))) /\ (G(F(p10)) -> G(F(p11))) +((((X (p5 U ! p1) U ! p1) U <> p0) U ! ((true -> p6) V [] [] true))) /\ (G(F(p10)) -> G(F(p11))) +(((<> p6 U X ((p1 /\ p7) U (X p1 \/ p6))) -> (<> [] p6 U <> p2))) /\ (G(F(p10)) -> G(F(p11))) +((((p5 U p7) U (p3 U <> p4)) -> (! p4 U X ! <> p3))) /\ (G(F(p10)) -> G(F(p11))) +((X (<> ([] p0 V X [] p0) U [] p5) U [] (<> p2 U [] p6))) /\ (G(F(p10)) -> G(F(p11))) +(<> ((((X p3 V X p7) U [] p5) U ((X p2 -> p1) U <> p2)) -> [] p5)) /\ (G(F(p10)) -> G(F(p11))) +((! p3 \/ (<> (p4 U (p4 U p3)) U ([] p6 -> <> p0)))) /\ (G(F(p10)) -> G(F(p11))) +(([] X ([] <> p4 U p6) -> [] ((p0 \/ X p0) -> ! <> (p3 U p6)))) /\ (G(F(p10)) -> G(F(p11))) +([] <> (<> ((p7 V (p7 \/ p6)) U p0) /\ X (X p1 -> ! ! p1))) /\ (G(F(p10)) -> G(F(p11))) +((<> (<> ((p4 U p6) \/ ! p3) U p3) -> [] (false \/ ([] p2 /\ p3)))) /\ (G(F(p10)) -> G(F(p11))) +(((p0 U p5) /\ [] (<> (p2 V ! p0) /\ <> [] ([] p2 V ! X p1)))) /\ (G(F(p10)) -> G(F(p11))) +((<> p2 -> (! p0 \/ <> ((! <> p4 -> ! p5) U p4)))) /\ (G(F(p10)) -> G(F(p11))) +((((p4 \/ X p5) U (p1 V p3)) V (<> <> (X p4 /\ p2) -> (p3 U p0)))) /\ (G(F(p10)) -> G(F(p11))) +(([] (p5 -> <> (p0 /\ p4)) U X <> (p5 U (! false -> p4)))) /\ (G(F(p10)) -> G(F(p11))) +((! ((p5 \/ <> X p2) U p3) V (<> (true U <> p0) \/ p1))) /\ (G(F(p10)) -> G(F(p11))) +((((! p1 U (p2 -> [] [] p3)) -> [] <> (p5 -> <> p3)) /\ [] X p4)) /\ (G(F(p10)) -> G(F(p11))) +(<> ((p1 U X p3) \/ <> X (([] p4 U (true U p3)) V ! (p4 U X p1)))) /\ (G(F(p10)) -> G(F(p11))) +((<> [] (! X p5 /\ <> (X p6 -> (p5 V p7))) U p5)) /\ (G(F(p10)) -> G(F(p11))) +((((p5 /\ p1) -> [] (<> (p1 U X p6) U (p5 U p5))) -> (X X p4 U p0))) /\ (G(F(p10)) -> G(F(p11))) +(([] <> p6 V (((p5 \/ p7) -> X X ! (p7 U p4)) U p0))) /\ (G(F(p10)) -> G(F(p11))) +((<> <> [] ((p6 \/ p6) V ! [] p5) \/ (X ! p6 U p0))) /\ (G(F(p10)) -> G(F(p11))) +(((p5 \/ (p3 U [] ! p7)) U <> X ((p0 \/ X p3) /\ ! ! p5))) /\ (G(F(p10)) -> G(F(p11))) +(<> ! <> [] ! (<> (p6 U p3) /\ [] ((<> [] p6 \/ p4) V p7))) /\ (G(F(p10)) -> G(F(p11))) +(((((p2 /\ (p1 \/ p2)) /\ p2) U X (p6 V p1)) U ((p7 -> ! p6) U p6))) /\ (G(F(p10)) -> G(F(p11))) +(((! p1 /\ p3) V [] <> ! <> (<> (p0 U p4) U X p7))) /\ (G(F(p10)) -> G(F(p11))) +(! (([] ((p2 U ! p1) U (p6 V p7)) \/ (<> p0 U p0)) -> (p3 U p0))) /\ (G(F(p10)) -> G(F(p11))) +(((! ! ((p1 \/ ((p2 V p0) V ! p1)) -> X p1) V ! p4) \/ p2)) /\ (G(F(p10)) -> G(F(p11))) +(((<> p0 U ! <> p7) \/ X (X ! [] X [] p5 U p4))) /\ (G(F(p10)) -> G(F(p11))) +((X (((p1 U p1) U p4) -> [] X ! p5) U (! p7 -> ! p5))) /\ (G(F(p10)) -> G(F(p11))) +((<> [] p0 V X ! (! p6 U (p3 V ! X ([] <> p1 \/ p1))))) /\ (G(F(p10)) -> G(F(p11))) +(([] (false U <> <> X p5) U (X p7 V [] (<> X p4 \/ (<> p2 -> p5))))) /\ (G(F(p10)) -> G(F(p11))) +((X [] p3 U <> ([] <> <> (p0 U false) \/ (! p5 \/ (! ! p2 -> p0))))) /\ (G(F(p10)) -> G(F(p11))) +((X p1 \/ ((X (! [] p0 U p7) U ! p0) U ! p2))) /\ (G(F(p10)) -> G(F(p11))) +(X ([] true U (X (p3 V [] p2) \/ (! p4 \/ <> p2)))) /\ (G(F(p10)) -> G(F(p11))) +([] (<> <> <> X ((p2 V ([] p3 /\ p2)) /\ ! <> [] p3) \/ p3)) /\ (G(F(p10)) -> G(F(p11))) +(X [] [] ((! p1 \/ p6) U <> X (! p2 U <> p1))) /\ (G(F(p10)) -> G(F(p11))) +(((true /\ [] p6) U X <> (<> ((p3 U p5) V [] (p6 -> p6)) U ! ! p3))) /\ (G(F(p10)) -> G(F(p11))) diff --git a/bench/spin13/big_2-strong_2.ltl b/bench/spin13/big_2-strong_2.ltl new file mode 100644 index 000000000..40b89cda6 --- /dev/null +++ b/bench/spin13/big_2-strong_2.ltl @@ -0,0 +1,100 @@ +((X ((p1 V <> ! p0) U p2) U [] ! <> ! X p4)) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(((p0 U (! <> <> p4 U <> X ! p5)) U [] (X p0 U X p0))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +([] ((<> p3 U p1) U ((((p1 U p5) \/ p5) U ! [] p0) /\ p1))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(! ((<> <> <> (p6 U p5) U <> X p1) /\ ! <> p2)) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(((<> p6 -> X X X p1) U (([] p3 \/ p6) V [] p3))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((X p4 -> ([] <> (X (X (p4 U ! p7) U <> p4) U [] p2) U p0))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((((p6 /\ <> false) V (! (<> p4 V p3) V [] p0)) V [] (p0 -> p5))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(! ((! p1 U p4) U (<> p7 U ((p0 -> ! p4) V [] p0)))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(X (<> p0 /\ (! ! ((p0 U [] p6) U ! (p3 U p1)) V (p5 \/ <> p2)))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(((! p4 /\ ((p2 U p0) U (! p6 -> (<> p2 \/ p6)))) -> X (p2 -> p1))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(((<> (p4 U <> p3) \/ [] [] (p2 U [] [] p1)) /\ ! ! (p5 U <> p3))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(([] <> (<> ! ! (p2 V p1) -> [] (p7 -> X p2)) -> <> ! X p2)) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(! (X (p1 /\ X X [] ! [] <> (p6 /\ X p1)) \/ (p5 -> p7))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(([] <> (<> ([] p3 -> [] X p3) V <> p3) U X X X p7)) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(<> ((p6 \/ p6) V ((<> [] X X X ! p1 U p1) -> <> p1))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(<> X <> X <> (X [] p2 -> (<> (true -> [] p2) /\ X p2))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((([] ! [] (p7 U p5) V X p0) -> (p5 -> [] X p5))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(([] [] (p2 \/ p1) -> (([] p3 U true) U X (X p6 U (p5 /\ <> p5))))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +([] ([] p1 /\ (<> p7 -> ((! p0 U p0) U <> <> p4)))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(((p2 V p3) U ! ((<> p4 \/ p5) -> (! (p5 \/ p4) V p7)))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((([] (<> (<> X p4 /\ [] p1) U p1) V [] <> X [] p5) U p1)) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(X [] X ! ((p4 U (p2 -> p1)) \/ ! (<> p5 \/ p4))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((((<> p7 U (p6 U p7)) -> (p4 -> p6)) -> <> X (p0 -> <> (<> p6 -> p0)))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((p6 \/ ([] (p1 /\ p7) U <> (p4 U ((p2 \/ p7) -> [] (p3 U p7)))))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(((<> (p0 U p0) /\ [] p4) V ! <> (p2 /\ <> <> (p7 -> [] p7)))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((<> X <> <> <> (p3 -> ([] ! p6 -> p5)) \/ (p5 \/ ! [] (p4 /\ p4)))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(((X <> <> true U ! p1) V ((! ! p7 V p3) U ! (p1 /\ p5)))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((<> [] (((p6 -> p1) V (p5 U p5)) U ! p2) /\ (<> (p2 U p5) /\ ! p4))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(([] (X ((p4 V (p5 /\ p7)) \/ (p1 U p5)) U ! p5) U (p2 U p6))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((! [] p5 /\ ((! (! p2 -> p6) \/ [] (p1 V p7)) U (<> p4 V [] p6)))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((<> p7 U <> ((p1 U <> p4) U X ! X [] [] p3))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(<> ([] X ((p3 /\ p2) -> ! X <> p4) U ((p0 /\ <> p6) -> [] p2))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(<> [] [] (p4 /\ <> ((X p7 U p3) U <> (p5 U ([] p4 V p2))))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(X ([] ((p5 /\ ! [] p2) U p6) U (! p6 V (p6 \/ p7)))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(((((p2 -> (p5 U p3)) U (p6 U p0)) V p3) -> [] [] p7)) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((([] p4 \/ X <> (X p6 U X p7)) /\ (p1 /\ ((p7 /\ X p2) \/ p1)))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((! ((! [] p3 \/ ! p7) /\ p5) U (X ! (X p2 -> p0) \/ X [] p5))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(((! p5 -> ! p4) U ((p3 V X X p2) U (<> p7 U X p2)))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(<> (X (<> X ((p3 U (p0 \/ p4)) U p6) U p1) V <> ! <> X ! p4)) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(! (<> p4 /\ <> (([] (p0 -> p4) /\ X p1) /\ X p0))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(<> ((((p2 /\ p7) -> X p4) U true) U X (p5 \/ ! false))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((X ((p2 /\ [] [] ! p1) U <> p5) \/ <> ! X [] (<> X p2 U p5))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((! (p1 -> [] ! ([] p3 U [] [] p6)) /\ (p3 U p2))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((p4 U <> (X ((<> ([] p1 V p5) U X p6) U <> p4) \/ (false \/ p1)))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(<> (p6 U ! [] X <> (! (p3 U (X p6 U true)) -> (X X p5 V p4)))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((([] p1 V ! p5) V <> ! ([] ! [] p2 U [] p4))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(((((<> p0 -> p1) U (p3 -> p7)) \/ (<> p7 V (p0 U p0))) -> ! p6)) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(((X p4 U <> ([] p2 -> (p1 V p3))) \/ (! p6 U <> p4))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(X ([] [] p2 U (X (X [] p7 U <> [] p2) -> (p4 /\ X p2)))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((p5 -> (<> p2 U (((! ! p5 U (p2 -> ! p2)) U <> p1) V p5)))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(X ((! (p4 /\ p1) \/ p6) U [] (<> (p6 U ! p6) V p4))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((<> (p1 \/ ([] (p7 /\ p0) -> p5)) \/ (p4 U (p5 /\ p1)))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((([] <> p0 -> ([] <> <> <> p2 V ((X p4 /\ X p5) U p6))) /\ ! p6)) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(([] ! (p5 V p7) V ((p0 V ! p2) U [] (p7 \/ ! [] [] p3)))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((! [] p1 -> ((p4 U p0) V (! (p5 V p4) U ! [] (p7 V p5))))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((<> X [] [] p2 \/ <> X <> ((p0 U p0) U (p1 /\ (p4 -> p3))))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(! ((((p4 \/ p7) V p0) U (p2 U p4)) V (! p7 U ! p2))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((! p3 U ((((! p7 \/ p6) -> ! p5) U (p2 V p1)) /\ ! ! p0))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(((p3 U p2) U (<> (X (p4 /\ ! (p0 V X p6)) V <> p1) -> p3))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((((p4 U (<> p0 V <> p1)) U p1) -> (((X p3 U (false /\ p6)) U false) U p5))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(! [] (([] p4 -> (p7 V ! true)) \/ (! p3 V ! ! p2))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(((p2 \/ p7) U ! (p6 \/ X ((p6 -> [] p1) V [] ! ((p3 U p7) U p5))))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(<> (X ((! (p7 U true) U (p6 V p7)) V X p5) \/ X p4)) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(X <> <> ! ((! (p6 V true) -> X p3) V X ! (! p0 U p0))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((((X (p5 U ! p1) U ! p1) U <> p0) U ! ((true -> p6) V [] [] true))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(((<> p6 U X ((p1 /\ p7) U (X p1 \/ p6))) -> (<> [] p6 U <> p2))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((((p5 U p7) U (p3 U <> p4)) -> (! p4 U X ! <> p3))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((X (<> ([] p0 V X [] p0) U [] p5) U [] (<> p2 U [] p6))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(<> ((((X p3 V X p7) U [] p5) U ((X p2 -> p1) U <> p2)) -> [] p5)) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((! p3 \/ (<> (p4 U (p4 U p3)) U ([] p6 -> <> p0)))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(([] X ([] <> p4 U p6) -> [] ((p0 \/ X p0) -> ! <> (p3 U p6)))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +([] <> (<> ((p7 V (p7 \/ p6)) U p0) /\ X (X p1 -> ! ! p1))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((<> (<> ((p4 U p6) \/ ! p3) U p3) -> [] (false \/ ([] p2 /\ p3)))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(((p0 U p5) /\ [] (<> (p2 V ! p0) /\ <> [] ([] p2 V ! X p1)))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((<> p2 -> (! p0 \/ <> ((! <> p4 -> ! p5) U p4)))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((((p4 \/ X p5) U (p1 V p3)) V (<> <> (X p4 /\ p2) -> (p3 U p0)))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(([] (p5 -> <> (p0 /\ p4)) U X <> (p5 U (! false -> p4)))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((! ((p5 \/ <> X p2) U p3) V (<> (true U <> p0) \/ p1))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((((! p1 U (p2 -> [] [] p3)) -> [] <> (p5 -> <> p3)) /\ [] X p4)) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(<> ((p1 U X p3) \/ <> X (([] p4 U (true U p3)) V ! (p4 U X p1)))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((<> [] (! X p5 /\ <> (X p6 -> (p5 V p7))) U p5)) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((((p5 /\ p1) -> [] (<> (p1 U X p6) U (p5 U p5))) -> (X X p4 U p0))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(([] <> p6 V (((p5 \/ p7) -> X X ! (p7 U p4)) U p0))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((<> <> [] ((p6 \/ p6) V ! [] p5) \/ (X ! p6 U p0))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(((p5 \/ (p3 U [] ! p7)) U <> X ((p0 \/ X p3) /\ ! ! p5))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(<> ! <> [] ! (<> (p6 U p3) /\ [] ((<> [] p6 \/ p4) V p7))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(((((p2 /\ (p1 \/ p2)) /\ p2) U X (p6 V p1)) U ((p7 -> ! p6) U p6))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(((! p1 /\ p3) V [] <> ! <> (<> (p0 U p4) U X p7))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(! (([] ((p2 U ! p1) U (p6 V p7)) \/ (<> p0 U p0)) -> (p3 U p0))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(((! ! ((p1 \/ ((p2 V p0) V ! p1)) -> X p1) V ! p4) \/ p2)) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(((<> p0 U ! <> p7) \/ X (X ! [] X [] p5 U p4))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((X (((p1 U p1) U p4) -> [] X ! p5) U (! p7 -> ! p5))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((<> [] p0 V X ! (! p6 U (p3 V ! X ([] <> p1 \/ p1))))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(([] (false U <> <> X p5) U (X p7 V [] (<> X p4 \/ (<> p2 -> p5))))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((X [] p3 U <> ([] <> <> (p0 U false) \/ (! p5 \/ (! ! p2 -> p0))))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +((X p1 \/ ((X (! [] p0 U p7) U ! p0) U ! p2))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(X ([] true U (X (p3 V [] p2) \/ (! p4 \/ <> p2)))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +([] (<> <> <> X ((p2 V ([] p3 /\ p2)) /\ ! <> [] p3) \/ p3)) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(X [] [] ((! p1 \/ p6) U <> X (! p2 U <> p1))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) +(((true /\ [] p6) U X <> (<> ((p3 U p5) V [] (p6 -> p6)) U ! ! p3))) /\ (G(F(p10)) -> G(F(p11))) /\ (G(F(p12)) -> G(F(p13))) diff --git a/bench/spin13/big_2.ltl b/bench/spin13/big_2.ltl new file mode 100644 index 000000000..76123504f --- /dev/null +++ b/bench/spin13/big_2.ltl @@ -0,0 +1,100 @@ +(X ((p1 V <> ! p0) U p2) U [] ! <> ! X p4) +((p0 U (! <> <> p4 U <> X ! p5)) U [] (X p0 U X p0)) +[] ((<> p3 U p1) U ((((p1 U p5) \/ p5) U ! [] p0) /\ p1)) +! ((<> <> <> (p6 U p5) U <> X p1) /\ ! <> p2) +((<> p6 -> X X X p1) U (([] p3 \/ p6) V [] p3)) +(X p4 -> ([] <> (X (X (p4 U ! p7) U <> p4) U [] p2) U p0)) +(((p6 /\ <> false) V (! (<> p4 V p3) V [] p0)) V [] (p0 -> p5)) +! ((! p1 U p4) U (<> p7 U ((p0 -> ! p4) V [] p0))) +X (<> p0 /\ (! ! ((p0 U [] p6) U ! (p3 U p1)) V (p5 \/ <> p2))) +((! p4 /\ ((p2 U p0) U (! p6 -> (<> p2 \/ p6)))) -> X (p2 -> p1)) +((<> (p4 U <> p3) \/ [] [] (p2 U [] [] p1)) /\ ! ! (p5 U <> p3)) +([] <> (<> ! ! (p2 V p1) -> [] (p7 -> X p2)) -> <> ! X p2) +! (X (p1 /\ X X [] ! [] <> (p6 /\ X p1)) \/ (p5 -> p7)) +([] <> (<> ([] p3 -> [] X p3) V <> p3) U X X X p7) +<> ((p6 \/ p6) V ((<> [] X X X ! p1 U p1) -> <> p1)) +<> X <> X <> (X [] p2 -> (<> (true -> [] p2) /\ X p2)) +(([] ! [] (p7 U p5) V X p0) -> (p5 -> [] X p5)) +([] [] (p2 \/ p1) -> (([] p3 U true) U X (X p6 U (p5 /\ <> p5)))) +[] ([] p1 /\ (<> p7 -> ((! p0 U p0) U <> <> p4))) +((p2 V p3) U ! ((<> p4 \/ p5) -> (! (p5 \/ p4) V p7))) +(([] (<> (<> X p4 /\ [] p1) U p1) V [] <> X [] p5) U p1) +X [] X ! ((p4 U (p2 -> p1)) \/ ! (<> p5 \/ p4)) +(((<> p7 U (p6 U p7)) -> (p4 -> p6)) -> <> X (p0 -> <> (<> p6 -> p0))) +(p6 \/ ([] (p1 /\ p7) U <> (p4 U ((p2 \/ p7) -> [] (p3 U p7))))) +((<> (p0 U p0) /\ [] p4) V ! <> (p2 /\ <> <> (p7 -> [] p7))) +(<> X <> <> <> (p3 -> ([] ! p6 -> p5)) \/ (p5 \/ ! [] (p4 /\ p4))) +((X <> <> true U ! p1) V ((! ! p7 V p3) U ! (p1 /\ p5))) +(<> [] (((p6 -> p1) V (p5 U p5)) U ! p2) /\ (<> (p2 U p5) /\ ! p4)) +([] (X ((p4 V (p5 /\ p7)) \/ (p1 U p5)) U ! p5) U (p2 U p6)) +(! [] p5 /\ ((! (! p2 -> p6) \/ [] (p1 V p7)) U (<> p4 V [] p6))) +(<> p7 U <> ((p1 U <> p4) U X ! X [] [] p3)) +<> ([] X ((p3 /\ p2) -> ! X <> p4) U ((p0 /\ <> p6) -> [] p2)) +<> [] [] (p4 /\ <> ((X p7 U p3) U <> (p5 U ([] p4 V p2)))) +X ([] ((p5 /\ ! [] p2) U p6) U (! p6 V (p6 \/ p7))) +((((p2 -> (p5 U p3)) U (p6 U p0)) V p3) -> [] [] p7) +(([] p4 \/ X <> (X p6 U X p7)) /\ (p1 /\ ((p7 /\ X p2) \/ p1))) +(! ((! [] p3 \/ ! p7) /\ p5) U (X ! (X p2 -> p0) \/ X [] p5)) +((! p5 -> ! p4) U ((p3 V X X p2) U (<> p7 U X p2))) +<> (X (<> X ((p3 U (p0 \/ p4)) U p6) U p1) V <> ! <> X ! p4) +! (<> p4 /\ <> (([] (p0 -> p4) /\ X p1) /\ X p0)) +<> ((((p2 /\ p7) -> X p4) U true) U X (p5 \/ ! false)) +(X ((p2 /\ [] [] ! p1) U <> p5) \/ <> ! X [] (<> X p2 U p5)) +(! (p1 -> [] ! ([] p3 U [] [] p6)) /\ (p3 U p2)) +(p4 U <> (X ((<> ([] p1 V p5) U X p6) U <> p4) \/ (false \/ p1))) +<> (p6 U ! [] X <> (! (p3 U (X p6 U true)) -> (X X p5 V p4))) +(([] p1 V ! p5) V <> ! ([] ! [] p2 U [] p4)) +((((<> p0 -> p1) U (p3 -> p7)) \/ (<> p7 V (p0 U p0))) -> ! p6) +((X p4 U <> ([] p2 -> (p1 V p3))) \/ (! p6 U <> p4)) +X ([] [] p2 U (X (X [] p7 U <> [] p2) -> (p4 /\ X p2))) +(p5 -> (<> p2 U (((! ! p5 U (p2 -> ! p2)) U <> p1) V p5))) +X ((! (p4 /\ p1) \/ p6) U [] (<> (p6 U ! p6) V p4)) +(<> (p1 \/ ([] (p7 /\ p0) -> p5)) \/ (p4 U (p5 /\ p1))) +(([] <> p0 -> ([] <> <> <> p2 V ((X p4 /\ X p5) U p6))) /\ ! p6) +([] ! (p5 V p7) V ((p0 V ! p2) U [] (p7 \/ ! [] [] p3))) +(! [] p1 -> ((p4 U p0) V (! (p5 V p4) U ! [] (p7 V p5)))) +(<> X [] [] p2 \/ <> X <> ((p0 U p0) U (p1 /\ (p4 -> p3)))) +! ((((p4 \/ p7) V p0) U (p2 U p4)) V (! p7 U ! p2)) +(! p3 U ((((! p7 \/ p6) -> ! p5) U (p2 V p1)) /\ ! ! p0)) +((p3 U p2) U (<> (X (p4 /\ ! (p0 V X p6)) V <> p1) -> p3)) +(((p4 U (<> p0 V <> p1)) U p1) -> (((X p3 U (false /\ p6)) U false) U p5)) +! [] (([] p4 -> (p7 V ! true)) \/ (! p3 V ! ! p2)) +((p2 \/ p7) U ! (p6 \/ X ((p6 -> [] p1) V [] ! ((p3 U p7) U p5)))) +<> (X ((! (p7 U true) U (p6 V p7)) V X p5) \/ X p4) +X <> <> ! ((! (p6 V true) -> X p3) V X ! (! p0 U p0)) +(((X (p5 U ! p1) U ! p1) U <> p0) U ! ((true -> p6) V [] [] true)) +((<> p6 U X ((p1 /\ p7) U (X p1 \/ p6))) -> (<> [] p6 U <> p2)) +(((p5 U p7) U (p3 U <> p4)) -> (! p4 U X ! <> p3)) +(X (<> ([] p0 V X [] p0) U [] p5) U [] (<> p2 U [] p6)) +<> ((((X p3 V X p7) U [] p5) U ((X p2 -> p1) U <> p2)) -> [] p5) +(! p3 \/ (<> (p4 U (p4 U p3)) U ([] p6 -> <> p0))) +([] X ([] <> p4 U p6) -> [] ((p0 \/ X p0) -> ! <> (p3 U p6))) +[] <> (<> ((p7 V (p7 \/ p6)) U p0) /\ X (X p1 -> ! ! p1)) +(<> (<> ((p4 U p6) \/ ! p3) U p3) -> [] (false \/ ([] p2 /\ p3))) +((p0 U p5) /\ [] (<> (p2 V ! p0) /\ <> [] ([] p2 V ! X p1))) +(<> p2 -> (! p0 \/ <> ((! <> p4 -> ! p5) U p4))) +(((p4 \/ X p5) U (p1 V p3)) V (<> <> (X p4 /\ p2) -> (p3 U p0))) +([] (p5 -> <> (p0 /\ p4)) U X <> (p5 U (! false -> p4))) +(! ((p5 \/ <> X p2) U p3) V (<> (true U <> p0) \/ p1)) +(((! p1 U (p2 -> [] [] p3)) -> [] <> (p5 -> <> p3)) /\ [] X p4) +<> ((p1 U X p3) \/ <> X (([] p4 U (true U p3)) V ! (p4 U X p1))) +(<> [] (! X p5 /\ <> (X p6 -> (p5 V p7))) U p5) +(((p5 /\ p1) -> [] (<> (p1 U X p6) U (p5 U p5))) -> (X X p4 U p0)) +([] <> p6 V (((p5 \/ p7) -> X X ! (p7 U p4)) U p0)) +(<> <> [] ((p6 \/ p6) V ! [] p5) \/ (X ! p6 U p0)) +((p5 \/ (p3 U [] ! p7)) U <> X ((p0 \/ X p3) /\ ! ! p5)) +<> ! <> [] ! (<> (p6 U p3) /\ [] ((<> [] p6 \/ p4) V p7)) +((((p2 /\ (p1 \/ p2)) /\ p2) U X (p6 V p1)) U ((p7 -> ! p6) U p6)) +((! p1 /\ p3) V [] <> ! <> (<> (p0 U p4) U X p7)) +! (([] ((p2 U ! p1) U (p6 V p7)) \/ (<> p0 U p0)) -> (p3 U p0)) +((! ! ((p1 \/ ((p2 V p0) V ! p1)) -> X p1) V ! p4) \/ p2) +((<> p0 U ! <> p7) \/ X (X ! [] X [] p5 U p4)) +(X (((p1 U p1) U p4) -> [] X ! p5) U (! p7 -> ! p5)) +(<> [] p0 V X ! (! p6 U (p3 V ! X ([] <> p1 \/ p1)))) +([] (false U <> <> X p5) U (X p7 V [] (<> X p4 \/ (<> p2 -> p5)))) +(X [] p3 U <> ([] <> <> (p0 U false) \/ (! p5 \/ (! ! p2 -> p0)))) +(X p1 \/ ((X (! [] p0 U p7) U ! p0) U ! p2)) +X ([] true U (X (p3 V [] p2) \/ (! p4 \/ <> p2))) +[] (<> <> <> X ((p2 V ([] p3 /\ p2)) /\ ! <> [] p3) \/ p3) +X [] [] ((! p1 \/ p6) U <> X (! p2 U <> p1)) +((true /\ [] p6) U X <> (<> ((p3 U p5) V [] (p6 -> p6)) U ! ! p3)) diff --git a/bench/spin13/html.bottom b/bench/spin13/html.bottom new file mode 100644 index 000000000..0bedc43da --- /dev/null +++ b/bench/spin13/html.bottom @@ -0,0 +1,621 @@ +; + +google.setOnLoadCallback(draw_charts); + +var fields = {}; +var distinct_values = []; +var ninputs; +var inputs_table; +var ntools; +var ifield; +var tfield; + var nfields; + var nresults; + var results; + var hashres = {}; + var linecmp; + var linecmp_options = { + hAxis: {title: 'input', viewWindow: {}, format: '#', + maxAlternation: 3, minTextSpacing: 5, maxTextLines: 3, + slantedText: false }, + legend: {position: 'top', alignment: 'end'}, + pointSize: 4, + chartArea: {width: '90%'} + } + var input_line; + var input_dashboard; + + // Tool-indexed tables + var sumresults_table; + var tools_table; + var cross_table; + var cross_details; + function register_tool_indexed_table(table) + { + google.visualization.events.addListener(table, 'select', + function(){ select_tools(table.getSelection()); + }); + } + + function select_tools(selection) + { + tools_table.setSelection(selection); + sumresults_table.setSelection(selection); + cross_table.setSelection(selection); + cross_details.setSelection(selection); + } + + function select_input(t) + { + $('#single_input_select').val(t).trigger("change"); + inputs_table.setSelection([{row: t}]); + } + + function draw_input_line() + { + input_line.setOptions(linecmp_options) + //input_line.draw(linecmp); + input_dashboard.draw(linecmp); + } + + function change_input_line() + { + // line graph data + linecmp = new google.visualization.DataTable(); + var column = $('#input_select').val(); + linecmp.addColumn('string', 'input'); // Discrete values for the LineChart + linecmp.addColumn('number', 'input_'); // Continuous values for the control + for (var t = 0; t < ntools; ++t) + linecmp.addColumn('number', 'tool ' + t); + for (var i = 0; i < ninputs; ++i) + { + var res = [i.toString(), i]; + for (var t = 0; t < ntools; ++t) + { + var d = hashres[[t,i]]; + if (d) + res.push(d[column]); + else + res.push(null); + } + linecmp.addRow(res); + } + } + + function setup_input_line() + { + change_input_line(); + + var datacols = [] + for (var t = 0; t < ntools; ++t) + datacols.push(t + 2); + + var control = new google.visualization.ControlWrapper({ + controlType: 'ChartRangeFilter', + containerId: 'input_control', + options: { + filterColumnIndex: 1, + ui: { + chartType: 'LineChart', + chartOptions: { + chartArea: {width: '90%'}, + hAxis: {baselineColor: 'none'} + }, + chartView: { + columns: [1].concat(datacols) // [1] == continuous values for the control + }, + minRangeSize: 1 + } + }, + state: {range: {start: 0, end: ninputs}} + }); + + input_line = new google.visualization.ChartWrapper({ + chartType: 'LineChart', + containerId: 'input_line', + options: linecmp_options, + dataTable: linecmp, + view: {columns: [0].concat(datacols)} // [0] == discrete values for the line chart + }); + input_dashboard = new google.visualization.Dashboard(document.getElementById('input_dashboard')); + input_dashboard.bind(control, input_line); + + draw_input_line(); + } + + function update_input_line() + { + change_input_line(); + draw_input_line(); + } + + function update_cross_table() + { + var crossdata = new google.visualization.DataTable(); + var crossdatadet = new google.visualization.DataTable(); + + var crosscol = $('#cross_select').val(); + var crosscol2 = $('#cross_select2').val(); + crossdata.addColumn('string', '↓ greater than →'); + crossdatadet.addColumn('string', '↓ greater than →'); + for (var t = 0; t < ntools; ++t) + { + crossdata.addColumn('number', 'tool ' + t); + crossdatadet.addColumn('string', 'tool ' + t); + } + for (var w = 0; w < ntools; ++w) + { + var r = []; + var d = []; + var wrap = function(i) { return '' + i + ''; }; + for (var b = 0; b < ntools; ++b) + { + var bres = 0; + var dres = []; + if (w != b) + for (var i = 0; i < ninputs; ++i) + { + var wi = hashres[[w,i]]; + if (wi == undefined) + continue; + var bi = hashres[[b,i]]; + if (bi == undefined) + continue; + var wv = wi[crosscol]; + var bv = bi[crosscol]; + if (wv > bv) + { + ++bres; + dres.push(wrap(i)); + } + else if ((wv == bv) && crosscol2 >= 0) + { + var wv = wi[crosscol2]; + var bv = bi[crosscol2]; + if (wv > bv) + { + ++bres; + dres.push(wrap(i)); + } + } + } + else + bres = null; + r[b] = bres; + d[b] = dres.join(' '); + } + crossdata.addRow(['tool ' + w].concat(r)); + crossdatadet.addRow(['tool ' + w].concat(d)); + } + for (var c = 1; c < ntools + 1; ++c) + { + var range = crossdata.getColumnRange(c); + var rangeformatter = new google.visualization.ColorFormat(); + rangeformatter.addRange(range['min'], range['min'] + 1, 'green', null); + rangeformatter.addRange(range['max'], null, 'red', null); + rangeformatter.format(crossdata, c); + } + cross_table = new google.visualization.Table(document.getElementById('cross_table')); + register_tool_indexed_table(cross_table); + cross_table.draw(crossdata, {allowHtml: true}); + cross_details = new google.visualization.Table(document.getElementById('cross_details')); + register_tool_indexed_table(cross_details); + cross_details.draw(crossdatadet, {allowHtml: true}); + } + + + function update_scatter_table() + { + var tool1 = $('#tool1_select').val(); + var tool2 = $('#tool2_select').val(); + var f = $('#scatter_select').val(); + var bycolor = parseInt($('#bycolor_select').val()); + var fname = rawdata.fields[f]; + + + var scatterdata = new google.visualization.DataTable(); + scatterdata.addColumn({type: 'number', role: 'domain'}); + + var ndv = 1; + var dv = {}; + if (bycolor >= 0) + { + // Give each value a column number. + var v = results.getDistinctValues(bycolor); + ndv = v.length; + for (var i = 0; i < ndv; ++i) + { + dv[v[i]] = i; + scatterdata.addColumn({type: 'number', role: 'data', label: rawdata.fields[bycolor] + '=' + v[i] }); + scatterdata.addColumn({type: 'string', role: 'tooltip'}); + } + scatterdata.addColumn({type: 'number', role: 'data', label: 'disagreement' }); + scatterdata.addColumn({type: 'string', role: 'tooltip'}); + } + else + { + scatterdata.addColumn({type: 'number', role: 'data'}); + scatterdata.addColumn({type: 'string', role: 'tooltip'}); + } + var max1; + for (var i = 0; i < ninputs; ++i) + { + var i1 = hashres[[tool1, i]]; + var i2 = hashres[[tool2, i]]; + if (i1 == undefined || i2 == undefined) + continue; + row = [i1[f]]; + var col = 1; + if (bycolor >= 0) + { + for (col = 1; col < 2 * ndv + 3; ++col) + row[col] = null; + var v = i1[bycolor]; + col = dv[v] * 2 + 1; + if (v != i2[bycolor]) + col = ndv * 2 + 1; + } + var v2 = i2[f]; + row[col] = v2; + row[col + 1] = 'input ' + i; + if (max1 == undefined || v2 > max1) + max1 = v2; + scatterdata.addRow(row); + } + var max = scatterdata.getColumnRange(0)['max']; + if (max1 > max) + max = max1; + + var legend = (bycolor >= 0) ? { position: 'right', alignment: 'center' } : 'none'; + scatter_table = new google.visualization.ScatterChart(document.getElementById('scatter_table')); + scatter_table.draw(scatterdata, { + hAxis: {title: fname + ' from tool ' + tool1, maxValue: max}, + vAxis: {title: fname + ' from tool ' + tool2, maxValue: max}, + legend: legend, + chartArea: { left:80, width:420, height:420 }, + pointSize: 5 + }); + google.visualization.events.addListener(scatter_table, 'select', + function(){ var sel = scatter_table.getSelection(); + var row = sel[0]['row']; + var col = sel[0]['column']; + if ((row == undefined) || (col == undefined)) + return; + // The row might not match the input number + // if some results were missing. Use the + // tooltip instead. + var t = scatterdata.getValue(row, col + 1).substr(6); + select_input(t); + }); + } + + function update_single_input_bars() + { + var i = parseInt($('#single_input_select').val()); + var column_table = new google.visualization.DataTable(); + column_table.addColumn({type: 'string', label: 'measurements', role: 'domain'}) + for (var t = 0; t < ntools; ++t) + { + if (hashres[[t,i]] == undefined) + continue; + column_table.addColumn({type: 'number', label: 'tool ' + t, role: 'data'}) + } + + for (var m = 0; m < nfields; ++m) + { + if (m == ifield || m == tfield) + continue; + var tmp = []; + for (var t = 0; t < ntools; ++t) + { + var rt = hashres[[t,i]]; + if (rt == undefined) + continue; + tmp.push(rt[m]); + } + var max = Math.max.apply(Math, tmp); + var row = [rawdata.fields[m]]; + for (var j = 0; j < tmp.length; ++j) + row.push({v: tmp[j] / max, f: tmp[j].toString()}); + column_table.addRow(row); + } + single_input_bars = new google.visualization.ColumnChart(document.getElementById('single_input_bars')); + single_input_bars.draw(column_table, { + legend: {position: 'top', alignment: 'end'}, + vAxis: { textPosition: 'none' }, + chartArea: { width: '100%' }, + bar: { groupWidth: '80%' }, + allowHtml: true }); + } + + function draw_charts() { + var tools_table_data = new google.visualization.DataTable(); + tools_table_data.addColumn('number', 'id', 'id'); + tools_table_data.addColumn('string', 'command', 'command'); + ntools = rawdata.tool.length; + for (var r = 0; r < ntools; ++r) + { + tools_table_data.addRow([r, rawdata.tool[r]]); + } + + inputs_table_data = new google.visualization.DataTable(); + inputs_table_data.addColumn('number', 'id', 'id'); + inputs_table_data.addColumn('string', 'input', 'input'); + ninputs = rawdata.formula.length; + for (var r = 0; r < ninputs; ++r) + { + inputs_table_data.addRow([r, rawdata.formula[r]]); + } + + results = new google.visualization.DataTable(); + nfields = rawdata.fields.length; + for (var c = 0; c < nfields; ++c) + { + var name = rawdata.fields[c]; + results.addColumn('number', name, name); + fields[name] = c; + } + // FIXME: we should uses rawdata.inputs to set ifield and tfield + tfield = fields['tool']; + ifield = fields['formula']; + nresults = rawdata.results.length; + for (var r = 0; r < nresults; ++r) + { + var row = rawdata.results[r]; + results.addRow(row); + hashres[[row[tfield],row[ifield]]] = row; + } + + var paging_options = { height: '20em' }; + + tools_table = new google.visualization.Table(document.getElementById('tools_table')); + register_tool_indexed_table(tools_table); + tools_table.draw(tools_table_data, paging_options); + + inputs_table = new google.visualization.Table(document.getElementById('inputs_table')); + google.visualization.events.addListener(inputs_table, 'select', + function(){ var sel = inputs_table.getSelection(); + if (sel.length != 1) + return; + select_input(sel[0]['row']); + }); + inputs_table.draw(inputs_table_data, paging_options); + + + var results_table = new google.visualization.Table(document.getElementById('results_table')); + results_table.draw(results, paging_options); + + // Do we have all any missing input for some tool? + var missing = [['', 'missing inputs']]; + for (var t = 0; t < ntools; ++t) + { + var m = []; + for (var i = 0; i < ninputs; ++i) + { + if (hashres[[t,i]] == undefined) + { + m.push('' + i + ''); + } + } + if (m.length) + missing.push(['tool ' + t, m.join(" ")]); + } + if (missing.length > 1) + { + var missing_table_data = google.visualization.arrayToDataTable(missing, false); + var missing_table = new google.visualization.Table(document.getElementById('missing_table')); + missing_table.draw(missing_table_data, {allowHtml: true}); + } + + var aggreg = [{column:ifield, aggregation: google.visualization.data.count, type: 'number'}] + var sumshow = [0, 1]; + var col = 2; + for (var c = 0; c < nfields; ++c) + { + if (c != ifield && c != tfield) + { + aggreg.push({column:c, aggregation: google.visualization.data.sum, type: 'number'}) + aggreg.push({column:c, aggregation: google.visualization.data.avg, type: 'number'}) + aggreg.push({column:c, aggregation: google.visualization.data.min, type: 'number'}) + aggreg.push({column:c, aggregation: google.visualization.data.max, type: 'number'}) + sumshow.push(col); + col += 4; + } + } + var sumresults = new google.visualization.data.group(results, [tfield], aggreg); + var redformatter = new google.visualization.ColorFormat(); + redformatter.addRange(0, ninputs, 'black', 'red'); + sumresults.setColumnLabel(1, 'inputs'); + redformatter.format(sumresults, 1); + // Compute highlight the min and max in each column. + for (var c = 2; c < sumshow.length; ++c) + { + var col = sumshow[c]; + var range = sumresults.getColumnRange(col); + var rangeformatter = new google.visualization.ColorFormat(); + rangeformatter.addRange(range['min'], range['min'] + 1, 'green', null); + rangeformatter.addRange(range['max'], null, 'red', null); + rangeformatter.format(sumresults, col); + } + + var sumresults_view = new google.visualization.DataView(sumresults); + sumresults_view.setColumns(sumshow); + + sumresults_table = new google.visualization.Table(document.getElementById('sumresults_table')); + google.visualization.events.addListener(sumresults_table, 'select', + function(){ select_tools(sumresults_table.getSelection()); + }); + sumresults_table.draw(sumresults_view, {allowHtml: true}); + + // Transpose the avg/min/max values that are in avgresults_view + // Instead of + // | C1 | avg | min | max | C2 | avg | min | max + // T1 | 10 | 11 | 12 | 13 | 14 | 15 | 16 | 17 + // T2 | 20 | 21 | 22 | 23 | 24 | 25 | 26 | 27 + // We want + // | T1 | min | max | T2 | min | max + // C1 | 11 | 12 | 13 | 21 | 22 | 23 + // C2 | 15 | 16 | 17 | 25 | 26 | 27 + // Additionally, we should normalize each cell. + + var column_table = new google.visualization.DataTable(); + column_table.addColumn({type: 'string', label: 'measurements', role: 'domain'}) + for (var t = 0; t < ntools; ++t) + { + column_table.addColumn({type: 'number', label: 'tool ' + t, role: 'data'}) + column_table.addColumn({type: 'number', role: 'interval'}) + column_table.addColumn({type: 'number', role: 'interval'}) + } + var pos = 3; + for (var m = 0; m < nfields; ++m) + { + if (m != ifield && m != tfield) + { + var row = [rawdata.fields[m]]; + var max = sumresults.getColumnRange(pos + 2)['max']; + for (var t = 0; t < ntools; ++t) + { + row.push({v: sumresults.getValue(t, pos)/max, f: "avg " + sumresults.getValue(t, pos).toFixed(2)}, + {v: sumresults.getValue(t, pos + 1)/max, f: "min " + sumresults.getValue(t, pos + 1).toString()}, + {v: sumresults.getValue(t, pos + 2)/max, f: "max " + sumresults.getValue(t, pos + 2).toString()}); + } + pos += 4; + column_table.addRow(row); + } + } + avgresults_bars = new google.visualization.ColumnChart(document.getElementById('avgresults_bars')); + avgresults_bars.draw(column_table, { + legend: {position: 'top', alignment: 'end'}, + vAxis: { textPosition: 'none' }, + chartArea: { width: '100%' }, + bar: { groupWidth: '80%' }, + allowHtml: true }); + + var sel = $('#input_select'); + var sel2 = $('#scatter_select'); + var sel3 = $('#bycolor_select'); + var first = true; + sel3.append($("