Safe Decomposition of Startup Requirements
159
we define its semantics formally by defining the predicate Reach((C 1 , j 1 , t 1 ), . . . ,
(C n , j n , t n )), which is true iff the phases P
C1
j1 . . . P
Cn
jn are reachable at local times
t 1 . . . t n .
Definition 3 (Reachability for local requirements) Given the specification
{C 1 . . . C n } and the time points t 1 ∈ R . . . t n ∈ R, we inductively define the predicate Reach((C 1 , j 1 , t 1 ), . . . , (C n , j n , t n )) as follows:
– (base case) Reach((C 1 , 1, 0), . . . , (C n , 1, 0)) holds and for all i ∈ {1 . . . n} it
holds that (state dependencies): ((C 1 , 1), . . . , (C n , 1)) |= ψ
Ci
1
– (timed transition) if Reach((C 1 , j 1 , t 1 ), . . . , (C n , j n , t n )) and there exists a
δ ∈ R such that t i + δ ≤ u
Ci
ji+1 for all i ∈ {1 . . . n}, then
Reach((C 1 , j 1 , t 1 + δ), . . . , (C n , j n , t n + δ)).
– (discrete transition) if Reach((C 1 , j 1 , t 1 ), . . . , (C n , j n , t n )) and there exists a
δ ∈ R and a M ⊆ {1, . . . , n} such that:
1. for all i ∈ {1 . . . n} such that j i < |C i |, t i + δ ∈ [l
Ci
ji+1 , u
Ci
ji+1 ] if i ∈ M ,
and t i + δ ≤ u
Ci
ji+1 otherwise;
2. for all i ∈ M , it holds that (signal dependencies):
((C 1 , j 1 ), . . . , (C n , j n )) |= φ
Ci
ji+1
3. for all i ∈ M , it holds that (state dependencies - entry):
((C 1 , j 1 ), . . . , (C n , j n )) |= ψ
Ci
ji+1
4. for all i ∈ {1 . . . n}, it holds that (state dependencies - invariant):
((C 1 , j
1 ), . . . , (C n , j
n )) |= ψ
Ci
j
i
then it holds that Reach((C 1 , j
1 , t
1 ), . . . , (C n , j
n , t
n )), where j
i = j i + 1 and
t
i = 0 if i ∈ M and j i < |C i |, and j
i = j i and t
i = t i + δ otherwise.
We define the predicate Comp S to be true iff there are no reachable states
in S such that no component can proceed to its next phase.
Definition 4 (Compatibility for local requirements) Given the set of local requirements S = {C 1 . . . C n }, the predicate Comp S is true iff:
∀j 1 ∈ {1 . . . |C 1 | − 1} . . . ∀j n ∈ {1 . . . |C n | − 1} ∀t 1 . . . t n ∈ R
Reach((C 1 , j 1 , t 1 ), . . . , (C n , j n , t n )) ⇒
∃M ⊆ {1 . . . n}
M = ∅ ∧ Reach((C 1 , j
1 , t
1 ), . . . , (C n , j
n , t
n ))
where j
i = j i + 1 and t
i = 0 for all i ∈ M , or j
i = j i and t
i = t i otherwise.
If Comp S holds, we say that C 1 . . . C n are compatible, or equivalently that S is
compatible.
For example, in Fig. 1a, predicate Reach((A, 1, 4), (B, 1, 4)) holds, but predicate Reach((A, 1, 4), (B, 2, 0)) does not, because for all δ ∈ R and for all S ⊆
{1 . . . n}, predicate Reach((A, 1, 4), (B, 2, 0)) is false.
Strict Semantics The above definition adopts a weakly-monotonic model of time,
where discrete transitions are instantaneous and, therefore, the system may be
in two different states at the same instant. The definition and the reductions to
model checking and SMT can be easily adapted to have a strict semantics.
159
we define its semantics formally by defining the predicate Reach((C 1 , j 1 , t 1 ), . . . ,
(C n , j n , t n )), which is true iff the phases P
C1
j1 . . . P
Cn
jn are reachable at local times
t 1 . . . t n .
Definition 3 (Reachability for local requirements) Given the specification
{C 1 . . . C n } and the time points t 1 ∈ R . . . t n ∈ R, we inductively define the predicate Reach((C 1 , j 1 , t 1 ), . . . , (C n , j n , t n )) as follows:
– (base case) Reach((C 1 , 1, 0), . . . , (C n , 1, 0)) holds and for all i ∈ {1 . . . n} it
holds that (state dependencies): ((C 1 , 1), . . . , (C n , 1)) |= ψ
Ci
1
– (timed transition) if Reach((C 1 , j 1 , t 1 ), . . . , (C n , j n , t n )) and there exists a
δ ∈ R such that t i + δ ≤ u
Ci
ji+1 for all i ∈ {1 . . . n}, then
Reach((C 1 , j 1 , t 1 + δ), . . . , (C n , j n , t n + δ)).
– (discrete transition) if Reach((C 1 , j 1 , t 1 ), . . . , (C n , j n , t n )) and there exists a
δ ∈ R and a M ⊆ {1, . . . , n} such that:
1. for all i ∈ {1 . . . n} such that j i < |C i |, t i + δ ∈ [l
Ci
ji+1 , u
Ci
ji+1 ] if i ∈ M ,
and t i + δ ≤ u
Ci
ji+1 otherwise;
2. for all i ∈ M , it holds that (signal dependencies):
((C 1 , j 1 ), . . . , (C n , j n )) |= φ
Ci
ji+1
3. for all i ∈ M , it holds that (state dependencies - entry):
((C 1 , j 1 ), . . . , (C n , j n )) |= ψ
Ci
ji+1
4. for all i ∈ {1 . . . n}, it holds that (state dependencies - invariant):
((C 1 , j
1 ), . . . , (C n , j
n )) |= ψ
Ci
j
i
then it holds that Reach((C 1 , j
1 , t
1 ), . . . , (C n , j
n , t
n )), where j
i = j i + 1 and
t
i = 0 if i ∈ M and j i < |C i |, and j
i = j i and t
i = t i + δ otherwise.
We define the predicate Comp S to be true iff there are no reachable states
in S such that no component can proceed to its next phase.
Definition 4 (Compatibility for local requirements) Given the set of local requirements S = {C 1 . . . C n }, the predicate Comp S is true iff:
∀j 1 ∈ {1 . . . |C 1 | − 1} . . . ∀j n ∈ {1 . . . |C n | − 1} ∀t 1 . . . t n ∈ R
Reach((C 1 , j 1 , t 1 ), . . . , (C n , j n , t n )) ⇒
∃M ⊆ {1 . . . n}
M = ∅ ∧ Reach((C 1 , j
1 , t
1 ), . . . , (C n , j
n , t
n ))
where j
i = j i + 1 and t
i = 0 for all i ∈ M , or j
i = j i and t
i = t i otherwise.
If Comp S holds, we say that C 1 . . . C n are compatible, or equivalently that S is
compatible.
For example, in Fig. 1a, predicate Reach((A, 1, 4), (B, 1, 4)) holds, but predicate Reach((A, 1, 4), (B, 2, 0)) does not, because for all δ ∈ R and for all S ⊆
{1 . . . n}, predicate Reach((A, 1, 4), (B, 2, 0)) is false.
Strict Semantics The above definition adopts a weakly-monotonic model of time,
where discrete transitions are instantaneous and, therefore, the system may be
in two different states at the same instant. The definition and the reductions to
model checking and SMT can be easily adapted to have a strict semantics.