Everyone who once worked as an analyst knows that one of the most ambiguous, errorprone part of building a software is the requisite engineering. It’s a hell of a task to know what the client wants and how to build a system that meets his expectations.
Bugs in the software specification are hundred, thousand times more expensive than bugs on internal logic, because in order to fix it you frequently need to change the behavior of your software, demanding a complete rethinking on your software architecture.
Alloy Analyzer is a tool for building models. Its very purpose is to find a specific instance of your model that contradicts your expectations about it. Because a model can have thousand or even infinite instances, it’s restricted to a certain scope. A model can be thought as a highhighlevel abstraction of your software. It may not find a bug of implementation, but it can spots illegal states that your software can assume, hence helping to find bugs in specification level.
On today tutorial, we are going to learn how to specify a redblack tree in Alloy.
The very first thing you need to know about Alloy is Signature. Signature is an abstraction of a realworld entity. Signature also can be thought as a set of relations. Making a parallel, signatures are equivalent to classes in objectoriented programming.
Signatures are declared as the following:
1 2 3 

For our redblack tree, we are just going to need one signature: Node. A node of the tree.
1 2 3 

In the same way that our classes in OOP need attributes, so need our signatures. With the difference that here attributes are called relations. Relations have a name, cardinality and set of other signatures we want to relate to. They are declared as the following:
1 2 3 

Example:
1 2 3 

A relation name must be unique inside a signature. The most common types of cardinality is one
(one instance of signature A is related to one and only one instance of signature B), lone
(one instance of signature A is related to zero or one instance of signature B), set
(one instance of signature A is related to zero or more instances of signature B) and some
(one instance of signature A is related to one or more instances of signature B), where A is the signature that contains that relation and B are the signatures refferenced by the relation.
For our redblack tree, the signature node must contain as least four relations:
1 2 3 4 5 6 

 parent: The parent node. It’s lone because the root node doesn’t have any parent.
 left: The left child node. It’s lone because a node may not have a left child.
 right: The right child node. It’s lone because a node may not have a right child.
 children: The set of children node. It may seem redundant, but it will help us to constrain our model later on.
Now let’s start validating our model! There are two ways to check models in Alloy: Automatic and manual checks. Although automatic checks are more useful for our purposes, manual checks are good enough in the building phase of our model because we can see “what’s going on”.
For manual checks, first add one predicate to our model (more about predicates later on):
1 2 3 4 5 

The statement “run” run a predicate for a certain scope (we need a scope because there may be infinite instances of our model). Now you just need to execute it:
A message will appear in the rightside of the screen indicating if any instance was found (on manual check, unlike automatic check, it’s bad when none instance is found, because it means that there wasn’t any instance for that scope that attended to your models contraints, meaning there is some logical contradiction).
Now you just need to click on “Instance” to start visualizing the existing instances for your current model.
Here, a instance is representated like a directed graph, what’s very useful for us, because the graph representation is the tree itself. :))
And oops… We already found a bug (many, actually). First: A node is being parent of itself (what’s not allowed in trees, because trees don’t allow cycles), and a node is being at the same time parent and left child of another node (what’s not allowed, again, because the noncycle constraint).
As you can see, the sole reason of those bugs is because we are allowing our tree to make cycles. We need to add some constraint to forbid it. But how? With facts!
Facts are constraints that must be valid all the time. They are declared as the following:
1 2 3 

The very first fact we are going to add is that the set of children is the union of right and left child. We need that before going on with the next facts.
1 2 3 

Wow, slow down, slow down!
First, “all” has the same semantic of the universal quantifier. It means that something must be valid for all elements of a set. In this case, we are using as set “Node”, meaning all instances of the signature Node, and we are naming each particular instance being iterated as “n”, so we can access it on the “all” body.
In the “all” body, we are setting the “children” set as the union (in Alloy, unions are representated as the “+” operator) between left and right children (that also are sets, but unitary ones). Yea, that’s the dirty fact about Alloy: As it’s a formal specification tool, everything is grounded on the Set Theory.
Now let’s specify a fact about the parent of the nodes: If a Node A is parent of another Node B, then Node B is inside Node A’s children. Makes sense, right? :))
But before that, we need to specify that the tree must there be have one and only one root. Root is a node that has no parent, so it’s pretty straightforward:
1 2 3 

“no” is a operator that returns true if the set is empty. “one” indicates that there must be one and only one element inside the set that attends to its condition.
Now we have everything necessary to constrain a node parent:
1 2 3 4 5 

First, for every element inside a node’s children, then the child parent is the node itself. Nothing more fair!
Second, if a Node A is parent of another Node B, then Node B must be inside Node A’s children. The “=>” operator means “implies”. If the left side of implies is true, then, by definition, the right side must also be true (however, if the left side is false, nothing can be said about the right side).
If you run a manual check now, you will notice that many inconsistences were fixed, but many remain. Let’s fix some of them:
First, in none moment we define that left and right child must be different. Hence, something like that can happen in our current model:
That’s the tricky part about understanding modeling in Alloy: If we don’t define anything, everything may be possible!
Let’s fix partially this problem:
1 2 3 

Actually, this is a more strong constraint than if we defined something like that:
1 2 3 

Because, in the latter, only the left and right child of the immediate node must be different, but nothing is said about their possible children. So, something like that could happen: Node A has Node B as left child and Node C as right child, and Node B has Node C as right child. So, the disjunction must be tree level, not node level. That’s why I came with the first solution.
Yea, you can use the relation name independent of the signature. It will return a set of tuples <Node, Node> representating the relation. The “&” operator is equals to “disjoint”. It returns true if, for each element in the first set, it’s not inside the second set.
Just that solved a lot of trouble for us, but we still have the “cycle” problem, our, oh! so hated bug. Let’s solve it once for all!
1 2 3 4 

Hmmm…. What’s going on? We get any two nodes: n1 and n2. If n1 is a child of n2, then n2 can’t be a child of n1, otherwise, there would be a cycle!
Of course, the same rule is valid for all the children of n1 downto the leaves nodes: n2 can’t be a child of any node on a level below n1. But how do we get all children below n1 level? Using the “*” operator! It applies the relation (children, in our case) recursively until it can’t be applied anymore (when the node is leaf).
Now let’s get everything together:
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 

Wow!! All this work just to specify a consistent tree, not even a BST, imagine a redblack tree! Fortunately, a good part of Alloy syntax was covered in this simple tutorial. On the next part of this tutorial, we will learn how to make our tree a redblack tree. Until there!
And if you can’t hold the curiosity, here’s the complete code for the redblack tree:
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 
