* bench/emptchk/formulae.ltl: New file.
This commit is contained in:
Alexandre Duret-Lutz
parent
de472c74b4
commit
cddca67fda
2 changed files with 190 additions and 0 deletions
|
|
@ -1,5 +1,7 @@
|
||||||
2005-01-29 Alexandre Duret-Lutz <adl@gnu.org>
|
2005-01-29 Alexandre Duret-Lutz <adl@gnu.org>
|
||||||
|
|
||||||
|
* bench/emptchk/formulae.ltl: New file.
|
||||||
|
|
||||||
* src/tgbaalgos/gtec/gtec.hh (couvreur99_check): Document poprem.
|
* src/tgbaalgos/gtec/gtec.hh (couvreur99_check): Document poprem.
|
||||||
|
|
||||||
* bench/emptchk/README: Make clearer that spin is needed.
|
* bench/emptchk/README: Make clearer that spin is needed.
|
||||||
|
|
|
||||||
188
bench/emptchk/formulae.ltl
Normal file
188
bench/emptchk/formulae.ltl
Normal file
|
|
@ -0,0 +1,188 @@
|
||||||
|
p0 U (p1 & G p2)
|
||||||
|
p0 U (p1 & X (p2 U p3))
|
||||||
|
p0 U (p1 & (X (p2 & (F (p3 & (X (F (p4 & X (F (p5 & (X (F p6))))))))))))
|
||||||
|
F (p0 & XGp1)
|
||||||
|
F (p0 & X (p1 & XFp2))
|
||||||
|
F (p0 & X (p1 U p2))
|
||||||
|
FGp0 | FGp1
|
||||||
|
G (!p0 | (p1 U p2))
|
||||||
|
F (p0 & (XF (p1 & XF (p2 & XF p3))))
|
||||||
|
GFp0 & GFp1 & GFp2 & GFp3 & GFp4
|
||||||
|
(p0 U (p1 U p2)) | (p1 U (p2 U p0)) | (p2 U (p0 U p1))
|
||||||
|
G (! p0 | (p1 U (G p2 | G p3)))
|
||||||
|
p=1Uq=1
|
||||||
|
p=1U(q=1Ur=1)
|
||||||
|
!(p=1U(q=1Ur=1))
|
||||||
|
G(F(p=1))->G(F(q=1))
|
||||||
|
F(p=1)UG(q=1)
|
||||||
|
G(p=1)Uq=1
|
||||||
|
!(F(F(p=1))<->F(p=1))
|
||||||
|
!(G(F(p=1))->G(F(q=1)))
|
||||||
|
G(F(p=1))^G(F(q=1))
|
||||||
|
p=1R(p=1+q=1)
|
||||||
|
(X(p=1)UX(q=1))+!X(p=1Uq=1)
|
||||||
|
(X(p=1)Uq=1)+!X(p=1U(p=1*q=1))
|
||||||
|
G(p=1->F(q=1))*((X(p=1)Uq=1)+!X(p=1U(p=1*q=1)))
|
||||||
|
G(p=1->F(q=1))*((X(p=1)UX(q=1))+!X(p=1Uq=1))
|
||||||
|
G(p=1->F(q=1))
|
||||||
|
!G(p=1->X(q=1Rr=1))
|
||||||
|
!(G(F(p=1))+F(G(q=1)))
|
||||||
|
G(F(p=1)*F(q=1))
|
||||||
|
F(p=1)*F(p=0)
|
||||||
|
((X(q=0))*(r=0))R(X((((s=0)U(p=0))R(r=0))U((s=0)R(r=0))))
|
||||||
|
(G(q=1+G(F(p=1)))*G(r=1+G(F(p=0))))+G(q=1)+G(r=1)
|
||||||
|
(G(q=1+F(G(p=1)))*G(r=1+F(G(p=0))))+G(q=1)+G(r=1)
|
||||||
|
!((G(q=1+G(F(p=1)))*G(r=1+G(F(p=0))))+G(q=1)+G(r=1))
|
||||||
|
!((G(q=1+F(G(p=1)))*G(r=1+F(G(p=0))))+G(q=1)+G(r=1))
|
||||||
|
G(q=1+X(G(p=1)))*G(r=1+X(G(p=0)))
|
||||||
|
G(p=1+(X(q=1)*X(q=0)))
|
||||||
|
(p=1Uq=1)+(q=1Up=1)
|
||||||
|
[](!a)
|
||||||
|
<>b -> (!a U b)
|
||||||
|
[](c -> [](!a))
|
||||||
|
[]((c & !b & <>b) -> (!a U b))
|
||||||
|
[](c & !b -> (!a U (b | []!a)))
|
||||||
|
<>(a)
|
||||||
|
!b U ((a & !b) | []!b)
|
||||||
|
[](!c) | <>(c & <>a)
|
||||||
|
[](c & !b -> (!b U ((a & !b) | []!b)))
|
||||||
|
[](c & !b -> (!b U (a & !b)))
|
||||||
|
<>b -> ((!a & !b) U (b | ((a & !b) U (b | ((!a & !b) U (b | ((a & !b) U (b | (!a U b)))))))))
|
||||||
|
[]((c & <>b) -> ((!a & !b) U (b | ((a & !b) U (b | ((!a & !b) U (b | ((a & !b) U (b | (!a U b))))))))))
|
||||||
|
[](c -> ((!a & !b) U (b | ((a & !b) U (b | ((!a & !b) U (b | ((a & !b) U (b | (!a U (b | []!a)) | []a)))))))))
|
||||||
|
[](a)
|
||||||
|
<>b -> (a U b)
|
||||||
|
[](c -> [](a))
|
||||||
|
[]((c & !b & <>b) -> (a U b))
|
||||||
|
[](c & !b -> (a U (b | [] a)))
|
||||||
|
!a U (d | []!a)
|
||||||
|
<>b -> (!a U (d | b))
|
||||||
|
[]!c | <>(c & (!a U (d | []!a)))
|
||||||
|
[]((c & !b & <>b) -> (!a U (d | b)))
|
||||||
|
[](c & !b -> (!a U ((d | b) | []!a)))
|
||||||
|
[](a -> <>d)
|
||||||
|
<>b -> (a -> (!b U (d & !b))) U b
|
||||||
|
[](c -> [](a -> <>d))
|
||||||
|
[]((c & !b & <>b) -> (a -> (!b U (d & !b))) U b)
|
||||||
|
[](c & !b -> ((a -> (!b U (d & !b))) U (b | [](a -> (!b U (d & !b))))))
|
||||||
|
<>a -> (!a U (d & !a & X(!a U e)))
|
||||||
|
<>b -> (!a U (b | (d & !a & X(!a U e))))
|
||||||
|
([]!c) | (!c U (c & <>a -> (!a U (d & !a & X(!a U e)))))
|
||||||
|
[]((c & <>b) -> (!a U (b | (d & !a & X(!a U e)))))
|
||||||
|
[](c -> (<>a -> (!a U (b | (d & !a & X(!a U e))))))
|
||||||
|
(<>(d & X<>e)) -> ((!d) U a)
|
||||||
|
<>b -> ((!(d & (!b) & X(!b U (e & !b)))) U (b | a))
|
||||||
|
([]!c) | ((!c) U (c & ((<>(d & X<>e)) -> ((!d) U a))))
|
||||||
|
[]((c & <>b) -> ((!(d & (!b) & X(!b U (e & !b)))) U (b | a)))
|
||||||
|
[](c -> (!(d & (!b) & X(!b U (e & !b))) U (b | a) | [](!(d & X<>e))))
|
||||||
|
[] (d & X<> e -> X(<>(e & <> a)))
|
||||||
|
<>b -> (d & X(!b U e) -> X(!b U (e & <> a))) U b
|
||||||
|
[] (c -> [] (d & X<> e -> X(!e U (e & <> a))))
|
||||||
|
[] ((c & <>b) -> (d & X(!b U e) -> X(!b U (e & <> a))) U b)
|
||||||
|
[] (c -> (d & X(!b U e) -> X(!b U (e & <> a))) U (b | [] (d & X(!b U e) -> X(!b U (e & <> a)))))
|
||||||
|
[] (a -> <>(d & X<>e))
|
||||||
|
<>b -> (a -> (!b U (d & !b & X(!b U e)))) U b
|
||||||
|
[] (c -> [] (a -> (d & X<> e)))
|
||||||
|
[] ((c & <>b) -> (a -> (!b U (d & !b & X(!b U e)))) U b)
|
||||||
|
[] (c -> (a -> (!b U (d & !b & X(!b U e)))) U (b | [] (a -> (d & X<> e))))
|
||||||
|
[] (a -> <>(d & !f & X(!f U e)))
|
||||||
|
<>b -> (a -> (!b U (d & !b & !f & X((!b & !f) U e)))) U b
|
||||||
|
[] (c -> [] (a -> (d & !f & X(!f U e))))
|
||||||
|
[] ((c & <>b) -> (a -> (!b U (d & !b & !f & X((!b & !f) U e)))) U b)
|
||||||
|
[] (c -> (a -> (!b U (d & !b & !f & X((!b & !f) U e)))) U (b | [] (a -> (d & !f & X(!f U e)))))
|
||||||
|
!a U ((a U ((!a U ((a U ([]!a | []a)) | []!a)) | []!a)) | []!a)
|
||||||
|
<>c -> (!c U (c & (!a U ((a U ((!a U ((a U ([]!a | []a)) | []!a)) | []!a)) | []!a))))
|
||||||
|
!(p0 U (p1 & G p2))
|
||||||
|
!(p0 U (p1 & X (p2 U p3)))
|
||||||
|
!(p0 U (p1 & (X (p2 & (F (p3 & (X (F (p4 & X (F (p5 & (X (F p6)))))))))))))
|
||||||
|
!(F (p0 & XGp1))
|
||||||
|
!(F (p0 & X (p1 & XFp2)))
|
||||||
|
!(F (p0 & X (p1 U p2)))
|
||||||
|
!(FGp0 | FGp1)
|
||||||
|
!(G (!p0 | (p1 U p2)))
|
||||||
|
!(F (p0 & (XF (p1 & XF (p2 & XF p3)))))
|
||||||
|
!(GFp0 & GFp1 & GFp2 & GFp3 & GFp4)
|
||||||
|
!((p0 U (p1 U p2)) | (p1 U (p2 U p0)) | (p2 U (p0 U p1)))
|
||||||
|
!(G (! p0 | (p1 U (G p2 | G p3))))
|
||||||
|
!(p=1Uq=1)
|
||||||
|
!(p=1U(q=1Ur=1))
|
||||||
|
!(!(p=1U(q=1Ur=1)))
|
||||||
|
!(G(F(p=1))->G(F(q=1)))
|
||||||
|
!(F(p=1)UG(q=1))
|
||||||
|
!(G(p=1)Uq=1)
|
||||||
|
!(!(F(F(p=1))<->F(p=1)))
|
||||||
|
!(!(G(F(p=1))->G(F(q=1))))
|
||||||
|
!(G(F(p=1))^G(F(q=1)))
|
||||||
|
!(p=1R(p=1+q=1))
|
||||||
|
!((X(p=1)UX(q=1))+!X(p=1Uq=1))
|
||||||
|
!((X(p=1)Uq=1)+!X(p=1U(p=1*q=1)))
|
||||||
|
!(G(p=1->F(q=1))*((X(p=1)Uq=1)+!X(p=1U(p=1*q=1))))
|
||||||
|
!(G(p=1->F(q=1))*((X(p=1)UX(q=1))+!X(p=1Uq=1)))
|
||||||
|
!(G(p=1->F(q=1)))
|
||||||
|
!(!G(p=1->X(q=1Rr=1)))
|
||||||
|
!(!(G(F(p=1))+F(G(q=1))))
|
||||||
|
!(G(F(p=1)*F(q=1)))
|
||||||
|
!(F(p=1)*F(p=0))
|
||||||
|
!(((X(q=0))*(r=0))R(X((((s=0)U(p=0))R(r=0))U((s=0)R(r=0)))))
|
||||||
|
!((G(q=1+G(F(p=1)))*G(r=1+G(F(p=0))))+G(q=1)+G(r=1))
|
||||||
|
!((G(q=1+F(G(p=1)))*G(r=1+F(G(p=0))))+G(q=1)+G(r=1))
|
||||||
|
!(!((G(q=1+G(F(p=1)))*G(r=1+G(F(p=0))))+G(q=1)+G(r=1)))
|
||||||
|
!(!((G(q=1+F(G(p=1)))*G(r=1+F(G(p=0))))+G(q=1)+G(r=1)))
|
||||||
|
!(G(q=1+X(G(p=1)))*G(r=1+X(G(p=0))))
|
||||||
|
!(G(p=1+(X(q=1)*X(q=0))))
|
||||||
|
!((p=1Uq=1)+(q=1Up=1))
|
||||||
|
!([](!a))
|
||||||
|
!(<>b -> (!a U b))
|
||||||
|
!([](c -> [](!a)))
|
||||||
|
!([]((c & !b & <>b) -> (!a U b)))
|
||||||
|
!([](c & !b -> (!a U (b | []!a))))
|
||||||
|
!(<>(a))
|
||||||
|
!(!b U ((a & !b) | []!b))
|
||||||
|
!([](!c) | <>(c & <>a))
|
||||||
|
!([](c & !b -> (!b U ((a & !b) | []!b))))
|
||||||
|
!([](c & !b -> (!b U (a & !b))))
|
||||||
|
!(<>b -> ((!a & !b) U (b | ((a & !b) U (b | ((!a & !b) U (b | ((a & !b) U (b | (!a U b))))))))))
|
||||||
|
!([]((c & <>b) -> ((!a & !b) U (b | ((a & !b) U (b | ((!a & !b) U (b | ((a & !b) U (b | (!a U b)))))))))))
|
||||||
|
!([](c -> ((!a & !b) U (b | ((a & !b) U (b | ((!a & !b) U (b | ((a & !b) U (b | (!a U (b | []!a)) | []a))))))))))
|
||||||
|
!([](a))
|
||||||
|
!(<>b -> (a U b))
|
||||||
|
!([](c -> [](a)))
|
||||||
|
!([]((c & !b & <>b) -> (a U b)))
|
||||||
|
!([](c & !b -> (a U (b | [] a))))
|
||||||
|
!(!a U (d | []!a))
|
||||||
|
!(<>b -> (!a U (d | b)))
|
||||||
|
!([]!c | <>(c & (!a U (d | []!a))))
|
||||||
|
!([]((c & !b & <>b) -> (!a U (d | b))))
|
||||||
|
!([](c & !b -> (!a U ((d | b) | []!a))))
|
||||||
|
!([](a -> <>d))
|
||||||
|
!(<>b -> (a -> (!b U (d & !b))) U b)
|
||||||
|
!([](c -> [](a -> <>d)))
|
||||||
|
!([]((c & !b & <>b) -> (a -> (!b U (d & !b))) U b))
|
||||||
|
!([](c & !b -> ((a -> (!b U (d & !b))) U (b | [](a -> (!b U (d & !b)))))))
|
||||||
|
!(<>a -> (!a U (d & !a & X(!a U e))))
|
||||||
|
!(<>b -> (!a U (b | (d & !a & X(!a U e)))))
|
||||||
|
!(([]!c) | (!c U (c & <>a -> (!a U (d & !a & X(!a U e))))))
|
||||||
|
!([]((c & <>b) -> (!a U (b | (d & !a & X(!a U e))))))
|
||||||
|
!([](c -> (<>a -> (!a U (b | (d & !a & X(!a U e)))))))
|
||||||
|
!((<>(d & X<>e)) -> ((!d) U a))
|
||||||
|
!(<>b -> ((!(d & (!b) & X(!b U (e & !b)))) U (b | a)))
|
||||||
|
!(([]!c) | ((!c) U (c & ((<>(d & X<>e)) -> ((!d) U a)))))
|
||||||
|
!([]((c & <>b) -> ((!(d & (!b) & X(!b U (e & !b)))) U (b | a))))
|
||||||
|
!([](c -> (!(d & (!b) & X(!b U (e & !b))) U (b | a) | [](!(d & X<>e)))))
|
||||||
|
!([] (d & X<> e -> X(<>(e & <> a))))
|
||||||
|
!(<>b -> (d & X(!b U e) -> X(!b U (e & <> a))) U b)
|
||||||
|
!([] (c -> [] (d & X<> e -> X(!e U (e & <> a)))))
|
||||||
|
!([] ((c & <>b) -> (d & X(!b U e) -> X(!b U (e & <> a))) U b))
|
||||||
|
!([] (c -> (d & X(!b U e) -> X(!b U (e & <> a))) U (b | [] (d & X(!b U e) -> X(!b U (e & <> a))))))
|
||||||
|
!([] (a -> <>(d & X<>e)))
|
||||||
|
!(<>b -> (a -> (!b U (d & !b & X(!b U e)))) U b)
|
||||||
|
!([] (c -> [] (a -> (d & X<> e))))
|
||||||
|
!([] ((c & <>b) -> (a -> (!b U (d & !b & X(!b U e)))) U b))
|
||||||
|
!([] (c -> (a -> (!b U (d & !b & X(!b U e)))) U (b | [] (a -> (d & X<> e)))))
|
||||||
|
!([] (a -> <>(d & !f & X(!f U e))))
|
||||||
|
!(<>b -> (a -> (!b U (d & !b & !f & X((!b & !f) U e)))) U b)
|
||||||
|
!([] (c -> [] (a -> (d & !f & X(!f U e)))))
|
||||||
|
!([] ((c & <>b) -> (a -> (!b U (d & !b & !f & X((!b & !f) U e)))) U b))
|
||||||
|
!([] (c -> (a -> (!b U (d & !b & !f & X((!b & !f) U e)))) U (b | [] (a -> (d & !f & X(!f U e))))))
|
||||||
|
!(!a U ((a U ((!a U ((a U ([]!a | []a)) | []!a)) | []!a)) | []!a))
|
||||||
|
!(<>c -> (!c U (c & (!a U ((a U ((!a U ((a U ([]!a | []a)) | []!a)) | []!a)) | []!a)))))
|
||||||
Loading…
Add table
Add a link
Reference in a new issue