@
Page numbers refer to
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.
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.
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 firstorder 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 is a firstorder 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 50  

univ  The universal set, containing everything 
none  The empty set 
Set operators 52  

Symbol  Name  Result 
+  Union  A set 
&  Intersection  
  Difference  
in  Subset  T or F 
=  Equality 
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])c ≡ a(R.S)c 
~  Transpose  ~R  a(~R)b iff bRa 
^  Transitive closure  ^R 
a(^R)b
iff

*  Reflexive transitive closure  *R 
a(^R)b
iff

<:  Domain restriction  Set<:R 
a(Set<:R)b
iff
a∈Set and aRb 
:>  Range restriction  R:>Set 
a(R:>Set)b
iff
aRb and b∈Set 
++  Override  R++S 
a(R++S)b
(S overriding R) iff

True and false  

Any nonempty set or relation  True 
none  False 
Logical operators 69  

Symbol  Keyword  Name or result 
!  not  negation 
&&  and  conjunction 
  or  disjunction 
=>  implies  (material) implication 
else  A=>B else C ≡ (A&&B)(!A&&C)  
<=>  iff  logical equivalence 
Quantifiers and predicates 70  

For any variable v, relation R, set Set, and formula Φ  
Quantification
Q v:Set  Φ 
Predicate on relations
Q R 

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 
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,
and 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 toplevel signature or a subsignature.
There are two ways:
(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.)
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.
71 disj before a list of variables restricts their bindings to be disjoint.
For variables v, u and set Set,
v,u:Set
allows v and u to have the same value, while
disj v,u:Set
restricts them to have different (disjoint) values.
80 The prefix operator # (cardinality) on a relation produces the relation's size. The result is a nonnegative integer that can be operated on with +  = < > =< >=. Positive integer literals can appear in cardinality expressions.
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.)
The Alloy language adds these constructs to the Alloy logic:
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.
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.
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. 
@
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.