Formal Specification

External transition function

case of S

init

If com = in then in := run ; s := 0 ; S : = Atap; flag:= 0

else error

Atap

If com = off then in:= stop ; s := 0 ; S : = init; flag:= 0

else error

Remp.

If com = off then van:= close ; s := 0 ; S : = init; flag:=1

else error

Formal specification

Output function

case of flag

0 send-out in

1 send-out van

2 send-out in, van

Diapositiva precedente

Diapositiva successiva

Torna alla prima diaposiva

Visualizza versione grafica