On the previous tutorial, we learnt how to build a consistent tree in Alloy.
On this tutorial, we are finally going to build a RedBlack Tree, respecting all its properties.
If you remember, a RedBlack 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:
1 2 3 4 

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:
1 2 3 4 5 

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 RedBlack Tree. As you know, in a redblack 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 

For our case:
1 2 3 

And now we just need to add a relation to our signature “Node”:
1 2 3 4 

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 redblack tree properties. Let’s fix it, starting by the most trivial fact:
1 2 3 4 

“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:
1 2 3 4 5 

Also easy to understand!
And finally, let’s fix the black height:
1 2 3 4 

“#” 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 blackheight property.
If you try to execute the model right now, you will see a very different scenario:
Our redblack tree is alive!
You can see the source code below:
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 
