Skip to content

Instantly share code, notes, and snippets.

@y-taka-23
Last active July 27, 2018 12:53
Show Gist options
  • Save y-taka-23/6171102 to your computer and use it in GitHub Desktop.
Save y-taka-23/6171102 to your computer and use it in GitHub Desktop.
Alloy による自動販売機のモデリング
// ************************************
// ジュースの自動販売機のモデル
// ************************************
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 {}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment