Rodin User’s Handbook v.2.8: The refined machine with data refinement for peds

2.8.4 The refined machine with data refinement for peds_go

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

MACHINE

mac1

REFINES

mac

SEES

ctx1

VARIABLES

$\tt cars\_ go$

$\tt peds\_ colour$

INVARIANTS

$\tt inv4 :$

$\it peds\_ colour \in \{ red, green \}$

$\tt gluing :$

$\it peds\_ go = TRUE \mathbin \Leftrightarrow peds\_ colour = green$

EVENTS

Initialisation

begin

$\tt act1 :$

$\it cars\_ go := FALSE$

$\tt init4 :$

$\it peds\_ colour := red$

end

Event

set_peds_green $\mathrel {\widehat=}$

refines

set_peds_go

when

$\tt grd1 :$

$\it cars\_ go = FALSE$

then

$\tt act2 :$

$\it peds\_ colour := green$

end

Event

set_peds_red $\mathrel {\widehat=}$

refines

set_peds_stop

begin

$\tt act1 :$

$\it peds\_ colour := red$

end

Event

set_cars $\mathrel {\widehat=}$

refines

set_cars

any

$\it new\_ value$

where

$\tt grd1 :$

$\it new\_ value \in BOOL$

$\tt grd2 :$

$\it new\_ value = TRUE \mathbin \Rightarrow peds\_ colour = red$

then

$\tt act1 :$

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

end

END

Rodin Handbook

2.8.4 The refined machine with data refinement for peds_go