Skip to content

Instantly share code, notes, and snippets.

What would you like to do?
Alloy tutorial: Static modelling: Einstein's riddle
open util/ordering[House]
enum Color {Red, White, Blue, Green, Yellow}
enum Pet {Birds, Cats, Dogs, Fish, Horses}
enum Cigar {Blend, BlueMaster, Dunhill, PallMall, Prince}
enum Beverage {Beer, Coffee, Milk, Tea, Water}
sig House {
color: disj Color
abstract sig Owner {
house: disj House,
pet: disj Pet,
cigar: disj Cigar,
beverage: disj Beverage
one sig Brit extends Owner {}
one sig Swede extends Owner {}
one sig Dane extends Owner {}
one sig Norwegian extends Owner {}
one sig German extends Owner {}
fact constraints {
one b: Brit | = Red
one s: Swede | = Dogs
// TODO: add more predicates
#House = 5
run {} for 5
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment