room.als

enum Person { Alice, Bob, Rafa }

enum Language { English, Ithkuil }

one sig Room {
    people : set Person
}

fun speaks : Person -> Language {
    Alice -> English +
    Alice -> Ithkuil +
    Bob -> English
}

pred canSpeak[p : Person, l : Language] {
    l in speaks[p]
}

assert everybodySpeaksEnglish {
    all p : Room.people | canSpeak[p, English]
}

assert notEverybodySpeaksEnglish {
    some p : Room.people | not canSpeak[p, English]
}

fact { Room.people = Alice + Bob + Rafa }

check everybodySpeaksEnglish
-- Counterexample found. Assertion is invalid.
check notEverybodySpeaksEnglish
-- No counterexample found. Assertion may be valid.