Derived Constructs

Frequently used derived constructs are listed in table 3–6.

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 o¬2f 2 1 exists | | | ----------------------------------------------------------

Table 4: Frequently used temporal derived constructs

|-------------------------------------------------| | f ^= skip ;f next | | Cmore ^= true non-empty interval | | empty ^= C¬more 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 )* ∧ fin¬f 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 | | | ------------------------------------------------------------------------------------

December 8, 2009