Alloy is a lightweight software modeling tool that is utilized for software design and verification via automated analysis. Alloy provides a visualization tool to graphically represent models, and an evaluation tool to interact with models. I previously posted instructions for installing Alloy via Visual Studio Code, my preferred method of running Alloy. This post assumes you have performed the installation steps and are familiar with creating and running the example model. This post is an introduction to the modeling process. The example model below is constructed in successive steps, building in complexity as new features of Alloy are utilized.
The first step to constructing a model is to define signatures. A signature represents a class of objects. Alloy refers to an individual object of a class as an "atom". The signature below declares a class of objects called People.
sig People {}
At this point, a solution that satisfies the above model may contain any number of People objects, including the empty set. Running Alloy on this model will result in a potentially infinite number of solutions containing some number of atoms. The line below will run the model:
run {}
The images below are examples of solutions that Alloy generated. The first image is how Alloy renders the empty set of People, while the second is an instance consisting of two People.
This trivial example shows the minimum requirements for an Alloy model.
The following source introduces a constraint on the model, referred to as a "fact". Declaring a constraint as a fact assumes that the constraint always holds for any and every instance of the model. The some in the fact below is a multiplicity argument. There are several:
set - Any numberone - Exactly onelone - At most onesome - At least oneIn the fact below, the multiplicity some enforces that any model Alloy generates must contain one or more People.
fact
{
some People
}
Executing Alloy on this model will result in an infinite number of possible solutions, all containing at least one People atom. The empty set from Part 1 will no longer appear in the generated solutions because it does not satisfy the constraint added with the above fact. All facts must hold for all models. It is possible to over-constrain a model in such a way that no solution exists. This is one of the challenging parts of modeling a complex system with a large set of global constraints. As trivial example, a conflicting fact could be added to the model:
fact
{
#People = 0
}
In this fact, the # symbol is the cardinality operator. This fact specifies that the number of People atoms is 0. This directly conflicts with the previous fact that requires at least one People atom in the model. Running the model with this contradictory fact results in the following output from Alloy:
No instance found. Predicate may be inconsistent
Removing the contradictory fact allows Alloy to generate solutions.
The signature below introduces a new atom to represent a person's name. The People signature is modified to include a relation between People and Name. In the context of object oriented programming, this is analogous to a field or member variable.
sig Name {}
sig People
{
person_name: Name
}
Running Alloy results in a set of instances of the model in which People atoms have Name atoms associated with them. For example:
Notice that the atoms People and Name are represented by boxes, and those boxes are related by directional arrows representing the defined person_name relation. It is also possible for one Name to be shared between multiple People atoms:
This is accurate to the real system being modeled (Obviously more than one person can have the same name.). However, it is important to be cognizant of the relationships Alloy generates because these often reveal unexpected aspects of the system. Therefore, it is important to generate multiple solutions to explore the instances that satisfy the constraints. Using the New button quickly results in a model with undesired behavior. For example, the image below depicts a Name atom that doesn't belong to a People atom, i.e. a name that exists but has never been given to a person.
Aside from bringing up a philosophical question, "If no one has been given a name, does that name exist?", this highlights the importance of exploring the visualizer and interacting with Alloy's solutions. This type of unexpected result may be significant for the system being modeled; for example, a computer user account that does not have a password may indicate a vulnerability. At the highest level, an unexpected result indicates that the model is missing a constraint. The job of the analyst is to determine if the constraint is missing as a result of a mistake in the model, or if it is missing as a result of a constraint missing from the underlying system, i.e. a "real" problem.
To address the behavior described in Part 3, a new constraint is added in the form of a fact.
fact
{
all n: Name | //For all set members in the set of Name atoms (n)
n in People.person_name //n must be in the set of names given to people
}
The above fact follows the syntax: <quantifier> <variable name>: <bounding expression> | <constraining expression>. That is:
<quantifier> - all - in this case, referring to the entire set of atoms defined by the bounding expression<variable name> - n - the variable name assigned to a given member of the set defined by the bounding expression.<bounding expression> - Name - the bounding expression that defines the set to be constrained. In this case, all Name atoms<constraining expression> - n in People.person_name - the constraint placed on the members of the bounding expression setIn English, the above constraint specifies "For all n that exist in the set of Name atoms, n must be in the person_name set of some member of the People set. This brings up another syntactic feature of Alloy, the join operator ., in the expression People.person_name, which is discussed shortly. For now, it is important to note that running this model will now result in a set of solutions for which any Name atom that exists must be associated with a People atom; i.e., for a name to exist, it must have been given to a person.
Using the signature name, People with the join operator . followed by the relation name person_name, essentially states "the set created by joining all the person_name sets from all People atoms. This can be explored in the Alloy evaluator window. For example, using the above model, executing the following: People.person_name results in the output set: {Name$0, Name$1}. This set is the set of all names that exist in the instance of the model. On the other hand, running People$1.person_name returns the set {Name$0}. This is the set of Name atoms in the person_name set of Person 1, i.e. person 1's name. The example shows why the evaluator window is a valuable tool for experimenting with and understanding various syntax and logic features Alloy provides. It can be useful for debugging a model by manually exploring expressions and verifying the resulting output matches expectations.
Alloy contains some features borrowed from the object oriented programming paradigm. A critical concept in this category is inheritance. If you are already familiar with this concept, the Alloy equivalents are straightforward and you should skip to Part 5 -B below. If not, Let's take an example of objects, three modes of transportation and some of their components:
These distinct modes of transportation have both unique and common features. This means we can define a prototypical vehicle that captures the common traits. This is the parent class. E.g.
Here, the Transportation class captures the common elements of the object types. All that is left is for the child classes to inherit these traits, then extend them by adding the type-specific features; in this case, all objects inherit Engine, Seats and Passengers, but the car extends the parent by adding a sunroof, the plane by adding wings, and the boat by adding an anchor. Extension and Inheritance are ubiquitous object oriented programming concepts. Now the diagram might look like this:
It is worth noting that the above diagrams are very informal. There are entire suites of tools dedicated to modeling so-called class diagrams with conventions for symbology etc. but the quick Google drawings above convey the important details.
There is one more important concept to explore in this area. In the above diagram, there are classes that can be instantiated; that is, you can have an instance of a car, plane or boat. However, what would an instance of the Transportation class be? What does this actually mean? You can't ride in a "transportation" like you can a boat or car. That is because it is not a concrete physical object, it's a conceptual prototype. Transportation is an abstract concept. Abstract and Concrete are again object oriented programming concepts. To properly construct this relationship, the parent Transportation class should be marked as abstract to indicate that it cannot exist, only concrete extensions of the class may exist. Part B shows how this applies to an Alloy model.
The People signature is modified to be an abstract signature. Below it, two concrete signatures, Man and Woman, extend the People signature, inheriting the person_name trait in the process.
abstract sig People
{
person_name: one Name
}
sig Man extends People {}
sig Woman extends People {}
Running this model will now produce instances that contain some Man and Woman atoms, but no abstract People atoms. However, because Man and Woman are still extensions of the People signature, constraints that were added earlier, for example some People, still apply to the Man and Woman atoms. Notice that both Man and Woman have the inherited person_name relation as well.
Note: this instance of the model shows a man and woman sharing the same name. This may be the case in reality (some names are unisex), or it may be a missing constraint one might add. This is pointed out to again emphasize the importance of exploring and understanding Alloy's visualizations to reveal hidden or unforeseen behavior.
Some new signatures were added to capture the concept of a person being either alive (Alive) or dead (Dead).
sig Alive in People {}
sig Dead in People{}
The in keyword here states that the sets Alive and Dead are fully contained in the People set, i.e. Alive and Dead are subsets of the People set. Running the model produces some unexpected results. For example, in the instance below, Woman 0 is neither alive nor dead:
And in this instance, Woman 1 is both alive and dead.
A Venn Diagram of these sets would look like this:
Clearly these conditions (marked with "??") do not match the expected behavior of the underlying system being modeled (save for belief in the undead and ghosts). This is indicative of missing constraints. Lets assume we had a requirement for our system that no person could be alive and dead at the same time. We can capture that requirement as an assertion made on the model. For example:
assert NoAliveAndDead
{
no p: People | (p in Alive && p in Dead)
}
Here the assert keyword is used to define a new assertion named NoAliveAndDead. The body of the assertion specifies that there exists no member of People p, such that p is a member of the set Alive and (&&) a member of the set Dead; i.e. there can't be a person that is both alive and dead. We can ask Alloy to search for a counterexample to this claim by running a check on the assertion:
check NoAliveAndDead
Running this results in the output:
Counterexample found. Assertion is invalid.
And indeed, opening the counterexample in the visualizer shows an instance with a woman, Woman 1, who is both alive and dead. Notice that the assertion appears in the box for the atom in question:
A similar requirement may be that every person must be either Alive or Dead:
assert AliveOrDead
{
all p: People | (p in Alive || p in Dead)
}
This assertion states that for all p in the universe of People, p must be in Alive or (||) p must be in Dead. Let's check that assertion:
check AliveOrDead
Again, alloy reports that a counter example was found, and sure enough, in the visualization of the counterexample, Woman 0 is neither alive nor dead.
Lets add some constraints to this model to correct for these conditions. The following can be added to enforce that no person can be alive and dead.
fact
{
all p: People |
p in Dead <=> p not in Alive
}
This fact introduces implications. The syntax X => Y can be read as "Condition X implies Condition Y". This is called the implication operator. In the example fact, the bi-implication operator is used, <=>. This can be read as "Condition X implies Y AND Condition Y implies X". In this example, for all p in the universe of People, p in Dead implies p not in Alive AND p not in Alive implies p in Dead; i.e. if a person is dead, they are not alive, and vice-versa. After adding this constraint, the previous NoAliveAndDead assertion can be checked again. This results in Alloy no longer finding a counterexample showing a person who is both alive and dead:
No counterexample found. Assertion may be valid.
After adding the above constraint, the Venn diagram now shows the Alive and Dead sets disjoint from each other, i.e. they do not overlap. disjoint and other concepts relating to set theory will come up frequently when modeling with Alloy.
Now, the other constraint, that all people must be either alive or dead, must be added:
fact
{
People = Alive + Dead
}
This fact uses the union operator +. This states that the set of People atoms is exactly equivalent to the union of the Alive and Dead sets. "Union" here means the result of combining both sets. This means that the entire universe of People is exactly the same as combining all Alive and Dead people. There are no People atoms that exist outside of those two sets. The Venn diagram helps to visualize this, and the region of "neither alive nor dead" has been removed:
Now, re-checking the AliveOrDead assertion results in Alloy reporting that no counterexample could be found.
This section is more of a footnote regarding the run operator used to execute the model. Up until now, run {} has been used in which the {} is an empty predicate. However, this predicate can contain expressions. For example, the some people constraint used previously could instead be placed in the run predicate:
run { some People }
It is important to note the distinction between this predicate and the global fact used before. It is only relevant to this line of execution. If a run/check/etc. command appears somewhere else in the file, the some people will no longer apply. In addition to the predicate, the run command can be bounded by a scope. For example:
run { some People } for 5 but exactly 3 Name
The scope specifies that the model should be limited to 5 atoms from each type, except for Name, for which there should be exactly 3. This is useful for constraining the effort required to solve the model, or for requesting that Alloy construct a model within certain bounds. However, one must be cautious with the scope. It is possible to place bounds on Alloy that make a solution impossible. For example:
run { some People } for 1 but exactly 2 Name
This scope says there can only be one People atom, but specifies that there must be 2 Name atoms. This contradicts our previous constraint that every Name atom must be assigned to a person. Two Name would imply there are 2 People, but the scope bounds the model to only one People atom.
Below is the complete Alloy model used in this example.
//This signature represents a name
sig Name {}
//This signature represents people
abstract sig People
{
person_name: one Name
}
//This signature represents men and women
sig Man extends People {}
sig Woman extends People {}
//This signature represents being alive or dead.
sig Alive in People {}
sig Dead in People{}
//Facts about People
fact
{
People = Alive + Dead //All people are alive or dead
all p: People |
p in Dead <=> p not in Alive //People are not alive AND dead
}
//Facts about names
fact
{
all n: Name |
n in People.person_name //All names are assigned to a person
}
//Assert that no person can be alive AND dead
assert NoAliveAndDead
{
no p: People | (p in Alive && p in Dead)
}
//Assert everyone must be alive OR dead
assert AliveOrDead
{
all p: People | (p in Alive || p in Dead)
}
//Check the assertions
check NoAliveAndDead
check AliveOrDead
//Generate a representative model
run {
some People
} for 5 but exactly 3 Name
Hopefully this post provides a useful introduction to Alloy and some of the features it provides. It should be noted that there are numerous ways to express the same logical conditions, and there are very likely more concise and "cleaner" ways to express the model described in this document. The best resource for learning Alloy and refining your modeling is the Alloy website, the official Alloy tutorial and the official book. In future posts, I plan to demonstrate a few more Alloy concepts with riddle solving models.