A.3.3 床屋のパラドックス - Model Base

更新日2011-09-03
[ Alloy Analyzer ] / [ 抽象によるソフトウェア設計／付録 A 練習問題 解答例 ]

---

( a ) 解析器を使い、モデルが実際に矛盾していることを示せ

sig Man {shaves: set Man}
one sig Barber extends Man {}
fact {
Barber.shaves = {m: Man | m not in m.shaves}
}
 
run {}for 4 Man

村人4人の世界でインスタンスは発見されなかった。

Executing "Run run$1 for 4 Man"
  Solver=minisat(jni) Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=20
  116 vars. 19 primary vars. 167 clauses. 297ms.
  No instance found. Predicate may be inconsistent. 0ms.

( b ) 村人を男（髭を剃る必要がある者）と女性（必要のない者）に分けた新たなモデルを作成し、今度は簡単な解があることを示せ

abstract sig Person{}
sig Woman extends Person{}
sig Man extends Person{shaves: set Man}
one sig Barber in Person {}
fact {
  Barber.shaves = {m: Man | m not in m.shaves}
  }
 
run {}for 4 Person

女性が床屋になってくれたことで解が現れた。

---

( c ) もっと抜本的な解がEdsger Dijkstraによって示された。それは、床屋がいない可能性を許容するというものだ。これに従って最初のモデルを書き直し、解が得られることを示せ

one sig Barber から one をとる。

sig Man {shaves: set Man}
sig Barber extends Man {}
fact {
  Barber.shaves = {m: Man | m not in m.shaves}
  }
 
run {}for 4 Man

---

( d) 最後に、元のモデルで複数の床屋がいるような変更を試して、やはり解が得られることを示せ

sig Man {shaves: set Man}
sig Barber extends Man {}
fact {
  -- 複数の床屋がいる
  #Barber > 1
  Barber.shaves = {m: Man | m not in m.shaves}
  }
 
run {}for 4 Man

なんだが、法規制の盲点をついた○○のようだ。。。

---