Skip to content
Snippets Groups Projects
Commit 86348637 authored by Michael Leuschel's avatar Michael Leuschel
Browse files

add Alloy Einstein puzzle visualisation

parent 65ccb737
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
Einstein/Houses.svg 0 → 100644
+ 82
− 0
View file @ 86348637
<svg xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
xmlns:svg="http://www.w3.org/2000/svg"
xmlns="http://www.w3.org/2000/svg"
width="1024" height="512"
version="1.1" id="svg2">
<g transform="translate(0,122) scale(0.25 0.25)">
<path
style="fill-opacity:1;stroke:#000000;stroke-width:12;stroke-linecap:butt;stroke-linejoin:round;stroke-miterlimit:4;stroke-opacity:1;stroke-dasharray:none"
fill="red"
d="m 16,256 240,-192 96,72 0,-32 48,0 0,72 96,80 -48,0 0,192 -120,0 0,-160 -96,0 0,160 -168,0 0,-192 z"
transform="translate(0,-122)"
id = "house1"
/>
</g>
<g transform="translate(125,122) scale(0.25 0.25)">
<path
style="fill-opacity:1;stroke:#000000;stroke-width:12;stroke-linecap:butt;stroke-linejoin:round;stroke-miterlimit:4;stroke-opacity:1;stroke-dasharray:none"
fill="green"
d="m 16,256 240,-192 96,72 0,-32 48,0 0,72 96,80 -48,0 0,192 -120,0 0,-160 -96,0 0,160 -168,0 0,-192 z"
transform="translate(0,-122)"
id = "house2"
/>
</g>
<g transform="translate(250,122) scale(0.25 0.25)">
<path
style="fill-opacity:1;stroke:#000000;stroke-width:12;stroke-linecap:butt;stroke-linejoin:round;stroke-miterlimit:4;stroke-opacity:1;stroke-dasharray:none"
fill="blue"
d="m 16,256 240,-192 96,72 0,-32 48,0 0,72 96,80 -48,0 0,192 -120,0 0,-160 -96,0 0,160 -168,0 0,-192 z"
transform="translate(0,-122)"
id = "house3"
/>
</g>
<g transform="translate(375,122) scale(0.25 0.25)">
<path
style="fill-opacity:1;stroke:#000000;stroke-width:12;stroke-linecap:butt;stroke-linejoin:round;stroke-miterlimit:4;stroke-opacity:1;stroke-dasharray:none"
fill="white"
d="m 16,256 240,-192 96,72 0,-32 48,0 0,72 96,80 -48,0 0,192 -120,0 0,-160 -96,0 0,160 -168,0 0,-192 z"
transform="translate(0,-122)"
id = "house4"
/>
</g>
<g transform="translate(500,122) scale(0.25 0.25)">
<path
style="fill-opacity:1;stroke:#000000;stroke-width:12;stroke-linecap:butt;stroke-linejoin:round;stroke-miterlimit:4;stroke-opacity:1;stroke-dasharray:none"
fill="orange"
d="m 16,256 240,-192 96,72 0,-32 48,0 0,72 96,80 -48,0 0,192 -120,0 0,-160 -96,0 0,160 -168,0 0,-192 z"
transform="translate(0,-122)"
id = "house5"
/>
</g>
<text x="0" y="60" font-size ="12" font-family="sans-serif">
<tspan x="52" dy = "0.0em" id="nationality1">nationality</tspan>
<tspan x="175" dy = "0.0em" id="nationality2">nationality</tspan>
<tspan x="300" dy = "0.0em" id="nationality3">nationality</tspan>
<tspan x="425" dy = "0.0em" id="nationality4">nationality</tspan>
<tspan x="550" dy = "0.0em" id="nationality5">nationality</tspan>
</text>
<text x="0" y="230" font-size ="12" font-family="sans-serif">
<tspan x="52" dy = "0.0em" id="pet1">Pet</tspan>
<tspan x="175" dy = "0.0em" id="pet2">Pet</tspan>
<tspan x="300" dy = "0.0em" id="pet3">Pet</tspan>
<tspan x="425" dy = "0.0em" id="pet4">Pet</tspan>
<tspan x="550" dy = "0.0em" id="pet5">Pet</tspan>
</text>
<text x="0" y="250" font-size ="12" font-family="sans-serif">
<tspan x="52" dy = "0.0em" id="cigarette1">cigarette</tspan>
<tspan x="175" dy = "0.0em" id="cigarette2">cigarette</tspan>
<tspan x="300" dy = "0.0em" id="cigarette3">cigarette</tspan>
<tspan x="425" dy = "0.0em" id="cigarette4">cigarette</tspan>
<tspan x="550" dy = "0.0em" id="cigarette5">cigarette</tspan>
</text>
<text x="0" y="270" font-size ="12" font-family="sans-serif">
<tspan x="52" dy = "0.0em" id="drink1">drink</tspan>
<tspan x="175" dy = "0.0em" id="drink2">drink</tspan>
<tspan x="300" dy = "0.0em" id="drink3">drink</tspan>
<tspan x="425" dy = "0.0em" id="drink4">drink</tspan>
<tspan x="550" dy = "0.0em" id="drink5">drink</tspan>
</text>
</svg>
\ No newline at end of file
Einstein/einstein_puzzle_als.json 0 → 100644
+ 18
− 0
View file @ 86348637
{
"svg": "Houses.svg",
"items": [
{
"for": {"from":1, "to":5},
"id": "house%0",
"attr": "fill",
"value" :"color_House(%0-1)"
},
{
"for": {"from":1, "to":5},
"repeat": ["pet","nationality","cigarette","drink"],
"id": "%1%0",
"attr": "text",
"value" :"%1_House(%0-1)"
}
]
}
\ No newline at end of file
Einstein/einsteins_puzzle.als 0 → 100644
+ 76
− 0
View file @ 86348637
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 constraints {
// There are five houses, each of a different color.
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
// In each house lives a man of a different nationality.
no disj h,h': House | h.nationality = h'.nationality
// 1. The Englishman lives in the red house.
some h: House | (h.nationality = Englishman) and (h.color = red)
// 2. The Swede keeps dogs.
some h: House | (h.nationality = Swede) and (h.pet = dog)
// 3. The Dane drinks tea.
some h: House | (h.nationality = Dane) and (h.drink = tea)
// 4. The green house is just to the left of the white one.
some disj h, h': House | (h.color = green) and (h'.color = white) and (h'.prev = h)
// 5. The owner of the green house drinks coffee.
some h: House | (h.color = green) and (h.drink = coffee)
// 6. The Pall Mall smoker keeps birds.
some h: House | (h.cigarette = Pall_Mall) and (h.pet = bird)
// 7. The owner of the yellow house smokes Dunhills.
some h: House | (h.color = yellow) and (h.cigarette = Dunhills)
// 8. The man in the center house drinks milk.
some h: House | (some h.prev.prev) and (some h.next.next) and (h.drink = milk)
// 9. The Norwegian lives in the first house.
some h: House | (h = first) and (h.nationality = Norwegian)
// 10. The Blend smoker has a neighbor who keeps cats.
some disj h,h': House | (h.cigarette = Blend) and (h'.pet = cat) and ((h.prev = h') or (h.next = h'))
// 11. The man who smokes Blue Masters drinks beer.
some h: House | (h.cigarette = Blue_Masters) and (h.drink = beer)
// 12. The man who keeps horses lives next to the Dunhill smoker.
some disj h,h': House | (h.pet = horse) and (h'.cigarette = Dunhills) and ((h.next = h') or (h.prev = h'))
// 13. The German smokes Prince.
some h: House | (h.nationality = German) and (h.cigarette = Prince)
// 14. The Norwegian lives next to the blue house.
some disjoint h,h': House | (h.nationality = Norwegian) and (h'.color= blue) and (h.next = h')
// 15. The Blend smoker has a neighbor who drinks water.
some disj h,h': House | (h.cigarette = Blend) and (h'.drink = water) and ((h.next = h') or (h.prev = h'))
}
run {} for 5
\ No newline at end of file
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment