Alloy による非同期通信チャネルのモデリング (キューの仕様については https://gist.github.com/y-taka-23/8202051 を参照のこと)

alloy_channel.als

// **************************************************
//  通信チャネルとしてキューを用いたモデル
// **************************************************

open util/ordering[Time]
open alloy_queue[Request]

sig Time {}            // 時刻パラメータ
sig Client, Server {}  // 通信に参加するクライアントとサーバ
sig Request {}         // クライアントがサーバに送るメッセージ

// 通信チャネル : 簡単にするためクライアントからサーバへの片道通信のみ考える
sig Channel {
    queue    : disj Queue one -> Time,  // 各時刻におけるメッセージキューの状態
    sender   : Client,                  // 送信側クライアント 
    receiver : Server,                  // 受信側サーバ
    buffer   : Int                      // バッファサイズ
} {
    buffer > 0
    all t : Time | (queue.t).size <= buffer
}

// 同じ通信ノード間に二重に張られているチャンネルは存在しない
fact simpleChannel {
    all disj ch1, ch2 : Channel |
        ch1.sender != ch2.sender or  ch1.receiver != ch2.receiver
}

// 無駄なキューは生成しない
fact noIsolateQueue {
    all q : Queue | some t : Time, ch : Channel | q in ch.queue.t
}

// 無駄なクライアント / サーバは生成しない
fact noIsolateNode {
    Client in Channel.sender
    Server in Channel.receiver
}

// 時刻 t と t' との間でチャネル ch 内の状況が変化しない
pred inactive (t, t' : Time, ch : Channel) {
    let q = ch.queue.t, q' = ch.queue.t' | equiv[q, q']
}

// リクエスト送信 : 時刻 t と t' との間でクライアント c が
//                チャネル ch にリクエスト r を送信
pred sendRequest (t, t' : Time, c : Client, ch : Channel, r : Request) {
    c in ch.sender
    r not in Channel.(queue.t).values
    let q = ch.queue.t, q' = ch.queue.t' | enqueue[q, q', r]
    all ch0 : Channel - ch | inactive[t, t', ch0]
}

// リクエスト受信 : 時刻 t と t' との間でサーバ s が
//                チャネル ch からリクエスト r を受信
pred receiveRequest (t, t' : Time, s : Server, ch : Channel, r : Request) {
    s in ch.receiver
    r not in Channel.(queue.t').values
    let q = ch.queue.t, q' = ch.queue.t' | dequeue[q, q', r]
    all ch0 : Channel - ch | inactive[t, t', ch0]
}

// 初期状態 :すべてのチャネルは空
pred init (t : Time) {
    all ch : Channel | empty[ch.queue.t]
}

// 状態遷移に関する制約
fact trases {
    init[first]
    all t : Time - last | let t' = t.next |
        some c : Client, ch : Channel, r : Request | sendRequest[t, t', c, ch, r] or
        some s : Server, ch : Channel, r : Request | receiveRequest[t, t', s, ch, r]
}

// チャネル容量が一杯になると送信できなくなる
assert senderWaiting {
    all t, t' : Time, c : Client, ch : Channel, r : Request |
        (ch.queue.t).size = ch.buffer implies not sendRequest[t, t', c, ch, r]
}

// チャネルが空になると受信できなくなる
assert receiverWaiting {
    all t, t' : Time, s : Server, ch : Channel, r : Request |
        empty[ch.queue.t] implies not receiveRequest[t, t', s, ch, r]
}

check senderWaiting   for 5
check receiverWaiting for 5
run {}                for 5