/** Concurrency: State Models and Java Programs
 *             Jeff Magee and Jeff Kramer
 *  
 */

// Cruise Control System

set Sensors = {engineOn,engineOff,on,off,
               resume,brake,accelerator} 
set Engine  = {engineOn,engineOff} 
set Prompts = {clearSpeed,recordSpeed,
               enableControl,disableControl} 

SENSORSCAN = ({Sensors} -> SENSORSCAN).

INPUTSPEED = (engineOn -> CHECKSPEED),
CHECKSPEED = (speed -> CHECKSPEED
             |engineOff -> INPUTSPEED 
             ).

THROTTLE =(setThrottle -> zoom -> THROTTLE).

SPEEDCONTROL = DISABLED,
DISABLED =({speed,clearSpeed,recordSpeed}->DISABLED
          | enableControl -> ENABLED 
          ), 
ENABLED = ( speed -> setThrottle -> ENABLED 
          |{recordSpeed,enableControl} -> ENABLED
          | disableControl -> DISABLED
          ).

CRUISECONTROLLER = INACTIVE,
INACTIVE =(engineOn -> clearSpeed -> ACTIVE),
ACTIVE   =(engineOff -> INACTIVE
          |on->recordSpeed->enableControl->CRUISING
          ),
CRUISING =(engineOff -> INACTIVE
          |{ off,brake,accelerator} 
                      -> disableControl -> STANDBY
          |on->recordSpeed->enableControl->CRUISING
          ),
STANDBY  =(engineOff -> INACTIVE
          |resume -> enableControl -> CRUISING
          |on->recordSpeed->enableControl->CRUISING
          ).

property CRUISESAFETY = 
	({off,accelerator, brake,disableControl} -> CRUISESAFETY
	|{on,resume} -> SAFETYCHECK
	),
SAFETYCHECK =
	({on,resume} -> SAFETYCHECK
	|{off,accelerator,brake} -> SAFETYACTION
	|disableControl -> CRUISESAFETY
	), 
SAFETYACTION =(disableControl->CRUISESAFETY).


||CONTROL =
     (CRUISECONTROLLER||SPEEDCONTROL||CRUISESAFETY).

||CRUISECONTROLSYSTEM = 
     (CONTROL||SENSORSCAN||INPUTSPEED||THROTTLE).

||CRUISEMINIMIZED = (CRUISECONTROLSYSTEM) 
                    @ {Sensors,speed}.