885a535184
* bench/ltl2tgba/sum.py: New file. * bench/ltl2tgba/.gitignore, bench/ltl2tgba/Makefile.am, bench/ltl2tgba/README, bench/ltl2tgba/algorithms, bench/ltl2tgba/big, bench/ltl2tgba/defs.in, bench/ltl2tgba/known, bench/ltl2tgba/small: Rewrite this benchmark completely. Also drop support of Wring and Modella, as we cannot get them to work reliably. * bench/ltl2tgba/formulae.ltl: Rewrite in Spot's syntax. * bench/ltl2tgba/lbtt2csv.pl, bench/ltl2tgba/ltl2baw.in, bench/ltl2tgba/parseout.pl: Delete these scripts, no longer needed. * configure.ac: Do not output ltl2baw.pl anymore.
92 lines
4.1 KiB
Text
92 lines
4.1 KiB
Text
[](!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))))
|