Rodin Handbook





 

2.8.7 The Refined Machine with All Data Refinement

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

MACHINE

mac1

REFINES

mac

SEES

ctx1

VARIABLES
$\tt  peds\_ colour $
$\tt  cars\_ colours $
INVARIANTS
$\tt  inv4 :$

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

$\tt  inv5 :$

$\it  cars\_ colours \subseteq COLOURS $

$\tt  gluing\_ peds :$

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

$\tt  gluing\_ cars :$

$\it  cars\_ go = TRUE \mathbin \Leftrightarrow green \in cars\_ colours $

EVENTS
Initialisation
begin
$\tt  init4 :$

$\it  peds\_ colour := red $

$\tt  init5 :$

$\it  cars\_ colours := \{  red \}  $

end
Event

set_peds_green $\mathrel {\widehat=}$

refines

set_peds_go

when
$\tt  grd1 :$

$\it  green \notin cars\_ colours $

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_colours $\mathrel {\widehat=}$

refines

set_cars

any
$\it  new\_ value\_ colours $
where
$\tt  grd1 :$

$\it  new\_ value\_ colours \subseteq COLOURS $

$\tt  grd2 :$

$\it  green \in new\_ value\_ colours \mathbin \Rightarrow peds\_ colour = red $

$\tt  grd\_ y\_ r :$

$\it  cars\_ colours = \{  yellow \}  \mathbin \Rightarrow new\_ value\_ colours = \{  red \}  $

$\tt  grd\_ r\_ ry :$

$\it  cars\_ colours = \{  red \}  \mathbin \Rightarrow new\_ value\_ colours = \{  red, yellow \}  $

$\tt  grd\_ ry\_ g :$

$\it  cars\_ colours = \{  red, yellow \}  \mathbin \Rightarrow new\_ value\_ colours = \{  green \}  $

$\tt  grd\_ g\_ y :$

$\it  cars\_ colours = \{  green \}  \mathbin \Rightarrow new\_ value\_ colours = \{  yellow \}  $

with
$\tt  new\_ value :$

$\tt  new\_ value = TRUE \mathbin \Leftrightarrow green \in new\_ value\_ colours $

then
$\tt  act1 :$

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

end
END