[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)))

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