レイトン教授で始めるAlloy Analyzer入門
8月15日にギークバーで使った資料をアップします。
レイトン教授で始めるAlloy Analyzer入門
資料に出てくる3つの問題のAlloyによるチートコードは次の通りです。さぁ、あなたもAlloyでレイトン教授の攻略を始めよう!
View more presentations from osiire
//No50 enum Cow { A, B, C, D, E } sig Liar in Cow {} { #Liar = 3 } // ソーウ種は3匹 pred whoIsLiar { not A in Liar iff D in Liar not B in Liar iff C in Liar not C in Liar iff not A in Liar not D in Liar iff E in Liar not E in Liar iff B in Liar } run whoIsLiar
// No.039 abstract sig Color {} one sig Red, Blue, White extends Color {} sig Shirt { // シャツ color : disj Color } sig Trousers { // ズボン color : disj Color } sig Person { shirt : disj Shirt, trousers : disj Trousers } one sig A, B, C extends Person {} fact { // 全員上下バラバラの色 all p : Person | not p.shirt.color = p.trousers.color // Cだけは自分の色を着ていない。 not C.shirt.color = White && not C.trousers.color = White Red in A.shirt.color + A.trousers.color Blue in B.shirt.color + B.trousers.color // Cのズボンは赤。 C.trousers.color = Red } pred problem {} run problem
//No.87 abstract sig Number { // 二次元配列。 table : Number -> one Card } one sig N1, N2, N3, N4 extends Number {} enum Card { S, H, C, D } // スペード、ハート、クラブ、ダイヤ fact { // 行と列で4種類並ぶ all row : Number | table[row, Number] = Card all cols : Number | table[Number, cols] = Card // 斜め1 table[N1, N1] + table[N2, N2] + table[N3, N3] + table[N4, N4] = Card // 斜め2 table[N1, N4] + table[N2, N3] + table[N3, N2] + table[N4, N1] = Card // 初期制限 table[N1, N1] = D table[N1, N3] = C table[N3, N1] = H table[N4, N2] = S } pred show() {} run show