Rodin Handbook





 

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