Automatic Testing of LUSTRE/SCADE Programs 181
that
current always operates on an already sampled expression, so the clock that determines
its output activation should be the one on which the input is sampled.
Let us assume the path p = m, x,M
1
,M
2
,M
3
,M
4
,c in the example of Section 7.1.2,
displayed in bold in Figure 7.5. Following the same procedure for the activation condi-
tion computation and starting from the last path edge, the activation conditions for the
intermediate unit paths are
AC (p)= false -> AC (p
1
), where p
1
= m,x,M
1
,M
2
,M
3
,M
4
AC (p
1
)=true and AC (p
2
), where p
2
= m,x,M
1
,M
2
,M
3
AC (p
2
)=false -> pre (AC (p
3
)), where p
3
= m,x,M
1
,M
2
AC (p
3
)=c and AC (p
4
), where p
4
= m,x,M
1
AC (p
4
)=c and AC (p
5
), where p
5
= m,x
AC (p
5
)=c
After backward substitutions, ...