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.




 Übergeordnete Seite: Pp

 Feedback
Zu den Kontaktdetails des Verantwortlichen dieser Seite

 English
This page in english. Diese Seite auf englisch.