2.2.1 Overview

A model $M$ in DCharts 1.0 is defined by a tuple

$$<S,T,C,V,\Delta,P,L>$$

where:

• $S=\{s_1,s_2,...,s_m\}$ is a set of finite and enumerable states. $s_i$ ( $i\in [1,...,m]$) is a tuple
  
  $$<SN,DS,CS,HS,TP,EN,EX>$$
  
  
  where:
  • $SN$ is a string that represents a globally unique identifier (GUID) of the state. Every state in a given model has a unique GUID. GUIDs of states in different models may be the same.

  • $DS$ is a boolean value that specifies whether state $s_i$ is a default state of its parent state. Among the children of a parent state there must be exactly one default state, unless all those children are orthogonal components (discussed later).

  • $CS$ is a boolean value that specifies whether state $s_i$ is an orthogonal component. If a state is an orthogonal component, all its siblings (other children of the same parent) must also be orthogonal components, and all those states are default states in their nature ($DS=true$).

  • $HS$ is an enumerated value that specifies whether state $s_i$ has a history in it, and, if it has a history, whether the history is deep history. Its possible values are defined with an enumerated type (explained later):
    
    $$HS = \{None, Normal, Deep\}$$
    
    

  • $TP$ is an enumerated value that specifies the transition priority within the scope of state $s_i$. The scope of a state includes the state itself, all its children states, and all the transitions from that state and its children states. Possible values of $TP$ are defined below (explained later):
    
    $$TP = \{Keep, ITF, OTF, RTO\}$$
    
    

  • $EN$ is a list of sequentially executed enter actions. These actions are executed when the state is entered (whether from other states or from this state itself). In DCharts 1.0, there is no strict definition of actions. This part is subject to change in later versions, where a more rigorous definition of action code will be given. However, actions must conform to several rules. Those rules are discussed in section 2.2.8.

  • $EX$ is a list of sequentially executed exit actions. These actions are executed when the state is exited (whether the destination is another state or this state itself). This part is subject to change in later versions, where a more rigorous definition of action code will be given. Some rules of actions are further discussed in section 2.2.8.

• $T=\{t_1,t_2,...,t_n\}$ is a set of transitions. $t_i$ ( $i\in [1,...,n]$) is a tuple
  
  $$<SRC,DES,E,\gamma,G,\lambda,HS_T,Prio>$$
  
  
  where:
  • $SRC\in S$ is the source state.

  • $DES\in S$ is the destination state.

  • $E$ is a string that represents the event name. This event triggers the transition. The event name should not contain a ``.'' (which is used in inter-model communication via ports), unless the transition handles an incoming message. In that case, the event name is the input port name followed by a dot, and then followed by the message name.

  • $\gamma=\{\gamma_1,\gamma_2,...,\gamma_k\}$ is a set of variables that represent the formal parameters. Each parameter is a variable. In DCharts 1.0, there is no strict definition of variables. Section 2.2.4 offers a loose definition of variables.

  • $G$ is a boolean expression that specifies the guard. In DCharts 1.0, there is no strict definition of guards. One of the few requirements is that they can be evaluated to a boolean result at the time when the event of the transition is received. Guards are further discussed in section 2.2.8.

  • $\lambda$ is a list of sequentially executed actions. In DCharts 1.0, there is no strict definition of actions. This part is subject to change in later versions, where a more rigorous definition on action code will be given. Several rules of actions are discussed in section 2.2.8.

  • $HS_T$ is a boolean variable that specifies whether the transition goes to the history of the destination state (if it has a normal history or deep history) or the default substate of it (if it has substates).

  • $Prio$ is an integer number (may be positive or negative) that specifies the priority of the transition. In case a conflict occurs that cannot be solved by transition ordering (discussed later), the transition with the smallest $Prio$ number has the highest priority.

• $C:S\rightarrow 2^S$ is a function that defines the parent-children relationship of all the states. It maps any state to the set of its children states. All the states in a model and their parent-children relations form a tree (with states as nodes and relations as edges).

• $V=\{v_1,v_2,...,v_s\}$ is the set of variables. In DCharts 1.0, there is no strict definition of variables. The only requirement is that every variable has a GUID and provides a certain amount of storage. This part is implementation-dependent. It is subject to change in later versions, where a more rigorous definition of variables and the operations on them will be given.

• $\Delta:S\rightarrow M$ is the mapping of importations. If $\Delta$ is defined for a state $s_i$, the result of the function gives the definition of a model which is imported into $s_i$. Importing a model into a state means, in theory, including all its states and transitions in that state. The states defined in the imported model become substates of the importation state. The transitions between the states of the imported model are preserved. An implementation of DCharts must provide a means to modify the GUIDs in the submodels, so that they never conflict with the GUIDs of the importing model. (Note that the imported model itself may import models, and a model may import multiple models.) It is allowed for a model to import itself. Such a recursive specification allows for the dynamic creation of arbitrary-sized models (discussed later).

• $P=\{p_1,p_2,...,p_t\}$ is the set of ports. In DCharts 1.0, a port $p_i$ ( $i\in [1,...,t]$) is a tuple $<PN,PT>$ (later versions of DCharts may add more information to a port to further specify it), where:
  • $PN$ is the GUID of the port. This GUID has a different name space from the GUIDs of states. As a result, even if the $PN$ of a port is equal to the $SN$ of a state, no conflict occurs. There is no restriction on a port name, except that it must not contain a ``.'' or a space.

  • $PT$ is the type of the port. In DCharts 1.0, the following types are defined (later versions of DCharts may add more information):
    
    $$PT=\{InOut, In, Out\}$$
    
    

• $L=\{l_1,l_2,...,l_u\}$ a set of mappings from ports in one model to the ports of other models. $l_i$, with $i\in [1,...,u]$, is a tuple $<PN_1,<M,PN_2>>$, where:
  • $PN_1$ is the GUID of a port in this model (the model that contains the definition of this $l_i$).

  • $M$ is another model, which the currently specified model connects to.

  • $PN_2$ is the GUID of a port in model $M$.

  Note that if $P_1$ of model $M_1$ is connected to $P_2$ of model $M_2$ with a single connection, either $M_1$ or $M_2$ specifies this connection, but not both. The model in with the connection is specified looks up the other model when the simulation or execution of it starts.

  If in a simulation or execution, more than one model (or component) $M_1,M_2,...,M_v$ has exactly the same definition ( $M_1=M_2=...=M_v$), a link $l=<PN_1,<M_i,PN_2>>$ ( $i\in [1,2,...,v]$) in $L$ implies that $PN_1$ is connected to $PN_2$ of all those models with the same definition.