ソフトウェア科学基礎（近代科学社）練習問題1.9

「ソフトウェア科学基礎」http://books.livedoor.com/item/2024302
の練習問題1.9より。
宝石の入ったつづらを当てる問題。

Alloyで。

/*
「ソフトウェア科学基礎」練習問題1.9

　pred showの中で、honesty,liarを変更し、
どちらであっても宝石(Jewel)と繋がるつづらが宝石のつづら
*/
//つづら
abstract sig Basket {
content : one Content
}
one sig BigBasket,SmallBasket extends Basket {}

//中身
abstract sig Content {}
one sig Jewel,Ghost extends Content {}

//貼り紙「2つのつづらには違うものが入っている」
pred bill1 {
no disj b,b':Basket | b.content = b'.content
}

//貼り紙「大きいつづらには魑魅魍魎が入っている」
pred bill2 {
all b:BigBasket | b.content = Ghost
}

//正直雀
pred honesty {
bill1 and bill2
}

//嘘つき雀
pred liar {
not bill1 and not bill2
}

pred show {
liar
}

run show