Information Technology Reference
In-Depth Information
Algorithm 2 .
Conjunctive forward reachability algorithm.
δ
1
,...,δ
n
1:
input
:
Q
init
, {
},Σ
2:
let
Q
0
:=
Q
init
,k
:= 0;
3:
repeat
4:
k
:=
k
+1;
Q
k
:=
Q
k−
1
∪{q |∃q ∈ Q
k−
1
, ∃σ ∈ Σ,∀i ∈{
1
,...,n}
such that
δ
i
(
q
i
,σ
)=
q
i
5:
}
;
6:
until
Q
k
=
Q
k−
1
7:
return
Q
k
which prevents the conjunctive partitioning technique from being applied to large sys-
tems. The disjunctive partitioning, explained subsequently, on the other hand, is then
shown to be an appropriate partitioning technique for SCT.
Assuming
A
=
q
1
,...,q
n
{
A
1
,...,A
n
}
and
q
=
, the disjunctive transition func-
tion
δ
i
of
A
i
, is defined based on the event
σ
Σ
i
and the dependency set
D
(
A
i
)
:
∈
D
(
A
i
)=
{A
j
∈ A |∃A
i
∈ A
where
Σ
i
∩ Σ
j
=
∅} .
(4)
⎛
⎞
⎛
q
k
⎞
δ
i
(
q,σ
)=
q
k
σ
⎝
ζ
i,j
(
q
j
,σ
)
⎠
∧
⎝
⎠
.
↔
(5)
A
j
∈D
(
A
i
)
A
k
∈D
(
A
i
)
ζ
i,j
(
q
j
,σ
)=
δ
j
(
q
j
,σ
)if
σ
Σ
i
Σ
j
∈
∩
(6)
q
j
otherwise
.
Additionally, the total transition function is defined as:
δ
=
1
≤i≤n
δ
i
.
(7)
The construction of the dependency set for each automaton can be obtained through
calculating which automaton shares any event with it. Taking Example 1 as an example,
for the automaton
A
, since it shares the events
use
R
1
,
use
R
2
with the automaton
C
and
the event
use
R
2
with the automaton
D
,
D
(
A
)
can be constructed as follows:
D
(
A
)=
{
A, C, D
}
.
q
1
,q
1
,q
1
,q
1
Besides, the total transition function defined for the state
and the event
can be obtained by computing
δ
A
and
δ
C
,since
use
R
1
use
R
1
only belongs to
Σ
A
and
Σ
C
. By using (5) and (6), it can be inferred that
,use
R
1
)=
δ
A
(
q
1
,q
1
,q
1
,q
1
q
1
,q
1
,q
1
,q
1
,use
R
1
)
δ
(
=
δ
C
(
q
1
,q
1
,q
1
,q
1
,use
R
1
)=
q
2
,q
1
,q
2
,q
1
.
Notice that the disjunctive transition function represented in BDDs, is shown explicitly
here to easily understand.
