Instantly share code, notes, and snippets.

# nagachika/puzzle_1.alloy

Created February 5, 2012 06:24
Show Gist options
• Save nagachika/1743472 to your computer and use it in GitHub Desktop.
alloy exercise for a puzzle
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 enum Cap { Black, White } abstract sig Children { cap: one Cap, visible: set Children } one sig A extends Children {} { visible = none cap = Black } one sig B extends Children {} { visible = none cap = White } one sig C extends Children {} { visible = B cap = Black } one sig D extends Children {} { visible = B + C cap = White } fact { #cap.Black = 2 and #cap.White = 2 } pred CanAnswer(c: Children) { #(c.visible :>cap.Black) = 2 or #(c.visible :> cap.White) = 2 } run { no c: Children | CanAnswer [c] }
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 // 帽子の色 enum Cap { Black, White } abstract sig Children { cap: one Cap, // かぶっている帽子の色 visible: set Children // 見える他の子供 } // A, B, C, D の条件 one sig A extends Children {} { visible = none cap = Black } one sig B extends Children {} { visible = none cap = White } one sig C extends Children {} { visible = B cap = Black } one sig D extends Children {} { visible = B + C cap = White } fact { #cap.Black = 2 and #cap.White = 2 } // c の帽子の色の合計のいずれかが num なら真 pred CountCapNumber (c: Children, num: Int) { #c :> cap.Black = num or #c :> cap.White = num } // 前をみた瞬間に答えられるか pred すぐに回答できる (c: Children) { CountCapNumber [c.visible, 2] } // 他の子の回答(ができないこと)を待って答えられるか pred 少しして回答できる (c: Children) { // すぐに回答する子はいない no a: Children | すぐに回答できる [a] // 答えられない誰かが自分を見ているなら、共通して見える子の帽子の色が // 1=(2-1)なら回答できる some a: Children | c in a.visible and CountCapNumber [c.visible & a.visible, 1] } pred 回答できる { some c: Children | すぐに回答できる [c] or 少しして回答できる [c] } run 回答できる