ITL
© 1996-2016







3 Derived Constructs

Frequently used derived constructs are listed in table 36.


Table 3: Frequently used non-temporal derived constructs
|--------------------------------------------------------|
|false     ^=   true              false value               |
|f  ∨ f   ^=   (f  ∧ f )       or                      |
|f1 ⊃ f2  ^=   f  1∨ f   2        implies                  |
|f1 ≡ f2  ^=   (f1⊃ f2) ∧ (f ⊃ f ) equivalent              |
|∃1v  o f2 ^=   ∀1v  o2f     2   1  exists                   |
----------------------------------------------------------



Table 4: Frequently used temporal derived constructs
|-------------------------------------------------|
|   f     ^=   skip ;f       next                   |
| Cmore    ^=     true        non-empty interval       |
| empty   ^=   Cmore        empty interval          |
| inf      ^=   true ;false     infinite interval         |
| isinf(f)  ^=   inf ∧ f       is in finite              |
| finite    ^=   inf         finite interval           |
| isfin(f)  ^=   finite ∧ f     is finite                |
| fmore    ^=   more ∧ finite  non-empty finite interval |
|   f     ^=   finite;f       sometimes               |
| ! f     ^=     f        always                  |
|   f     ^=     f        weak next              |
| ci f     ^=   f C;true       some initial subinterval  |
| I f     ^=   (i f)      all initial subintervals    |
| a f     ^=   finite;f ;true  some subinterval         |
| A f     ^=   (a f)      all subintervals          |
----------------------------------------------------



Table 5: Frequently used concrete derived constructs
|-----------------------------------------------------------------------|
| iff then f else f  =^  (f ∧ f ) ∨ (f ∧ f ) if then else                  |
| iff0then f1    2  =^  if0f th1en f else0emp2ty  if then                      |
| fin0f     1        =^  ! (e0mpty ⊃1f)         final state                   |
| sfin f             =^   (fin(f))            strong final state             |
| haltf             =^  ! (empty ≡ f)         terminate interval when       |
| shaltf            =^   (halt(f))           strong terminate interval when |
| keep f            =^  A (skip ⊃ f)          all unit subintervals         |
| keepnow f         =^  i (skip ∧ f)          initial unit subinterval       |
| fω               =^  isinf(isfin(f)*)         infinite chopstar             |
| fstar(f)          =^  isfin(isfin(f)*) ∨                                   |
|                      isfin(isfin(f)*);isinf(f)  finite chopstar                |
| whilef do f       =^  (f ∧ f )* ∧ finf     while loop                    |
| repeat0f unt1ilf     =^  f 0;(wh1ile f do 0f)    repeat loop                   |
--------0-----1---------0---------1----0----------------------------------



Table 6: Frequently used derived constructs related to expressions
|----------------------------------------------------------------------------------|
| A := exp     ^=    A = exp                            assignment                    |
| A ≈ exp      ^=   C!(A = exp)                          equal in interval              |
| A ← exp     ^=   finite ∧ (finA ) = exp                 temporal assignment            |
| A gets exp   ^=   keep(A ← exp)                        gets                          |
| stable A      ^=   A gets A                             stability                      |
| padded A     ^=   (stable(A);skip) ∨ empty               padded expression              |
| A <~ exp    ^=   (A ← exp) ∧ paddedA                 padded temporal assignment     |
| goodindexA   ^=   keep(A ← A ∨ A ←  A+ 1)              increasing index                |
| intlen(exp)   ^=   ∃I o (I = 0) ∧ (I gets I + 1) ∧ (I ← exp) interval length            |
------------------------------------------------------------------------------------