Alloy is a formal specification language designed for modeling systems and software with precision.
As a declarative object-oriented language, it is underpinned by a robust mathematical framework, allowing for the creation of abstract models that represent complex systems effectively. One of the key features of Alloy is its accompanying tool, which enables users to simulate their specifications and conduct formal verification of system properties using bounded model checking. This verification process ensures that the models adhere to specified constraints and properties, thereby enhancing reliability in system design.
In the context of programming paradigms, declarative programming stands out by emphasizing the what of computation rather than the how. As stated, “Declarative programming expresses the logic of a computation without detailing its control flow.” This approach allows developers to articulate the desired outcomes of a program while abstracting away the intricate control mechanisms that dictate execution. In requirements engineering, Alloy serves as a vital tool for formally delineating the domain of a system, including its properties and necessary operations. By providing a clear and unambiguous specification of requirements, Alloy facilitates a deeper understanding of the system’s expected behavior.
In the realm of software design, Alloy proves invaluable for modeling components and their interactions within a system. Every real-world system possesses unique properties and constraints that govern its functionality. Through automated formal verification, Alloy can systematically assess whether these properties hold true and whether constraints are consistently upheld throughout the system’s operation. This capability significantly mitigates the risk of errors, ensuring that the designed system behaves as intended.
Prominent figures in the field, such as physicist Richard P. Feynman, have emphasized the importance of self-awareness in scientific inquiry, famously stating
Quote
“The first principle is that you must not fool yourself, and you are the easiest person to fool.”
Richard P. Feynman
This principle underscores the necessity of rigorous verification practices, particularly in high-stakes environments like aerospace engineering. Notably, many organizations, including Intel and NASA, leverage formal verification techniques to affirm the accuracy of CPU operations and to validate executable source code in their space missions.
The theoretical backbone of Alloy is grounded in first-order predicate logic combined with relational calculus, representing a carefully curated subset of relational algebra. This combination provides a cohesive framework for modeling individuals, sets, and relations with minimal reliance on arithmetic operations. Additionally, the introduction of mutable sets and relations in Alloy 6 marks a significant advancement, enabling models to reflect changes over time, which is essential for dynamic systems. Despite its capabilities, Alloy is best suited for small, exploratory specifications, making it a potent tool for rapid analysis.
Example: address book
The given example of an address book can be modelled elegantly using Alloy, a formal specification language. In this model, the address book consists of names linked to corresponding addresses, and each address book can hold several such mappings. To represent this structure, Alloy provides the ability to define different entities and their relationships in a declarative manner, focusing on what the system should express rather than the operational steps of implementation.
graph TD
Name
Addresses
Books
We start by defining the basic entities in our system: Name, Addr, and Book. In the Alloy specification, we declare these as signatures (sig), which represent sets of atoms. Atoms in Alloy are the primitive, indivisible entities that cannot be further decomposed or interpreted. In this context, Name, Addr, and Book represent sets of such atoms, each set containing the distinct elements we are interested in modelling.
sig Name, Addr {} sig Book { addr: Name -> lone Addr }
The relational structure of the address book is defined by the addr field within the Book signature. The addr field links each Name to an Addr, but it does so within the context of a particular Book. This ternary relation can be represented as a three-column table, where each row links a specific Book to a specific Name and a corresponding Addr. Mathematically, the relation can be written as follows:
Here, the relation indicates that Book1 (denoted as B1) links Name1 (N1) to Address1 (A1), and Name2 (N2) to Address2 (A2). Similarly, Book2 (B2) links Name1 (N1) to Address2 (A2).
In Alloy, the cardinality of these relationships is governed by specific constraints. For instance, in the model, the keyword lone is used to indicate that each Name can be associated with at most one Addr within a Book. This restriction ensures that no name in a particular address book is linked to more than one address, providing clarity and structure to the model.
Alloy provides several cardinality keywords to control the multiplicity of relations:
one: Specifies that there must be exactly one element.
lone: Specifies that there can be zero or one element.
some: Specifies that there must be one or more elements.
In the context of the address book model, the use of lone for the addr relation reflects the constraint that each name corresponds to at most one address within a given book, ensuring a one-to-one or one-to-zero relationship between names and addresses.
Atoms and Relations in Alloy
Definition
In Alloy, atoms are the basic building blocks that represent the indivisible entities of a system. They are immutable and uninterpreted, meaning that they are simply placeholders without internal structure. Relations, on the other hand, associate these atoms with one another. A relation in Alloy is essentially a set of tuples, where each tuple is an ordered sequence of atoms.
In our example, Name, Addr, and Book are sets of atoms, while addr is a relation that associates these sets. Since addr is a ternary relation, each tuple in this relation consists of three atoms: a book, a name, and an address.
Relations in Alloy are fundamental constructs that represent sets of ordered -tuples of atoms, where denotes the arity (number of components) of the relation. Alloy’s relational model enables users to express complex associations between different entities in a system through typed relations. The type of a relation is defined by its declaration, determining the nature of the elements contained within it. For instance, a relation of type Person -> String contains pairs where the first component is of type Person and the second is a String.
Unary Relations
Unary relations are essentially sets consisting of a single column, representing a collection of individual entities. For example:
In this example, addr links Book entries with corresponding Name and Addr entities.
Join (.) Operations in Alloy
One of the powerful features of Alloy’s relational model is the ability to perform join operations between relations. For instance, consider the expression myName.(Book.addr). This expression involves two join operations: first between the Book relation and the addr relation, and then between the resulting set and myName.
First Join: Book.addr
The first step is to compute the inner join of Book with addr. This operation results in a set of tuples from addr where the first component is either B0 or B1, corresponding to the elements in the Book relation.
This set contains the names and their corresponding addresses for all entries in the Book.
Second Join: myName.(Book.addr)
Next, we perform the join operation between myName and the resulting set from the first join, Book.addr. The operation filters the tuples in Book.addr, keeping only those where the first component matches N1, which is the element contained in myName.
The result of this join operation myName.(Book.addr) yields:
myName.(Book.addr) = {(A1), (A2)}
This final result represents the set of addresses linked to N1, demonstrating the effectiveness of join operations in retrieving specific relational data based on defined relationships.
Static Analysis in Alloy
Static analysis in Alloy involves exploring the structure of a model by examining its components and relationships without executing operations over time. This is typically achieved using predicates and constraints to specify the properties we want to investigate.
To start with static analysis, we define an empty predicate named show. This serves as the basis for our exploration of the model’s instances. In the provided example, the run command is set to limit the exploration to 3 instances for each entity (like Name and Addr) while allowing only 1 instance of Book:
pred show {}run show for 3 but 1 Book
Once we have our basic predicate, we can add constraints to refine our queries. For example, we can enforce that a specific Book must contain more than one address associated with it. This is accomplished by modifying the show predicate:
pred show [b: Book] { #b.addr > 1}
#b.addr counts the number of address entries associated with the book b, and the constraint #b.addr > 1 ensures that at least two addresses are present.
Next, we can add a constraint to ensure that the number of distinct addresses is greater than one and that there are multiple names associated with these addresses:
pred show [b: Book] { #b.addr > 1 #Name.(b.addr) > 1}
Here, the expression #Name.(b.addr) counts the distinct names linked to the addresses in book b, ensuring that there is a diversity of names associated with the multiple addresses.
Finally, we examine a more complex predicate to determine whether it can be satisfied:
pred show [b: Book] { #b.addr > 1 some n: Name | #n.(b.addr) > 1}
This predicate states that there should be more than one address in the book and at least one name n that is associated with more than one address in that book. This introduces an additional requirement, making it more challenging to satisfy. Depending on the specific instances defined in the model, it may or may not be possible to fulfill this constraint, which can be evaluated by running the predicate in Alloy.
Dynamic Analysis in Alloy
Dynamic analysis involves modeling the changes that occur within the system over time, focusing on how operations affect the state of the system. In Alloy, this is often represented through predicates that specify how entities change in response to operations.
We can create a predicate that simulates adding a new address and name to a book. The add predicate captures the relationship between the book before (b) and after (bpost) the addition of a name and address:
pred add [b, bpost: Book, n: Name, a: Addr] { bpost.addr = b.addr + n -> a}
In this predicate, bpost.addr represents the updated address list after adding the new entry (n -> a) to the existing addresses in b.
To ensure that there are multiple names in the updated book, we can define a showAdd predicate:
pred showAdd [b, bpost: Book, n: Name, a: Addr] { add[b, bpost, n, a] #Name.(bpost.addr) > 1}
that invokes the add operation and adds a constraint that ensures more than one name is present in the bpost version of the book.
In addition to adding entries, we can model the deletion of names from the address book. The del predicate specifies how to remove a name and its associated address:
pred del [b, bpost: Book, n: Name] { bpost.addr = b.addr - n -> Addr}
This predicate updates bpost.addr to reflect the removal of the entry associated with the name n. The operation captures the change in the book’s state by defining how the address entries are adjusted.
Comparison table between static and dynamic analysis in Alloy:
Aspect
Static Analysis
Dynamic Analysis
Purpose
Examines the structure of the model without changes over time.
Models how the state of the system evolves over time.
Focus
Focuses on entities, their relationships, and constraints in a single snapshot.
Focuses on the operations that modify the system’s state.
Scope
Describes the system at a given point in time (unchanging state).
Describes the behavior of the system across multiple states (before and after operations).
Predicates
Defines constraints that must be true for specific configurations of the model.
Defines operations that change the system’s state, such as adding or deleting elements.
Key Operators
Involves counting (#), set relations, and joins.
Uses operations like addition (+) and subtraction (-) to model state changes.
Common Use
Verifies properties like constraints, invariants, and relationships among entities.
Simulates and validates the effect of operations, ensuring the system behaves as expected over time.
Output
Generates snapshots of valid model configurations (instances).
Simulates transitions between system states, showing the evolution over time.
Example
Ensuring that a Book has more than one address linked to it.
Modeling an operation that adds or removes a name from the address book.
Temporal Aspects
No concept of time or state transitions—static snapshot only.
Introduces time by comparing system states before and after operations.
Typical Queries
“Is there a configuration where this constraint holds?”
“What happens to the system when this operation is executed?”
Assertions and Counterexamples in Alloy
In Alloy, assertions allow us to formally express properties that we believe hold true in our model. We can use assertions to verify that certain operations, like adding and deleting elements, behave as expected.
In the first example, we want to check if performing a delete operation after an add operation returns the system to its initial state. The assertion delUndoesAdd is defined as follows:
assert delUndoesAdd { all b, bpost, bppost: Book, n: Name, a: Addr | add[b, bpost, n, a] and del[bpost, bppost, n] implies b.addr = bppost.addr }check delUndoesAdd for 3
This assertion states that for all instances of books (b, bpost, bppost), if we can add an address associated with a name and then delete that name from the updated book, the address set of the original book (b.addr) should equal the address set of the book after deletion (bppost.addr).
A counterexample is a specific scenario where the assertion fails. When Alloy checks an assertion, it actively searches for such counterexamples. For the first assertion, if no counterexample is found, it suggests that the assertion may hold true within the defined scope; however, it does not guarantee that it will always be true outside that scope.
In the second assertion, we redefine delUndoesAdd to include a condition that no addresses are linked to n in the original book:
assert delUndoesAdd { all b, bpost, bppost: Book, n: Name, a: Addr | no n.(b.addr) and add[b, bpost, n, a] and del[bpost, bppost, n] implies b.addr = bppost.addr}check delUndoesAdd for 3
In this modified assertion, we are specifically looking at scenarios where the initial book does not contain any addresses linked to the name being added. The aim is to determine whether, under these conditions, the assertion still holds true.
NOTE
If Alloy finds a counterexample when running this check, it indicates that the assertion can be violated under certain circumstances, further emphasizing the limitations of bounded verification. Bounded verification checks only within a defined scope, meaning that while it can provide confidence in the correctness of assertions for small configurations, it does not guarantee their truth across all possible cases.
Testing vs. Bounded Verification
When comparing testing and bounded verification, the following distinctions can be made:
Testing involves evaluating a few cases of arbitrary size, often randomly selected or designed based on experience or intuition. It may not cover all possible configurations, potentially leaving gaps in coverage.
Bounded Verification, on the other hand, systematically examines all cases within a certain bound, ensuring that all configurations up to that limit are analyzed. However, it does not guarantee correctness beyond the defined scope, meaning that valid configurations may exist outside of what has been checked.
Functions in Alloy
Functions in Alloy allow us to encapsulate logic and operations that can be reused throughout the model. For instance, we can define a function to retrieve the addresses in a book corresponding to a specific name:
fun lookup [b: Book, n: Name] : set Addr { n.(b.addr) }
This function takes a Book and a Name as parameters and returns the set of addresses associated with that name in the specified book.
We can also use the lookup function in assertions to verify that operations maintain expected relationships. In the example below, we check whether adding a new address to the book does not affect the addresses corresponding to other names:
assert addLocal { all b, bpost: Book, n1, n2: Name, a: Addr | add[b, bpost, n1, a] and n1 != n2 implies lookup[b, n2] = lookup[bpost, n2] }check addLocal for 3 but 2 Book
In this assertion, we ensure that if we add an address linked to n1, the addresses linked to n2 in the original book (b) remain unchanged in the updated book (bpost). This illustrates how functions can be integrated into assertions to verify specific behaviors and relationships in the model.
Example: Family Relationships in Alloy
In this Alloy model, we define a system that captures family relationships such as fathers, mothers, husbands, and wives. These relationships are modeled as relations between Person, Man, and Woman entities.
NOTE
Signatures:
Person: This is an abstract signature that serves as a base class for Man and Woman.
Man and Woman: These signatures extend Person, representing men and women in the family system.
Relationships:
father and mother: These are relationships (fields) that link each Person to their father and mother. They use the lone multiplicity, meaning each person can have at most one father and one mother.
wife and husband: These fields link a Man to a Woman (and vice versa) as marital relationships. Each man can have at most one wife, and each woman can have at most one husband.
The corresponding Alloy model is structured as follows:
abstract sig Person { father: lone Man, mother: lone Woman}sig Man extends Person { wife: lone Woman}sig Woman extends Person { husband: lone Man}
Signatures and Fields:
A signature represents a set of atoms (e.g., Person, Man, Woman).
Fields represent relationships between atoms in a signature and other atoms. For example, father is a field in Person that relates a Person to a Man.
Multiplicity: The multiplicity keyword lone ensures that each Person has at most one father or mother. Other multiplicities include:
one: exactly one
some: one or more
lone: zero or one
set: any number (including zero)
Extending Signatures: The extends keyword is used to create subtypes of a signature. In this case, Man and Woman extend Person, meaning they inherit the fields from Person.
Abstract Signatures: An abstract signature like Person cannot have direct instances. Only signatures that extend it (Man and Woman) can have instances.
Modelling the "Grandpa" Problem
In this model, we want to explore a recursive family relationship: can a person be their own grandparent? While biologically impossible, it is possible to test terminologically using relations in the model.
We define a function grandpas that returns the grandfathers of a given person p. This is done by combining the mother and father relations of the person and then checking their father field.
fun grandpas [p: Person] : set Person { p.(mother+father).father}
This function works as follows:
It combines the mother and father relations of the person (p.(mother + father)), resulting in the person’s parents.
Then, it follows the father relation of each parent to find the grandfathers.
Can You Be Your Own Grandpa?
We then define a predicate ownGrandpa that checks whether a person is their own grandparent. The predicate holds true if the person is in the set of their grandfathers:
pred ownGrandpa [p: Person] { p in p.grandpas}
This checks whether p is contained in the set returned by grandpas[p].
Running the Alloy Model
To test the validity of the ownGrandpa predicate, we run the Alloy model over a small set of instances. The command to execute this is:
run ownGrandpa for 4 Person
This command attempts to generate scenarios with up to 4 Person instances, testing whether any person can be their own grandparent. If a valid instance of this configuration exists, Alloy will produce an example; otherwise, it will confirm that no such configuration exists within the given bounds.
Identifying and Fixing the Problem
Upon running the model, we encountered a scenario where a person (Man1) was found to be their own grandfather, which is an invalid case. This issue stems from the fact that the current specification allows circular references between people in the family tree. In particular, Man0 is both the father and grandfather of himself, which is logically incorrect.
This issue can be visualized using the following diagram:
To fix this issue, we need to introduce a transitive closure constraint in the model, ensuring that no person can be their own ancestor, directly or indirectly. This means that for any person p, neither they nor any of their ancestors (father, mother, grandfather, grandmother, etc.) can appear again in their ancestry.
We can achieve this by using a recursive relation over the mother and father fields. Here’s the Alloy constraint that prevents circular ancestor relationships:
fact { no p: Person | p in p.(mother+father) or p in (p.(mother+father)).(mother+father) or p in ((p.(mother+father)).(mother+father)).(mother+father)}
The first condition, p in p.(mother+father), ensures that a person cannot directly be their own parent (i.e., they are not their own father or mother).
The second condition, p in (p.(mother+father)).(mother+father), ensures that a person cannot be their own grandparent by checking their parents’ parents.
The third condition extends this to further generations, ensuring that a person cannot be their own great-grandparent, and so on.
This recursive pattern can continue as far as needed to ensure that no circular ancestor relationships exist within the bounds of the model.
Transitive Closure
Transitive closure is a powerful concept in Alloy used to describe relationships where a connection can exist through multiple intermediate nodes. It allows us to extend the relationships defined in a model to include all reachable nodes from a given starting node.
Definitions
Transitive Closure: Denoted as ^r, it includes all pairs of nodes connected directly or indirectly by relation r.
Reflexive Transitive Closure: Denoted as *r, it adds reflexive pairs (each node is related to itself) to the transitive closure.
Consider a simple example with nodes and a relation named next:
In this case, starting from first, we can reach all nodes in Node through the next relation.
Constraints Using Transitive Closure
No One Can Be Their Own Ancestor: To enforce the rule that no one can be their own ancestor, we can apply the transitive closure to the mother and father relations:
fact { no p: Person | p in p.^(mother + father)}
This constraint ensures that for any person p, they cannot appear in their own ancestry chain.
Spousal Relationships: Another common relationship modeled in Alloy is that of spouses. If is the husband of , then is the wife of . This can be expressed using the iff operator:
fact { all m: Man, w: Woman | m.wife = w iff w.husband = m}
Transpose Operator (~)
The transpose operator~ allows us to reverse binary relations, making it easier to express relationships symmetrically.
We can also use the transpose operator to simplify spousal relationships:
fact { wife = ~husband}
This states that the wife relation is simply the transpose of the husband relation, ensuring that the model maintains consistency in family relationships.
Understanding facts in Alloy
In Alloy, facts are a fundamental construct used to express global constraints that must always hold true within a given model. They can contain multiple constraints combined logically using and.
Example
For example, a fact can specify relationships and constraints involving persons, as shown below:
fact { no p: Person | p in p.^(mother + father) wife = ~husband}
In this example, two constraints are specified:
No Self-Ancestors: The first constraint asserts that no person can be their own ancestor. This is enforced by applying the transitive closure to both the mother and father relations, ensuring that a person cannot be found in their own ancestry.
Spousal Relationship: The second constraint establishes that the wife relationship is the transpose of the husband relationship, ensuring symmetry in these relationships.
While both facts and predicates are used to express constraints in Alloy, there are key differences between the two:
Scope: Facts are global constraints that must hold for every instance of atoms and relations in the model. In contrast, predicates are local and need to be explicitly invoked to evaluate their truth or to explore instances.
Invocation: Facts are always considered true within the model, while predicates require invocation through statements like run or check to evaluate their conditions.
Adding Assertions
Assertions in Alloy are used to specify properties that we expect to hold true within the model and are designed to be checked for validity. If an assertion fails, it indicates the existence of a counterexample, highlighting an instance where the assertion does not hold.
Example
To assert that no man can also be his own father, we can define the following assertion:
assert NoSelfFather { no m: Man | m = m.father}check NoSelfFather
In this case, the assertion NoSelfFather states that there cannot be any instance of a Man where that man is equal to his own father. The command check NoSelfFather invokes the Alloy tool to search for any counterexamples to this assertion. If a counterexample exists, it indicates a violation of the stated property, and Alloy will provide an instance that demonstrates this failure.
We defined social conventions to ensure that certain relationships in family trees, like the spousal and parental connections, are logically sound. We started by ensuring that no one can be both a spouse and an ancestor. However, we also need to address the issue of common ancestors between spouses.
The first fact, SocialConvention, ensures that no person can have a spouse (wife or husband) who is also one of their ancestors:
fact SocialConvention { no ((wife+husband) & ^(mother+father))}
This fact uses a transitive closure (^) to include all ancestors and ensures that the sets of wife/husband relations and mother/father relations are disjoint.
Despite the previous fact, spouses (wife and husband) can still have common ancestors. Consider the following situation represented by a family tree:
graph LR
Man1 -- father --> Man0
Man1 -- wife --> Woman -- father --> Man0
Woman -- husband --> Man1
Here, both Man1 and Woman share the same ancestor (Man0), which violates the idea of completely distinct ancestral lines.
To ensure that spouses do not share any common ancestors, we introduce an updated fact, SocialConvention2:
fact SocialConvention2 { all m: Man, w: Woman | (m.wife = w and w.husband = m) implies not (m in w.^(father+mother) or w in m.^(father+mother))}
This fact ensures that if m is the husband of w, and vice versa, neither m nor w can be in the other’s ancestral line. This uses a similar transitive closure operator to include all ancestors.
An alternative way to address the common ancestor issue is by defining a function ancestors to return all ancestors of a given person:
fun ancestors [p: Person]: set Person { p.^(mother+father)}
We can then use this function to define a stronger fact, noCommonAncestors, which checks that spouses do not share ancestors:
fact noCommonAncestors { all p1: Man, p2: Woman | p1 -> p2 in wife implies ancestors[p1] & ancestors[p2] = none}
Here, we check that the intersection of the ancestors of p1 (the husband) and p2 (the wife) is an empty set, ensuring that they do not share any ancestors.
Another approach to addressing this issue is using a combination of the transpose operator (~) and ancestor relations:
pred noCommonAncestors { all p1: Man, p2: Woman | p1->p2 in wife implies ancestors[p1] & ancestors[p2] = none }pred SocialConvention3 { no ((wife+husband) & (mother+father).~(mother+father))}
This fact ensures that no spouse relationship overlaps with the reverse of the parent relationship, preventing direct shared ancestor loops.
To confirm that the fact noCommonAncestors is stronger than SocialConvention3, we can create an assertion and check for counterexamples:
assert Stronger { noCommonAncestors implies SocialConvention3}check Stronger for 8assert NotStronger { SocialConvention3 implies noCommonAncestors}check NotStronger for 8
Running these checks in Alloy helps verify that noCommonAncestors offers a stricter guarantee of disjoint ancestral lines compared to SocialConvention3.
Despite these facts, there are still edge cases where the model might allow strange familial relationships. For example, it is possible for someone to be both a father and a grandfather of another person:
In this scenario, Man1 is both the father and grandfather of Man0. To prevent such cases, we introduce an additional constraint:
fact SocialConvention4 { all p1: Person, p2: Person | p1 in p2.(mother+father) implies p1.(mother+father) & p2.(mother+father) = none}
This fact ensures that if p1 is an ancestor of p2, their ancestral lines remain disjoint, preventing cases where one person occupies multiple ancestral roles for another.
Mutable Relations in Alloy
Alloy allows for a more dynamic modeling approach by introducing mutable relations, which can evolve over time without requiring explicit representation of the states before and after changes. This is particularly useful in scenarios like managing an address book, where entries may be added or removed.
Previously, we defined an address book with immutable relations:
sig Name, Addr {}sig Book { addr: Name -> lone Addr}
In this setup, to model the evolution of the address book (e.g., after adding or deleting entries), we had to create distinct versions of the book (b and bpost) for before and after the operation. This required us to explicitly define how the relation changed:
pred add [b, bpost: Book, n: Name, a: Addr] { bpost.addr = b.addr + n -> a}
With the new var keyword, we can declare relations that can change over time:
sig Name, Addr {}sig Book { var addr: Name -> lone Addr}
Definition
The var keyword indicates that the addr relation is mutable, allowing it to be modified directly without the need for separate versions of the book.
We have that, initially (first instant) the address book is empty; then, after that, it has 1 address in it and, after that, it has 2 address in it and so on.
Modeling Temporal Changes
Now, we can represent the evolution of the address book more succinctly. For instance, if we want to demonstrate that the address book starts empty and then gradually adds addresses, we can use the after operator:
pred show [b: Book] { #b.addr = 0 after (#b.addr = 1 and after #b.addr = 2)}
This indicates that the number of addresses in the book transitions from 0 to 1, and then to 2, at successive time steps.
We can also use the sequence operator (;) to express the same idea more concisely:
pred show [b: Book] { #b.addr = 0 ; #b.addr = 1 ; #b.addr = 2}
When we want to visualize the evolution of the address book, we can run the predicate with a specified number of steps:
run show for 3 but 1 Book, 3 steps
This tells Alloy to simulate the changes over 3 time steps, allowing us to see how the addr relation evolves.
As a result of running the predicate, we would see the address book in its first two instants represented visually. In the initial state (first instant), the address book is empty, and in the second instant, it contains one address.
To visualize these changes, you would typically create an image that captures the evolution of the address book over the defined time steps, showing how entries are added dynamically.
New add and delete Predicates
In the mutable relations setup, we can now define add and delete operations more straightforwardly. The use of the prime symbol (') indicates the next state of the relation:
pred add [b: Book, n: Name, a: Addr] { b.addr' = b.addr + n -> a}pred del [b: Book, n: Name] { b.addr' = b.addr - n -> Addr}
Here, b.addr' denotes the state of b.addr after the addition or deletion of an entry.
This assertion checks if deleting an entry after adding it restores the address book to its original state:
assert delUndoesAdd { all b: Book, n: Name, a: Addr | no n.(b.addr) and add[b, n, a] and after del[b, n] implies b.addr = b.addr''}
In this assertion:
no n.(b.addr) ensures that the name n does not initially belong to the address book.
add[b, n, a] adds n and a to the book.
after del[b, n] specifies that n is removed from the book at the next instant.
The implication states that if the conditions are met, then the address book b after two instants (b.addr'') should be the same as it was initially.
The always Operator
To extend this assertion to cover all time instants, we can use the always operator, allowing us to express a condition that must hold at all times:
assert alwDelUndoesAdd { all b: Book, n: Name, a: Addr | always (no n.(b.addr) and add[b, n, a] and after del[b, n] implies b.addr = b.addr'')}
Here, the assertion indicates that no matter when the operation occurs, the condition must hold.
Example: Device Status
We can illustrate the use of these temporal operators with a different context, such as device statuses:
sig Device { var status: DevStatus}enum DevStatus { Working, Broken }
where enum is an useful abbreviation to avoid declaring the abstract signature.
one sig Working extends DevStatus { ... }one sig Broken extends DevStatus { ... }
In this example, the Device signature has a mutable relation status, which can take values defined in the DevStatus enumeration.
We can express constraints regarding device statuses using temporal logic:
fact NoRepair { all d: Device | always (d.status = Broken implies after always d.status = Broken)}
This fact asserts that once a device’s status is Broken, it cannot change back to Working. The use of the always operator emphasizes that this condition holds true for all time instants, reflecting a permanent state change.
New Temporal Operators in Alloy: eventually, historically, before, and once
With the introduction of the eventually, historically, before, and once operators, Alloy provides a powerful mechanism to reason about states and events over time, especially when modeling systems with complex behaviors.
The eventually Operator
The eventually operator allows us to express that a certain condition will be true at some point in the future. For example, we can state that if a device is currently working, it will eventually break:
fact NotAlwaysFunctioning { all d: Device | always (d.status = Working implies eventually d.status = Broken)}
In this fact, we assert that a device cannot remain in a working state indefinitely; it must transition to a broken state at some point.
The historically Operator
The historically operator lets us express that a condition has been true in all previous states leading up to the current state. For instance, if a device is currently working, it must have been working since the beginning:
fact NowWorkingPreviouslyWorking { all d: Device | always (d.status = Working implies historically d.status = Working)}
This fact ensures that a device cannot suddenly start working without having been in a working state previously.
The before Operator
The before operator is similar to historically, allowing us to express that a condition held true in the previous instant:
fact NowWorkingPreviouslyWorking2 { all d: Device | always (d.status = Working implies before d.status = Working)}
This fact emphasizes that if a device is currently working, it was also working in the previous state.
The once Operator
The once operator is used to indicate that a condition must have been true at least once in the past. For example, we can express that if a device is broken, it must have broken at some point in the past:
fact IfBrokenDidBreak { all d: Device | always (d.status = Broken implies once break[d])}
Here, the break predicate captures the event of a device changing from a working state to a broken state:
pred break[d: Device] { d.status = Working d.status' = Broken}
Summary of temporal operators
Future
Past
always
historically
eventually
once
after
before
Example: Message Deletion from Mailbox
To illustrate the use of these temporal operators in a different context, we can model a mailbox system where messages can be deleted and later restored. This model will introduce the concept of “trash,” representing messages that are no longer in the main mailbox but can be restored.
Signatures
In Alloy, signatures represent sets of objects in your model, and mutable signatures add flexibility to how these sets can change over time.
var sig Message {}var sig Trashed in Message {}
var: This keyword indicates that the signature is mutable, meaning that its members can change over time.
in: The statement Trashed in Message means that Trashed is a subset of Message, allowing for the dynamic inclusion of messages in the trash. This setup enables messages to be regularly categorized, trashed, and then restored again.
Predicates for System Operations
Deletion Operation
pred delete[m: Message] { m not in Trashed Trashed' = Trashed + m Message' = Message}
This predicate captures the logic of deleting a message. It ensures that:
The message m is not already in the trash (m not in Trashed).
The trashed set is updated to include the message (Trashed' = Trashed + m).
The total set of messages (Message) remains unchanged.
Restore Operation
pred restore[m: Message] { restoreEnabled[m] Trashed' = Trashed - m Message' = Message}pred restoreEnabled[m: Message] { m in Trashed}
The restore predicate allows a trashed message to be restored. It:
Checks if the message is enabled for restoration (restoreEnabled[m]).
Updates the trashed set to remove the message (Trashed' = Trashed - m).
Change in System State: Emptying Trash
pred deleteTrashed { #Trashed > 0 after #Trashed = 0 Message' = Message - Trashed}
This predicate represents the action of emptying the trash. It states that if there are messages in the trash (#Trashed > 0), then after this operation, the trash should be empty (after #Trashed = 0), and the total messages should be updated accordingly.
No State Change
pred doNothing { Message' = Message Trashed' = Trashed}
The doNothing predicate signifies that the state of both the Message and Trashed sets remains unchanged.
Receiving Messages
pred receiveMessages { #Message' > #Message Trashed' = Trashed}
This predicate allows for the arrival of new messages. It states that the number of messages should increase while the trash remains the same.
System Behavior Fact
fact systemBehavior { no Trashed // Initially, the trash is empty always ( (some m: Message | delete[m] or restore[m]) or deleteTrashed or receiveMessages or doNothing )}
This fact defines the potential actions that can occur within the system. At any moment, one of the following can happen:
A message can be deleted or restored.
The trash can be emptied.
New messages can arrive.
Nothing happens, maintaining the current state.
Assertions to Test System Behavior
Restore After Delete
assert restoreAfterDelete { all m: Message | always restore[m] implies once delete[m]}
This assertion checks that if a message is restored, it must have been deleted at some point in the past.
Delete All Messages
assert deleteAll { always ( (Message in Trashed and deleteTrashed) implies after always no Message)}
This assertion ensures that if all messages are trashed and the trash is emptied, then there will be no messages remaining in the mailbox after that point.
Messages Never Change
assert messagesNeverChange { always (Message' in Message and Message in Message')}
This assertion verifies that the set of messages does not change over time.
If Messages Are Not Deleted, Trash Not Emptied
assert ifMessagesNotDeletedTrashNotEmptied { (always all m: Message | not delete[m]) implies always not deleteTrashed}
This assertion checks that if no messages are ever deleted, then the trash will never be emptied.
Interrail Management System Example
A Person wants to organize an interrail. An interrail is a type of travel where the traveler can move to different cities by train. The person has a pass where all the cities he can visit are specified. The travel includes European cities. Cities must be interconnected through railways in order to create an itinerary. We assume that the Person can move only to the cities that he has not visited yet. We want to keep track of whether the person is traveling or has arrived at the final destination.
Signatures
The code begins with the sig declarations, where sig is short for “signature” and represents an abstract set or type.
sig City { linkedWith: some City, name: disj one EuropeanCity}enum EuropeanCity {Milan, Berlin, Paris, London, Vienna, Prague, Stockholm, Amsterdam, Copenhagen}sig Person { pass: some City, var loc: City, var visited_cities: set City, var status: Status}enum Status {Travelling, AtDestination}
The City signature represents each city on the traveler’s itinerary. The attribute linkedWith: some City specifies that each city has a set of other cities it is connected to through railways. The keyword some denotes that linkedWith must include at least one city. name: disj one EuropeanCity represents the name of each city, which must be distinct (disj) and correspond to a unique value in the EuropeanCity enumeration. Alloy defines EuropeanCity as an enumeration containing specific cities: Milan, Berlin, Paris, London, Vienna, Prague, Stockholm, Amsterdam, and Copenhagen.
The Person signature models a traveler and includes several attributes: pass, loc, visited_cities, and status. The pass attribute (some City) specifies that each person has a set of cities they are permitted to visit. The var keyword preceding loc, visited_cities, and status indicates that these attributes are mutable. loc represents the current location of the person, visited_cities is a set of cities the person has already visited, and status (of type Status) indicates whether they are still Travelling or have reached AtDestination.
Facts and Assertions
Following the signatures, a series of fact statements are defined. In Alloy, a fact is a condition that must always hold in the model.
The BidirectionConnection fact enforces that the linkedWith relationship is symmetric, meaning if c1 is linked to c2, then c2 must also be linked to c1. This is expressed using iff (if and only if) and further ensures that no city is linked to itself (c1 != c2). Additionally, c1.*linkedWith = City requires that the graph of linked cities is fully connected, covering all cities in the model.
// Two cities are connected to each otherfact BidirectionConnection { all c1, c2: City | c1 in c2.linkedWith iff c2 in c1.linkedWith and !(c1 = c2) and c1.*linkedWith = City}
The NoVisitedCitiesAtTheBeginning fact sets the initial condition that no city has been marked as visited by any person.
// At the beginning of the interrail, the traveler has not visited any cities yetfact NoVisitedCitiesAtTheBeginning { all p: Person | no p.visited_cities}
Predicates in Alloy, defined with pred, describe actions or conditions that can vary across states. The move predicate models a valid travel action for a person. It specifies that a city c can only be the target of a move if it meets several conditions: it is linked to the person’s current location (c in p.loc.linkedWith), it is listed in the person’s pass (c in p.pass), it has not been visited (c not in p.visited_cities), and it is different from the current location (c not in p.loc). After moving, the loc attribute of the person is updated to c, and c is added to visited_cities. This process models movement and the updating of visited cities.
// A given person travels to a given citypred move[p: Person, c: City] { c in p.loc.linkedWith and c in p.pass and c not in p.visited_cities and c not in p.loc p.loc' = c c in p.visited_cities'}// A given person has movedpred moved[p: Person] { some c: City | move[p,c]}// A person stays in his locationpred unmoved[p: Person] { p.loc = p.loc'}
The moved predicate uses existential quantification (some) to assert that a person moves if there exists at least one city where the move predicate holds true. Conversely, the unmoved predicate asserts that the person’s location remains the same, expressed by p.loc = p.loc'.
// Travelers start their journey form Milan and eventually they will come back to Milanfact StartingFromMilanAndComingBack { all p: Person | p.loc.name = Milan and p.status = Travelling and after (eventually (p.loc.name = Milan and p.status = AtDestination))}
The StartingFromMilanAndComingBack fact enforces that every person starts their journey in Milan (p.loc.name = Milan) and initially has the status Travelling. The use of temporal logic (eventually) models the condition that they will return to Milan and change their status to AtDestination at the end.
// Travelers do not come back to Milan if they have not visisted all the cities of the pass beforefact VisitingAllCities { all p: Person, c: City | (c in p.pass and !(c.name = Milan)) implies (always (after !(p.loc.name = Milan) until (c in p.visited_cities)))}
The VisitingAllCities fact specifies that, before returning to Milan, the traveler must visit every city listed in their pass. This is enforced using temporal operators, where always (after !(p.loc.name = Milan) until (c in p.visited_cities)) ensures that for any city c on the person’s pass (except Milan), they will eventually reach it before their return to Milan.
// The people are travelling since their departurefact Departure { all p: Person | always (moved[p] implies (p.status = Travelling since p.loc.name = Milan))}
In the Departure fact, temporal logic asserts that if a person is moving (moved[p]), they must have started traveling from Milan with status Travelling.
assert Departure2{ all p: Person | always (p.status = Travelling implies (p.loc.name = Milan triggered p.status = Travelling))}check Departure2
Assertions in Alloy, defined with assert, are intended to be verified. The Departure2 assertion checks that if a person has the status Travelling, this state change was triggered by their departure from Milan.
// If a person visits a city, the city remains forever among the visited citiesfact VisitingIsForever { all p: Person, c: City | always (c in p.visited_cities implies always c in p.visited_cities)}// If a city is not one of the visited cities, it has never been visited so farfact NeverVisitedCities { all c: City, p: Person | always (c not in p.visited_cities implies historically c not in p.visited_cities)}// If a city is one of the visited cities, it has been visited at some point in the pastfact VisitedCities { all c: City, p: Person | always (c in p.visited_cities implies once move[p, c])}
Additional facts ensure consistent tracking of cities. VisitingIsForever establishes that once a city is in visited_cities, it remains so indefinitely. NeverVisitedCities and VisitedCities respectively confirm that any city not in visited_cities was never visited and that any city in visited_cities must have been visited at some point.
// In any state, a person either stays where he is or goes to another placefact MovingOrNot { all p: Person | always (moved[p] or unmoved[p])}// After arriving in Milan, a person is no longer travellingfact NoLongerTraveling { all p: Person | after (p.loc.name = Milan releases p.status = Travelling)}
The MovingOrNot fact mandates that a person is either moving to another city or remaining stationary, expressed with moved[p] or unmoved[p]. The NoLongerTraveling fact dictates that upon arriving back in Milan, the traveler’s status changes to indicate they are no longer traveling.
Finally, the world1 predicate sets up a specific scenario for testing. The predicate specifies that the model will contain six cities and two travelers and sets constraints on the number of visited cities to observe different stages of travel. run world1 for 10 instructs Alloy to simulate this scenario for up to 10 steps, allowing the model analyzer to explore possible behaviors and verify the constraints.
pred world1{ #City = 6 and #Person = 2 #Person.visited_cities' = 2; #Person.visited_cities' = 4; #Person.visited_cities' = 6}run world1 for 10
