Tango with code

A blog about frustration and anger

Red-Black Tree in Alloy II

| Comments

On the previous tutorial, we learnt how to build a consistent tree in Alloy.

On this tutorial, we are finally going to build a Red-Black Tree, respecting all its properties.

If you remember, a Red-Black Tree is also a BST (Binary Search Tree). So we need to make a BST before we can do a RBT.

BST properties are pretty simple:

For each node X:
- Left child data is always smaller than X’s.
- Right child data is always greater than X’s.

And that’s it!

The first thing we need to increment on our previous model is the “data” concept. Data will be representated as an integer number:

RedBlackTree.als
1
2
3
4
sig Node {
  ...
  data : one Int
}

With only that, we already can see a difference in our model:

As you can see, each node is associated with an integer number. In order to ease the visualization, let’s modify our theme to put the “data” relation inside each node.

Click on “theme”:

On “relations”, select “data” (1), turn “Show as arcs” off and “Show as attribute” on (2). After that, click on “Apply” (3).

Much better, right? :))

Now we need only one fact in order to transform our current model in a BST:

RedBlackTree.als
1
2
3
4
5
fact organizeLeftAndRightUsingData {
  all n: Node |
      (all l: n.left.*children | n.data > l.data) and
      (all r: n.right.*children | n.data < r.data)
}

It’s pretty easy to understand what it is doing: For each node (all), its data is greater than all its left children (recursively), and is smaller than all its right children (recursively).

That’s it!

Now let’s do our next step toward a Red-Black Tree. As you know, in a red-black tree, each node has one of those two colors: red or black. We play with those colors in order to make the tree balanced, that is, make left and right children with more or less with the same height. In order to ensure that, there are two properties we must respect:

1) All children of a red node is black.

2) The black height, that is, the number of black nodes from the root node of the three until a leaf, is the same for all the leaves.

By convenction, we always make the root node as black.

Similar to the BST, the first thing we need to add is the “color” concept. Color will be representated as an enum. In Alloy, enumerations have the following syntax:

1
2
3
enum [Name] {
  [ Values ]
}

For our case:

RedBlackTree.als
1
2
3
enum Color {
  RED, BLACK
}

And now we just need to add a relation to our signature “Node”:

RedBlackTree.als
1
2
3
4
sig Node {
  ...
  color: one Color
}

If you try to execute the model, we may get something like this (alike data, I also transformed “color” in an attribute):

As expected, it’s not respecting the red-black tree properties. Let’s fix it, starting by the most trivial fact:

RedBlackTree.als
1
2
3
4
fact rootIsBlack {
  all n: Node |
      no children.n => n.color = BLACK
}

“If a node has no parent, then its color is black!”.

As we defined previously that there was only a node that has no parent, then, by definition, it’s the root.

The second fact we are going to add is going to make all children of a red node black:

RedBlackTree.als
1
2
3
4
5
fact redNodeChildrenAreBlack {
  all n: Node |
      n.color = RED =>
          all c: n.children | c.color = BLACK
}

Also easy to understand!

And finally, let’s fix the black height:

RedBlackTree.als
1
2
3
4
fact blackHeightIsSameToAllPaths {
  all n: Node |
      #(n.left.*children - color.RED)  = #(n.right.*children - color.RED)
}

“#” is an operator in Alloy that returns the number of elements in a set. So, in our fact above, we are saying that, for all nodes, the number of red nodes in the left child is equals to the number of red nodes in the right child. It’s the same thing as to say that the number of black nodes is equal to them both, hence, respecting the black-height property.

If you try to execute the model right now, you will see a very different scenario:

Our red-black tree is alive!

You can see the source code below:

RedBlackTree.als
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
module RedBlackTree

enum Color { BLACK, RED }

sig Node {
  parent: lone Node,
  left: lone Node,
  right: lone Node,
  children: set Node,
  data: one Int,
  color: one Color    
}

pred isRoot[n: Node] {
  no n.parent
}

// facts about nodes 
fact makeChildren {
  all n: Node | n.children = n.left + n.right
}

fact makeParent {
  all n: Node |
      (all c : n.children | c.parent = n)
  all n1, n2 : Node | n1 = n2.parent => n2 in n1.children
}

fact noCycles {
  all n1, n2: Node |
          (n1 in n2.children) => n2 !in n1.*children
}

fact leftAndRightAreDisjoint {
  no left & right
}

fact theresOnlyOneRoot {
  one n: Node | isRoot[n]
}

// facts about data
fact dataIsUnique {
  all n1, n2: Node | n1 != n2 => n1.data != n2.data
}

fact organizeLeftAndRightUsingData {
  all n: Node |
      (all l: n.left.*children | n.data > l.data) and
      (all r: n.right.*children | n.data < r.data)
}

// facts about node colors
fact rootIsBlack {
  all n: Node |
      no children.n => n.color = BLACK
}

fact redNodeChildrenAreBlack {
  all n: Node |
      n.color = RED =>
          all c: n.children | c.color = BLACK
}

fact blackHeightIsSameToAllPaths {
  all n: Node |
      #(n.left.*children - color.RED)  = #(n.right.*children - color.RED)
}

pred show[] {
  #left > 2
  #right > 2
  all d: Node.data | d > 0
}

run show for 10

Comments