# Clafer Cheat Sheet The cheat sheet is based on the [grammar](https://github.com/gsdlab/clafer/blob/develop/src/clafer.cf) and the [generated syntax documentation](https://github.com/gsdlab/clafer/raw/master/doc/clafer.pdf). The cheat sheet additionally provides commentary and type information, while sacrificing formality of the grammar. This document is a copy of [CheatSheet.md](https://github.com/gsdlab/clafer/blob/develop/doc/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: ``: ``` ``` ### 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 ``:. ``: ``` ``` An abstract clafer does not have any instances directly, only through concrete clafers extending it. By default, clafers are concrete (not 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..*`. ``: ``` xor or mux opt .. ``` 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 `->>` (bag). ``: ``` -> ->> ``` 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..*` ``: ``` ? * + .. ..* ``` Reference clafers can be given values using an initializer: constant using `=` and default using `:=` (no backend currently supports default). ``: ``` = := ``` #### Examples * We declare two concrete clafers, `B` nested under `A`. Both have group cardinality `0..*`, , no super, no reference, no initializer, and multiplicity `1`. ``` A B ``` * 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 `CD`. ``` 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 = | <...> ``` #### 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 top-level, meaning it must be true for each instance of the model: ``` [ ] ``` Or nested, meaning it must be true for each instance of the context clafer: ``` [ ] ``` 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 [ ] ``` 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 >> ``` Maximize ``` << maximize >> ``` ## Expressions ### Boolean expressions These expressions produce either true or false. There are no true and false literals in the language. Boolean logic: ``: ``` if then else <=> => || xor && ! ``` Quantified expressions: Simply quantified: `lone` means less than one. `some` means at least one. `not` is a synonym of `no`. ``: ``` lone one some no not ``` Quantified with local declarations: ``: ``` all disj | all | one disj | one | some disj | some | no disj | no | ``` ``: ``` : ; <...> ``` Numeric comparisons: ``: ``` < > <= >= ``` Overloaded comparisons (can be sets of instances or primitive values): ``: ``` = != in not in ``` ### Numeric expressions ``: ``` + - * / % - sum product # ``` ### String expressions ``: ``` "*" ``` ### Set expressions Expressions which result in sets. `.` is relational join `,` is a synonym for union `++`. ``: ``` if then else ++ , -- ** . ``` ### Relational expressions `:>` is range restriction. `<:` is domain restriction. ``: ``` :> <: ``` ### 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. ``: ``` 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 to ChocoSolver ``: ``` [choco| |] ``` # Backend Compatibility The following table provides versions in which support for a given feature was added to Alloy-based and Choco-based 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 `:=`	-	-