Alloy tutorial: Static modelling: Einstein's riddle

EinsteinsRiddle.als

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 | b.house.color = Red
        one s: Swede | s.pet = Dogs
        // TODO: add more predicates

        #House = 5
}

run {} for 5

// https://udel.edu/~os/riddle.html

@GonzaloBelvisi Here is an example of binary tree:

abstract sig Node {}
sig Empty extends Node {}
sig Data extends Node {
    num: Int,
    left: Node, 
    right: Node -- note: if this was Data, our tree would ever end!
}

pred btree {
    -- root reaches everything
    some r: Node | 
        -- what's wrong with the line below? It doesn't include r
        -- Node in r.^(left + right)
        Node in r.^(left + right) + r
        
    all n: Node | {
        -- no cycles
        n not in n.^(left + right)
        
        -- at most one parent for each node
        -- not one, because that would disallow the root
        lone n.~(left + right) 
        
        -- distinct children if any
        -- one approach: this enforces that there be multiple Emptys, we're
        -- not going to use it to let us change our approach to leaf nodes
        -- n.left != n.right
        
        -- instead
        no n.left & n.right
    }
}

run btree for 8

This BT can create instances like this: