Hello! (First of all, I’m unsure if this forum is a good place to ask for suggestions. Please redirect me somewhere if not 
)
I’m trying out Alloy 6, and as one of my first models I’ve been solving the Five houses puzzle. (I plan to try some of the temporal logic stuff next, and then go try it on some Actual Work Stuff 
.)
Here is my model:
Model
sig House {
position: one Position,
color: one Color,
person: one Person,
drink: one Drink,
smoke: one Smoke,
pet: one Pet,
leftNeighbour: lone House,
rightNeighbour: lone House,
}
enum Color { Red, White, Green, Yellow, Blue }
enum Position { First, Second, Third, Fourth, Fifth }
enum Person { Brit, Swede, Dane, Norwegian, German }
enum Drink { Tea, Coffee, Milk, Beer, Water }
enum Smoke { PallMall, Dunhill, BlueMaster, Prince, Blend }
enum Pet { Dogs, Birds, Cats, Horses, Fish }
fact house_count { #House = 5 }
fact left_neighbours {
all h1,h2: House |
(h1.position = First and h2.position = Second or
h1.position = Second and h2.position = Third or
h1.position = Third and h2.position = Fourth or
h1.position = Fourth and h2.position = Fifth)
iff h2.leftNeighbour = h1
}
fact right_neighbours { all h1,h2: House | h1.leftNeighbour = h2 implies h2.rightNeighbour = h1 }
fact all_distinct {
all disj h1,h2: House |
h1.position != h2.position and
h1.color != h2.color and
h1.person != h2.person and
h1.drink != h2.drink and
h1.smoke != h2.smoke and
h1.pet != h2.pet
}
fact hints {
all h: House |
(h.person = Brit implies h.color = Red) and
(h.person = Swede implies h.pet = Dogs) and
(h.person = Dane implies h.drink = Tea) and
(h.color = Green implies h.leftNeighbour.color = White) and
(h.color = Green implies h.drink = Coffee) and
(h.smoke = PallMall implies h.pet = Birds) and
(h.color = Yellow implies h.smoke = Dunhill) and
(h.position = Third implies h.drink = Milk) and
(h.person = Norwegian implies h.position = First) and
(h.smoke = Blend implies h.leftNeighbour.pet = Cats or h.rightNeighbour.pet = Cats) and
(h.pet = Horses implies h.leftNeighbour.smoke = Dunhill or h.rightNeighbour.smoke = Dunhill) and
(h.smoke = BlueMaster implies h.drink = Beer) and
(h.person = German implies h.smoke = Prince) and
(h.person = Norwegian implies h.leftNeighbour.color = Blue or h.rightNeighbour.color = Blue) and
(h.smoke = Blend implies h.leftNeighbour.drink = Water or h.rightNeighbour.drink = Water)
}
run {} for 5
It is working already! (In the sense that one of the valid instances is a solution to the puzzle.) But things could be improved.
Could you give me some feedback on better ways to represent aspects of the solution?
Things I’ve been struggling with
(sorry for imprecise descriptions of what went wrong - I mostly just remember “hm, that didn’t help”)
1. More succintly represent neighbours and facts about "exactly of the two neighbours is …"
Currently in the hints fact I need to do things like:
h.smoke = Blend implies h.leftNeighbour.pet = Cats or h.rightNeighbour.pet = Cats
This seems like it could be shortened to
h.smoke = Blend implies h.(leftNeighbour + rightNeighbour).pet = Cats
but that didn’t seem to help.
I’ve also tried to add a property to House:
neighbour: some House
combined with a fact:
neighbour = leftNeighbour + rightNeighbour
but this seemed to make things worse.
I’ve also tried to express it differently (it is neighbour if it is left neighbour or it is right neighbour) but didn’t succeed there either.
(I can try to give concrete Alloy code if needed, I don’t have those iterations saved anymore)
2. Somehow the rules about neighbours allow for loops / multiple left neighbours / being my own neighbour
I’d have thought the rules left_neighbours and right_neighbours disallow this but apparently not. Any ideas on what I’m missing?
3. Somehow using relation arrows for First->Second->Third->Fourth->Fifth?
The rule left_neighbours seems quite wordy. Is there a way to express this order easier? I haven’t checked ordering module yet, I just know that it exists…
These are things I know about, but I’ll be glad if you point out more things to improve or aspects where you see my mental model about Alloy is wrong.