The article An OCL Extension for Real-Time Constraints describes and interesting extension to OCL for the specification of time constraints.
New types OclConfiguration and OclPath are defined along with a new post() operation which is able to generate a set of possible OclPath for a specified time interval.
At pag. 18, the article presents an interesting example:
We first request that new workpieces have to periodically arrive at the input buffer within time intervals of at most 100 time units. In other words, state Loading can always be reached within 100 time units. The corresponding OCL expression is:
context Buffer inv: Loader@post[1,100]->forAll(p:OclPath | p->includes(Loading))
From my understanding, the previous expression declares the invariant that all the possible OclPath(s) in the interval between 1 and 100 time units have to include the state Loading. Whereas I believe that the correct expression shall state that all the possible OclPath(s) generated after 100 time units have to contain the state Loading:
context Buffer inv: Loader@post[100]->forAll(p:OclPath | p->includes(Loading))
