// ************************************************************************** // // eses eses // eses eses // eses eseses esesese eses Embedded Systems Group // ese ese ese ese ese // ese eseseses eseseses ese Department of Computer Science // eses eses ese eses // eses eseses eseseses eses University of Kaiserslautern // eses eses // // ************************************************************************** // // Someone who lives in Dreadsbury Mansion killed aunt Agatha. Agatha, // the butler, and Charles live in Dreadsbury Mansion, and are the // only people who live therein. A killer always hates his victim, and // is never richer than his victim. Charles hates no one that aunt // Agatha hates. Agatha hates everyone except the butler. The butler // hates everyone not richer than aunt Agatha and the butler hates // everyone that Agatha hates. No one hates everyone and Agatha is not // the butler. Who killed aunt Agatha? // // ************************************************************************** module AuntAgatha(bool k_A,k_B,k_C, // killer is either Agatha, the Butler, or Charles r_AA,r_AB,r_AC, // the "richer than" relation r_BA,r_BB,r_BC, r_CA,r_CB,r_CC, h_AA,h_AB,h_AC, // the "hates" relation h_BA,h_BB,h_BC, h_CA,h_CB,h_CC, !facts ) { facts = // ---- the killer is Agatha, the butler, or Charles: (k_A | k_B | k_C) & // ---- a killer always hates the victim: (k_A -> h_AA) & (k_B -> h_BA) & (k_C -> h_CA) & // ---- a killer is never richer than the victim (k_A -> !r_AA) & (k_B -> !r_BA) & (k_C -> !r_CA) & // ---- Charles hates no one that aunt Agatha hates. (h_AA -> !h_CA) & (h_AB -> !h_CB) & (h_AC -> !h_CC) & // ---- Agatha hates everyone except the butler. (h_AA & !h_AB & h_AC) & // ---- The butler hates everyone not richer than aunt Agatha (!r_AA -> h_BA) & (!r_BA -> h_BB) & (!r_CA -> h_BC) & // ---- and the butler hates everyone that Agatha hates. (h_AA -> h_BA) & (h_AB -> h_BB) & (h_AC -> h_BC) & // ---- No one hates everyone: (!h_AA | !h_AB | !h_AC) & (!h_BA | !h_BB | !h_BC) & (!h_CA | !h_CB | !h_CC); } satisfies { hates : assert facts -> h_AA & !h_AB & h_AC & h_BA & !h_BB & h_BC & !h_CA & !h_CC; richer : assert facts -> !r_AA & r_BA; killer : assert facts -> k_A & !k_B & !k_C; }