
Reactive Testing of Nondeterministic Systems 435
Algorithm 1 Build control structure of the tester
1: E
c
T
←∅; E
o
T
←∅; S
a
T
←S
S
; S
p
T
←∅; I
T
←O
S
; O
T
←I
S
; V
T
←V
S
2: for all s ∈ S
S
do
3: find E
out
S
(s)
4:
while E
out
S
(s) = ∅ do
5:
get e =(s, p, a,o,u,q) from E
out
S
(s)
6: add s
p
to S
p
T
{passive state}
7: add (s, p, ∅,a,∅,s
p
)toE
c
T
{controllable transition}
8: add (s
p
,true, o,∅,u,q)toE
o
T
{observable trans.}
9: E
out
S
(s) ←E
out
S
(s) −{e}
10:
find E
out
S
(s,a,p) from E
out
S
(s)
11: E
out
S
(s) ←E
out
S
(s) −E
out
S
(s,a,p)
12: while E
out
S
(s,a,p) = ∅ do
13: get e =(s, p,a,o, u, q) from E
out
S
(s,a,p)
14: add (s
p
,true, o,∅,u,q)toE
o
T
{observable trans.}
15: E
out
S
(s,a,p) ←E
out
S
(s,a,p) −{e}
16: end while
17: