The article An OCL Extension for Real-Time Constraints describes and interesting extension to OCL for the specification of time constraints.
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
context Buffer inv: Loader@post->forAll(p:OclPath | p->includes(Loading))