zkat’s diary

技術ブログ

Alloyに入門している

Alloyを用いたモデル検査が行えるようになりたくて、勉強をしています。 勉強がてら、「顧客が商品を買う」という挙動についてAlloyで記述してみました。

open util/boolean

sig Consumer {}
sig Product {
    price: Consumer -> one Int,
    bought : Consumer -> one Bool,
    billed: Consumer -> one Bool,
    paid:  Consumer -> one Bool
}

fact {
    all product : Product, consumer : Consumer |
        // 支払いが済んでいるということは、請求されたということ
        (consumer.(product.paid) = True implies consumer.(product.billed) = True) and
        // 購入したならば請求が立つ。 請求が立っているならば購入された。
        (consumer.(product.bought) = True iff consumer.(product.billed) = True) and
        // 金額は0円以上
        (consumer.(product.price) >= 0)
}

pred showTwoProductOneConsumer(){
    #Product = 1
    #Consumer = 1
}

run showTwoProductOneConsumer

これを実行すると下記のような例が出力されました。

f:id:zkat:20190415225750j:plain
alloy-sample
顧客が品物を買ってくれて、請求が立っているけど支払いはまだ。金額は3円。みたいな内容を表していると思います。 predで述語を定義し実行することで、その条件を満たす例を挙げてくれる様です。

Alloyのはまりどころに関してですが.(ドット)による演算の意味を正しく理解しなければならないなと思いました。 オブジェクト指向的な意味でのオブジェクトフィールドの参照と捉えていましたが、全くの別物でした。 集合ABをそれぞれ、A=\{ (a,b),(c,d) \}B=\{ (b,α),(d,γ) \}とする時A.B\{ (a,α),(c,γ) \}となる様な演算です。