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);
Read more about this topic: SP-DEVS, Atomic SP-DEVS
Famous quotes containing the words formal and/or definition:
“The manifestation of poetry in external life is formal perfection. True sentiment grows within, and art must represent internal phenomena externally.”
—Franz Grillparzer (17911872)
“Was man made stupid to see his own stupidity?
Is God by definition indifferent, beyond us all?
Is the eternal truth mans fighting soul
Wherein the Beast ravens in its own avidity?”
—Richard Eberhart (b. 1904)