[Alloy Analyzer] Cruise Control System1

ESEC2014でのAlloy Analyzerのデモを
担当することになった。

SyncStitch版だけでなく、Alloy Analyzer版のモデルもCruise Control System
にすることになった。

とにかく、短時間で説明可能なモデルを作成する。

CruiseControlSystem1.als

module CruiseControlSystem

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

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

sig SpeedControl {
    hasControl: one ControlStatus,
    targetSpeed: one Speed,
    currentSpeed: one Speed
}

pred clearSpeed[c,c':SpeedControl] {
    // clearSpeed発生時、事後の速度は何にするべきか?
    c'.targetSpeed = Null // もしNoneの場合、enableであったらどんな動作をするか?
}

pred recordSpeed[c,c':SpeedControl] {
    c'.targetSpeed = c.currentSpeed // 現在速度を目標速度として設定してよいのか?
}

pred enableControl[c,c':SpeedControl] {
    c'.targetSpeed = c.targetSpeed
    c'.hasControl = enable
    // targetSpeedが設定されていなかった場合はどうするか?
}

pred disableControl[c,c':SpeedControl] {
    c'.hasControl = disable
}

// 制御中に目標速度が初期化されてはいけない
assert enableControlAndTargetSpeedIsNull {
    no disj c,c':SpeedControl | {
        enableControl[c,c'] and
        c'.targetSpeed = Null and
        c'.hasControl = enable
    }
}

// 目標速度は制限速度内でなければならない
assert validTargetSpeed {
    all disj c,c':SpeedControl | { 
        recordSpeed[c,c'] implies c'.targetSpeed not in (Zero + VeryHigh)
    }
}


check enableControlAndTargetSpeedIsNull

check validTargetSpeed