Instantly share code, notes, and snippets.

# note/EinsteinsRiddle.als

Created May 21, 2020 19:13
Show Gist options
• Save note/6198d7d3e01fd8220cd683b1f4320d5d to your computer and use it in GitHub Desktop.
Alloy tutorial: Static modelling: Einstein's riddle
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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 commented Feb 28, 2023

Hi, i am a student from Montevideo, Uruguay, i want to know who to build a BinaryTree in Alloy, is this possible?

### mehmetakifakkus commented Oct 21, 2023

@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