[SincStitch]Cruise Control System

Concurrency
Chapter 8:Model-Based Design
より。

自動車のCruise Control Systemのモデル。
LTSAでは、
set DisableActions = {off,brake,accelerator}としたうえで、
モデル内でDisableActions -> INACTIVEとできる。
SyncStitchではどうやるんだろ。
とりあえず地道に展開した。

Definitions

(define-event engineOn)
(define-event engineOff)
(define-event on)
(define-event off)
(define-event resume)
(define-event brake)
(define-event accelerator)

(define-event speed)
(define-event enableControl)
(define-event disableControl)
(define-event clearSpeed)
(define-event recordSpeed)
(define-event setThrottle)

(define-event zoom)

INPUTSPEED

(define-process INPUTSPEED
  (! engineOn CHECKSPEED))

(define-process CHECKSPEED
  (alt
	(! speed CHECKSPEED)
	(! engineOff INPUTSPEED)))

SPEEDCONTROL

(define-process DISABLED
  (alt
	(! speed DISABLED)
	(! clearSpeed DISABLED)
	(! recordSpeed DISABLED)
	(! enableControl ENABLED)))

(define-process ENABLED
  (alt
	(! speed (! setThrottle ENABLED))
	(! recordSpeed ENABLED)
	(! enableControl ENABLED)
	(! disableControl DISABLED)))

CRUISECONTROLLER

(define-process INACTIVE
  (alt
	(! engineOn (! clearSpeed ACTIVE))
	(! off INACTIVE)
	(! brake INACTIVE)
	(! accelerator INACTIVE)))

(define-process ACTIVE
  (alt
	(! engineOff INACTIVE)
	(! on (! recordSpeed (! enableControl CRUISING)))
	(! off ACTIVE)
	(! brake ACTIVE)
	(! accelerator ACTIVE)))

(define-process CRUISING
  (alt
	(! engineOff INACTIVE)
	(! off (! disableControl STANDBY))
	(! brake (! disableControl STANDBY))
	(! accelerator (! disableControl STANDBY))
	(! on (! recordSpeed (! enableControl CRUISING)))))

(define-process STANDBY
  (alt
	(! engineOff INACTIVE)
	(! resume (! enableControl CRUISING))
	(! on (! recordSpeed (! enableControl CRUISING)))
	(! off STANDBY)
	(! brake STANDBY)
	(! accelerator STANDBY)))

これを合成することで、まずい動作を発見するぞ。