diff --git a/ChangeLog b/ChangeLog index 3be332d0a..c0c008249 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,7 @@ 2005-01-29 Alexandre Duret-Lutz + * bench/emptchk/formulae.ltl: New file. + * src/tgbaalgos/gtec/gtec.hh (couvreur99_check): Document poprem. * bench/emptchk/README: Make clearer that spin is needed. diff --git a/bench/emptchk/formulae.ltl b/bench/emptchk/formulae.ltl new file mode 100644 index 000000000..847863e34 --- /dev/null +++ b/bench/emptchk/formulae.ltl @@ -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)))))