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

Update formulae.ltl not to use uncommon operators.

Browse source 
* 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.
This commit is contained in:
Alexandre Duret-Lutz 2011-11-24 21:50:36 +01:00
parent fd98345c17
commit fdf8878db3
3 changed files with 41 additions and 32 deletions
Download patch file Download diff file Expand all files Collapse all files

8
ChangeLog
View file

@ -1,3 +1,11 @@
2011-11-24 Alexandre Duret-Lutz <adl@lrde.epita.fr>
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 <adl@lrde.epita.fr>
More documentation.

1
THANKS
View file

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

64
bench/emptchk/formulae.ltl
View file

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