DelayedCopy

Delayed Copy

Delayed Copy
INTENTION This pattern is applicable if one phenomenon, represented by the term t2 is a time displaced modification of another phenomenon, represented by the term t1, with a maximal time delay $\tau$ and w.r.t. a modifying function, represented by f.
SIGNATURE $\mathcal{V}^{\mathit{fo}} = \emptyset$, $\mathcal{V}^{\mathit{fu}} = \{f\}$, $\mathcal{V}^{\mathit{te}} = \{t_1, t_2\}$, $\mathcal{V}^{\mathit{ti}} = \{\tau\}$
FORMAL $\square(t_1 \vartriangleright^f_\tau t_2)$
NATURAL LANGUAGE For each time point, excluding the first $\tau$ time units, the value of t2 is the result of the application of the function represented by f to a value that t1 has had in the last $\tau$ time units.
Examples
EXAMPLE 1
  FORMAL $\square( \mathit{envEntity}
\vartriangleright^{\mathit{modifyReaction}}_{\le \mathit{reactionTime}}
\mathit{measuredEntity})$
  NATURAL
LANGUAGE
For each time point, excluding the first $\mathit{reactionTime}$ time units, the measured value is the result of the application of the function represented by $\mathit{modifyReaction}$ to a value that the phenomenon in the real world has had in the last $\mathit{reactionTime}$ time units.
Theorem Part
THEOREM SIGNATURE $\mathcal{V}^{\mathit{fo}} = \emptyset$, $\mathcal{V}^{\mathit{fu}} = \{f_1, f_2, g\}$, $\mathcal{V}^{\mathit{te}} = \{t_1, t_2, t_3\},
\mathcal{V}^{\mathit{ti}} = \{\tau_1, \tau_2\}$
THEOREM 1 Transitivity
  FORMAL $(\square( t_1 \vartriangleright^{f_1}_{\le \tau_1} t_2) \wedge
\square( t_2 \...
..._1(x))))
\rightarrow \square( t_1 \vartriangleright^g_{\le \tau_1+\tau_2} t_3)$
  EXPLANATION This theorem expresses the transitivity of this pattern.





 

 
Go to the contact details of the person in charge of this page

 
This page in german. Diese Seite auf deutsch.