// **************************************************************************
//
//    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;
}