kencoba

(define-channel t-f (x) '((0) (1)))
(define-channel t-b (x) '((0) (1)))

(define-channel f-c (x) '((0) (1)))
(define-channel b-c (x) '((0) (1)))
(define-channel g-c (x) '((0) (1)))

(define-event gate-open)
(define-event gate-close)

kencoba

(deadlock SYS)
(trace SPEC SYS)
(failure SPEC SYS)

kencoba

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

(define-process ACTIVE
  (alt
    (! engineOff INACTIVE)

kencoba

(define-process INACTIVE
  (alt
    (? ss-cc (x)
       (eqv? x 'engineOn)
       (! cc-sc ('clearSpeed) ACTIVE))
    (? ss-cc (x)
       (or (eqv? x 'off) (eqv? x 'brake) (eqv? x 'accelerator))
       INACTIVE)))

(define-process ACTIVE

kencoba

; Definitions
(define-channel rch (x) '((0) (1)))
(define-channel sch (x) '((0) (1)))

; Receiver
(define-process Receiver
  (? rch (x) (= x 0) (! sch (0) Receiver)))

; Sender : Deadlockの例1 SenderもReceiverもメッセージ受信待ち
(define-process Sender

kencoba

(define-event on)
(define-event off)

(define-channel switch-ch (x) '((0)))

kencoba

(define-event ok)
(define-event ng)

(define-event ping)

(define-channel rch (x) '((ping)))
(define-channel sch (x) '((ok) (ng)))
(define-channel cch (x) '((ok)))

kencoba

(define-event in)
(define-event out)

(define-event send)
(define-event data)
(define-event err)

(define-event ack)
(define-event nak)

kencoba

module CruiseControlSystem

/*
    Initial model of Cruise Control System
    Kenichi Kobayashi
*/

enum ControlStatus { enable,disable }
enum Speed { Null, Zero, Low, Normal, High, VeryHigh }

kencoba

(defun rgb-string-to-values (val)
  (interactive)
  (format " %d %d %d"
          (string-to-number  (substring val 0 2) 16)
          (string-to-number  (substring val 2 4) 16)
          (string-to-number  (substring val 4 6) 16)
          ))

; test
(rgb-string-to-values "ffffff")