// Murder-in-the-family.als
// Marcin Szlenk 2020

// 1. Launch the Alloy Analyzer.
// 2. Select the Open icon and load this file.
// 3. Select the Execute icon to run the 'run' command.
// 4. Select the Show icon to show an instance of the model. Examine the diagram.
// 5. Select the Next icon to ask for another instance.

// Complete the model (only the lines with 'TO DO') and solve the below puzzle
// (from Summers 1968):

// Murder occurred one evening in the home of a married couple
// and their son and daughter. One member of the family murdered
// another member, the third member witnessed the crime, and the
// fourth member was an accessory after the fact.
//
// 1. The accessory and the witness were of opposite sex.
// 2. The oldest member and the witness were of opposite sex.
// 3. The youngest member and the victim were of opposite sex.
// 4. The accessory was older than the victim.
// 5. The father was the oldest member.
// 6. The killer was not the youngest member.
//
// Which one of the four father, mother, son, or daughter was the killer?

// to witness the crime — być świadkiem przestępstwa;
// accessory — współsprawca (pomagający, ale nie uczestniczący w przestępstwie).

abstract sig Sex {}
one sig Woman, Man extends Sex {}

abstract sig Role {}
one sig Killer, Victim, Witness, Accessory extends Role {}

abstract sig Person {
    sex: one Sex,
    role: one Role,
    olderThan: set Person
}

one sig Father, Mother, Son, Daughter extends Person {}

fact {
    //each person plays a different role
    all r: Role | one role.r
    //'olderThan' has no cycles
    no p: Person | p in p.^olderThan
    //'olderThan' is transitive
    all p1, p2, p3: Person |
        p1->p2 in olderThan and p2->p3 in olderThan =>
            p1->p3 in olderThan
}

pred Oldest[p: Person] {
    no olderThan.p
}

pred Youngest[p: Person] {
    no p.olderThan
}

fact WhatWeKnow {
    // The parents are older than their children
    (Father + Mother) -> (Son + Daughter) in olderThan

    // The father and the son are men, while
    // the mother and the daughter are women

    Father.sex = Man // TO DO
    Son.sex = Man
    Daughter.sex = Woman
    Mother.sex = Woman

    // 1. The accessory and the witness were of opposite sex.
    all p1, p2: Person | p1.role = Accessory and p2.role = Witness => p1.sex != p2.sex

    // 2. The oldest member and the witness were of opposite sex.

    all p1: Person | Oldest[p1] => p1.role != Witness
    all disj p1, p2: Person | Oldest[p1] and p2.role = Witness => p1.sex != p2.sex

    // 3. The youngest member and the victim were of opposite sex.

    all p1: Person | Youngest[p1] => p1.role != Victim
    all disj p1, p2: Person | Youngest[p1] and p2.role = Victim => p1.sex != p2.sex

    // 4. The accessory was older than the victim.

    all disj p1, p2: Person | p1.role = Accessory and p2.role = Victim => p2 in p1.olderThan

    // 5. The father was the oldest member.

    Father.olderThan = Mother + Daughter + Son

    // 6. The killer was not the youngest member.

    all p1: Person | p1.role = Killer => not Youngest[p1]

}

run {}