SP-DEVS - Atomic SP-DEVS - Formal Definition

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

where

• is a finite set of input events;
• is a finite set of output events;
• is a finite set of states;
• is the initial state;
• is the time advanced function which defines the lifespan of a state where is the set of non-negative rational numbers plus infinity.
• is the external transition function which defines how an input event changes a state of the system.
• is the output and internal transition function where and 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.

Formal Representation of Crosswalk Controller

The above controller shown in Fig. 2 can be written as where ={?p}; ={!g:0, !g:1, !w:0, !w:1}; ={BG, BW, G, GR, R, W, D}; =BG, (BG)=0.5,(BW)=0.5, (G)=30, (GR)=30,(R)=2, (W)=26, (D)=2; (G,?p)=GR, (s,?p)=s if s G; (BG)=(!g:1, BW), (BW)=(!w:0, G),(G)=(, G), (GR)=(!g:0, R), (R)=(!w:1, W), (W)=(!w:0, D), (D)=(!g:1, G);