From fdf8878db3ba7babd56c3cfd2da4d77158a188dd Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 24 Nov 2011 21:50:36 +0100 Subject: [PATCH] Update formulae.ltl not to use uncommon operators. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * bench/emptchk/formulae.ltl: Do not use + and * in the list of formulas. Use | and & instead. The * operator was removed on 2010-01-30. Reported by Étienne Renault. --- ChangeLog | 8 +++++ THANKS | 1 + bench/emptchk/formulae.ltl | 64 +++++++++++++++++++------------------- 3 files changed, 41 insertions(+), 32 deletions(-) diff --git a/ChangeLog b/ChangeLog index 144c01df7..443ce7372 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,11 @@ +2011-11-24 Alexandre Duret-Lutz + + Update formulae.ltl not to use uncommon operators. + + * bench/emptchk/formulae.ltl: Do not use + and * in the list of + formulas. Use | and & instead. The * operator was removed on + 2010-01-30. Reported by Étienne Renault. + 2011-11-23 Alexandre Duret-Lutz More documentation. diff --git a/THANKS b/THANKS index e64120bd7..856eac58b 100644 --- a/THANKS +++ b/THANKS @@ -1,6 +1,7 @@ We are grateful to these people for their comments, help, or suggestions. +Étienne Renault Gerard J. Holzmann Heikki Tauriainen Jean-Michel Couvreur diff --git a/bench/emptchk/formulae.ltl b/bench/emptchk/formulae.ltl index 847863e34..478abf8aa 100644 --- a/bench/emptchk/formulae.ltl +++ b/bench/emptchk/formulae.ltl @@ -19,24 +19,24 @@ 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)) +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) +!(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)) @@ -113,24 +113,24 @@ G(p=1+(X(q=1)*X(q=0))) !(!(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))) +!(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)) +!(!(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)))