ITL
© 1996-2015







25 Derived First Order ITL formulae

Here are derived ITL formulae that use temporal variables:

A := e =^  (CA ) = e                   assignment
A ←  e =^  finite ∧ (fin A) = e            temporalassignm ent
A gets e=^ A(skip ⊃ A ←  e)            gets
stableA =^  A geots A                    stability
len(n)  =^  ∃I  (I = 0) ∧ (I gets I + 1)
               ∧ (I ←  n)              intervallength