うそつき牛（レイトン教授） - TLA+メモ@ウィキ

うそつき牛 (レイトン教授)

問題概要

5頭の牛A,B,C,D,Eがいる。2頭はトンホー種（本当のことしか言わない）、3頭はソーウ種（ウソしか言わない）である。
次の会話がなされている場合、ソーウ種はどれか。

• A「Dはソーウ種だ」
• B「Cはトンホー種ではない」
• C「Aはソーウ種ではない」
• D「Eはソーウ種だ」
• E「Bはトンホー種ではない」

モデル

------------------------------- MODULE layton -------------------------------
EXTENDS Naturals, Sequences, FiniteSets, TLC
 
(*-- Constant Declaration --*)
(* 牛の種類は、トンホー種かソーウ種のどちらかである *)
CONSTANT Tonho, Sou
 
(*-- Definition --*)
(* タプルの要素のうち特定の値のものをカウントする *)
Count(t,n) == LET S == {i \in DOMAIN t : t[i] = n} IN Cardinality(S)
 
 
 
(*--algorithm layton {
 (* グローバル変数宣言 *)
    variables type = [i \in 1..5 |-> Tonho],    (* 各牛の種類 *)
    pattern \in [1..5 -> {Tonho,Sou}];    (* 全パターン *)
 
 (* define(演算子)定義 *)
 define
 {
 (* 牛の種類に関する制約 *)
CowSpec == 
    /\ (type[1] = Tonho) <=> (type[4] = Sou)    (* Aがトンホー種の場合、Dはソーウ種である *)
    /\ (type[2] = Tonho) <=> (type[3] /= Tonho) (* Bがトンホー種の場合、Cはトンホー種でない *)
    /\ (type[3] = Tonho) <=> (type[1] /= Sou)  (* Cがトンホー種の場合、Aはソーウ種でない *)
    /\ (type[4] = Tonho) <=> (type[5] = Sou)   (* Dがトンホー種の場合、Eはソーウ種である *)
    /\ (type[5] = Tonho) <=> (type[2] /= Tonho)(* Eがトンホー種の場合、Bはトンホー種でない *)
    /\ Count(type, Tonho) = 2 (* トンホー種は2頭 *)
};
 
 (* アルゴリズム本体、もしくはプロセス宣言 *)
 {
    type := pattern;
 }
}*)
\* BEGIN TRANSLATION
VARIABLES type, pattern, pc
 
(* define statement *)
CowSpec ==
    /\ (type[1] = Tonho) <=> (type[4] = Sou)
    /\ (type[2] = Tonho) <=> (type[3] /= Tonho)
    /\ (type[3] = Tonho) <=> (type[1] /= Sou)
    /\ (type[4] = Tonho) <=> (type[5] = Sou)
    /\ (type[5] = Tonho) <=> (type[2] /= Tonho)
    /\ Count(type, Tonho) = 2
 
 
vars == << type, pattern, pc >>
 
Init == (* Global variables *)
        /\ type = [i \in 1..5 |-> Tonho]
        /\ pattern \in [1..5 -> {Tonho,Sou}]
        /\ pc = "Lbl_1"
 
Lbl_1 == /\ pc = "Lbl_1"
         /\ type' = pattern
         /\ pc' = "Done"
         /\ UNCHANGED pattern
 
(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == pc = "Done" /\ UNCHANGED vars
 
Next == Lbl_1
           \/ Terminating
 
Spec == Init /\ [][Next]_vars
 
Termination == <>(pc = "Done")
 
\* END TRANSLATION 
(*-- Model Checking --*)
 
=============================================================================
 

解説

以下の記事を参考にした。

Alloyでパズル (1) ウソつき問題

検証する際には不変条件に「~CowSpec」(CowSpecの否定)を指定する。CowSpecがTrueとなると反例として結果が表示される。

ポイント1

変数を定義する際に\inで定義すると集合内の値を順番に変数に設定して検証する。
ここでは関数の集合"[1..5 -> {Tonho,Sou}]"で牛の全組み合わせを生成している。

pattern \in [1..5 -> {Tonho,Sou}]; (* 全パターン *)

問題の解答

• 【A】と【C】と【E】