# Feedback / improvements for the 5-houses puzzle model

**URL:** <https://alloytools.discourse.group/t/feedback-improvements-for-the-5-houses-puzzle-model/248>\
**Category:** models\
**Created:** [March 19, 2022, 12:48pm UTC](https://alloytools.discourse.group/t/feedback-improvements-for-the-5-houses-puzzle-model/248 "2022-03-19T12:48:29Z")\
**Posts on this page:** 4\
**Page:** 1

<div class="post-metadata">

**Author:** ![Janiczek](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/janiczek/32/131_2.png) [@Janiczek](https://alloytools.discourse.group/u/Janiczek)\
**Post date:** [March 19, 2022, 12:48pm UTC](https://alloytools.discourse.group/t/feedback-improvements-for-the-5-houses-puzzle-model/248/1 "2022-03-19T12:48:29Z")

</div>

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](https://udel.edu/~os/riddle.html). (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**
>
> ```alloy
> 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:

```auto
h.smoke = Blend implies h.leftNeighbour.pet = Cats or h.rightNeighbour.pet = Cats

```

This seems like it could be shortened to

```auto
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:

```auto
neighbour: some House

```

combined with a fact:

```auto
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**

 ![Screenshot 2022-03-19 at 13.37.58](https://global.discourse-cdn.com/free1/uploads/alloytools/original/1X/bd2a5523c94c0e93b384e15f91b62ee9069223f6.png)

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.

---

<div class="post-metadata">

**Author:** ![Janiczek](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/janiczek/32/131_2.png) [@Janiczek](https://alloytools.discourse.group/u/Janiczek)\
**Post date:** [March 19, 2022, 3:05pm UTC](https://alloytools.discourse.group/t/feedback-improvements-for-the-5-houses-puzzle-model/248/2 "2022-03-19T15:05:18Z")

</div>

Update: by trying to resolve the self-cycle I believe I’ve fixed most other non-symmetric neighbour relationships:

```auto
fact right_neighbours { all h1,h2: House | h1.leftNeighbour = h2 iff h2.rightNeighbour = h1 }

```

(changed from implies to iff)

---

<div class="post-metadata">

**Author:** ![grayswandyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/grayswandyr/32/17_2.png) [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)\
**Post date:** [March 19, 2022, 3:26pm UTC](https://alloytools.discourse.group/t/feedback-improvements-for-the-5-houses-puzzle-model/248/3 "2022-03-19T15:26:40Z")

</div>

Hi  
I think your modeling style is essentially OK, even if there are other possible approaches. In my version of this problem, I had the following differences wrt your model:

First, houses are combined with their color, and similarly for persons with their nationality. I also moved some relations in `Person`.

```auto
abstract sig House { owner : one Person }
one sig Red, White, Green, Yellow, Blue extends House {}
abstract sig Person {
  drink: one Drink,
  smoke: one Smoke,
  pet: one Pet, }
one sig Brit, Swede, Dane, Norwegian, German extends Person {}

```

Second, I specified that all fields are bijections (that is, they are `one` in both directions), e.g.:

```auto
fact {
  owner in House one -> Person
  drink in Person one -> Drink
  ...
}

```

Finally, I imposed a total order on `House` with `open util/ordering[House]`. This automatically adds various `fun`ctions, such as `first`, `prev` and `next` (no need for a left or right neighbor function or field). Also, notice this module imposes an exact bound on house.

Alloy will infer by itself that the cardinality of `House` is 5 because it is abstract and extended by 5 `one sig`s.

Using all this eases the specification of constraints and the addition of a `neighbors` relation, e.g.:

```auto
fun neighbors : House -> House { next + prev }

fact hints {
  owner.Brit = Red
  Swed.pet = Dogs
  Green = White.prev
  ...
}

```

Hope this helps.  
EDIT: rewrote the part on `ordering` and the scope of `House` (it was wrong as stated).

---

<div class="post-metadata">

**Author:** ![peter.kriens](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/peter.kriens/32/3_2.png) [@peter.kriens](https://alloytools.discourse.group/u/peter.kriens)\
**Post date:** [March 21, 2022, 4:27pm UTC](https://alloytools.discourse.group/t/feedback-improvements-for-the-5-houses-puzzle-model/248/4 "2022-03-21T16:27:45Z")

</div>

Did you see [Alloy model of the Einstein puzzle - Stack Overflow](https://stackoverflow.com/questions/47969967/alloy-model-of-the-einstein-puzzle) ?