Thomas A. Alspaugh

The book

Page numbers refer to

Daniel Jackson. Software Abstractions: Logic, Language, and Analysis. MIT Press, 2006.

How to update the book for Alloy 4.

The book is interesting, well written, and valuable for a novice Alloy user, but not absolutely essential if you just want to try Alloy out and play with it.

Obtaining the Alloy Analyzer

Download the free Alloy Analyzer from the Alloy Community. There are several online tutorials there as well, and an assortment of Alloy models you can play with.

Using Alloy

Alloy is a language for producing models (the Alloy language); a logic for saying things about these models (the Alloy logic); and an analyzer for checking a model, exploring the space of possible instances of the model, and checking the things that have been said about the model against a lot of instances (the Alloy Analyzer).

The kinds of models you can produce are similar to an OWL ontology or a UML class diagram. However, unlike a UML diagram (unless fully annotated with OCL), an Alloy model completely specifies the possible instances of the model. An Alloy model consists of a group of sets and relations, defined in a first-order relational logic, with additional constructs so you can name and reuse sets and relations, make assertions, and tell the Alloy analyzer how you want everything checked.

The Alloy analyzer will then generate interesting instances of your model and check them, using a sophisticated approach based on SAT solvers. The analyzer won't be able to generate all instances of your model (unless it is a very simple model indeed), since in general there are an infinite number of them. So it will generate the ones that are likely to be most interesting, within the size limits you specify.

The Alloy logic

The Alloy logic is a first-order logic in which the domain is the set of all relations, and terms include relational expressions such as joins.

Everything in Alloy is a relation!

As a result, the operators apply to relations, sets, and scalars, and there are very few cases that produce no result.

Set constants and operations

Set constants 50
univ The universal set, containing everything
none The empty set
Set operators 52
+ Union A set
& Intersection
- Difference
in Subset T or F
= Equality

Example: set.als

Sets set.als
//  Examples for sets

abstract sig Person {}
one sig Ann, Bob, Chip //  A set of three people
extends Person {}

abstract sig Dog {}
one sig Fido, Gruff, Hero //  A set of three dogs
extends Dog {}

pred show {}
run show

// assert noneInPerson {
//   none in Person
// }
//  alloy gives compilation warning that this is always true

// no, none
pred noNone {
  no none
run noNone

// in
assert personInUniv {
  Person in univ
check personInUniv

// +
assert dogInUnion {
  Dog in (Dog + Person)
check dogInUnion
//  Interesting that alloy doesn't warn of this at compile time

// assert noIntersection {
//   no (Dog & Person)
// }
//  alloy gives compilation warning that this is always true

// some, &
pred someIntersection {
  some (Dog & (Dog + Person))
run someIntersection

// -
pred someDifference {
  some univ - Person
run someDifference

// =
assert dogsTheDifference {
  Dog = ((Dog + Person) - Person)
check dogsTheDifference


Relation constants and operations

Relation constants 50
iden The identity relation
Relation operators, each producing another relation as a result 55
For relations R and S, sets Set, and elements a, b, c, and d
Symbol Name Syntax Meaning
-> (Arrow) product R->S a(R->S)c iff …
. Join R.S a(R.S)c iff
there is a b such that aRb and bSc
[] Join (a second notation for it) S[R] a(S[R])ca(R.S)c
~ Transpose ~R a(~R)b iff bRa
^ Transitive closure ^R a(^R)b iff
  1. aRb, or
  2. for some c,
    aRc and cRb, or
  3. for some c and d,
    aRc and cRd and dRb, or
* Reflexive transitive closure *R a(^R)b iff
  1. ab, or
  2. aRb, or
  3. for some c,
    aRc and cRb, or
<: Domain restriction Set<:R a(Set<:R)b iff
aSet and aRb
:> Range restriction R:>Set a(R:>Set)b iff
aRb and bSet
++ Override R++S a(R++S)b
(S overriding R) iff
  1. (if there is some c such that aSc)
    aSb, or
  2. (otherwise)
    aRb or

Example: relation.als

Relations and logic relation.als
//  Relations and logic

abstract sig Dog { }
one sig Fido, Gruff, Hero //  A set of three dogs
extends Dog {}

abstract sig Person {
  hasOneDog: Dog,
  hasDogs: some Dog,
  bestFriend: one Person
one sig Ann, Bob, Chip //  A set of three people
extends Person {}

pred show {}
run show

// arrow product ->
fun x: Person->Dog {
  Ann->Fido +
  Bob->Fido +
pred xInHasDogs {
  x in hasDogs
run xInHasDogs

// dot join .
pred fidoInOne {
  Fido in
  Person.hasOneDog     //  Somebody has Fido as only dog.
run fidoInOne

pred fidoInSome {
  Fido in
  Person.hasDogs       //  Somebody has Fido as one of their dogs
run fidoInSome

// dot join and quantifier
pred fidoInEvery {
  all p:Person |
  Fido in p.hasDogs    //  Everybody has Fido as one of their dogs
run fidoInEvery

// box join []
pred dogInEvery {
  Dog in
  hasOneDog[Person]    // fidoInOne, reversed (box)
run dogInEvery

// transpose ~
pred chipInEvery {
  Chip in
  Dog.~hasOneDog       //  Chip in transposed hasOneDog
run chipInEvery

// transitive closure ^
pred closing {
  Bob not in Ann.bestFriend
  Bob in Ann.^bestFriend
run closing

// domain restriction <:
// range restriction :>
pred restrictions {
  (Person <: iden :> Dog)
  in hasOneDog         //  Restrictions on iden
run restrictions

// override ++
pred override [p:Person->Dog] {
  p not in
  Ann->Gruff)          //  Overriding every tuple beginning with Ann
run override


Logical operators

True and false
Any non-empty set or relation True
none False
Logical operators 69
SymbolKeywordName or result
! not negation
&& and conjunction
|| or disjunction
=> implies (material) implication
else A=>B else C(A&&B)||(!A&&C)
<=> iff logical equivalence

Example: else.als

//  Else

abstract sig A {}
sig B extends A {}

pred true {      //  Always true
  some a:A | a in A
run true

pred false {     //  Always false
  some a:A | a not in A
run false

pred elseTTT {  true  implies true  else true   }
run  elseTTT           //  should be true

pred elseTTF {  true  implies true  else false  }
run  elseTTF           //  should be true

pred elseTFT {  true  implies false else true   }
run  elseTFT           //  should be FALSE

pred elseTFF {  true  implies false else false  }
run  elseTFF           //  should be FALSE

pred elseFTT {  false implies true  else true   }
run  elseFTT           //  should be true

pred elseFTF {  false implies true  else false  }
run  elseFTF           //  should be FALSE

pred elseFFT {  false implies false else true   }
run  elseFFT           //  should be true

pred elseFFF {  false implies false else false  }
run  elseFFF           //  should be FALSE


Quantifiers and predicates

Quantifiers and predicates 70
For any variable v, relation R, set Set, and formula Φ
Q v:Set | Φ
Predicate on relations
all universal quantifier
all v:Set | Φ   is true iff Φ is true for
every value of v in Set
some existential quantifier
some v:Set | Φ   is true iff Φ is true for
one or more values of v in Set
size of R is 1 or greater
no negated existential quantifier
no v:Set | Φ   is true iff Φ is true for
no value of v in Set
size of R is 0
lone zero or one exists
lone v:Set | Φ   is true iff Φ is true for
no more than one value of v in Set
size of R is 0 or 1
one exactly one exists
one v:Set | Φ   is true iff Φ is true for
exactly one value of v in Set
size of R is 1

Example: genealogy.als

Genealogy (genealogy.als)
//  Quantifiers and predicates

abstract sig Person {           //  Signature
  child : set Person            //  Any number of children
                                //  (see <a href='#multiplicity'>set</a>)

fact {              //  (A fact about the model;  see <a href='#fact'>fact</a>)
  no p: Person |                //  No one ...
  p in p.^child                 //  ... is their own descendant

sig Man extends Person { }      //  Men are people

sig Woman extends Person { }    //  Women are people

//  Because both extend Person, everyone in this model is either
//  a man or a woman but not both.

fact {
  all p: Person |               //  Every person ...
  lone m: Man | p in m.child    //  ... has at most one father

fact {
  all p: Person |               //  Every person ...
  lone w: Woman | p in w.child  //  ... has at most one mother

fact {
  some Person                   //  Let's rule out the boring case of no people

pred show {}
run show

let 73
let x = e | A A with every occurrence of x replaced by expression e


(Parts of this subsection describe the Alloy language.)

Each set of atoms is defined by a signature, with keyword sig.

A signature can contain zero or more relation declarations, separated by commas. Each declaration names a (binary) relation between the set defined by the signature and a set or relation.

  //  Simple example
  abstract sig Person {     // Signature
    father: lone Man,       //   A declaration
    mother: lone Woman      //   Another declaration
  sig Man extends Person {
    wife: lone Woman
  sig Woman extends Person {
    husband: lone Man
Relationships among signatures
S in T
U in T
subset Every S is a T,
every U is a T
An S can also be a U
S extends T
U extends T
extension An S cannot also be a U

The extended signature must be either a top-level signature or a subsignature.

Constraining a declaration

There are two ways:

  1. with set or relation multiplicity constraints in the signature. These are a quick shorthand. The example above has several of these (all are lone).
  2. with a fact 117 that states a constraint on the set or relation. The constraint is expressed in the Alloy logic.

    (The fact keyword may be omitted if the fact is only about the relations of a single signature, and it immediately follows that signature — then it is a signature fact, and is implicitly universally quantified over the signature's set, and may use this as if it were the variable of this implied quantification.) 

Multiplicity constraints in declarations

Set declarations with multiplicities 76
e is a expression producing a set (arity 1)
x: set e x a subset of e
x: lone e x empty or a singleton subset of e
x: some e x a nonempty subset of e
x: one e x a singleton subset of e
(i.e. a scalar)
x: e x a singleton subset of e
(equivalent to one)
Relation declarations with -> multiplicities 77
A and B are expressions producing a relation
m and n are some, lone, one, or not present (which is equivalent to set)
r: A m -> n B m elements of A map to each element of B
each element of A maps to n elements of B


117 A fact contains a formula in the Alloy logic that is assumed to always be true. See the Alloy language for more details.

Example: constraints.als

Signatures, declarations, and constraints (constraints.als)
//  Example signatures, declarations, and constraints

//  The motivations for this example are:
//    - people have friends, and a person can have a best friend
//       (but only one)
//    - a best friend is also a friend
//    - people can have dogs;  one person can have several
//    - dogs tend to focus on one person (their "owner", in this model)
//    - A proverb:  A dog is man's best friend.  So, what if someone's
//      best friend is a dog rather than a person?  What would that mean?

//  One way this might work out is to theorize that if a person's
//  best friend is a dog, it is going to be that person's dog
//  (not someone else's).
//  How would we say this in logic (and thus in Alloy)?

sig Dog {
  owner: lone Person   //  Each dog is focused on his/her owner.
                       //  But a stray dog could have 0 owners, so "lone".

sig Person {
  friend: set Person,  //  Any number of friends (0 to whatever)
    lone (Person+Dog), //  But at most only one best friend (0 or 1)
  dog: set Dog         //  Any number of dogs

//  This next thing is a signature fact -- it is only about Person
//  (the signature immediately before it).
//  Note the use of the "this" keyword,
//  and the absence of the "fact" keyword.
  this not in friend    //  We don't say that someone is their own friend.
//  Because it's a signature fact, we don't have to say which Person's
//  friend and best friend we are talking about -- it's as though we had
//  said
//    all p: Person | p not in p.friend
//  in an ordinary fact.

//  Can only have one signature fact, so this next one is just a fact
//  (with a "fact" keyword)
fact {
  bestFriend :> Person //  The part of the bestFriend relation
                       //  that links Persons to Persons (not to Dogs) ...
  in friend            //  is a sub-relation of friend.
//  That is, if someone's best friend is a person (not a dog),
//  then that best friend is also a friend.

fact {
  bestFriend :> Dog    //  The part of the bestFriend relation
                       //  that links Persons to Dogs ...
  in dog               //  is a sub-relation of dog.
//  That is, if someone's best friend is a dog (not a person),
//  then that dog is the person's dog.

pred show {}
run show

fact {
  all d: Dog |         //  For every dog,
  all p: d.owner |     //  ... the dog's owner ...
  d in           //  ... has that dog
}                      //  I don't think this can be made a signature fact
                       //  for either Dog or Person:
                       //  it talks about both Dogs and Persons.

assert dogOwnerAssert {//  I think this assertion says the same thing.
  owner                //  Dog -> lone Person
  ~dog                 //  Dog -> Person
check dogOwnerAssert   //  So it should always be true (no counterexample).

assert ownerDogAssert {//  This assertion says something else
  dog                  //  Person -> Dog
  ~owner               //  Person lone -> Dog
check ownerDogAssert   //  Alloy will find a counterexample for this.

//  To make ownerDogAssert valid, we need another fact (uncomment it):
//fact {
//  all p:Person | all | p = d.owner

//  (Recall that "valid" means "true for every world".



71 disj before a list of variables restricts their bindings to be disjoint.

For variables v, u and set Set,


allows v and u to have the same value, while

disj v,u:Set

restricts them to have different (disjoint) values.

Example: disj.als

// disj

abstract sig Person {
  likes: Person
one sig Ann, Bob, Chip //  A world of three people
extends Person {}

pred show {}
run show

pred friends [p,q: Person] {
  p in q.likes         //  q likes p
  q in p.likes         //  p likes q
run friends            //  p and q can be same person

pred friendsDisj [disj p,q: Person] {
                       //  p and q must be different people
  p in q.likes         //  q likes p
  q in p.likes         //  p likes q
run friendsDisj        //  probably what was expected


Cardinality constraints

80 The prefix operator # (cardinality) on a relation produces the relation's size. The result is a non-negative integer that can be operated on with + - = < > =< >=. Positive integer literals can appear in cardinality expressions.

The Alloy language

The Alloy language uses the Alloy logic plus some other constructs to make models. In Alloy, a model is "a description of a software abstraction" 4.

(Recall that in FOL a model means something different.) 

Language constructs

The Alloy language adds these constructs to the Alloy logic:

  1. A module line gives the relative pathname of the model's file (minus the ".als" suffix). The pathname is relative to the directory that imported module pathnames are going to be relative to. (Obviously, the module line is mostly redundant with the file's full pathname.) 
  2. A sig (signature) declares one or more sets of atoms, and their relations to other sets.
  3. A fun (function) defines a way of getting a relation (or set, or atom). It can take parameters that are used in getting its result. It can define a relation (usually using ->) and make use of it to produce its result. It is a FOL function for the Alloy logic, in which expressions are relations.
  4. A pred (predicate) defines a formula (true or false). It can take parameters that are used in getting its result. It is a FOL predicate for the Alloy logic.
  5. A fact defines a formula that you assume is valid (always true, for any world). The Alloy analyzer uses facts as axioms in constructing its examples and counterexamples.
  6. You run a predicate in order to see the examples (if any) the Alloy analyzer finds for which the predicate is true.

    You define the scope that the analyzer checks by saying things like "run for 3" or "run for 3 but 4 Dog". The analyzer will then check only possible examples that contain no more than that many of atoms from each set.

    If it finds an example, then the predicate is satisfiable.

    If it finds no examples, the predicate may be either invalid (false for all possible examples); or it may be satisfiable but not within the scope you used.

  7. An assert (assertion) defines a formula that you claim will always be true. An assertion differs from a fact in that the Alloy analyzer will check an assertion to see if it is true for all the examples in a scope, whereas the analyzer assumes each fact is true and uses them to constrain which examples it looks at.
  8. You check an assertion in order to see whether the Alloy analyzer finds any counterexamples.

    You define the scope as for a run command.

    If it finds a counterexample, then the predicate is unsatisfiable.

    If it finds no counterexamples, the predicate may be either valid (true for all possible examples); or it may be unsatisfiable but not within the scope you used.

Which construct to use where?

  1. Writing a model (Alloy file) that might need to import other models? Use module.
  2. Need a set of atoms? Use a sig.
  3. Need an expression, whose value is a function (or set, or scalar)? Use a fun (function).
  4. Need a formula, whose value is true or false? Use a pred (predicate).
  5. Need to state an axiom that you want to be true always? Use a fact (function).
  6. Need an example for which a pred is true? run the predicate to see if one exists. It's like using an existential quantifier over all the predicate's parameters.
  7. Want to claim something is always true? Use an assert (assertion).
  8. Want to see if an assert is unsatisfiable? check the assertion to see if any counterexample can be found.


Signatures 91
sig A {fields} Declares a set A of atoms
sig A extends B {fields} Declares a subset A of set B, disjoint from
all other extends subsets of B
sig A in B {fields} Declares a subset A of B
sig A in B + C {fields} Declares a subset A of the union (+) of sets B and C
abstract sig A {fields} Declares a set A that contains no atoms
other than the ones in its subsets (if any)
one  sig A {fields} Declares a singleton set A
lone sig A {fields} Declares a set A of 0 or 1 atom
some sig A {fields} Declares a nonempty set A
sig A, B {fields} Declares two sets A and B of atoms
Wherever A appeared above, a list of names can appear
Fields (in a signature for set A) 95
f: e Declares a relation f that's a subset of A->e.
e can be any expression that produces a set —
union, intersection, … , any combination.
f: lone e Each A is related to no e or one e.
f: one e Each A is related to exactly one e.
f: some e Each A is related to at least one e.
f: g->h Each A is related to a relation from g to h.
f: one g lone -> some h The multiplicities have their usual meanings.
Here, each A is related to exactly one relation
relating each g to 1 or more h's, and
each h is related to 0 or 1 g.


Function 121s
fun Name [parameters] : type {e} Defines a function, with the given name and (possibly empty) parameters,
and producing a relation (or set, or scalar) of the given type.
The result is defined by the expression e, which may reference the parameters.


Predicates 121
pred Name [parameters] {f} Defines a predicate, with the given name and (possibly empty) parameters.
A predicate always produces true or false, so no type is needed.
The result is defined by the formula f, which may reference the parameters.


Facts 117
fact {e} The expression e is a constraint that
the analyzer will assume is always true.
fact Name {e} You can name a fact if you wish;
the analyzer will ignore the name.


Assertions 124
assert Name {f} Defines an assertion, with the given name. Assertions take no parameters.
An assertion always produces true or false, so no type is needed.
The result is defined by the formula f.

Learnt by experience

When to use @

The cryptic message

  A type error has occurred:
  This cannot be a legal relational join where
  left hand side is …
  right hand side is …

if given for a join in a signature fact, can mean that the last relation before the offending '.' has the same name as a relation in the signature; in this case, the Alloy Analyzer will grab the name as belonging to this rather than the result of the preceding join. The solution is to put a @ after the dot; the @ disables the grab for this.

I found out about this from an Alloy community post.

flip bgunflip