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
これを実行すると下記のような例が出力されました。
顧客が品物を買ってくれて、請求が立っているけど支払いはまだ。金額は3円。
みたいな内容を表していると思います。
pred
で述語を定義し実行することで、その条件を満たす例を挙げてくれる様です。
Alloyのはまりどころに関してですが.(ドット)
による演算の意味を正しく理解しなければならないなと思いました。
オブジェクト指向的な意味でのオブジェクトフィールドの参照と捉えていましたが、全くの別物でした。
集合、をそれぞれ、、とする時はとなる様な演算です。