5.1 Mapping from Non-recursive DCharts to Statecharts with Variables

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 $V$ 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:

• Importation.

• Transition priorities.

• Transition parameters.

• Ports and connections.

Since the variable set $V$ 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.

Lemma 1   Importation of non-recursive DCharts models can be flattened to be the state hierarchy of original statecharts.

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. $\Box$

Lemma 2   There exists an ordering over all the transitions in every DCharts model. According to this ordering, when an event causes a conflict at run-time, the first enabled transition in the list always has the highest priority.

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 $l$. When $\vert l\vert$ is equal to the number of transitions in the model, the algorithm terminates, and the ordering of the transitions in $l$ 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($l_s$, $l$)
/* merge two sets of transitions with insertion sort
$l_s$: the transitions to be merged with $l$. The $SRC$ of these transitions has no parent-children relation with the $SRC$ of transitions in $l$. Conflicts between transitions in the two lists can only be solved with their $Prio$ number.
$l$: another set of transitions
return: the union of $l_s$ and $l$. The transitions are sorted by priority.
*/
for $t$ in $l_s$
added = false
for $t'$ in $l$
if $E_{t}=E_{t'} \wedge Prio_{t}<=Prio_{t'}$ then
insert $t$ into $l$ right before $t'$
added = true
break
if !added then
append $t$ to the end of $l$
return $l$

function order($states$, $ITF$)
/* sort the transitions
$states$: a set of states belonging to the same parent
$ITF$: whether the parent of the states in $states$ is set to be inner-transition-first or not
return: the list $l$ of transitions whose $SRC$ is in $states$ or $Substate(s)$ where $s\in states$. The transitions are sorted by priority.
*/
$l$ = []
for $s$ in $states$
$l_{ts}$ = [transitions with $SRC$ = $s$]
sort $l_{ts}$ in the increasing order of the $Prio$ numbers of the transitions
if $s$ is $ITF$ then
next_ITF = $true$
elif $s$ is $OTF$ then
next_ITF = $false$
elif $s$ is $RTO$ then
next_ITF = not ITF
else
next_ITF = ITF
if $ITF$ then
$l_s$ = $l_{ts}$ + order($C(s)$, next_ITF)
else
$l_s$ = order($C(s)$, next_ITF) + $l_{ts}$
merge($l_s$, $l$)
return $l$

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 $Prio$ 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 $Top_s$, and parameter $InnerTransitionFirst$ contains the global option of the model that decides whether its top-level states are inner-transition-first by default. The invocation $order(Top_s, InnerTransitionFirst)$ 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 $ITF$, 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 $OTF$ 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 $Prio$ 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 $Prio$ number appears before the transitions with larger $Prio$ numbers triggered by the same event.

According to the semantics of transition priority, the ITF and OTF settings of transitions are considered before their $Prio$ numbers. This algorithm is correct because it sorts $Prio$ on the basis that the ordering of ITF and OTF is already created and is preserved over the merging of two lists. $\Box$

Comments 1   Although this algorithm ensures that the transition with higher total priority always appear before the others with lower total priorities in the sorted list, it does not remove all the potential conflicts. It is still possible that two transitions have exactly the same total priority. Those two transitions ($t1$ and $t2$) always have the following properties:

• $SRC_{t1}=SRC_{t2}$ or $SRC_{t1}$ and $SRC_{t2}$ belong to two sibling orthogonal components. In that case, the ITF and OTF settings cannot solve the conflict, and it is possible that the model is in $SRC_{t1}$ and $SRC_{t2}$ at the same time.

• $E_{t1}=E_{t2}$. When this event is raised and $G_{t1}=true \wedge G_{t2}=true$ at run-time, both transitions are enabled.

• $Prio_{t1}=Prio_{t2}$. In this case, the $Prio$ number cannot solve the conflict.

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.

Comments 2   In the implementation of SVM, this algorithm that sorts transitions in the order of their priorities is employed. It effectively decreases the run-time computation for choosing a transition in case of a conflict. Because the first enabled transition in the list always has the highest priority among all the enabled transitions, the simulator simply picks the first one and triggers it. The sorting is done only once for every model or submodel in a simulation.

Lemma 3   Transition priorities can be simulated with additional guards.

Proof Lemma 2 suggests a way in which all the transitions can be sorted in a list $l$. Suppose $l$ 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. $\Box$

Lemma 4   Transition parameters can be simulated with variables.

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 $V$ 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. $\Box$

Lemma 5   Ports and connections can be simulated in a stand-alone statecharts model.

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 $SRC$ 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. $\Box$

Theorem 2   Non-recursive DCharts models can be mapped to statecharts with variables that have the same behavior.

Proof This is easily proved on the basis of Lemma 1 to Lemma 5. $\Box$

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.