Rodin User’s Handbook v.2.8: The Final Traffic Light Model

2.4.5 The Final Traffic Light Model

$\includegraphics[width=7mm]{img/pencil_64.png}$

MACHINE

mac

VARIABLES

$\tt cars\_ go$

$\tt peds\_ go$

INVARIANTS

$\tt inv1 :$

$\it cars\_ go \in BOOL$

$\tt inv2 :$

$\it peds\_ go \in BOOL$

$\tt inv3 :$

$\it \lnot (cars\_ go = TRUE \land peds\_ go = TRUE)$

EVENTS

Initialisation

begin

$\tt act1 :$

$\it cars\_ go := FALSE$

$\tt act2 :$

$\it peds\_ go := FALSE$

end

Event

set_peds_go $\mathrel {\widehat=}$

when

$\tt grd1 :$

$\it cars\_ go = FALSE$

then

$\tt act1 :$

$\it peds\_ go := TRUE$

end

Event

set_peds_stop $\mathrel {\widehat=}$

begin

$\tt act1 :$

$\it peds\_ go := FALSE$

end

Event

set_cars $\mathrel {\widehat=}$

any

$\it new\_ value$

where

$\tt grd1 :$

$\it new\_ value \in BOOL$

$\tt grd2 :$

$\it new\_ value = TRUE \mathbin \Rightarrow peds\_ go = FALSE$

then

$\tt act1 :$

$\it cars\_ go := new\_ value$

end

END

Rodin Handbook

2.4.5 The Final Traffic Light Model