Alloy による自動販売機のモデリング

alloy_vender.als

// ************************************
//   ジュースの自動販売機のモデル
// ************************************

open util/ordering[Time]

// 時刻パラメータ
sig Time {}

// 簡略化のため、コインの額面とジュースの種類はそれぞれ 1 種類とする
sig Coin {}
sig Bottle {}

// 利用者
one sig User {
    coins   : Coin -> Time,    // 所持金
    bottles : Bottle -> Time,  // 所持しているジュース
}

// 自動販売機
one sig Machine {
    poolCoins  : Coin -> Time,    // コイン溜め
    salesCoins : Coin -> Time,    // 売上箱
    bottles    : Bottle -> Time,  // ストックされているジュース
}

// 各時刻においてコイン、ジュースはちょうど一カ所に存在する
fact uniquelyAssigned {
    all t : Time {
        // コインは利用者、コイン溜め、売上箱のどこかに
        let uc = User.coins.t,
                pc = Machine.poolCoins.t,
                    sc = Machine.salesCoins.t {
            all c : Coin | c in uc + pc + sc
            no  c : Coin | c in uc & (pc + sc)
            no  c : Coin | c in pc & sc
        }
        // ジュースは利用者、自動販売機のどちらかに
        let ub = User.bottles.t,
                mb = Machine.bottles.t {
            all b : Bottle | b in ub + mb
            no  b : Bottle | b in ub & mb
        }
    }
}

// 状態遷移イベント
abstract sig Event {
    // 複数のイベントが同時に発生することはない (disj) とする
    pre, post : disj Time,  // イベント前時刻とイベント後時刻
} {
    // イベントにはちょうど 1 単位時間かかる
    post = pre.next
}

// 利用者がコインを投入するイベント
sig insertCoin extends Event {
    coin : Coin,  // 投入されるコイン
} {
    // 利用者の所持金から投入される
    coin in User.coins.pre
    // コインが利用者 --> コイン溜めに移動
    User.coins.post         = User.coins.pre - coin
    Machine.poolCoins.post  = Machine.poolCoins.pre + coin
    // それ以外は変化なし
    Machine.salesCoins.post = Machine.salesCoins.pre
    User.bottles.post       = User.bottles.pre
    Machine.bottles.post    = Machine.bottles.pre    
}

// ボタンが押下されたが何も起こらないイベント
sig pushButtonInVain extends Event {
} {
    // コイン溜めにコインがない
    no c : Coin | c in Machine.poolCoins.pre
    // 状態は変化なし
    User.coins.post         = User.coins.pre
    Machine.poolCoins.post  = Machine.poolCoins.pre
    Machine.salesCoins.post = Machine.salesCoins.pre
    User.bottles.post       = User.bottles.pre
    Machine.bottles.post    = Machine.bottles.pre    
}

// ジュースを実際に販売するイベント
sig getBottle extends Event {
    coin   : Coin,    // 売上に計上されるコイン
    bottle : Bottle,  // 出てくるジュース
} {
    // コイン溜めにあるコインが消費される
    coin in Machine.poolCoins.pre
    // 自動販売機にストックされていたジュースが出てくる
    bottle in Machine.bottles.pre
    // コインがコイン溜め --> 売上箱に移動
    Machine.poolCoins.post  = Machine.poolCoins.pre - coin
    Machine.salesCoins.post = Machine.salesCoins.pre + coin
    // ジュースが自動販売機 --> 利用者に移動
    User.bottles.post    = User.bottles.pre + bottle
    Machine.bottles.post = Machine.bottles.pre - bottle 
    // 利用者の所持金は変化なし
    User.coins.post = User.coins.pre
}

// 初期状態
pred init (t : Time) {
    // コイン溜めは空
    no c : Coin | c in Machine.poolCoins.t
}

// 各時刻に、ちょうど 1 つのイベントが生じる
fact traces {
    init[first]
    all t : Time - last | let t' = t.next |
        one e : Event | e.pre = t && e.post = t'
}

// 投入したコイン以上のジュースを買うことはできない
assert noOverSelling {
    all t : Time |
        #User.bottles.t - #User.bottles.first
            <= #User.coins.first - #User.coins.t
}
check noOverSelling

run {}