Alloy 爱因斯坦谜题模型
Alloy model of the Einstein puzzle
[更新] 感谢@Daniel Jackson 和@Peter Kriens 的出色见解，我修复了我的 Alloy 模型。现在 Alloy 分析器生成一个实例。我写下了这个问题并展示了解决方案。我为 5 个房子中的每一个显示颜色、国籍、饮料、香烟和宠物。对了，养鱼的是德国人。 Here 是我写的。
我创建了一个 Alloy 爱因斯坦谜题模型。见下文。当我 运行 我的模型时， Alloy 分析器发现了几个实例。我以为只有一个实例（一个解决方案）。这让我想知道我的模型是否正确。你看到我的模型有问题吗？爱因斯坦难题应该只有一种解法吗？
这是爱因斯坦谜题：
同一条路上有五栋相邻的不同颜色的房子。每个房子里住着一个不同国籍的人。每个人都有他最喜欢的饮料，他最喜欢的 b运行d 香烟，并养着特定种类的宠物。以下是限制条件：
1. The Englishman lives in the red house.
2. The Swede keeps dogs.
3. The Dane drinks tea.
4. The green house is just to the left of the white one.
5. The owner of the green house drinks coffee.
6. The Pall Mall smoker keeps birds.
7. The owner of the yellow house smokes Dunhills.
8. The man in the center house drinks milk.
9. The Norwegian lives in the first house.
10. The Blend smoker has a neighbor who keeps cats.
11. The man who smokes Blue Masters drinks beer.
12. The man who keeps horses lives next to the Dunhill smoker.
13. The German smokes Prince.
14. The Norwegian lives next to the blue house.
15. The Blend smoker has a neighbor who drinks water.
要回答的问题是：谁养鱼？
这是我的 Alloy 模型：
open util/ordering[House]
sig House {
color: Color,
nationality: Nationality,
drink: Drink,
cigarette: Cigarette,
pet: Pet
}
abstract sig Color {}
one sig red extends Color {}
one sig green extends Color {}
one sig yellow extends Color {}
one sig blue extends Color {}
one sig white extends Color {}
abstract sig Nationality {}
one sig Englishman extends Nationality {}
one sig Swede extends Nationality {}
one sig Dane extends Nationality {}
one sig German extends Nationality {}
one sig Norwegian extends Nationality {}
abstract sig Drink {}
one sig tea extends Drink {}
one sig coffee extends Drink {}
one sig milk extends Drink {}
one sig beer extends Drink {}
one sig water extends Drink {}
abstract sig Cigarette {}
one sig Pall_Mall extends Cigarette {}
one sig Dunhills extends Cigarette {}
one sig Blend extends Cigarette {}
one sig Blue_Masters extends Cigarette {}
one sig Prince extends Cigarette {}
abstract sig Pet {}
one sig dog extends Pet {}
one sig bird extends Pet {}
one sig horse extends Pet {}
one sig cat extends Pet {}
one sig fish extends Pet {}
fact {
some disj h1, h2, h3, h4, h5: House | h1.color = red and h2.color = green and h3.color = yellow and h4.color = blue and h5.color = white
no disj h,h': House | h.nationality = h'.nationality
some h: House | (h.nationality = Englishman) and (h.color = red)
some h: House | (h.nationality = Swede) and (h.pet = dog)
some disj h, h': House | (h.color = green) and (h'.color = white) and (h'.prev = h)
some h: House | (h.color = green) and (h.drink = coffee)
some h: House | (h.cigarette = Pall_Mall) and (h.pet = bird)
some h: House | (h.color = yellow) and (h.cigarette = Dunhills)
some h: House | (some h.prev.prev) and (some h.next.next) and (h.drink = milk)
some h: House | (h = first) and (h.nationality = Norwegian)
some h: House | (h.cigarette = Blue_Masters) and (h.drink = beer)
some disj h,h': House | (h.pet = horse) and (h'.cigarette = Dunhills) and ((h.next = h') or (h.prev = h'))
some h: House | (h.nationality = German) and (h.cigarette = Prince)
some disj h,h': House | (h.nationality = Norwegian) and (h'.color= blue) and (h.next = h')
some disj h,h': House | (h.cigarette = Blend) and (h'.drink = water) and (h.next = h')
}
pred Who_keeps_fish {
some h: House | h.pet = fish
}
run Who_keeps_fish for 5
puzzle 应该有唯一解。
不过，由于不完全对称性破缺，我不会对发现多个实例感到惊讶。更令人惊讶的是（并向我暗示你的模型有问题）是生成的第一个实例同时有挪威人和德国人养鱼。看起来好像你需要添加房屋的居住者饲养不同宠物的约束（即宠物关系是单射的）。
我认为您的代码文本与原始定义的偏差太大。根据我的经验，当您必须遵循现有规范时，在 Alloy 中尽可能按文字表达文本至关重要。 IE。你拟合模型，使词汇匹配原始规范（拼图）。
在这种情况下，房子似乎是推理的中心点。所以我创建了一个拥有不同属性的 House atom。我命名了这些字段，以便它们与描述中的单词相匹配。然后我使用 ~ 来获得正确的词序。 IE。 'the Englishman lives' 变为 'Englishman.~lives' 或 'lives.Englishman'。我发现此策略对于使用 Alloy（或任何正式语言）非常重要。验证的责任应该在底层模型上，而不是在我试图解释数学符号的大脑上。我认为这与创建 DSL 的方法类似。
然后我得到了一个具有以下模型的解决方案：
open util/ordering[House]
enum Color { red, green, yellow, blue, white}
enum Nationality { Englishman, Swede, Dane, German, Norwegian}
enum Drink { tea, coffee, milk, beer, water}
enum Cigarette {Pall_Mall, Dunhills, Blend, Blue_Masters, Prince}
enum Pet { dogs, birds, horses, cats, fish }
sig House {
colored : disj Color,
lives : disj Nationality,
drinks : disj Drink,
smoker : disj Cigarette,
keeps : disj Pet
}
pred House.hasNeighbourWho[ other : House ] {
other in this.(prev+next)
}
let centerHouse = first.next.next
fact {
// 1. The Englishman lives in the red house.
Englishman.~lives in colored.red
// 2. The Swede keeps dogs.
Swede.~lives in keeps.dogs
// 3. The Dane drinks tea.
Dane.~lives in drinks.tea
// 4. The green house is just to the left of the white one.
green.~colored = colored.white.prev
// 5. The owner of the green house drinks coffee.
green.~colored = drinks.coffee
// 6. The Pall Mall smoker keeps birds.
Pall_Mall.~smoker = keeps.birds
// 7. The owner of the yellow house smokes Dunhills.
yellow.~colored = smoker.Dunhills
// 8. The man in the center house drinks milk.
centerHouse = drinks.milk
// 9. The Norwegian lives in the first house.
Norwegian.~lives = first
// 10. The Blend smoker has a neighbor who keeps cats.
Blend.~smoker.hasNeighbourWho[ keeps.cats ]
// 11. The man who smokes Blue Masters drinks beer.
Blue_Masters.~smoker = drinks.beer
// 12. The man who keeps horses lives next to the Dunhill smoker.
keeps.horses.hasNeighbourWho[smoker.Dunhills]
// 13. The German smokes Prince.
German.~lives = smoker.Prince
// 14. The Norwegian lives next to the blue house.
Norwegian.~lives.hasNeighbourWho[colored.blue]
// 15. The Blend smoker has a neighbor who drinks water.
Blend.~smoker.hasNeighbourWho[drinks.water]
}
pred solution[ p : House ] {
p = keeps.fish
}
run solution for 5 but exactly 5 House
已更新 删除元数据并使用 disj 代替
原来的解决方案似乎忽略了没有主人拥有相同的宠物、香烟和饮料的限制。
no disj h,h': House | h.pet = h'.pet // otherwise there are solutions with green and white house having both dog as pet
no disj h,h': House | h.cigarette = h'.cigarette // not really required
no disj h,h': House | h.drink = h'.drink // not really required
如上所述，如果没有这些，您将获得非法解决方案。
Here is a rendering constructed with ProB showing an illegal solution
更正后，您get this solution with ProB (using Alloy2B and VisB：
（如果您对可视化感兴趣，请参阅 here）
[更新] 感谢@Daniel Jackson 和@Peter Kriens 的出色见解，我修复了我的 Alloy 模型。现在 Alloy 分析器生成一个实例。我写下了这个问题并展示了解决方案。我为 5 个房子中的每一个显示颜色、国籍、饮料、香烟和宠物。对了，养鱼的是德国人。 Here 是我写的。
我创建了一个 Alloy 爱因斯坦谜题模型。见下文。当我 运行 我的模型时， Alloy 分析器发现了几个实例。我以为只有一个实例（一个解决方案）。这让我想知道我的模型是否正确。你看到我的模型有问题吗？爱因斯坦难题应该只有一种解法吗？
这是爱因斯坦谜题：
同一条路上有五栋相邻的不同颜色的房子。每个房子里住着一个不同国籍的人。每个人都有他最喜欢的饮料，他最喜欢的 b运行d 香烟，并养着特定种类的宠物。以下是限制条件：
1. The Englishman lives in the red house.
2. The Swede keeps dogs.
3. The Dane drinks tea.
4. The green house is just to the left of the white one.
5. The owner of the green house drinks coffee.
6. The Pall Mall smoker keeps birds.
7. The owner of the yellow house smokes Dunhills.
8. The man in the center house drinks milk.
9. The Norwegian lives in the first house.
10. The Blend smoker has a neighbor who keeps cats.
11. The man who smokes Blue Masters drinks beer.
12. The man who keeps horses lives next to the Dunhill smoker.
13. The German smokes Prince.
14. The Norwegian lives next to the blue house.
15. The Blend smoker has a neighbor who drinks water.
要回答的问题是：谁养鱼？
这是我的 Alloy 模型：
open util/ordering[House]
sig House {
color: Color,
nationality: Nationality,
drink: Drink,
cigarette: Cigarette,
pet: Pet
}
abstract sig Color {}
one sig red extends Color {}
one sig green extends Color {}
one sig yellow extends Color {}
one sig blue extends Color {}
one sig white extends Color {}
abstract sig Nationality {}
one sig Englishman extends Nationality {}
one sig Swede extends Nationality {}
one sig Dane extends Nationality {}
one sig German extends Nationality {}
one sig Norwegian extends Nationality {}
abstract sig Drink {}
one sig tea extends Drink {}
one sig coffee extends Drink {}
one sig milk extends Drink {}
one sig beer extends Drink {}
one sig water extends Drink {}
abstract sig Cigarette {}
one sig Pall_Mall extends Cigarette {}
one sig Dunhills extends Cigarette {}
one sig Blend extends Cigarette {}
one sig Blue_Masters extends Cigarette {}
one sig Prince extends Cigarette {}
abstract sig Pet {}
one sig dog extends Pet {}
one sig bird extends Pet {}
one sig horse extends Pet {}
one sig cat extends Pet {}
one sig fish extends Pet {}
fact {
some disj h1, h2, h3, h4, h5: House | h1.color = red and h2.color = green and h3.color = yellow and h4.color = blue and h5.color = white
no disj h,h': House | h.nationality = h'.nationality
some h: House | (h.nationality = Englishman) and (h.color = red)
some h: House | (h.nationality = Swede) and (h.pet = dog)
some disj h, h': House | (h.color = green) and (h'.color = white) and (h'.prev = h)
some h: House | (h.color = green) and (h.drink = coffee)
some h: House | (h.cigarette = Pall_Mall) and (h.pet = bird)
some h: House | (h.color = yellow) and (h.cigarette = Dunhills)
some h: House | (some h.prev.prev) and (some h.next.next) and (h.drink = milk)
some h: House | (h = first) and (h.nationality = Norwegian)
some h: House | (h.cigarette = Blue_Masters) and (h.drink = beer)
some disj h,h': House | (h.pet = horse) and (h'.cigarette = Dunhills) and ((h.next = h') or (h.prev = h'))
some h: House | (h.nationality = German) and (h.cigarette = Prince)
some disj h,h': House | (h.nationality = Norwegian) and (h'.color= blue) and (h.next = h')
some disj h,h': House | (h.cigarette = Blend) and (h'.drink = water) and (h.next = h')
}
pred Who_keeps_fish {
some h: House | h.pet = fish
}
run Who_keeps_fish for 5
puzzle 应该有唯一解。 不过，由于不完全对称性破缺，我不会对发现多个实例感到惊讶。更令人惊讶的是（并向我暗示你的模型有问题）是生成的第一个实例同时有挪威人和德国人养鱼。看起来好像你需要添加房屋的居住者饲养不同宠物的约束（即宠物关系是单射的）。
我认为您的代码文本与原始定义的偏差太大。根据我的经验，当您必须遵循现有规范时，在 Alloy 中尽可能按文字表达文本至关重要。 IE。你拟合模型，使词汇匹配原始规范（拼图）。
在这种情况下，房子似乎是推理的中心点。所以我创建了一个拥有不同属性的 House atom。我命名了这些字段，以便它们与描述中的单词相匹配。然后我使用 ~ 来获得正确的词序。 IE。 'the Englishman lives' 变为 'Englishman.~lives' 或 'lives.Englishman'。我发现此策略对于使用 Alloy（或任何正式语言）非常重要。验证的责任应该在底层模型上，而不是在我试图解释数学符号的大脑上。我认为这与创建 DSL 的方法类似。
然后我得到了一个具有以下模型的解决方案：
open util/ordering[House]
enum Color { red, green, yellow, blue, white}
enum Nationality { Englishman, Swede, Dane, German, Norwegian}
enum Drink { tea, coffee, milk, beer, water}
enum Cigarette {Pall_Mall, Dunhills, Blend, Blue_Masters, Prince}
enum Pet { dogs, birds, horses, cats, fish }
sig House {
colored : disj Color,
lives : disj Nationality,
drinks : disj Drink,
smoker : disj Cigarette,
keeps : disj Pet
}
pred House.hasNeighbourWho[ other : House ] {
other in this.(prev+next)
}
let centerHouse = first.next.next
fact {
// 1. The Englishman lives in the red house.
Englishman.~lives in colored.red
// 2. The Swede keeps dogs.
Swede.~lives in keeps.dogs
// 3. The Dane drinks tea.
Dane.~lives in drinks.tea
// 4. The green house is just to the left of the white one.
green.~colored = colored.white.prev
// 5. The owner of the green house drinks coffee.
green.~colored = drinks.coffee
// 6. The Pall Mall smoker keeps birds.
Pall_Mall.~smoker = keeps.birds
// 7. The owner of the yellow house smokes Dunhills.
yellow.~colored = smoker.Dunhills
// 8. The man in the center house drinks milk.
centerHouse = drinks.milk
// 9. The Norwegian lives in the first house.
Norwegian.~lives = first
// 10. The Blend smoker has a neighbor who keeps cats.
Blend.~smoker.hasNeighbourWho[ keeps.cats ]
// 11. The man who smokes Blue Masters drinks beer.
Blue_Masters.~smoker = drinks.beer
// 12. The man who keeps horses lives next to the Dunhill smoker.
keeps.horses.hasNeighbourWho[smoker.Dunhills]
// 13. The German smokes Prince.
German.~lives = smoker.Prince
// 14. The Norwegian lives next to the blue house.
Norwegian.~lives.hasNeighbourWho[colored.blue]
// 15. The Blend smoker has a neighbor who drinks water.
Blend.~smoker.hasNeighbourWho[drinks.water]
}
pred solution[ p : House ] {
p = keeps.fish
}
run solution for 5 but exactly 5 House
已更新 删除元数据并使用 disj 代替
原来的解决方案似乎忽略了没有主人拥有相同的宠物、香烟和饮料的限制。
no disj h,h': House | h.pet = h'.pet // otherwise there are solutions with green and white house having both dog as pet
no disj h,h': House | h.cigarette = h'.cigarette // not really required
no disj h,h': House | h.drink = h'.drink // not really required
如上所述，如果没有这些，您将获得非法解决方案。 Here is a rendering constructed with ProB showing an illegal solution
更正后，您get this solution with ProB (using Alloy2B and VisB： （如果您对可视化感兴趣，请参阅 here）