- Clafer Cheat Sheet
- Predefined sets
- Declarations of model elements
- Backend Compatibility
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.
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
Declarations of model elements
A clafer model consists of clafers, enums, constraints, assertions, optimization objectives, and escapes:
<clafer> <enum> <constraint> <assertion> <objective> <Alloy escape> <ChocoSolver escape>
A clafer defines a set of its instances. Clafer nesting defines the nesting (structure) of instances. The only mandatory part of clafer declaration is
<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).
Group cardinality restricts the valid number of children of the clafer:
0..*, or a range
n..m. The default group cardinality is
xor or mux opt <int literal>..<int literal>
A clafer inherits group cardinality, children, and reference of its super clafer.
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
-> <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
? * + <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).
= <set expression> := <set expression>
- We declare two concrete clafers,
A. Both have group cardinality
0..*, , no super, no reference, no initializer, and multiplicity
- An abstract clafer
A, with group cardinality
xor, which inherits from
B, whose instances can only point to instances from set
C ++ D, whose each instance points to a different instance from set
abstract xor A : B -> C ++ D 1..* = CD
An enumeration is syntactic sugar to declare an abstract clafer and concrete clafers inheriting from it to represent its literals.
enum <name> = <literal> | <...>
A with literals
enum A = B | C | D
which is desugared to
abstract A B : A C : A D : A
Constraint is a boolean expression that we require to be true.
A constraint can be top-level, 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.
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.
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 <numeric expression> >>
<< maximize <numeric expression> >>
These expressions produce either true or false. There are no true and false literals in the language.
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>
lone means less than one.
some means at least one.
not is a synonym of
lone <set expression> one <set expression> some <set expression> no <set expression> not <set expression>
Quantified with local declarations:
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>
<name> : <set 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):
<set expression> = <set expression> <set expression> != <set expression> <set expression> in <set expression> <set expression> not in <set 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>
Expressions which result in sets.
. is relational join
, is a synonym for union
<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>
:> is range restriction.
<: is domain restriction.
<name> <relation expression> :> <set expression> <set expression> <: <relation expression>
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.
<name> this parent dref
Escapes allow to write fragments of code in the target language of the clafer compiler: Alloy or ChocoSolver.
Escape to Alloy
[alloy| <Alloy code> |]
Escape to ChocoSolver
[choco| <ChocoSolver code> |]
The following table provides versions in which support for a given feature was added to Alloy-based and Choco-based backend.
|Nested abstract clafers||0.3.9||0.4.4|
|Group cardinality inheritance||0.3.9||0.4.2|
|Reference refinement and redefinition||0.4.0||0.4.4|