David Harel's statecharts [4] do not formalize variables. The state hierarchy of models only allows finite and enumerable number of states. Obviously, it is impossible to map DCharts to original statecharts, since the variable sets of DCharts models may contain variables that have infinite and continuous state space.
Now suppose the use of variables is allowed in statecharts. This variant of statecharts is called statecharts with variables. It becomes interesting to show that non-recursive DCharts can be mapped to this statecharts variant. Statecharts with variables are simpler than DCharts. If this mapping can be proved, it is implied that the only DCharts extensions that enhance the expressiveness of statecharts are recursion and variables.
To show that non-recursive DCharts can be mapped to statecharts with variables, the following semantic extensions must be explicitly transformed into statecharts structures:
Since the variable set is supported by statecharts with variables, it is not discussed in this mapping. Other semantic elements of DCharts, such as state hierarchy, history, transitions, can be directly mapped to the corresponding entities of statecharts. They are not discussed, either.
Proof The algorithm discussed in section 2.3.3 shows a way in which importation in non-recursive DCharts can always be flattened. The result of this flattening does not contain any importation state.
Proof This lemma can be proved by an algorithm which manages to find out this ordering.
In this algorithm, the transitions in a model are sequentially appended to an initially empty list . When is equal to the number of transitions in the model, the algorithm terminates, and the ordering of the transitions in satisfies the requirements in this lemma.
Before the algorithm starts, the model must be flattened with the algorithm discussed in section 2.3.3.
The algorithm is summarized below:
function merge(, )
/* merge two sets of transitions with insertion sort
: the transitions to be merged with . The of these transitions has no parent-children relation with the of transitions in . Conflicts between transitions in the two lists can only be solved with their number.
: another set of transitions
return: the union of and . The transitions are sorted by priority.
*/
for in
added = false
for in
if
then
insert into right before
added = true
break
if !added then
append to the end of
return
function order(, )
/* sort the transitions
: a set of states belonging to the same parent
: whether the parent of the states in is set to be inner-transition-first or not
return: the list of transitions whose is in or where . The transitions are sorted by priority.
*/
= []
for in
= [transitions with = ]
sort in the increasing order of the numbers of the transitions
if is then
next_ITF =
elif is then
next_ITF =
elif is then
next_ITF = not ITF
else
next_ITF = ITF
if then
= + order(, next_ITF)
else
= order(, next_ITF) +
merge(, )
return
Note that it is assumed there are not two or more transitions with exactly the same total priority. If such transitions exist, conflicts among them cannot be solved with the ITF and OTF scheme and their number is the same. The ordering of such transitions with the above algorithm is implementation-dependent and not unique.
Suppose all the top-level states are in set , and parameter contains the global option of the model that decides whether its top-level states are inner-transition-first by default. The invocation always terminates since there are finite number of states in the model. The result is the transitions sorted by their total priority. If a state is set to be , transitions from this state are always placed after transitions from the substates of this state in the transition list. The opposite is true for states with the property.
The merge function merges two lists of transitions. It assumes that both lists are sorted according to the ITF and OTF convention, and tries to further sort the merged list in the order of numbers. Because the source states of transitions in the two lists do not have the parent-children relation, the merging does not affect the ITF and OTF sorting. It only guarantees that a transition with smaller number appears before the transitions with larger numbers triggered by the same event.
According to the semantics of transition priority, the ITF and OTF settings of transitions are considered before their numbers. This algorithm is correct because it sorts on the basis that the ordering of ITF and OTF is already created and is preserved over the merging of two lists.
It is the designer's responsibility to ensure that there are no such transitions in a model. The simulator cannot statically analyze the model and find out these transitions, since their guards usually cannot be evaluated statically. If these transitions are found at run-time, only one of them is fired. The choice is random or implementation-dependent.
Proof Lemma 2 suggests a way in which all the transitions can be sorted in a list . Suppose is statically obtained. An additional guard for each transition checks whether the transition is the first enabled transition in the list. This guard ensures that the choice of a transition in a conflict is unique and deterministic. The chosen transition always has the highest priority. Other transitions that are enabled are not fired since they order after the fired one. For simplicity, conflicts that cannot be solved with transition priorities are not considered.
Proof Transition parameters are themselves variables. If each transition is given a GUID, and the GUID of the transition is added to the names of its formal parameters, those parameter names share the same name space as the variable set of the model. All the transition parameters can thus be included in the variable set. To send an event with parameters, the action simply modifies the global variables converted from the parameters of the transition that handles the event, and sends the event without parameters.
Lists can be used as variables. So if more than one event in the global event list is going to trigger the same transition, parameters can be queued in a global parameter list.
Proof Ports and connections in DCharts allow to connect multiple models and run them in a single simulation. Statecharts do not provide this mechanism. However, the behavior of a combination of multiple DCharts models connected with ports can be simulated with a single stand-alone statecharts model.
Ports restrict the receivers of a message. Connections are established between ports of a model and ports of remote components whose names match a pattern. To simulate this in a statecharts model, the messages are transformed into events. The parameters are transformed into global variables (see Lemma 4). The name patterns and the port names of remote components are additional parameters sent with the event. Each transition triggered by this event checks the name pattern in its guard. Only those transitions with names (inherited from their states) matching the pattern are triggered.
To simulate the broadcast of messages, an event is duplicated. Each transition triggered by the event regenerates the event in its output actions. The event is repeatedly handled until it is ignored because no transition is able to handle it. To avoid handling a event more than once by the same transition, the transition must remember whether it has handled the most recent event. This implies adding states or variables to the model.
Proof This is easily proved on the basis of Lemma 1 to Lemma 5.
Theorem 2 proves that non-recursive DCharts are at most as powerful as statecharts with variables. Extensions such as transition priorities, importation and ports do not enhance the expressiveness of the formalism. However, they make it easier to design modular models.