レイトン教授で始める Alloy Analyzer入門

8月15日にギークバーで使った資料をアップします。

レイトン教授で始めるAlloy Analyzer入門

View more presentations from osiire

資料に出てくる３つの問題のAlloyによるチートコードは次の通りです。さぁ、あなたもAlloyでレイトン教授の攻略を始めよう！

//No50
enum Cow { A, B, C, D, E }
sig Liar in Cow {} { #Liar = 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