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

Add the Spin'13 benchmark.

Browse source 
* bench/spin13/: New directory.
* bench/Makefile.am, README, configure.ac: Add it.
* bench/ltl2tgba/sum.py: Display smaller tables.
This commit is contained in:
Alexandre Duret-Lutz 2013-02-25 09:27:04 +01:00
parent b6d4806dca
commit 969d927145
20 changed files with 2059 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

1
README
View file

@ -192,6 +192,7 @@ bench/ Benchmarks for ...
ltlclasses/ ... translation of more classes of LTL formulae, ltlclasses/ ... translation of more classes of LTL formulae,
scc-stats/ ... SCC statistics after translation of LTL formulae, scc-stats/ ... SCC statistics after translation of LTL formulae,
split-product/ ... parallelizing gain after splitting LTL automata, split-product/ ... parallelizing gain after splitting LTL automata,
spin13/ ... compositional suspension and other improvements,
wdba/ ... WDBA minimization (for obligation properties). wdba/ ... WDBA minimization (for obligation properties).
wrap/ Wrappers for other languages. wrap/ Wrappers for other languages.
python/ Python bindings for Spot and BuDDy python/ Python bindings for Spot and BuDDy

6
bench/Makefile.am
View file

@ -1,5 +1,5 @@
## Copyright (C) 2008, 2009, 2010, 2012 Laboratoire de Recherche et ## Copyright (C) 2008, 2009, 2010, 2012, 2013 Laboratoire de Recherche
## Développement de l'Epita (LRDE). ## et Développement de l'Epita (LRDE).
## Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), ## Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
## département Systèmes Répartis Coopératifs (SRC), Université Pierre ## département Systèmes Répartis Coopératifs (SRC), Université Pierre
## et Marie Curie. ## et Marie Curie.
@ -20,4 +20,4 @@
## along with this program. If not, see <http://www.gnu.org/licenses/>. ## along with this program. If not, see <http://www.gnu.org/licenses/>.
SUBDIRS = emptchk ltl2tgba scc-stats split-product ltlcounter \ SUBDIRS = emptchk ltl2tgba scc-stats split-product ltlcounter \
ltlclasses wdba ltlclasses wdba spin13

12
bench/ltl2tgba/sum.py
View file

@ -67,9 +67,9 @@ def process_file(filename):
print(r''' print(r'''
\section*{\texttt{%s}} \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:]))), " & ".join(rot(latex_escape(["tool", "count"] + data["fields"][2:]))),
"\\\\") "\\\\")
for i in range(0, ntools): 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"]: for i in data["tool"]:
header += 'c' header += 'c'
header += '}' header += '}'
@ -114,7 +114,7 @@ states and more transitions.
x += 1 x += 1
print("&", x, end=' ') print("&", x, end=' ')
print(r"\\") print(r"\\")
print(r'\end{tabular}') print(r'\end{tabular}}')
def main(): def main():
@ -129,7 +129,7 @@ def main():
args = p.parse_args() args = p.parse_args()
print(r'''\documentclass{article} print(r'''\documentclass{article}
\usepackage[a4paper,landscape,margin=2cm]{geometry} \usepackage[a4paper,landscape,margin=1cm]{geometry}
\usepackage{adjustbox} \usepackage{adjustbox}
\usepackage{array} \usepackage{array}
@ -138,7 +138,7 @@ def main():
l% l%
<{\egroup}% <{\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} \begin{document}
''') ''')

22
bench/spin13/Makefile.am Normal file
View file

@ -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 <http://www.gnu.org/licenses/>.
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

78
bench/spin13/README Normal file
View file

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

100
bench/spin13/big_2-fair_2.ltl Normal file
View file

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

100
bench/spin13/big_2-fair_3-3.ltl Normal file
View file

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

100
bench/spin13/big_2-strong_1.ltl Normal file
View file

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

100
bench/spin13/big_2-strong_2.ltl Normal file
View file

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

100
bench/spin13/big_2.ltl Normal file
View file

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

621
bench/spin13/html.bottom Normal file
View file

@ -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&nbsp;' + t);
crossdatadet.addColumn('string', 'tool&nbsp;' + t);
}
for (var w = 0; w < ntools; ++w)
{
var r = [];
var d = [];
var wrap = function(i) { return '<a class="inputnum" href="javascript: select_input(' + i + ');">' + i + '</a>'; };
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&nbsp;' + w].concat(r));
crossdatadet.addRow(['tool&nbsp;' + 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('<a class="inputnum" href="javascript: select_input(' + i + ');">' + i + '</a>');
}
}
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($("<option>").attr('value', -1).text('(nothing)'));
for (var c = 0; c < nfields; ++c)
{
if (c != ifield && c != tfield)
{
sel.append($("<option>").attr('value', c).text(rawdata.fields[c]));
sel2.append($("<option>").attr('value', c).text(rawdata.fields[c]));
if (first)
{
sel.val(c);
sel2.val(c);
first = false;
}
var dv = results.getDistinctValues(c).length;
distinct_values[c] = dv;
if (dv > 1 && dv <= 10)
sel3.append($("<option>").attr('value', c).text(rawdata.fields[c]));
}
}
$('#input_select').change(update_input_line);
setup_input_line()
// Cross chart.
var sel = $('#cross_select');
var sel2 = $('#cross_select2');
sel2.append($("<option>").attr('value', -1).text('(nothing)'));
sel2.val(-1);
var first = true;
for (var c = 0; c < nfields; ++c)
{
if (c != ifield && c != tfield)
{
sel.append($("<option>").attr('value', c).text(rawdata.fields[c]));
if (first)
{
sel.val(c);
first = false;
}
sel2.append($("<option>").attr('value', c).text(rawdata.fields[c]));
}
}
$('#cross_select').change(update_cross_table);
$('#cross_select2').change(update_cross_table);
update_cross_table()
var t1s = $('#tool1_select');
var t2s = $('#tool2_select');
var first = true;
var second = true;
for (var t = 0; t < ntools; ++t)
{
t1s.append($("<option>").attr('value', t).text('tool ' + t + ': ' + rawdata.tool[t]));
t2s.append($("<option>").attr('value', t).text('tool ' + t + ': ' + rawdata.tool[t]));
if (first)
{
t1s.val(t);
first = false;
}
else if (second)
{
t2s.val(t);
second = false;
}
}
t1s.change(update_scatter_table);
t2s.change(update_scatter_table);
$('#scatter_select').change(update_scatter_table);
$('#bycolor_select').change(update_scatter_table);
update_scatter_table();
var os = $('#single_input_select');
var first = true;
for (var i = 0; i < ninputs; ++i)
{
os.append($("<option>").attr('value', i).text(i + ': ' + rawdata.formula[i]));
if (first)
{
os.val(t);
first = false;
}
}
os.change(update_single_input_bars);
update_single_input_bars();
}
</script>
</head>
<body>
<div style="width: 25%; float: left;">
<h2>Tools</h2>
<div id="tools_table"></div>
</div>
<div style="width: 74%; float: right;">
<h2>Inputs</h2>
<div id="inputs_table"></div>
</div>
<h2 style="clear: both">Results</h2>
<div id="results_table"></div>
<h2>Missing results</h2>
<div id="missing_table">None</div>
<h1>Cumulative Summary</h1>
Each column shows a sum over all inputs processed by one tool. The second column shows the count of inputs processed.
Green and red highlight minimum and maximum values per column.
<div id="sumresults_table"></div>
<h1>Average Summary</h1>
<div id="avgresults_bars" style="height: 250px; width: '100%';"></div>
<h1>Line-Comparison</h1>
<select id="input_select"></select>
<div id="input_dashboard">
<div id="input_line" style="height: 250px;"></div>
<div id="input_control" style="height: 50px;"></div>
</div>
<h1>Cross-Comparison</h1>
Compare <select id="cross_select"></select> and in case of equality <select id="cross_select2"></select>.
<div id="cross_table"></div>
<br/>Details of the inputs counted in the above table:<br/>
<div id="cross_details"></div>
<h1>Tool vs. Tool Scatter</h1>
Compare <select id="tool1_select"></select> against <select id="tool2_select"></select> on <select id="scatter_select"></select> and color by <select id="bycolor_select"></select>.
<div id="scatter_table" style="height: 500px; width:'100%';"></div>
<h1>Single-Input Comparison</h1>
Input <select id="single_input_select"></select>
<div id="single_input_bars" style="height: 250px; width: '100%';"></div>
</body>
</html>

13
bench/spin13/html.top Normal file
View file

@ -0,0 +1,13 @@
<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<style type="text/css">
.inputnum {text-decoration: none; color: black}
</style>
<script type="text/javascript" src="https://www.google.com/jsapi"></script>
<script type="text/javascript">
google.load("jquery", "1");
google.load("visualization", "1", {packages:["corechart", "table", "controls"]});
var rawdata =

92
bench/spin13/known.ltl Normal file
View file

@ -0,0 +1,92 @@
[](!p0)
<>p1 -> (!p0 U p1)
[](p2 -> [](!p0))
[]((p2 & !p1 & <>p1) -> (!p0 U p1))
[](p2 & !p1 -> (!p0 U (p1 | []!p0)))
<>(p0)
!p1 U ((p0 & !p1) | []!p1)
[](!p2) | <>(p2 & <>p0)
[](p2 & !p1 -> (!p1 U ((p0 & !p1) | []!p1)))
[](p2 & !p1 -> (!p1 U (p0 & !p1)))
<>p1 -> ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | (!p0 U p1)))))))))
[]((p2 & <>p1) -> ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | (!p0 U p1))))))))))
[](p2 -> ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | (!p0 U (p1 | []!p0)) | []p0)))))))))
[](p0)
<>p1 -> (p0 U p1)
[](p2 -> [](p0))
[]((p2 & !p1 & <>p1) -> (p0 U p1))
[](p2 & !p1 -> (p0 U (p1 | [] p0)))
!p0 U (p3 | []!p0)
<>p1 -> (!p0 U (p3 | p1))
[]!p2 | <>(p2 & (!p0 U (p3 | []!p0)))
[]((p2 & !p1 & <>p1) -> (!p0 U (p3 | p1)))
[](p2 & !p1 -> (!p0 U ((p3 | p1) | []!p0)))
[](p0 -> <>p3)
<>p1 -> (p0 -> (!p1 U (p3 & !p1))) U p1
[](p2 -> [](p0 -> <>p3))
[]((p2 & !p1 & <>p1) -> (p0 -> (!p1 U (p3 & !p1))) U p1)
[](p2 & !p1 -> ((p0 -> (!p1 U (p3 & !p1))) U (p1 | [](p0 -> (!p1 U (p3 & !p1))))))
<>p0 -> (!p0 U (p3 & !p0 & X(!p0 U p4)))
<>p1 -> (!p0 U (p1 | (p3 & !p0 & X(!p0 U p4))))
([]!p2) | (!p2 U (p2 & <>p0 -> (!p0 U (p3 & !p0 & X(!p0 U p4)))))
[]((p2 & <>p1) -> (!p0 U (p1 | (p3 & !p0 & X(!p0 U p4)))))
[](p2 -> (<>p0 -> (!p0 U (p1 | (p3 & !p0 & X(!p0 U p4))))))
(<>(p3 & X<>p4)) -> ((!p3) U p0)
<>p1 -> ((!(p3 & (!p1) & X(!p1 U (p4 & !p1)))) U (p1 | p0))
([]!p2) | ((!p2) U (p2 & ((<>(p3 & X<>p4)) -> ((!p3) U p0))))
[]((p2 & <>p1) -> ((!(p3 & (!p1) & X(!p1 U (p4 & !p1)))) U (p1 | p0)))
[](p2 -> (!(p3 & (!p1) & X(!p1 U (p4 & !p1))) U (p1 | p0) | [](!(p3 & X<>p4))))
[] (p3 & X<> p4 -> X(<>(p4 & <> p0)))
<>p1 -> (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0))) U p1
[] (p2 -> [] (p3 & X<> p4 -> X(!p4 U (p4 & <> p0))))
[] ((p2 & <>p1) -> (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0))) U p1)
[] (p2 -> (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0))) U (p1 | [] (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0)))))
[] (p0 -> <>(p3 & X<>p4))
<>p1 -> (p0 -> (!p1 U (p3 & !p1 & X(!p1 U p4)))) U p1
[] (p2 -> [] (p0 -> (p3 & X<> p4)))
[] ((p2 & <>p1) -> (p0 -> (!p1 U (p3 & !p1 & X(!p1 U p4)))) U p1)
[] (p2 -> (p0 -> (!p1 U (p3 & !p1 & X(!p1 U p4)))) U (p1 | [] (p0 -> (p3 & X<> p4))))
[] (p0 -> <>(p3 & !p5 & X(!p5 U p4)))
<>p1 -> (p0 -> (!p1 U (p3 & !p1 & !p5 & X((!p1 & !p5) U p4)))) U p1
[] (p2 -> [] (p0 -> (p3 & !p5 & X(!p5 U p4))))
[] ((p2 & <>p1) -> (p0 -> (!p1 U (p3 & !p1 & !p5 & X((!p1 & !p5) U p4)))) U p1)
[] (p2 -> (p0 -> (!p1 U (p3 & !p1 & !p5 & X((!p1 & !p5) U p4)))) U (p1 | [] (p0 -> (p3 & !p5 & X(!p5 U p4)))))
!p0 U ((p0 U ((!p0 U ((p0 U ([]!p0 | []p0)) | []!p0)) | []!p0)) | []!p0)
<>p2 -> (!p2 U (p2 & (!p0 U ((p0 U ((!p0 U ((p0 U ([]!p0 | []p0)) | []!p0)) | []!p0)) | []!p0))))
p0 U p1
p0 U (p1 U p2)
!p0 R (!p1 R !p2)
(1 U (0 R !p0)) | (0 R (1 U p1))
(1 U p0) U (0 R p1)
(0 R p0) U p1
(1 U p0) & (1 U (1 U p0)) & (0 R !p0) & (0 R (0 R !p0))
(0 R (1 U p0)) & (1 U (0 R !p1))
((0 R (1 U p0)) & (1 U (0 R !p1))) | ((0 R (1 U p1)) & (1 U (0 R !p0)))
p0 R (p0 | p1)
(Xp0 U Xp1) | X(!p0 R !p1)
(Xp0 U p1) | X(!p0 R (!p0 | !p1))
(0 R (!p0 | (1 U p1))) & ((Xp0 U p1) | X(!p0 R (!p0 | !p1)))
(0 R (!p0 | (1 U p1))) & ((Xp0 U Xp1) | X(!p0 R !p1))
0 R (!p0 | (1 U p1))
1 U (p0 & X(!p1 U !p2))
(1 U (0 R !p0)) & (0 R (1 U !p1))
0 R ((1 U p0) & (1 U p1))
(1 U p0) & (1 U !p0)
(Xp1 & p2) R X(((p3 U p0) R p2) U (p3 R p2))
((0 R (p1 | (0 R (1 U p0)))) & (0 R (p2 | (0 R (1 U !p0))))) | (0 R p1) | (0 R p2)
((0 R (p1 | (1 U (0 R p0)))) & (0 R (p2 | (1 U (0 R !p0))))) | (0 R p1) | (0 R p2)
(0 R (p1 | X(0 R p0))) & (0 R (p2 | X(0 R !p0)))
0 R (p1 | (Xp0 & X!p0))
p0 | (p1 U p0)
p0 U (p1 & (0 R p2))
p0 U (p1 & X(p2 U p3))
p0 U (p1 & X(p2 & (1 U (p3 & X(1 U (p4 & X(1 U (p5 & X(1 U p6)))))))))
1 U (p0 & X(0 R p1))
1 U (p0 & X(p1 & X(1 U p2)))
1 U (p0 & X(p1 U p2))
(1 U (0 R p0)) | (1 U (0 R p1))
0 R (!p0 | (p1 U p2))
1 U (p0 & X(1 U (p1 & X(1 U (p2 & X(1 U p3))))))
(0 R (1 U p0)) & (0 R (1 U p1)) & (0 R (1 U p2)) & (0 R (1 U p3)) & (0 R (1 U p4))
(p0 U (p1 U p2)) | (p1 U (p2 U p0)) | (p2 U (p0 U p1))
0 R (!p0 | (p1 U ((0 R p2) | (0 R p3))))

100
bench/spin13/new-fair2.ltl Normal file
View file

@ -0,0 +1,100 @@
(F(FG!p2 | G(Gp0 U p1))) & ((FG(p10)) -> (GF(p11)))
(FGp0) & ((FG(p10)) -> (GF(p11)))
(F(Gp0 | F(FG!p1 R (!p2 | F!p3)))) & ((FG(p10)) -> (GF(p11)))
(FG(p0 & F(Gp0 R p1))) & ((FG(p10)) -> (GF(p11)))
(FG(!p0 & F(X!p1 | (p0 R p2))) U p0) & ((FG(p10)) -> (GF(p11)))
(F(Gp0 | G!p1)) & ((FG(p10)) -> (GF(p11)))
(F(Gp0 & (p1 U !p2))) & ((FG(p10)) -> (GF(p11)))
(FGp0 R X(p1 R (!p2 U X(p3 | GFp3)))) & ((FG(p10)) -> (GF(p11)))
(FGp0 U p1) & ((FG(p10)) -> (GF(p11)))
(F(p0 & F(p1 | (!p1 & !p2)))) & ((FG(p10)) -> (GF(p11)))
(F(p0 | F!p1 | (p2 R p3))) & ((FG(p10)) -> (GF(p11)))
(F(!p0 | G!p1 | Gp2)) & ((FG(p10)) -> (GF(p11)))
(F!p0 & ((Gp1 | (!p2 & !p3)) U Gp3)) & ((FG(p10)) -> (GF(p11)))
(Fp0 | (G!p1 R X((!p2 | !p3) R (!p1 & X!p2)))) & ((FG(p10)) -> (GF(p11)))
(Fp0 & (p1 U (p2 & p3)) & F(X!p4 | Gp0)) & ((FG(p10)) -> (GF(p11)))
(F(!p0 & !p1) | XF(p2 | X(p2 M p3))) & ((FG(p10)) -> (GF(p11)))
(F!p0 R ((p1 R p2) U (!p0 | !p3))) & ((FG(p10)) -> (GF(p11)))
((Fp0 U G!p1) | X(p2 | X(p2 M XF!p3))) & ((FG(p10)) -> (GF(p11)))
(F((p0 U Xp1) | XF(Fp1 R (!p2 R X!p0)))) & ((FG(p10)) -> (GF(p11)))
(F(!p0 W G(!p1 U !p2))) & ((FG(p10)) -> (GF(p11)))
(F(p0 | XFp1)) & ((FG(p10)) -> (GF(p11)))
(Fp0 | XG!p1) & ((FG(p10)) -> (GF(p11)))
(F(p0 & Xp1 & ((Xp2 & F(Gp4 & !p3)) | (X!p2 & G(F!p4 | p3))))) & ((FG(p10)) -> (GF(p11)))
(F(p1 | p0 | F(!p2 | !p3))) & ((FG(p10)) -> (GF(p11)))
(GF(Fp0 & X(p1 | X!p1))) & ((FG(p10)) -> (GF(p11)))
(GF(Gp1 & Fp0)) & ((FG(p10)) -> (GF(p11)))
(GF!p0 | G(!p0 | !p1)) & ((FG(p10)) -> (GF(p11)))
(G((Fp0 & (p1 | G!p2)) | (Fp3 & (!p1 | X(!p1 M X!p2))))) & ((FG(p10)) -> (GF(p11)))
(G(F(p0 & !p1) | X(!p0 | !p2))) & ((FG(p10)) -> (GF(p11)))
(GFp0 R ((XX(!p1 R !p2) | (!p1 & !p3)) U p4)) & ((FG(p10)) -> (GF(p11)))
(GFp0 U G(p0 | G!p1 | XFp2)) & ((FG(p10)) -> (GF(p11)))
(G((Fp0 U p1) U (p1 & F!p2))) & ((FG(p10)) -> (GF(p11)))
(GFp0 U XXXp1) & ((FG(p10)) -> (GF(p11)))
(G(Gp0 & (Fp1 | G!p2))) & ((FG(p10)) -> (GF(p11)))
(G(G!p0 | (!p1 & X!p1)) | XF(FG!p2 R !p0)) & ((FG(p10)) -> (GF(p11)))
(Gp0 | G(Fp1 | Gp2)) & ((FG(p10)) -> (GF(p11)))
(G(p0 & GF!p1) U (FG!p2 R Xp3)) & ((FG(p10)) -> (GF(p11)))
(G!p0 | G(p0 & Gp1)) & ((FG(p10)) -> (GF(p11)))
(Gp0 | (((p1 & (!p2 R !p3)) R p4))) & ((FG(p10)) -> (GF(p11)))
(Gp0 | ((p1 U p2) R F!p3)) & ((FG(p10)) -> (GF(p11)))
((Gp0 R !p1) R (FGp2 R F!p3)) & ((FG(p10)) -> (GF(p11)))
(G(!p0 U !p1) R ((p2 R !p3) U G(p1 | F!p4))) & ((FG(p10)) -> (GF(p11)))
(G(!p0 | X(!p0 M (p1 U p0))) U (p2 U p3)) & ((FG(p10)) -> (GF(p11)))
((G!p1 | XXXp0) U Gp2) & ((FG(p10)) -> (GF(p11)))
(!p0 & (FG!p1 | (GFp2 R (p0 | X(p0 M (p4 & p3)))))) & ((FG(p10)) -> (GF(p11)))
(p0 | F(G(p1 U p2) | (!p2 & !p3))) & ((FG(p10)) -> (GF(p11)))
(!p0 & Fp1 & FG(((p2 | !p3) R p1) U !p4)) & ((FG(p10)) -> (GF(p11)))
(!p0 | Fp1 | G!p2) & ((FG(p10)) -> (GF(p11)))
(!p0 | F(p1 | !p2)) & ((FG(p10)) -> (GF(p11)))
(!p0 | (Fp1 U (Fp2 R p0))) & ((FG(p10)) -> (GF(p11)))
(p0 | ((G!p1 U G!p2) R !p2)) & ((FG(p10)) -> (GF(p11)))
(p0 & (Gp1 | XXFp2)) & ((FG(p10)) -> (GF(p11)))
(!p0 | (((!p1 & Fp2) R (!p4 & p3)) & (G!p4 U !p2))) & ((FG(p10)) -> (GF(p11)))
((((p0 & !p1) | (p1 & !p0)) R F!p0) | G((p2 & ((!p0 & Gp3) | (p0 & F!p3))) | (!p2 & ((!p0 & F!p3) | (p0 & Gp3))))) & ((FG(p10)) -> (GF(p11)))
(p0 & (p1 U p2) & FGp3) & ((FG(p10)) -> (GF(p11)))
(p0 | (p1 U !p2) | FG(p4 | p3)) & ((FG(p10)) -> (GF(p11)))
((((!p0 & !p1) U !p2) R (!p3 R !p0)) U (p1 R p3)) & ((FG(p10)) -> (GF(p11)))
(p0 & !p1 & X(!p2 | GF(p3 & Xp2))) & ((FG(p10)) -> (GF(p11)))
((!p0 | (p2 & Gp1)) U X(Gp0 | (Xp4 & !p3))) & ((FG(p10)) -> (GF(p11)))
((!p0 R !p1) & (G((p2 U !p3) & (p4 R p5)) | (Fp1 U p1))) & ((FG(p10)) -> (GF(p11)))
((p0 R !p1) R (G!p2 R F!p3)) & ((FG(p10)) -> (GF(p11)))
((p0 R p1) U ((p3 | Fp2) & ((p2 | p3) U !p4))) & ((FG(p10)) -> (GF(p11)))
(!p0 R X((G!p1 & (!p2 | (!p1 & p3) | (p1 & !p3))) | (p2 & Fp1 & ((!p1 & !p3) | (p1 & p3))))) & ((FG(p10)) -> (GF(p11)))
((p0 R Xp1) & FG(p2 | X!p2)) & ((FG(p10)) -> (GF(p11)))
((p0 U p1) & G(FG!p2 & F(p3 R !p0))) & ((FG(p10)) -> (GF(p11)))
(!p0 U (p1 & ((!p2 | (p4 & !p3)) U (p5 R p6)))) & ((FG(p10)) -> (GF(p11)))
(!p0 W XG!p1) & ((FG(p10)) -> (GF(p11)))
(p0 | X(GF!p1 | (p0 M !p2))) & ((FG(p10)) -> (GF(p11)))
(!p0 | XGp0 | (FG(p1 U p0) U X!p2)) & ((FG(p10)) -> (GF(p11)))
(((!p0 & XG!p1) R !p2) R (p3 | Fp4)) & ((FG(p10)) -> (GF(p11)))
(p0 | X(p0 M Xp1) | (p2 & p3 & F(!p3 & X(!p3 W G!p4)))) & ((FG(p10)) -> (GF(p11)))
(p0 | ((Xp1 | (!p1 & ((!p0 U !p2) U p1))) R !p3)) & ((FG(p10)) -> (GF(p11)))
(p0 | X(p1 | !p2)) & ((FG(p10)) -> (GF(p11)))
(((p0 | Xp1) U (p2 R p3)) R ((p3 U p4) | G(!p5 | X!p0))) & ((FG(p10)) -> (GF(p11)))
(p1 | F!p0 | XF(p1 | !p2 | Fp3)) & ((FG(p10)) -> (GF(p11)))
((p1 | !p0) U ((p2 R XXp3) U (Fp4 U Xp3))) & ((FG(p10)) -> (GF(p11)))
((p1 | p0) U (!p2 & XFp3)) & ((FG(p10)) -> (GF(p11)))
(p1 | !p0 | X((p1 | !p0) M ((!p2 R !p3) | XG!p0))) & ((FG(p10)) -> (GF(p11)))
(XF(Gp0 | (p1 & (!p2 | p3)))) & ((FG(p10)) -> (GF(p11)))
(X(FGp0 U Gp1) U (Fp2 U Gp3)) & ((FG(p10)) -> (GF(p11)))
(XF(!p0 | Fp1)) & ((FG(p10)) -> (GF(p11)))
(XF(p0 & GF!p1)) & ((FG(p10)) -> (GF(p11)))
(X(Fp0 & (((p0 U Gp1) U (!p2 R !p3)) R (p4 | Fp5)))) & ((FG(p10)) -> (GF(p11)))
(XF(p0 | ((p1 R p2) R Xp3))) & ((FG(p10)) -> (GF(p11)))
(X(Fp0 & (p1 U p2))) & ((FG(p10)) -> (GF(p11)))
(XF(p0 & (p1 | Xp2))) & ((FG(p10)) -> (GF(p11)))
(X(F!p0 U Gp1)) & ((FG(p10)) -> (GF(p11)))
(XG((F!p0 & !p1) | (p1 & Gp0))) & ((FG(p10)) -> (GF(p11)))
(X(GF(!p0 & (p1 | !p2)) | (p2 & !p3 & (F!p4 U !p5)))) & ((FG(p10)) -> (GF(p11)))
(X(G((p0 & F!p1) U p2) U (!p2 R (p2 | p3)))) & ((FG(p10)) -> (GF(p11)))
(XGp0 & ((p1 R (p2 & F!p3)) | GF(!p4 | p3))) & ((FG(p10)) -> (GF(p11)))
(X(Gp0 U (GF!p0 | (p1 & Xp0)))) & ((FG(p10)) -> (GF(p11)))
(XGp0 | (XG!p0 & (!p1 | p3 | Xp2))) & ((FG(p10)) -> (GF(p11)))
(X!p0 | (FGp1 U p2)) & ((FG(p10)) -> (GF(p11)))
(Xp0 | ((!p1 | X(!p1 M (F!p1 U p2))) U !p3)) & ((FG(p10)) -> (GF(p11)))
(X((!p0 | p2 | !p1) U Gp0)) & ((FG(p10)) -> (GF(p11)))
(X(((p0 R F!p1) U p2) U Gp3)) & ((FG(p10)) -> (GF(p11)))
(Xp0 U (((p1 U p2) U p3) & (F!p4 U p2))) & ((FG(p10)) -> (GF(p11)))
(XXF!p1 & (p0 U !p1)) & ((FG(p10)) -> (GF(p11)))
(XXG((p0 | Fp1) & (!p0 R (p2 & !p3)))) & ((FG(p10)) -> (GF(p11)))

100
bench/spin13/new-strong1.ltl Normal file
View file

@ -0,0 +1,100 @@
(F(FG!p2 | G(Gp0 U p1))) & ((GF(p10)) -> (GF(p11)))
(FGp0) & ((GF(p10)) -> (GF(p11)))
(F(Gp0 | F(FG!p1 R (!p2 | F!p3)))) & ((GF(p10)) -> (GF(p11)))
(FG(p0 & F(Gp0 R p1))) & ((GF(p10)) -> (GF(p11)))
(FG(!p0 & F(X!p1 | (p0 R p2))) U p0) & ((GF(p10)) -> (GF(p11)))
(F(Gp0 | G!p1)) & ((GF(p10)) -> (GF(p11)))
(F(Gp0 & (p1 U !p2))) & ((GF(p10)) -> (GF(p11)))
(FGp0 R X(p1 R (!p2 U X(p3 | GFp3)))) & ((GF(p10)) -> (GF(p11)))
(FGp0 U p1) & ((GF(p10)) -> (GF(p11)))
(F(p0 & F(p1 | (!p1 & !p2)))) & ((GF(p10)) -> (GF(p11)))
(F(p0 | F!p1 | (p2 R p3))) & ((GF(p10)) -> (GF(p11)))
(F(!p0 | G!p1 | Gp2)) & ((GF(p10)) -> (GF(p11)))
(F!p0 & ((Gp1 | (!p2 & !p3)) U Gp3)) & ((GF(p10)) -> (GF(p11)))
(Fp0 | (G!p1 R X((!p2 | !p3) R (!p1 & X!p2)))) & ((GF(p10)) -> (GF(p11)))
(Fp0 & (p1 U (p2 & p3)) & F(X!p4 | Gp0)) & ((GF(p10)) -> (GF(p11)))
(F(!p0 & !p1) | XF(p2 | X(p2 M p3))) & ((GF(p10)) -> (GF(p11)))
(F!p0 R ((p1 R p2) U (!p0 | !p3))) & ((GF(p10)) -> (GF(p11)))
((Fp0 U G!p1) | X(p2 | X(p2 M XF!p3))) & ((GF(p10)) -> (GF(p11)))
(F((p0 U Xp1) | XF(Fp1 R (!p2 R X!p0)))) & ((GF(p10)) -> (GF(p11)))
(F(!p0 W G(!p1 U !p2))) & ((GF(p10)) -> (GF(p11)))
(F(p0 | XFp1)) & ((GF(p10)) -> (GF(p11)))
(Fp0 | XG!p1) & ((GF(p10)) -> (GF(p11)))
(F(p0 & Xp1 & ((Xp2 & F(Gp4 & !p3)) | (X!p2 & G(F!p4 | p3))))) & ((GF(p10)) -> (GF(p11)))
(F(p1 | p0 | F(!p2 | !p3))) & ((GF(p10)) -> (GF(p11)))
(GF(Fp0 & X(p1 | X!p1))) & ((GF(p10)) -> (GF(p11)))
(GF(Gp1 & Fp0)) & ((GF(p10)) -> (GF(p11)))
(GF!p0 | G(!p0 | !p1)) & ((GF(p10)) -> (GF(p11)))
(G((Fp0 & (p1 | G!p2)) | (Fp3 & (!p1 | X(!p1 M X!p2))))) & ((GF(p10)) -> (GF(p11)))
(G(F(p0 & !p1) | X(!p0 | !p2))) & ((GF(p10)) -> (GF(p11)))
(GFp0 R ((XX(!p1 R !p2) | (!p1 & !p3)) U p4)) & ((GF(p10)) -> (GF(p11)))
(GFp0 U G(p0 | G!p1 | XFp2)) & ((GF(p10)) -> (GF(p11)))
(G((Fp0 U p1) U (p1 & F!p2))) & ((GF(p10)) -> (GF(p11)))
(GFp0 U XXXp1) & ((GF(p10)) -> (GF(p11)))
(G(Gp0 & (Fp1 | G!p2))) & ((GF(p10)) -> (GF(p11)))
(G(G!p0 | (!p1 & X!p1)) | XF(FG!p2 R !p0)) & ((GF(p10)) -> (GF(p11)))
(Gp0 | G(Fp1 | Gp2)) & ((GF(p10)) -> (GF(p11)))
(G(p0 & GF!p1) U (FG!p2 R Xp3)) & ((GF(p10)) -> (GF(p11)))
(G!p0 | G(p0 & Gp1)) & ((GF(p10)) -> (GF(p11)))
(Gp0 | (((p1 & (!p2 R !p3)) R p4))) & ((GF(p10)) -> (GF(p11)))
(Gp0 | ((p1 U p2) R F!p3)) & ((GF(p10)) -> (GF(p11)))
((Gp0 R !p1) R (FGp2 R F!p3)) & ((GF(p10)) -> (GF(p11)))
(G(!p0 U !p1) R ((p2 R !p3) U G(p1 | F!p4))) & ((GF(p10)) -> (GF(p11)))
(G(!p0 | X(!p0 M (p1 U p0))) U (p2 U p3)) & ((GF(p10)) -> (GF(p11)))
((G!p1 | XXXp0) U Gp2) & ((GF(p10)) -> (GF(p11)))
(!p0 & (FG!p1 | (GFp2 R (p0 | X(p0 M (p4 & p3)))))) & ((GF(p10)) -> (GF(p11)))
(p0 | F(G(p1 U p2) | (!p2 & !p3))) & ((GF(p10)) -> (GF(p11)))
(!p0 & Fp1 & FG(((p2 | !p3) R p1) U !p4)) & ((GF(p10)) -> (GF(p11)))
(!p0 | Fp1 | G!p2) & ((GF(p10)) -> (GF(p11)))
(!p0 | F(p1 | !p2)) & ((GF(p10)) -> (GF(p11)))
(!p0 | (Fp1 U (Fp2 R p0))) & ((GF(p10)) -> (GF(p11)))
(p0 | ((G!p1 U G!p2) R !p2)) & ((GF(p10)) -> (GF(p11)))
(p0 & (Gp1 | XXFp2)) & ((GF(p10)) -> (GF(p11)))
(!p0 | (((!p1 & Fp2) R (!p4 & p3)) & (G!p4 U !p2))) & ((GF(p10)) -> (GF(p11)))
((((p0 & !p1) | (p1 & !p0)) R F!p0) | G((p2 & ((!p0 & Gp3) | (p0 & F!p3))) | (!p2 & ((!p0 & F!p3) | (p0 & Gp3))))) & ((GF(p10)) -> (GF(p11)))
(p0 & (p1 U p2) & FGp3) & ((GF(p10)) -> (GF(p11)))
(p0 | (p1 U !p2) | FG(p4 | p3)) & ((GF(p10)) -> (GF(p11)))
((((!p0 & !p1) U !p2) R (!p3 R !p0)) U (p1 R p3)) & ((GF(p10)) -> (GF(p11)))
(p0 & !p1 & X(!p2 | GF(p3 & Xp2))) & ((GF(p10)) -> (GF(p11)))
((!p0 | (p2 & Gp1)) U X(Gp0 | (Xp4 & !p3))) & ((GF(p10)) -> (GF(p11)))
((!p0 R !p1) & (G((p2 U !p3) & (p4 R p5)) | (Fp1 U p1))) & ((GF(p10)) -> (GF(p11)))
((p0 R !p1) R (G!p2 R F!p3)) & ((GF(p10)) -> (GF(p11)))
((p0 R p1) U ((p3 | Fp2) & ((p2 | p3) U !p4))) & ((GF(p10)) -> (GF(p11)))
(!p0 R X((G!p1 & (!p2 | (!p1 & p3) | (p1 & !p3))) | (p2 & Fp1 & ((!p1 & !p3) | (p1 & p3))))) & ((GF(p10)) -> (GF(p11)))
((p0 R Xp1) & FG(p2 | X!p2)) & ((GF(p10)) -> (GF(p11)))
((p0 U p1) & G(FG!p2 & F(p3 R !p0))) & ((GF(p10)) -> (GF(p11)))
(!p0 U (p1 & ((!p2 | (p4 & !p3)) U (p5 R p6)))) & ((GF(p10)) -> (GF(p11)))
(!p0 W XG!p1) & ((GF(p10)) -> (GF(p11)))
(p0 | X(GF!p1 | (p0 M !p2))) & ((GF(p10)) -> (GF(p11)))
(!p0 | XGp0 | (FG(p1 U p0) U X!p2)) & ((GF(p10)) -> (GF(p11)))
(((!p0 & XG!p1) R !p2) R (p3 | Fp4)) & ((GF(p10)) -> (GF(p11)))
(p0 | X(p0 M Xp1) | (p2 & p3 & F(!p3 & X(!p3 W G!p4)))) & ((GF(p10)) -> (GF(p11)))
(p0 | ((Xp1 | (!p1 & ((!p0 U !p2) U p1))) R !p3)) & ((GF(p10)) -> (GF(p11)))
(p0 | X(p1 | !p2)) & ((GF(p10)) -> (GF(p11)))
(((p0 | Xp1) U (p2 R p3)) R ((p3 U p4) | G(!p5 | X!p0))) & ((GF(p10)) -> (GF(p11)))
(p1 | F!p0 | XF(p1 | !p2 | Fp3)) & ((GF(p10)) -> (GF(p11)))
((p1 | !p0) U ((p2 R XXp3) U (Fp4 U Xp3))) & ((GF(p10)) -> (GF(p11)))
((p1 | p0) U (!p2 & XFp3)) & ((GF(p10)) -> (GF(p11)))
(p1 | !p0 | X((p1 | !p0) M ((!p2 R !p3) | XG!p0))) & ((GF(p10)) -> (GF(p11)))
(XF(Gp0 | (p1 & (!p2 | p3)))) & ((GF(p10)) -> (GF(p11)))
(X(FGp0 U Gp1) U (Fp2 U Gp3)) & ((GF(p10)) -> (GF(p11)))
(XF(!p0 | Fp1)) & ((GF(p10)) -> (GF(p11)))
(XF(p0 & GF!p1)) & ((GF(p10)) -> (GF(p11)))
(X(Fp0 & (((p0 U Gp1) U (!p2 R !p3)) R (p4 | Fp5)))) & ((GF(p10)) -> (GF(p11)))
(XF(p0 | ((p1 R p2) R Xp3))) & ((GF(p10)) -> (GF(p11)))
(X(Fp0 & (p1 U p2))) & ((GF(p10)) -> (GF(p11)))
(XF(p0 & (p1 | Xp2))) & ((GF(p10)) -> (GF(p11)))
(X(F!p0 U Gp1)) & ((GF(p10)) -> (GF(p11)))
(XG((F!p0 & !p1) | (p1 & Gp0))) & ((GF(p10)) -> (GF(p11)))
(X(GF(!p0 & (p1 | !p2)) | (p2 & !p3 & (F!p4 U !p5)))) & ((GF(p10)) -> (GF(p11)))
(X(G((p0 & F!p1) U p2) U (!p2 R (p2 | p3)))) & ((GF(p10)) -> (GF(p11)))
(XGp0 & ((p1 R (p2 & F!p3)) | GF(!p4 | p3))) & ((GF(p10)) -> (GF(p11)))
(X(Gp0 U (GF!p0 | (p1 & Xp0)))) & ((GF(p10)) -> (GF(p11)))
(XGp0 | (XG!p0 & (!p1 | p3 | Xp2))) & ((GF(p10)) -> (GF(p11)))
(X!p0 | (FGp1 U p2)) & ((GF(p10)) -> (GF(p11)))
(Xp0 | ((!p1 | X(!p1 M (F!p1 U p2))) U !p3)) & ((GF(p10)) -> (GF(p11)))
(X((!p0 | p2 | !p1) U Gp0)) & ((GF(p10)) -> (GF(p11)))
(X(((p0 R F!p1) U p2) U Gp3)) & ((GF(p10)) -> (GF(p11)))
(Xp0 U (((p1 U p2) U p3) & (F!p4 U p2))) & ((GF(p10)) -> (GF(p11)))
(XXF!p1 & (p0 U !p1)) & ((GF(p10)) -> (GF(p11)))
(XXG((p0 | Fp1) & (!p0 R (p2 & !p3)))) & ((GF(p10)) -> (GF(p11)))

100
bench/spin13/new-strong2.ltl Normal file
View file

@ -0,0 +1,100 @@
(F(FG!p2 | G(Gp0 U p1))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(FGp0) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(F(Gp0 | F(FG!p1 R (!p2 | F!p3)))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(FG(p0 & F(Gp0 R p1))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(FG(!p0 & F(X!p1 | (p0 R p2))) U p0) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(F(Gp0 | G!p1)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(F(Gp0 & (p1 U !p2))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(FGp0 R X(p1 R (!p2 U X(p3 | GFp3)))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(FGp0 U p1) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(F(p0 & F(p1 | (!p1 & !p2)))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(F(p0 | F!p1 | (p2 R p3))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(F(!p0 | G!p1 | Gp2)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(F!p0 & ((Gp1 | (!p2 & !p3)) U Gp3)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(Fp0 | (G!p1 R X((!p2 | !p3) R (!p1 & X!p2)))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(Fp0 & (p1 U (p2 & p3)) & F(X!p4 | Gp0)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(F(!p0 & !p1) | XF(p2 | X(p2 M p3))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(F!p0 R ((p1 R p2) U (!p0 | !p3))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
((Fp0 U G!p1) | X(p2 | X(p2 M XF!p3))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(F((p0 U Xp1) | XF(Fp1 R (!p2 R X!p0)))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(F(!p0 W G(!p1 U !p2))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(F(p0 | XFp1)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(Fp0 | XG!p1) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(F(p0 & Xp1 & ((Xp2 & F(Gp4 & !p3)) | (X!p2 & G(F!p4 | p3))))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(F(p1 | p0 | F(!p2 | !p3))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(GF(Fp0 & X(p1 | X!p1))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(GF(Gp1 & Fp0)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(GF!p0 | G(!p0 | !p1)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(G((Fp0 & (p1 | G!p2)) | (Fp3 & (!p1 | X(!p1 M X!p2))))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(G(F(p0 & !p1) | X(!p0 | !p2))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(GFp0 R ((XX(!p1 R !p2) | (!p1 & !p3)) U p4)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(GFp0 U G(p0 | G!p1 | XFp2)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(G((Fp0 U p1) U (p1 & F!p2))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(GFp0 U XXXp1) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(G(Gp0 & (Fp1 | G!p2))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(G(G!p0 | (!p1 & X!p1)) | XF(FG!p2 R !p0)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(Gp0 | G(Fp1 | Gp2)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(G(p0 & GF!p1) U (FG!p2 R Xp3)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(G!p0 | G(p0 & Gp1)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(Gp0 | (((p1 & (!p2 R !p3)) R p4))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(Gp0 | ((p1 U p2) R F!p3)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
((Gp0 R !p1) R (FGp2 R F!p3)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(G(!p0 U !p1) R ((p2 R !p3) U G(p1 | F!p4))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(G(!p0 | X(!p0 M (p1 U p0))) U (p2 U p3)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
((G!p1 | XXXp0) U Gp2) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(!p0 & (FG!p1 | (GFp2 R (p0 | X(p0 M (p4 & p3)))))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(p0 | F(G(p1 U p2) | (!p2 & !p3))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(!p0 & Fp1 & FG(((p2 | !p3) R p1) U !p4)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(!p0 | Fp1 | G!p2) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(!p0 | F(p1 | !p2)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(!p0 | (Fp1 U (Fp2 R p0))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(p0 | ((G!p1 U G!p2) R !p2)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(p0 & (Gp1 | XXFp2)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(!p0 | (((!p1 & Fp2) R (!p4 & p3)) & (G!p4 U !p2))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
((((p0 & !p1) | (p1 & !p0)) R F!p0) | G((p2 & ((!p0 & Gp3) | (p0 & F!p3))) | (!p2 & ((!p0 & F!p3) | (p0 & Gp3))))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(p0 & (p1 U p2) & FGp3) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(p0 | (p1 U !p2) | FG(p4 | p3)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
((((!p0 & !p1) U !p2) R (!p3 R !p0)) U (p1 R p3)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(p0 & !p1 & X(!p2 | GF(p3 & Xp2))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
((!p0 | (p2 & Gp1)) U X(Gp0 | (Xp4 & !p3))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
((!p0 R !p1) & (G((p2 U !p3) & (p4 R p5)) | (Fp1 U p1))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
((p0 R !p1) R (G!p2 R F!p3)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
((p0 R p1) U ((p3 | Fp2) & ((p2 | p3) U !p4))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(!p0 R X((G!p1 & (!p2 | (!p1 & p3) | (p1 & !p3))) | (p2 & Fp1 & ((!p1 & !p3) | (p1 & p3))))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
((p0 R Xp1) & FG(p2 | X!p2)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
((p0 U p1) & G(FG!p2 & F(p3 R !p0))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(!p0 U (p1 & ((!p2 | (p4 & !p3)) U (p5 R p6)))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(!p0 W XG!p1) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(p0 | X(GF!p1 | (p0 M !p2))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(!p0 | XGp0 | (FG(p1 U p0) U X!p2)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(((!p0 & XG!p1) R !p2) R (p3 | Fp4)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(p0 | X(p0 M Xp1) | (p2 & p3 & F(!p3 & X(!p3 W G!p4)))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(p0 | ((Xp1 | (!p1 & ((!p0 U !p2) U p1))) R !p3)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(p0 | X(p1 | !p2)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(((p0 | Xp1) U (p2 R p3)) R ((p3 U p4) | G(!p5 | X!p0))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(p1 | F!p0 | XF(p1 | !p2 | Fp3)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
((p1 | !p0) U ((p2 R XXp3) U (Fp4 U Xp3))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
((p1 | p0) U (!p2 & XFp3)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(p1 | !p0 | X((p1 | !p0) M ((!p2 R !p3) | XG!p0))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(XF(Gp0 | (p1 & (!p2 | p3)))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(X(FGp0 U Gp1) U (Fp2 U Gp3)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(XF(!p0 | Fp1)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(XF(p0 & GF!p1)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(X(Fp0 & (((p0 U Gp1) U (!p2 R !p3)) R (p4 | Fp5)))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(XF(p0 | ((p1 R p2) R Xp3))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(X(Fp0 & (p1 U p2))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(XF(p0 & (p1 | Xp2))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(X(F!p0 U Gp1)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(XG((F!p0 & !p1) | (p1 & Gp0))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(X(GF(!p0 & (p1 | !p2)) | (p2 & !p3 & (F!p4 U !p5)))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(X(G((p0 & F!p1) U p2) U (!p2 R (p2 | p3)))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(XGp0 & ((p1 R (p2 & F!p3)) | GF(!p4 | p3))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(X(Gp0 U (GF!p0 | (p1 & Xp0)))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(XGp0 | (XG!p0 & (!p1 | p3 | Xp2))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(X!p0 | (FGp1 U p2)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(Xp0 | ((!p1 | X(!p1 M (F!p1 U p2))) U !p3)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(X((!p0 | p2 | !p1) U Gp0)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(X(((p0 R F!p1) U p2) U Gp3)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(Xp0 U (((p1 U p2) U p3) & (F!p4 U p2))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(XXF!p1 & (p0 U !p1)) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))
(XXG((p0 | Fp1) & (!p0 R (p2 & !p3)))) & ((GF(p10)) -> (GF(p11))) & ((GF(p12)) -> (GF(p13)))

100
bench/spin13/new-weak3.ltl Normal file
View file

@ -0,0 +1,100 @@
(F(FG!p2 | G(Gp0 U p1))) & (GF(p10) & GF(p11) & GF(p12))
(FGp0) & (GF(p10) & GF(p11) & GF(p12))
(F(Gp0 | F(FG!p1 R (!p2 | F!p3)))) & (GF(p10) & GF(p11) & GF(p12))
(FG(p0 & F(Gp0 R p1))) & (GF(p10) & GF(p11) & GF(p12))
(FG(!p0 & F(X!p1 | (p0 R p2))) U p0) & (GF(p10) & GF(p11) & GF(p12))
(F(Gp0 | G!p1)) & (GF(p10) & GF(p11) & GF(p12))
(F(Gp0 & (p1 U !p2))) & (GF(p10) & GF(p11) & GF(p12))
(FGp0 R X(p1 R (!p2 U X(p3 | GFp3)))) & (GF(p10) & GF(p11) & GF(p12))
(FGp0 U p1) & (GF(p10) & GF(p11) & GF(p12))
(F(p0 & F(p1 | (!p1 & !p2)))) & (GF(p10) & GF(p11) & GF(p12))
(F(p0 | F!p1 | (p2 R p3))) & (GF(p10) & GF(p11) & GF(p12))
(F(!p0 | G!p1 | Gp2)) & (GF(p10) & GF(p11) & GF(p12))
(F!p0 & ((Gp1 | (!p2 & !p3)) U Gp3)) & (GF(p10) & GF(p11) & GF(p12))
(Fp0 | (G!p1 R X((!p2 | !p3) R (!p1 & X!p2)))) & (GF(p10) & GF(p11) & GF(p12))
(Fp0 & (p1 U (p2 & p3)) & F(X!p4 | Gp0)) & (GF(p10) & GF(p11) & GF(p12))
(F(!p0 & !p1) | XF(p2 | X(p2 M p3))) & (GF(p10) & GF(p11) & GF(p12))
(F!p0 R ((p1 R p2) U (!p0 | !p3))) & (GF(p10) & GF(p11) & GF(p12))
((Fp0 U G!p1) | X(p2 | X(p2 M XF!p3))) & (GF(p10) & GF(p11) & GF(p12))
(F((p0 U Xp1) | XF(Fp1 R (!p2 R X!p0)))) & (GF(p10) & GF(p11) & GF(p12))
(F(!p0 W G(!p1 U !p2))) & (GF(p10) & GF(p11) & GF(p12))
(F(p0 | XFp1)) & (GF(p10) & GF(p11) & GF(p12))
(Fp0 | XG!p1) & (GF(p10) & GF(p11) & GF(p12))
(F(p0 & Xp1 & ((Xp2 & F(Gp4 & !p3)) | (X!p2 & G(F!p4 | p3))))) & (GF(p10) & GF(p11) & GF(p12))
(F(p1 | p0 | F(!p2 | !p3))) & (GF(p10) & GF(p11) & GF(p12))
(GF(Fp0 & X(p1 | X!p1))) & (GF(p10) & GF(p11) & GF(p12))
(GF(Gp1 & Fp0)) & (GF(p10) & GF(p11) & GF(p12))
(GF!p0 | G(!p0 | !p1)) & (GF(p10) & GF(p11) & GF(p12))
(G((Fp0 & (p1 | G!p2)) | (Fp3 & (!p1 | X(!p1 M X!p2))))) & (GF(p10) & GF(p11) & GF(p12))
(G(F(p0 & !p1) | X(!p0 | !p2))) & (GF(p10) & GF(p11) & GF(p12))
(GFp0 R ((XX(!p1 R !p2) | (!p1 & !p3)) U p4)) & (GF(p10) & GF(p11) & GF(p12))
(GFp0 U G(p0 | G!p1 | XFp2)) & (GF(p10) & GF(p11) & GF(p12))
(G((Fp0 U p1) U (p1 & F!p2))) & (GF(p10) & GF(p11) & GF(p12))
(GFp0 U XXXp1) & (GF(p10) & GF(p11) & GF(p12))
(G(Gp0 & (Fp1 | G!p2))) & (GF(p10) & GF(p11) & GF(p12))
(G(G!p0 | (!p1 & X!p1)) | XF(FG!p2 R !p0)) & (GF(p10) & GF(p11) & GF(p12))
(Gp0 | G(Fp1 | Gp2)) & (GF(p10) & GF(p11) & GF(p12))
(G(p0 & GF!p1) U (FG!p2 R Xp3)) & (GF(p10) & GF(p11) & GF(p12))
(G!p0 | G(p0 & Gp1)) & (GF(p10) & GF(p11) & GF(p12))
(Gp0 | (((p1 & (!p2 R !p3)) R p4))) & (GF(p10) & GF(p11) & GF(p12))
(Gp0 | ((p1 U p2) R F!p3)) & (GF(p10) & GF(p11) & GF(p12))
((Gp0 R !p1) R (FGp2 R F!p3)) & (GF(p10) & GF(p11) & GF(p12))
(G(!p0 U !p1) R ((p2 R !p3) U G(p1 | F!p4))) & (GF(p10) & GF(p11) & GF(p12))
(G(!p0 | X(!p0 M (p1 U p0))) U (p2 U p3)) & (GF(p10) & GF(p11) & GF(p12))
((G!p1 | XXXp0) U Gp2) & (GF(p10) & GF(p11) & GF(p12))
(!p0 & (FG!p1 | (GFp2 R (p0 | X(p0 M (p4 & p3)))))) & (GF(p10) & GF(p11) & GF(p12))
(p0 | F(G(p1 U p2) | (!p2 & !p3))) & (GF(p10) & GF(p11) & GF(p12))
(!p0 & Fp1 & FG(((p2 | !p3) R p1) U !p4)) & (GF(p10) & GF(p11) & GF(p12))
(!p0 | Fp1 | G!p2) & (GF(p10) & GF(p11) & GF(p12))
(!p0 | F(p1 | !p2)) & (GF(p10) & GF(p11) & GF(p12))
(!p0 | (Fp1 U (Fp2 R p0))) & (GF(p10) & GF(p11) & GF(p12))
(p0 | ((G!p1 U G!p2) R !p2)) & (GF(p10) & GF(p11) & GF(p12))
(p0 & (Gp1 | XXFp2)) & (GF(p10) & GF(p11) & GF(p12))
(!p0 | (((!p1 & Fp2) R (!p4 & p3)) & (G!p4 U !p2))) & (GF(p10) & GF(p11) & GF(p12))
((((p0 & !p1) | (p1 & !p0)) R F!p0) | G((p2 & ((!p0 & Gp3) | (p0 & F!p3))) | (!p2 & ((!p0 & F!p3) | (p0 & Gp3))))) & (GF(p10) & GF(p11) & GF(p12))
(p0 & (p1 U p2) & FGp3) & (GF(p10) & GF(p11) & GF(p12))
(p0 | (p1 U !p2) | FG(p4 | p3)) & (GF(p10) & GF(p11) & GF(p12))
((((!p0 & !p1) U !p2) R (!p3 R !p0)) U (p1 R p3)) & (GF(p10) & GF(p11) & GF(p12))
(p0 & !p1 & X(!p2 | GF(p3 & Xp2))) & (GF(p10) & GF(p11) & GF(p12))
((!p0 | (p2 & Gp1)) U X(Gp0 | (Xp4 & !p3))) & (GF(p10) & GF(p11) & GF(p12))
((!p0 R !p1) & (G((p2 U !p3) & (p4 R p5)) | (Fp1 U p1))) & (GF(p10) & GF(p11) & GF(p12))
((p0 R !p1) R (G!p2 R F!p3)) & (GF(p10) & GF(p11) & GF(p12))
((p0 R p1) U ((p3 | Fp2) & ((p2 | p3) U !p4))) & (GF(p10) & GF(p11) & GF(p12))
(!p0 R X((G!p1 & (!p2 | (!p1 & p3) | (p1 & !p3))) | (p2 & Fp1 & ((!p1 & !p3) | (p1 & p3))))) & (GF(p10) & GF(p11) & GF(p12))
((p0 R Xp1) & FG(p2 | X!p2)) & (GF(p10) & GF(p11) & GF(p12))
((p0 U p1) & G(FG!p2 & F(p3 R !p0))) & (GF(p10) & GF(p11) & GF(p12))
(!p0 U (p1 & ((!p2 | (p4 & !p3)) U (p5 R p6)))) & (GF(p10) & GF(p11) & GF(p12))
(!p0 W XG!p1) & (GF(p10) & GF(p11) & GF(p12))
(p0 | X(GF!p1 | (p0 M !p2))) & (GF(p10) & GF(p11) & GF(p12))
(!p0 | XGp0 | (FG(p1 U p0) U X!p2)) & (GF(p10) & GF(p11) & GF(p12))
(((!p0 & XG!p1) R !p2) R (p3 | Fp4)) & (GF(p10) & GF(p11) & GF(p12))
(p0 | X(p0 M Xp1) | (p2 & p3 & F(!p3 & X(!p3 W G!p4)))) & (GF(p10) & GF(p11) & GF(p12))
(p0 | ((Xp1 | (!p1 & ((!p0 U !p2) U p1))) R !p3)) & (GF(p10) & GF(p11) & GF(p12))
(p0 | X(p1 | !p2)) & (GF(p10) & GF(p11) & GF(p12))
(((p0 | Xp1) U (p2 R p3)) R ((p3 U p4) | G(!p5 | X!p0))) & (GF(p10) & GF(p11) & GF(p12))
(p1 | F!p0 | XF(p1 | !p2 | Fp3)) & (GF(p10) & GF(p11) & GF(p12))
((p1 | !p0) U ((p2 R XXp3) U (Fp4 U Xp3))) & (GF(p10) & GF(p11) & GF(p12))
((p1 | p0) U (!p2 & XFp3)) & (GF(p10) & GF(p11) & GF(p12))
(p1 | !p0 | X((p1 | !p0) M ((!p2 R !p3) | XG!p0))) & (GF(p10) & GF(p11) & GF(p12))
(XF(Gp0 | (p1 & (!p2 | p3)))) & (GF(p10) & GF(p11) & GF(p12))
(X(FGp0 U Gp1) U (Fp2 U Gp3)) & (GF(p10) & GF(p11) & GF(p12))
(XF(!p0 | Fp1)) & (GF(p10) & GF(p11) & GF(p12))
(XF(p0 & GF!p1)) & (GF(p10) & GF(p11) & GF(p12))
(X(Fp0 & (((p0 U Gp1) U (!p2 R !p3)) R (p4 | Fp5)))) & (GF(p10) & GF(p11) & GF(p12))
(XF(p0 | ((p1 R p2) R Xp3))) & (GF(p10) & GF(p11) & GF(p12))
(X(Fp0 & (p1 U p2))) & (GF(p10) & GF(p11) & GF(p12))
(XF(p0 & (p1 | Xp2))) & (GF(p10) & GF(p11) & GF(p12))
(X(F!p0 U Gp1)) & (GF(p10) & GF(p11) & GF(p12))
(XG((F!p0 & !p1) | (p1 & Gp0))) & (GF(p10) & GF(p11) & GF(p12))
(X(GF(!p0 & (p1 | !p2)) | (p2 & !p3 & (F!p4 U !p5)))) & (GF(p10) & GF(p11) & GF(p12))
(X(G((p0 & F!p1) U p2) U (!p2 R (p2 | p3)))) & (GF(p10) & GF(p11) & GF(p12))
(XGp0 & ((p1 R (p2 & F!p3)) | GF(!p4 | p3))) & (GF(p10) & GF(p11) & GF(p12))
(X(Gp0 U (GF!p0 | (p1 & Xp0)))) & (GF(p10) & GF(p11) & GF(p12))
(XGp0 | (XG!p0 & (!p1 | p3 | Xp2))) & (GF(p10) & GF(p11) & GF(p12))
(X!p0 | (FGp1 U p2)) & (GF(p10) & GF(p11) & GF(p12))
(Xp0 | ((!p1 | X(!p1 M (F!p1 U p2))) U !p3)) & (GF(p10) & GF(p11) & GF(p12))
(X((!p0 | p2 | !p1) U Gp0)) & (GF(p10) & GF(p11) & GF(p12))
(X(((p0 R F!p1) U p2) U Gp3)) & (GF(p10) & GF(p11) & GF(p12))
(Xp0 U (((p1 U p2) U p3) & (F!p4 U p2))) & (GF(p10) & GF(p11) & GF(p12))
(XXF!p1 & (p0 U !p1)) & (GF(p10) & GF(p11) & GF(p12))
(XXG((p0 | Fp1) & (!p0 R (p2 & !p3)))) & (GF(p10) & GF(p11) & GF(p12))

100
bench/spin13/new.ltl Normal file
View file

@ -0,0 +1,100 @@
F(FG!p2 | G(Gp0 U p1))
FGp0
F(Gp0 | F(FG!p1 R (!p2 | F!p3)))
FG(p0 & F(Gp0 R p1))
FG(!p0 & F(X!p1 | (p0 R p2))) U p0
F(Gp0 | G!p1)
F(Gp0 & (p1 U !p2))
FGp0 R X(p1 R (!p2 U X(p3 | GFp3)))
FGp0 U p1
F(p0 & F(p1 | (!p1 & !p2)))
F(p0 | F!p1 | (p2 R p3))
F(!p0 | G!p1 | Gp2)
F!p0 & ((Gp1 | (!p2 & !p3)) U Gp3)
Fp0 | (G!p1 R X((!p2 | !p3) R (!p1 & X!p2)))
Fp0 & (p1 U (p2 & p3)) & F(X!p4 | Gp0)
F(!p0 & !p1) | XF(p2 | X(p2 M p3))
F!p0 R ((p1 R p2) U (!p0 | !p3))
(Fp0 U G!p1) | X(p2 | X(p2 M XF!p3))
F((p0 U Xp1) | XF(Fp1 R (!p2 R X!p0)))
F(!p0 W G(!p1 U !p2))
F(p0 | XFp1)
Fp0 | XG!p1
F(p0 & Xp1 & ((Xp2 & F(Gp4 & !p3)) | (X!p2 & G(F!p4 | p3))))
F(p1 | p0 | F(!p2 | !p3))
GF(Fp0 & X(p1 | X!p1))
GF(Gp1 & Fp0)
GF!p0 | G(!p0 | !p1)
G((Fp0 & (p1 | G!p2)) | (Fp3 & (!p1 | X(!p1 M X!p2))))
G(F(p0 & !p1) | X(!p0 | !p2))
GFp0 R ((XX(!p1 R !p2) | (!p1 & !p3)) U p4)
GFp0 U G(p0 | G!p1 | XFp2)
G((Fp0 U p1) U (p1 & F!p2))
GFp0 U XXXp1
G(Gp0 & (Fp1 | G!p2))
G(G!p0 | (!p1 & X!p1)) | XF(FG!p2 R !p0)
Gp0 | G(Fp1 | Gp2)
G(p0 & GF!p1) U (FG!p2 R Xp3)
G!p0 | G(p0 & Gp1)
Gp0 | (((p1 & (!p2 R !p3)) R p4))
Gp0 | ((p1 U p2) R F!p3)
(Gp0 R !p1) R (FGp2 R F!p3)
G(!p0 U !p1) R ((p2 R !p3) U G(p1 | F!p4))
G(!p0 | X(!p0 M (p1 U p0))) U (p2 U p3)
(G!p1 | XXXp0) U Gp2
!p0 & (FG!p1 | (GFp2 R (p0 | X(p0 M (p4 & p3)))))
p0 | F(G(p1 U p2) | (!p2 & !p3))
!p0 & Fp1 & FG(((p2 | !p3) R p1) U !p4)
!p0 | Fp1 | G!p2
!p0 | F(p1 | !p2)
!p0 | (Fp1 U (Fp2 R p0))
p0 | ((G!p1 U G!p2) R !p2)
p0 & (Gp1 | XXFp2)
!p0 | (((!p1 & Fp2) R (!p4 & p3)) & (G!p4 U !p2))
(((p0 & !p1) | (p1 & !p0)) R F!p0) | G((p2 & ((!p0 & Gp3) | (p0 & F!p3))) | (!p2 & ((!p0 & F!p3) | (p0 & Gp3))))
p0 & (p1 U p2) & FGp3
p0 | (p1 U !p2) | FG(p4 | p3)
(((!p0 & !p1) U !p2) R (!p3 R !p0)) U (p1 R p3)
p0 & !p1 & X(!p2 | GF(p3 & Xp2))
(!p0 | (p2 & Gp1)) U X(Gp0 | (Xp4 & !p3))
(!p0 R !p1) & (G((p2 U !p3) & (p4 R p5)) | (Fp1 U p1))
(p0 R !p1) R (G!p2 R F!p3)
(p0 R p1) U ((p3 | Fp2) & ((p2 | p3) U !p4))
!p0 R X((G!p1 & (!p2 | (!p1 & p3) | (p1 & !p3))) | (p2 & Fp1 & ((!p1 & !p3) | (p1 & p3))))
(p0 R Xp1) & FG(p2 | X!p2)
(p0 U p1) & G(FG!p2 & F(p3 R !p0))
!p0 U (p1 & ((!p2 | (p4 & !p3)) U (p5 R p6)))
!p0 W XG!p1
p0 | X(GF!p1 | (p0 M !p2))
!p0 | XGp0 | (FG(p1 U p0) U X!p2)
((!p0 & XG!p1) R !p2) R (p3 | Fp4)
p0 | X(p0 M Xp1) | (p2 & p3 & F(!p3 & X(!p3 W G!p4)))
p0 | ((Xp1 | (!p1 & ((!p0 U !p2) U p1))) R !p3)
p0 | X(p1 | !p2)
((p0 | Xp1) U (p2 R p3)) R ((p3 U p4) | G(!p5 | X!p0))
p1 | F!p0 | XF(p1 | !p2 | Fp3)
(p1 | !p0) U ((p2 R XXp3) U (Fp4 U Xp3))
(p1 | p0) U (!p2 & XFp3)
p1 | !p0 | X((p1 | !p0) M ((!p2 R !p3) | XG!p0))
XF(Gp0 | (p1 & (!p2 | p3)))
X(FGp0 U Gp1) U (Fp2 U Gp3)
XF(!p0 | Fp1)
XF(p0 & GF!p1)
X(Fp0 & (((p0 U Gp1) U (!p2 R !p3)) R (p4 | Fp5)))
XF(p0 | ((p1 R p2) R Xp3))
X(Fp0 & (p1 U p2))
XF(p0 & (p1 | Xp2))
X(F!p0 U Gp1)
XG((F!p0 & !p1) | (p1 & Gp0))
X(GF(!p0 & (p1 | !p2)) | (p2 & !p3 & (F!p4 U !p5)))
X(G((p0 & F!p1) U p2) U (!p2 R (p2 | p3)))
XGp0 & ((p1 R (p2 & F!p3)) | GF(!p4 | p3))
X(Gp0 U (GF!p0 | (p1 & Xp0)))
XGp0 | (XG!p0 & (!p1 | p3 | Xp2))
X!p0 | (FGp1 U p2)
Xp0 | ((!p1 | X(!p1 M (F!p1 U p2))) U !p3)
X((!p0 | p2 | !p1) U Gp0)
X(((p0 R F!p1) U p2) U Gp3)
Xp0 U (((p1 U p2) U p3) & (F!p4 U p2))
XXF!p1 & (p0 U !p1)
XXG((p0 | Fp1) & (!p0 R (p2 & !p3)))

221
bench/spin13/run.sh Executable file
View file

@ -0,0 +1,221 @@
#!/bin/sh
# -*- coding: utf-8 -*-
# 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 <http://www.gnu.org/licenses/>.
# This file produces a makefile (called run.mk) that runs all the
# configurations for our benchmarks possibly in parallel (using make
# -j8, for instance). The makefile in turn calls this script to run
# ltlcross, because the configuration of ltlcross is easier done in
# this shell script. We distinguish between these two uses of run.sh
# with the number of arguments: when no argument is given, we build a
# Makefile; when two arguments are given, we run ltlcross, reading
# formulas from standard input.
set -e
ltl2tgba=../../src/bin/ltl2tgba
ltlfilt=../../src/bin/ltlfilt
ltlcross=../../src/bin/ltlcross
# If two arguments are given, they should be
# ./run.sh formula.ltl prefix
# where prefix is "tgba-" or "ba-".
# The first argument is only used to name the resulting
# files and to decide if we should disable ltlcross
# check routines in order to check only positive or
# negative formulas.
if test $# = 2; then
f=$1
prefix=$2
case $2 in
tgba-)
opt=' --lbtt>%T'
ba=false
D=
d=
DB=
;;
ba-)
opt=' --spin>%N'
ba=:
D=D
d=d
DB=DB
;;
esac
opt="$opt --high"
nosim='-x !simul,!ba-simul'
set x
# Deter
$ba && set "$@" \
": LTL3BA NoSim NoSusp Deter; ltl3ba -A -M -f %s >%N" \
": LTL3BA Sim NoSusp Deter; ltl3ba -S -A -M -f %s >%N" \
": Cou99 '(Ad)' Deter; $ltl2tgba $opt $nosim --deter -x !degen-reset,!degen-lcache %f"
set "$@" \
": Cou99 '(A${D})' Deter; $ltl2tgba $opt $nosim --deter %f"
$ba && set "$@" \
": Cou99 '(ASd)' Deter; $ltl2tgba $opt -x !ba-simul,!degen-reset,!degen-lcache --deter %f" \
": Cou99 '(ASD)' Deter; $ltl2tgba $opt -x !ba-simul --deter %f"
set "$@" \
": Cou99 '(AS${DB})' Deter; $ltl2tgba $opt --deter %f"
$ba && set "$@" \
": Cou99 '(ASdB)' Deter; $ltl2tgba $opt --deter -x !degen-reset,!degen-lcache %f" \
": LTL3BA NoSim Susp Deter; ltl3ba -M -f %s >%N" \
": LTL3BA Sim Susp Deter; ltl3ba -S -M -f %s >%N"
set "$@" \
": Comp '(A${D})' Deter; $ltl2tgba -x comp-susp,!skel-simul $opt $nosim --deter %f" \
": Comp '(A${D})' Deter Early; $ltl2tgba -x comp-susp,!skel-simul,early-susp $opt $nosim --deter %f"
$ba && set "$@" \
": Comp '(ASD)' Deter; $ltl2tgba -x comp-susp,!ba-simul $opt --deter %f" \
": Comp '(ASD)' Deter Early; $ltl2tgba -x comp-susp,early-susp,!ba-simul $opt --deter %f"
set "$@" \
": Comp '(AS${DB})' Deter; $ltl2tgba -x comp-susp $opt --deter %f" \
": Comp '(AS${DB})' Deter Early; $ltl2tgba -x comp-susp,early-susp $opt --deter %f"
# Small
$ba && set "$@" \
": LTL3BA NoSim NoSusp; ltl3ba -A -f %s >%N" \
": LTL3BA Sim NoSusp; ltl3ba -S -A -f %s >%N" \
": Cou99 '(Ad)' Small; $ltl2tgba $opt $nosim --small -x !degen-reset,!degen-lcache %f"
set "$@" \
": Cou99 '(A${D})' Small; $ltl2tgba $opt $nosim --small %f"
$ba && set "$@" \
": Cou99 '(ASd)' Small; $ltl2tgba $opt -x !ba-simul,!degen-reset,!degen-lcache --small %f" \
": Cou99 '(ASD)' Small; $ltl2tgba $opt -x !ba-simul --small %f"
set "$@" \
": Cou99 '(AS${DB})' Small; $ltl2tgba $opt --small %f"
$ba && set "$@" \
": Cou99 '(ASdB)' Small; $ltl2tgba $opt --small -x !degen-reset,!degen-lcache %f" \
": LTL3BA NoSim Susp; ltl3ba -f %s >%N" \
": LTL3BA Sim Susp; ltl3ba -S -f %s >%N"
set "$@" \
": Comp '(A${D})' Small; $ltl2tgba -x comp-susp,!skel-wdba,!skel-simul $opt $nosim --small %f" \
": Comp '(A${D})' Small Early; $ltl2tgba -x comp-susp,!skel-wdba,!skel-simul,early-susp $opt $nosim --small %f"
$ba && set "$@" \
": Comp '(ASD)' Small; $ltl2tgba -x comp-susp,!skel-wdba,!ba-simul $opt --small %f" \
": Comp '(ASD)' Small Early; $ltl2tgba -x comp-susp,!no-skel-wdba,early-susp,!ba-simul $opt --small %f"
set "$@" \
": Comp '(AS${DB})' Small; $ltl2tgba -x comp-susp,!skel-wdba $opt --small %f" \
": Comp '(AS${DB})' Small Early; $ltl2tgba -x comp-susp,!skel-wdba,early-susp $opt --small %f"
# If the formulas are only positive or negative, disable checks so
# that ltlcross does not process the negation as well.
case $f in
*pos*|*neg*) set "$@" --no-check;;
esac
set "$@" --timeout=1200
shift
$ltlcross "$@" --json=$prefix$f.json --csv=$prefix$f.csv 2>$prefix$f.log
# Edit the JSON file to keep only the part of the name between ':' and ';',
# it's much more readable than the list of options...
perl -pi -e 's/":\s*(.*)\s*;.*"/"$1 "/' $prefix$f.json
exit $?
fi
if test $# -ne 0; then
echo "Wrong number of arguments." >&2
exit 1;
fi
# If no argument have been supplied, build a Makefile.
cat >run.mk <<\EOF
.PHONY: all _all
all: _all
.SUFFIXES: .json .html .tex .pdf
.json.html:
cat html.top $< html.bottom > $@.tmp
mv $@.tmp $@
.tex.pdf:
latexmk --pdf $<
EOF
all=
for prefix in tgba- ba-; do
presults=
for f in known.ltl; do
cat >>run.mk <<EOF
$prefix$f.stamp: $f $ltlcross $ltl2tgba
./run.sh $f $prefix <$f && touch \$@
$prefix$f.json $prefix$f.csv $prefix$f.log: $prefix$f.stamp
@:
EOF
presults="$presults $prefix$f.json"
done
for f in new.ltl new-fair2.ltl new-weak3.ltl new-strong1.ltl new-strong2.ltl; do
cat >>run.mk <<EOF
$prefix$f.pos.stamp: $f $ltlcross $ltl2tgba
./run.sh $f.pos $prefix <$f && touch \$@
$prefix$f.pos.json $prefix$f.pos.csv $prefix$f.pos.log: $prefix$f.pos.stamp
@:
$prefix$f.neg.stamp: $f $ltlcross $ltl2tgba
$ltlfilt --negate -F $f | ./run.sh $f.neg $prefix && touch \$@
$prefix$f.neg.json $prefix$f.neg.csv $prefix$f.neg.log: $prefix$f.neg.stamp
@:
EOF
presults="$presults $prefix$f.pos.json $prefix$f.neg.json"
done
v=`git describe --always --dirty 2>/dev/null ||
../../config.status --version | head -n 1 | cut -d' ' -f 3`
h=`hostname -f`
cat >>run.mk <<EOF
${prefix}sum.tex: $presults
../ltl2tgba/sum.py --intro "Version: $v; Date: `date -I`; Host: $h." \\
$presults >${prefix}sum.tex
EOF
log=`echo "$presults" | sed 's/json/log/g'`
csv=`echo "$presults" | sed 's/json/csv/g'`
html=`echo "$presults" | sed 's/json/html/g'`
all="$all ${prefix}sum.pdf ${prefix}sum.tex $results $csv $log $html"
done
arch=`date -I`.tar.xz
cat >>run.mk <<EOF
_all: $arch
FILES = $all
$arch: \$(FILES)
tar Jcvf \$@ \$(FILES)
@echo === \$@ ready ===
EOF
echo 'Now run "make -f run.mk" or preferably "make -f run.mk -j8".'
echo '(Adjusting -j8 to the number of processors on your machine.)'

1
configure.ac
View file

@ -123,6 +123,7 @@ AC_CONFIG_FILES([
bench/ltl2tgba/defs bench/ltl2tgba/defs
bench/scc-stats/Makefile bench/scc-stats/Makefile
bench/split-product/Makefile bench/split-product/Makefile
bench/spin13/Makefile
bench/wdba/Makefile bench/wdba/Makefile
doc/Doxyfile doc/Doxyfile
doc/Makefile doc/Makefile