Limited Invariance |
INTENTION |
This pattern is applicable if the fluttering of a phenomenon is
suppressed, i.e., if a phenomenon, represented by ,
reaches a
specific state, it remains in this state for at least
time
units. |
SIGNATURE |
,
,
,
![$\mathcal{V}^{\mathit{ti}} = \{\tau\}$](img6.gif) |
FORMAL |
![$\square(\bigtriangledown\limits_{\leq \tau} \varphi)$](img7.gif) |
NATURAL LANGUAGE |
Whenever
becomes true, it remains true for at least
time
units. |
Examples |
EXAMPLE 1 |
|
FORMAL |
![$\square(\bigtriangledown\limits_{\leq \mathit{T\_MinInf}}
(\mathit{indicatorLight} = 1))$](img8.gif) |
|
NATURAL
LANGUAGE |
Whenever an indicator light is switched on, it remains for at least
T_MinInf time units. |
Theorem Part |
THEOREM SIGNATURE |
,
,
,
![$\mathcal{V}^{\mathit{ti}} = \{\tau\}$](img6.gif) |
THEOREM 1 Expansion of
over ![$\wedge$](img11.gif) |
|
FORMAL |
![$\square( \bigtriangledown\limits_{\le \tau} (\varphi \wedge \psi)) \rightarrow
...
...edown\limits_{\le \tau} \varphi \vee
\bigtriangledown\limits_{\le \tau} \psi )$](img12.gif) |
|
EXPLANATION |
This theorem expresses how a conjunctive combination of two phenomena can
be expanded. |
THEOREM 2 Contraction of
over ![$\wedge$](img11.gif) |
|
FORMAL |
![$\square( \bigtriangledown\limits_{\le \tau} \varphi) \wedge
\square( \bigtrian...
...) \rightarrow
\square( \bigtriangledown\limits_{\le \tau} (\varphi \vee \psi))$](img13.gif) |
|
EXPLANATION |
This theorem expresses how a conjunctive combination of two instantiations
of this pattern can be contracted. |