Clafer Cheat Sheet
Clafer Cheat Sheet
The cheat sheet is based on the grammar and the generated syntax documentation. The cheat sheet additionally provides commentary and type information, while sacrificing formality of the grammar. This document is a copy of CheatSheet.md.
Predefined sets
Sets of primitive values
double
is a double precision floating point number (limited support by ChocoSolver backend). real
is an algebraic real (not supported by backends)
integer
double
real
string
Set of all clafer instances
clafer
Declarations of model elements
Element
A clafer model consists of clafers, enums, constraints, assertions, optimization objectives, and escapes:
<element>
:
<clafer>
<enum>
<constraint>
<assertion>
<objective>
<Alloy escape>
<ChocoSolver escape>
Clafer
A clafer defines a set of its instances. Clafer nesting defines the nesting (structure) of instances. The only mandatory part of clafer declaration is <name>
:.
<clafer>
:
<abstract?> <group cardinality?> <name> <super?> <reference?> <multiplicity?> <initializer?>
<elements*>
An abstract clafer does not have any instances directly, only through concrete clafers extending it. By default, clafers are concrete (not abstract).
<abstract>
:
abstract
Group cardinality restricts the valid number of children of the clafer: xor
= 1..1
, or
= 1..*
, mux
= 0..1
, opt
= 0..*
, or a range n..m
. The default group cardinality is 0..*
.
<group cardinality>
:
xor
or
mux
opt
<int literal>..<int literal>
A clafer inherits group cardinality, children, and reference of its super clafer.
<super>
:
: <name>
Instances of a reference clafer point to instances from the target set expression. When declared using >
(set), the instances pointed to cannot repeat per each instance of its parent, whereas duplicate values are allowed when declared using >>
(bag).
<reference>
:
> <set expression>
>> <set expression>
The number of instances of a clafer per each instance of its parent is restricted by multiplicity. The default multiplicity depends on the parent clafer’s group cardinality: if the group is 0..*
then the default multiplicity is 1
, otherwise it is 0..1
. Useful shorthands are ?
= 0..1
, *
= 0..*
+
= 1..*
<multiplicity>
:
?
*
+
<int literal>
<int literal>..<int literal>
<int literal>..*
Reference clafers can be given values using an initializer: constant using =
and default using :=
(no backend currently supports default).
<initializer>
:
= <set expression>
:= <set expression>
Examples
 We declare two concrete clafers,
B
nested underA
. Both have group cardinality0..*
, , no super, no reference, no initializer, and multiplicity1
.
A
B
 An abstract clafer
A
, with group cardinalityxor
, which inherits fromB
, whose instances can only point to instances from setC ++ D
, whose each instance points to a different instance from setCD
.
abstract xor A : B > C ++ D 1..* = CD
Enum
An enumeration is syntactic sugar to declare an abstract clafer and concrete clafers inheriting from it to represent its literals.
enum <name> = <literal>  <...>
Examples
An enumeration A
with literals B
, C
, and D
.
enum A = B  C  D
which is desugared to
abstract A
B : A
C : A
D : A
Constraint
Constraint is a boolean expression that we require to be true.
A constraint can be toplevel, meaning it must be true for each instance of the model:
[ <boolean expression> ]
Or nested, meaning it must be true for each instance of the context clafer:
<clafer>
[ <boolean expression> ]
A model instance is correct iff all constraints hold. Constraints are used for instance generation.
Assertion
An assertion is a boolean expression that we are checking whether it is true for all instances of the model. A failed assertion means there exists an instance for which the boolean expression is not true.
assert [ <boolean expression> ]
Assertions are used for verifying universal properties of a model.
Objective
Objectives guide the instance generation process to minimize or maximize the values of the given numeric expressions. All objectives in a model are equally important and optimal instances trade a worse value of one objective for an improved value of another one.
Minimize
<< minimize <numeric expression> >>
Maximize
<< maximize <numeric expression> >>
Expressions
Boolean expressions
These expressions produce either true or false. There are no true and false literals in the language.
Boolean logic:
<boolean expression>
:
if <boolean expression> then <boolean expression> else <boolean expression>
<boolean expression> <=> <boolean expression>
<boolean expression> => <boolean expression>
<boolean expression>  <boolean expression>
<boolean expression> xor <boolean expression>
<boolean expression> && <boolean expression>
! <boolean expression>
Quantified expressions:
Simply quantified:
lone
means less than one. some
means at least one. not
is a synonym of no
.
<boolean expression>
:
lone <set expression>
one <set expression>
some <set expression>
no <set expression>
not <set expression>
Quantified with local declarations:
<boolean expression>
:
all disj <local declarations>  <boolean expression>
all <local declarations>  <boolean expression>
one disj <local declarations>  <boolean expression>
one <local declarations>  <boolean expression>
some disj <local declarations>  <boolean expression>
some <local declarations>  <boolean expression>
no disj <local declarations>  <boolean expression>
no <local declarations>  <boolean expression>
<local declarations>
:
<name> : <set expression> ; <...>
Numeric comparisons:
<boolean expression>
:
<numeric expression> < <numeric expression>
<numeric expression> > <numeric expression>
<numeric expression> <= <numeric expression>
<numeric expression> >= <numeric expression>
Overloaded comparisons (can be sets of instances or primitive values):
<boolean expression>
:
<set expression> = <set expression>
<set expression> != <set expression>
<set expression> in <set expression>
<set expression> not in <set expression>
Numeric expressions
<numeric expression>
:
<int literal>
<double literal>
<real literal>
<numeric expression> + <numeric expression>
<numeric expression>  <numeric expression>
<numeric expression> * <numeric expression>
<numeric expression> / <numeric expression>
<numeric expression> % <numeric expression>
 <numeric expression>
sum <numeric expression>
product <numeric expression>
# <set expression>
String expressions
<string expression>
:
"<character>*"
Set expressions
Expressions which result in sets.
.
is relational join ,
is a synonym for union ++
.
<set expression>
:
<numeric expression>
<string expression>
<name>
if <boolean expression> then <set expression> else <set expression>
<set expression> ++ <set expression>
<set expression> , <set expression>
<set expression>  <set expression>
<set expression> ** <set expression>
<set expression> . <relation expression>
Relational expressions
:>
is range restriction. <:
is domain restriction.
<relation expression>
:
<name>
<relation expression> :> <set expression>
<set expression> <: <relation expression>
Identifiers
this
is a singleton set referring to an instance of the context clafer. parent
is a relation from the context clafer to its parent. dref
is a relation from the context reference clafer to its target set.
<identifier>
:
<name>
this
parent
dref
Escapes
Escapes allow to write fragments of code in the target language of the clafer compiler: Alloy or ChocoSolver.
Escape to Alloy
<Alloy escape>
:
[alloy
<Alloy code>
]
Escape to ChocoSolver
<ChocoSolver escape>
:
[choco
<ChocoSolver code>
]
Backend Compatibility
The following table provides versions in which support for a given feature was added to Alloybased and Chocobased backend.
Language Feature  Alloy  Choco 

Nested abstract clafers  0.3.9  0.4.4 
assert [ … ]

0.3.9  0.4.2 
product

  0.3.9 
Modulo division %

0.3.9  0.4.2 
Group cardinality inheritance  0.3.9  0.4.2 
Reference refinement and redefinition  0.4.0  0.4.4 
Escapes ([alloy … ] and [choco … ] ), dref , and **

0.4.1  0.4.1 
min and max

0.4.3  0.4.2 
<: and :>

0.3.0  0.4.2 
double , real

   
Default initializer :=

   