constant C  = ?
constant M1 = ?
constant M2 = ?
constant N1 = ?
constant N2 = ?
constant W  = ?
constant U1 = ?
constant U2 = ?
constant P  = ?

data PHYS_MSG =
		   STOP
		 | STEAM_BOILER_WAITING
		 | PHYSICAL_UNITS_READY
		 | PUMP_REPAIRED Pump_No
		 | PUMP_CTL_REPAIRED Pump_No
		 | LEVEL_REPAIRED
		 | STEAM_REPAIRED
		 | PUMP_FAILURE_ACKNOWLEDGEMENT Pump_No
		 | PUMP_CTL_FAILURE_ACKNOWLEDGEMENT Pump_No
		 | LEVEL_FAILURE_ACKNOWLEDGEMENT
		 | STREAM_OUTCOME_FAILURE_ACKNOWLEDGEMENT

data State = Initial | Waiting | Normal | Rescue | Degraded

type Pump_No = Int

type Pump_State =      (Pump_No, Bool)

type Pump_Ctl_State =  (Pump_No, Bool)

type Level = Int

type Steam = Int

box Handle_Stops
in  ( msg   :: PHYS_MSG, stop  :: Int initially 0 )
out ( msg'  :: PHYS_MSG, stop' :: Int )
match
	( STOP, stop ) -> if stop < 3 then ( *, stop+1 ) else ( *, * )
	( msg,  stop ) -> ( msg, stop )
;


box Distribute
in  ( msg   :: PHYS_MSG, state :: State initially Initial )
out ( msg'[1-5]  :: PHYS_MSG )
match
	( m, Initial ) ->  ( m, *, *, *, * )
|	( m, Waiting ) ->  ( *, m, *, *, * )
|	( m, Normal ) ->   ( *, *, m, *, * )
|	( m, Rescue ) ->   ( *, *, *, m, * )
|	( m, Degraded ) -> ( *, *, *, *, m )
;

box Initial
in  ( msg, q, v, ps, pcs )
out ( pu :: Bool, valve :: Bool, state :: State )
match
  ( STEAM_BOILER_WAITING, q, v, _, _ ) -> 
  	  if v != 0 then		( *, *, * )
  	  else if q >= n2 then	( *, True, Initial )
  	  else if q <= n1 then	( True, *, Initial )
  	  else 					( *, *, Waiting )
| ( _, _, _, _, _ ) -> ( *, *, Initial )
handle Timeout => ( *, *, * )
;

box Waiting
in  ( msg :: PHYS_MSG )
out ( pu :: Bool, valve :: Bool, state :: State )
match
  ( PHYSICAL_UNITS_READY) -> 
  	  if v != 0 then		( *, *, * )
  	  else if q >= n2 then	( *, True, Initial )
  	  else if q <= n1 then	( True, *, Initial )
  	  else 					( *, *, Waiting )
| ( _, _, _, _, _ ) -> ( *, *, Initial )
handle Timeout => ( *, *, * )
;

template Select{n}
in ( m[1-{n}] :: a )
out ( m' :: a )

match
	( m, *, *, *, * ) -> m
	( *, m, *, *, * ) -> m
	( *, *, m, *, * ) -> m
	( *, *, *, m, * ) -> m
	( *, *, *, *, m ) -> m
;

box 
  ( msg, q, v, ps, pcs, st ) ->
  ( STEAM_BOILER_WAITING, q, v, _, _, Initial, _ ) ->
	
box Program
in ( msg :: Maybe PHYS_MSG, q :: Level, v :: Steam,
     ps :: Pump_State, pcs :: Pump_Ctl_State, st :: State,
     stop :: Int initially 0 )
out
     stop' :: Int

match
  (Nothing, q, v, ps, pcs, st, stop ) ->
  (STOP, _, _, _, _, st, stop ) -> if stop < 3 then ( stop+1, st ) else ( stop, STOP)
  ( STEAM_BOILER_WAITING, q, v, _, _, Initial, _ ) ->
  	  if v != 0 then		( stop, STOP )
  	  else if q >= n2 then	( stop, INITIAL )
  	  else if q <= n1 then	( stop, INITIAL )
  	  else 					( stop, WAITING )
  ( PHYSICAL_UNITS_READY,