Formal Definition

The above controller for crosswalk lights can be modeled by an atomic SP-DEVS model. Formally, an atomic SP-DEVS is a 7-tuple

$${\displaystyle M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>}$$

where

• ${\displaystyle X}$ is a finite set of input events;
• ${\displaystyle Y}$ is a finite set of output events;
• ${\displaystyle S}$ is a finite set of states;
• ${\displaystyle s_{0}\in S}$ is the initial state;
• ${\displaystyle \tau :S\rightarrow \mathbb {Q} _{[0,\infty ]}}$ is the time advanced function which defines the lifespan of a state where ${\displaystyle \mathbb {Q} _{[0,\infty ]}}$ is the set of non-negative rational numbers plus infinity.
• ${\displaystyle \delta _{x}:S\times X\rightarrow S}$ is the external transition function which defines how an input event changes a state of the system.
• ${\displaystyle \delta _{y}:S\rightarrow Y^{\phi }\times S}$ is the output and internal transition function where ${\displaystyle Y^{\phi }=Y\cup \{\phi \}}$ and ${\displaystyle \phi \notin Y}$ denotes the silent event. The output and internal transition function defines how a state generates an output event, at the same time, how the state changes internally.^[1]

Formal Representation of Crosswalk Controller

The above controller shown in Fig. 2 can be written as ${\displaystyle M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>}$ where ${\displaystyle X}$={?p}; ${\displaystyle Y}$={!g:0, !g:1, !w:0, !w:1}; ${\displaystyle S}$={BG, BW, G, GR, R, W, D}; ${\displaystyle s_{0}}$=BG, ${\displaystyle \tau }$(BG)=0.5,${\displaystyle \tau }$(BW)=0.5, ${\displaystyle \tau }$(G)=30, ${\displaystyle \tau }$(GR)=30,${\displaystyle \tau }$(R)=2, ${\displaystyle \tau }$(W)=26, ${\displaystyle \tau }$(D)=2; ${\displaystyle \delta _{x}}$(G,?p)=GR, ${\displaystyle \delta _{x}}$(s,?p)=s if s ${\displaystyle \neq }$G; ${\displaystyle \delta _{y}}$(BG)=(!g:1, BW), ${\displaystyle \delta _{y}}$(BW)=(!w:0, G),${\displaystyle \delta _{y}}$(G)=(${\displaystyle \phi }$, G), ${\displaystyle \delta _{y}}$(GR)=(!g:0, R), ${\displaystyle \delta _{y}}$(R)=(!w:1, W), ${\displaystyle \delta _{y}}$(W)=(!w:0, D), ${\displaystyle \delta _{y}}$(D)=(!g:1, G);

Behaviors of a SP-DEVS model

Fig. 3. Event Segment and its State Trajectory of SP-DEVS model

To captured the dynamics of an atomic SP-DEVS, we need to introduce two variables associated to time. One is the lifespan, the other is the elapsed time since the last resetting. Let ${\displaystyle t_{s}\in \mathbb {Q} _{[0,\infty ]}}$ be the lifespan which is not continuously increasing but set by when a discrete event happens. Let ${\displaystyle t_{e}\in [0,\infty ]}$ denote the elapsed time which is continuously increasing over time if there is no resetting.

Fig.3. shows a state trajectory associated with an event segment of the SP-DEVS model shown in Fig. 2. The top of Fig.3. shows an event trajectory in which the horizontal axis is a time axis so it shows an event occurs at a certain time, for example, !g:1 occurs at 0.5 and !w:0 at 1.0 time unit, and so on. The bottom of Fig. 3 shows the state trajectory associated with the above event segment in which the state ${\displaystyle s\in S}$ is associated with its lifespan and its elapsed time in the form of ${\displaystyle (s,t_{s},t_{e})}$. For example, (G, 30, 11) denotes that the state is G, its lifespan is and the elapsed time is 11 time units. The line segments of the bottom of Fig. 3 shows the time flow of the elapsed time which is the only one continuous variable in SP-DEVS.

One interesting feature of SF-DEVS might be the preservation of schedule the restriction (3) of SP-DEVS which is drawn at time 47 in Fig. 3. when the external event ?p happens. At this moment, even though the state can change from G to GR, the elapsed time does not change so the line segment is not broken at time 47 and ${\displaystyle t_{e}}$ can grow up to ${\displaystyle t_{e}}$ which is 30 in this example. Due to this preservation of the schedule from input events as well as the restriction of the time advance to the non-negative rational number (see restriction (2) above), the height of every saw can be a non-negative rational number or infinity (as shown in the bottom of Fig. 3.) in a SP-DEVS model.

SP-DEVS is a sub-class of DEVS

A SP-DEVS model, ${\displaystyle M=<X,Y,S,s_{0},\tau ,\delta _{x},\delta _{y}>}$ is DEVS ${\displaystyle {\mathcal {M}}=<X,Y,S',s_{0}',ta,\delta _{ext},\delta _{int},\lambda >}$ where

• ${\displaystyle X,Y}$ of ${\displaystyle {\mathcal {M}}}$ are the same as those of ${\displaystyle M}$.
• ${\displaystyle S'=\{(s,t_{s}):s\in S,t_{s}\in \mathbb {T} ^{\infty }\}}$
• ${\displaystyle s_{0}'=(s_{0},\tau (s_{0}))}$
• Given a state ${\displaystyle (s,t_{s})\in S'}$, ${\displaystyle ta(s,t_{s})=t_{s}.}$
• Given a state ${\displaystyle (s,t_{s})\in S'}$ and an input event ${\displaystyle x\in X,\delta _{ext}(s,t_{s},t_{e},x)=(s',t_{s}-t_{e}){\text{ if }}\delta _{x}(s,x)=s'.}$
• Given a state ${\displaystyle (s,t_{s})\in S'}$, ${\displaystyle \delta _{int}(s,t_{s})=(s',\tau (s')}$ if ${\displaystyle \delta _{y}(s)=(y,s').}$
• Given a state ${\displaystyle (s,t_{s})\in S'}$, ${\displaystyle \lambda (s,t_{s})=y}$ if ${\displaystyle \delta _{y}(s)=(y,s').}$