L'articolo Un'estensione OCL per il real-time I vincoli descrivono un'estensione interessante per OCL per la specifica dei limiti di tempo.
Nuovi tipi OclConfiguration e OclPath sono definiti insieme a una nuova operazione post() che è in grado di generare un set di OclPath per un intervallo di tempo specificato.
A pag. 18, l'articolo presenta un esempio interessante:
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))
Da quanto ho capito, l'espressione precedente dichiara l'invariante che tutti i possibili OclPath (s) nell'intervallo tra 1 e 100 unità di tempo devono includere lo stato Loading . Considerando che ritengo che l'espressione corretta indichi che tutti i possibili OclPath (s) generati dopo 100 unità di tempo devono contenere lo stato Loading :
context Buffer inv: Loader@post[100]->forAll(p:OclPath | p->includes(Loading))