Database Reference
In-Depth Information
Nevertheless, for much more complicated transitions which may have hundreds or
thousands of lines of codes, analysis could be hard, if not impossible, to perform.)
1.
If there is no direct cycle constructed from states and transitions in the statechart, the
statechart will terminate and we may stop and say “no”; otherwise let S be the set of
such cycles. For each cycle s in S, if s contains a transition whose event can only be
generated externally or whose condition can only be set to true externally, s will not
cause non-termination and we may remove s from S.
2.
If there is no cycle constructed from internally generated events or conditions in the
statechart, the statechart will terminate and we may stop and say “no”; otherwise let
E be the set of such cycles.
3.
If there exists an element s in S and an element e in E such that the events that take
the system from one state to the other in s is a subsequence of e, then the statechart
will never terminate and we say “yes”; otherwise the statechart will terminate and we
say “no”.
Theorem 1.
Algorithm 1 specifi es suffi cient conditions for a statechart to terminate.
Proof:
In Step 1, if there is no direct cycle constructed from the states and transitions
in a statechart, the statechart will terminate since the activity associated with a state will
terminate and each state in the statechart will only be visited once. In case there is such
a cycle s, and there is a transition of s whose event can only be generated externally or
whose condition can only be set to true externally, the completion of s depends on external
interventions. Thus, s will eventually be stopped by external means. In Step 2, if there is no
cycle constructed from internally generated events or conditions in a statechart, the events
and conditions are not “self-feeding”, which means the events will eventually run out and
the conditions will eventually become false. On the other hand, in Step 3, if we can fi nd
such a cycle s and a self-feeding cycle e of events and conditions, then s will never stop
once s is started.
As an example, in Figure 7, S is {[A, B, A], [C, D, C]} and E is {[E1, E2, E3, E4,
E1]}. Let s be [A, B, A] and e be [E1, E2, E3, E4, E1]. The events that take the system
from one state to the other in s is [E1, E3], which is a subsequence of e. Thus the statechart
will never terminate.
In the Statechart Analysis section, we will use Algorithm1 to demonstrate its ability
to detect a non-termination problem from the actual workfl ow scenario illustrated in Figure
10. In the next section, we discuss confl uence.
Confl uence
Consider a set of non-prioritized transitions that are fi red at the same time. If the
fi nal status of the system does not depend on their order of execution, then the system is
confl uent
.
Whether a system is deterministic or not has a great impact on the confl uence of the
system. For example, in Figure 5, if C1 and C2 are not mutually exclusive, then both of them
could be true at the same time and thus the system needs to non-deterministically choose
either state B or state C to enter. To avoid situations like this, for each conditional routing,
we require the user to prioritize the alternatives so that in case there is a tie, a tiebreaker is
provided.
