Clafer, the language

v0.5.8

Clafer is a general-purpose lightweight structural and behavioral modeling language developed by GSD Lab, University of Waterloo, and MODELS group at IT University of Copenhagen. Clafer can be used for modeling of static hierarchical structures and for modeling the change of the structures over time (behavior). Clafer allows for naturally expressing variability in both the structure and behavior. The main goal of Clafer is to make modeling more accessible to a wider range of users and domains.

There are many possible applications of Clafer; however, three are prominent:

1. Product-Line Architecture Modeling - aims at representing and managing commonality and variability of assets in product lines and creating and verifying product configurations. Clafer naturally supports multi-staged configuration. By applying modeling patterns, Clafer can be used for feature modeling, architecture modeling (e.g., by applying EAST-ADL), and behavior modeling (e.g., hierarchical state transition systems). All these aspects naturally include variability.

2. Multi-Objective Product Optimization - aims at finding a set of products in a given product line that are optimal with respect to a set of objectives. Clafer multi-objective optimizer generates a Pareto front of optimal product configurations.

3. Domain Modeling - aims at improving the understanding of the problem domain in the early stages of software development and determining the requirements with fewer defects. This is also known as Concept Modeling or Ontology Modeling.

4. Concept Behavior Modeling - aims at eliciting how a structure of a concept evolved over time and checking properties of possible behaviors.

May applications actually combine the three. For example, see Technical Report: Case Studies on E/E Architectures for Power Window and Central Door Locks Systems.

For examples of behavior modeling, see Behavioral Modeling section on the wiki. Behavior models compile to the temporal logic of Alloy 6: ClaferIG generates their traces and checks their assertions. The Choco backend supports only static models.

Resources

• Learning Clafer
• Cheat Sheet
• Syntax Documentation
• Grammar

Clafer, the compiler

Clafer compiler provides a reference implementation of Clafer, the language. It translates models in Clafer to other formats (e.g., Alloy, JSON, JS, HTML, DOT) to allow for reasoning and processing with existing tools (Alloy Analyzer, Choco3, and GraphViz).

Currently, the compiler is used by

• Backends
  • Alloy-based Instance Generator (ClaferIG),
  • Choco3-based Instance Generator and Multi-Objective Optimizer (chocosolver.
• Web Frontends
  • Clafer Integrated Development Environment (ClaferIDE),
  • Clafer Configurator (ClaferConfigurator),
  • Multi-Objective Visualizer and Explorer, and
  • Clafer Wiki (ClaferWiki).

Contributors

• Michał Antkiewicz, Main developer.
• Kacper Bak, Original developer.
• Jimmy Liang, Developer.
• Luke Michael Brown, co-op student May-Aug 2013. Many improvements.
• Paulius Juodisius, customized BNFC generator and layout resolver.
• Rafael Olaechea, Multi-Objective Optimization extensions.

Getting the Clafer compiler

Clafer can be installed from a binary distribution (preferred), from Hackage, and from the source code.

Dependencies for running

The compiler itself needs nothing else. The following are optional, regardless of the installation method:

• Java 17 or newer, 64-bit (a runtime is enough)
  • only needed for validating the outputs (--validate) and for --ecore2clafer
• Alloy 6.2.0 (alloy6.2.0.jar)
  • only needed for validating the Alloy output (--validate)
• chocosolver.jar from chocosolver
  • only needed for validating the Choco output (--validate)
• ecore2clafer.jar (in this repository)
  • only needed for --ecore2clafer
• GraphViz
  • the program dot is needed only in the html mode for SVG graph generation, and for validating the graph outputs

--validate and --ecore2clafer look for the jars in the tools directory: the current directory, or the one given with --tooldir=<directory>.

Installation from binaries

Binary distributions of Clafer Tools (clafer, claferIG, and chocosolver with the jars they need; Linux x86-64 for the recent releases) can be downloaded from Clafer Tools - Binary Distributions.

1. Download the binaries and unpack them into a <target directory> of your choice.
2. Add the <target directory> to your system path so that the executables can be found.
3. The bundle contains alloy6.2.0.jar, chocosolver.jar, and ecore2clafer.jar: use --tooldir=<target directory> for --validate and --ecore2clafer.

Installation from Hackage

Clafer is available on Hackage and it can be installed using either cabal-install or stack.

Installation using cabal-install

Dependencies

• ghc-9.6.7 or ghc-9.12.4
• cabal-install-3.10.3 or newer

1. Use ghcup to install ghc and cabal
2. cabal update
3. cabal install clafer

cabal install clafer builds the package and installs its executable clafer into cabal's bin directory (~/.cabal/bin or ~/.local/bin; with cabal 3.12 or newer, cabal path --installdir prints it), which must be on your PATH. The build tools of the parser are built automatically. The executable is all that is needed: the library is not exposed to GHC unless it is installed with cabal install --lib clafer.

Note that exe:clafer and clafer:exe:clafer are targets inside a project (a checkout of this repository), not of cabal install from Hackage.

Installation using stack

Clafer is not part of Stackage snapshots, so give its version; its dependencies come from the snapshot. This release is tested with the snapshot nightly-2026-11-11:

1. Install stack
2. stack install clafer-0.5.8 --resolver nightly-2026-11-11

The executable is copied to ~/.local/bin.

Tools for validation

To use --validate, put alloy6.2.0.jar (and chocosolver.jar for the Choco output) into a directory, and pass it with --tooldir=<directory>. In a checkout of this repository, make alloy6.2.0.jar downloads the Alloy jar.

Installation from the source code

Dependencies

• stack
• Git

On Windows

• MSYS2
  • it is installed automatically by stack setup
  • update MSYS2 following the update procedure:
    • stack exec pacman -- -Sy
    • stack exec pacman -- --needed -S bash pacman pacman-mirrors msys2-runtime
    • restart shell if the runtime was updated
    • stack exec pacman -- -Su
  • stack exec pacman -- -S make wget unzip diffutils

Important: branches must correspond

All related projects are following the simultaneous release model. The branch master contains releases, whereas the branch develop contains code under development. When building the tools, the branches should match. Releases from branches 'masterare guaranteed to work well together. Development versions from branchesdevelop` should work well together but this might not always be the case.

Building

1. in some <source directory> of your choice, execute

• git clone https://github.com/gsdlab/clafer.git

2. in <source directory>/clafer, execute stack setup. This will install all dependencies, build tools, and MSYS2 (on Windows).
3. cd <source directory>

• make on Linux/Mac
• stack exec make on Windows

Installation

1. Execute

• make install to=<target directory> on Linux/Mac
• stack exec make install to=<target directory> on Windows

Note:

On Windows, use / with the make command instead of \, e.g., make install to=/c/clafer-tools-0.5.4/

Integration with text editors

• VS Code: clafer-vscode
• Sublime Text 4: ClaferToolsST
• VIM: clafer-vim

Usage

Clafer Compiler

(As printed by clafer --help)

Clafer 0.5.8

clafer [OPTIONS] [FILE]

Common flags:
  -m --mode=CLAFERMODE                    Generated output type. Available
                                          CLAFERMODEs are: 'alloy' (default,
                                          Alloy 6); 'json' (intermediate
                                          representation of Clafer model);
                                          'clafer' (the explicit model, with
                                          everything written out, as Choco
                                          solves it; a temporal model with its
                                          temporal modifiers and operators,
                                          which only Alloy solves);
                                          'html' (original model in HTML);
                                          'graph' (graphical representation
                                          written in DOT language); 'cvlgraph'
                                          (cvl notation representation written
                                          in DOT language); 'choco' (Choco
                                          constraint programming solver).
                                          Multiple modes can be specified at
                                          the same time, e.g., '-m alloy -m
                                          html'.
  -o --console-output                     Output code on console.
  -i --flatten-inheritance                Flatten inheritance ('alloy' mode
                                          only).
     --timeout-analysis=INT               Timeout for analysis.
  -l --no-layout                          Don't resolve off-side rule layout.
  -n --nl --new-layout                    Use new fast layout resolver
                                          (experimental).
  -c --check-duplicates                   Check duplicated clafer names in
                                          the entire model.
  -f --skip-resolver                      The names of the clafers are their
                                          UIDs, as in an explicit model: skip
                                          renaming them. Names must be unique;
                                          they are still resolved and checked.
     --explicit                           The model is an explicit model, as
                                          'clafer -m clafer' prints it, with
                                          every name a UID and every card
                                          written out, and its scopes in its
                                          scope file. Shorthand for -f -k -l
                                          --ss=none.
  -k --keep-unused                        Keep uninstantated abstract clafers
                                          ('alloy' mode only).
  -s --no-stats                           Don't print statistics.
  -v --validate                           Validate outputs of all modes, and
                                          exit with 1 if a tool rejects one.
                                          Uses '<tooldir>/alloy6.2.0.jar' for
                                          Alloy models,
                                          '<tooldir>/chocosolver.jar' for Choco
                                          models, dot for graphs, and clafer
                                          itself for explicit models, which
                                          must compile to themselves. Use
                                          '--tooldir' to override the default
                                          location ('.') of these tools.
     --tooldir=DIR                        Specify the tools directory
                                          ('validate' only). Default: '.'
                                          (current directory).
  -a --alloy-mapping                      Generate mapping to Alloy source
                                          code ('alloy' mode only).
     --self-contained                     Generate a self-contained html
                                          document ('html' mode only).
     --add-graph                          Add a graph to the generated html
                                          model ('html' mode only). Requires
                                          the "dot" executable to be on the
                                          system path.
     --sr --show-references               Whether the links for references
                                          should be rendered. ('html' and
                                          'graph' modes only).
     --add-comments                       Include comments from the source
                                          file in the html output ('html' mode
                                          only).
  -e --ecore2clafer                       Translate an ECore model into
                                          Clafer.
     --tl=INT --trace-len                 Define the maximum trace length.
     --ss=SCOPESTRATEGY --scope-strategy  Use scope computation strategy:
                                          none or simple (default).
     --check-afm --afm                    Throws an error if the cardinality
                                          of any of the clafers is above 1.
     --meta-data                          Generate a 'fully qualified
                                          name'-'least-partially-qualified
                                          name'-'unique ID' map ('.cfr-map').
                                          In Alloy and Choco modes, generate
                                          the scopes map ('.cfr-scope'); in
                                          Clafer mode, the explicit model's
                                          scope file with every scope
                                          ('.des.cfr-scope').
     --minint=INT                         Smallest integer value ('choco'
                                          mode only). Default: -128, chosen by
                                          chocosolver.
     --maxint=INT                         Largest integer value ('choco' mode
                                          only). Default: 127, chosen by
                                          chocosolver.
     --decimal-digits=INT                 Number of fractional digits of
                                          decimals ('choco' mode only).
                                          Default: the most fractional digits
                                          of the model's decimal literals.
     --import=FILE                        Compile the model with the model in
                                          FILE (a path or an http/https URL),
                                          which is compiled before it (and only
                                          once, if imported by several files).
                                          In '//# OPTIONS', FILE is relative to
                                          the model's folder or URL; options of
                                          the imported files are combined with
                                          the model's. Can be repeated.
     --import-root=DIR                    Allow only local imports inside
                                          DIR, after resolving '..' and
                                          symbolic links (command line only).
                                          Can be repeated; without it, any
                                          local file can be imported.
     --public-imports                     Allow only URL imports from public
                                          addresses, not from loopback,
                                          private, or link-local ones, without
                                          a proxy (command line only).
     --import-base=URL                    The URL from which the model's text
                                          was read: its imports are relative to
                                          the URL, and can only be URLs
                                          (command line only).
  -? --help                               Display help message
  -V --version                            Print version information
     --numeric-version                    Print just the version number

The dependencies among the command line arguments are described on the model wiki.

Multiple modes can be used at the same time. For example,

clafer model.cfr -m alloy -m json -m html -m graph --self-contained --show-references --no-stats

The mode -m alloy is only the default mode if no other modes are given. When other modes are given, the mode -m alloy must be added explicitly if needed.

Additionally, [OPTIONS] can also be specified directly in the model file by inserting the following compiler directive as the first line of the file:

//# OPTIONS [OPTIONS]

for example

//# OPTIONS --keep-unused -m=alloy

The directive is only recognized on the very first line of the file and must start exactly with //# OPTIONS (no leading whitespace).

Options given at command line override the options given in the file using //# OPTIONS which, in turn, override the defaults. An option that the compiler does not know is an error.

Models in several files

A model can import other files, which are compiled together with it as one model: --import=FILE, in its //# OPTIONS or on the command line, for example, a model of one system that imports the model of a design space:

//# OPTIONS --import=design-space.cfr
System : DesignSpace

or clafer System.cfr --import=design-space.cfr. The option can be repeated.

• In //# OPTIONS, the path is relative to the file containing the directive; on the command line, to the current directory.

• The model and the imported files can be URLs (http://, https://): clafer https://example.org/models/System.cfr. An import in a model read from a URL is relative to its URL (e.g., --import=design-space.cfr reads https://example.org/models/design-space.cfr), and such a model can only import URLs, not local files. A local model can import a URL, e.g., a design space published on a server: //# OPTIONS --import=https://example.org/models/design-space.cfr. A file:// URL is a local path.

• An imported file must be a .cfr file: a URL's path, without its query, must end with .cfr, also after a redirect, and a URL served as HTML, JSON or XML (by its Content-Type) is refused. A model cannot read other files or web pages, whose text the errors would show.

• The imports are followed transitively: an imported file may import other files. Each file is compiled only once, even if several files import it, and before the files importing it. An import cycle is an error.

• All files share one namespace, as if they were concatenated: a clafer defined in one file can be used in the others, and the same top-level name in two files is an error. There are no qualified names or separate compilation.

• The outputs are named after the compiled model (System.als, System.js, ...), in the current directory for a model read from a URL. Errors give the file in which they are, as in a model of one file: Compile error at design-space.cfr:12:5.... The spans of the JSON IR name their file ({"file": "design-space.cfr", "start": …, "end": …}), and the HTML output shows each file under its name.

• The options of all files are combined: the largest --maxint, --decimal-digits, --tl and --timeout-analysis, the smallest --minint, all modes and imports; -k, -c, --check-afm and -i if any file has them, -f only if all files have it. The layout (-l, --nl) and the scope strategy (--ss) must be the same in all files. Options of the compilation rather than of the model (-o, -s, -v, --tooldir, -a, --self-contained, --add-graph, --sr, --add-comments, --meta-data) are only allowed in the compiled model and on the command line.

• A model that may come from anyone, e.g., in a web tool, is compiled with options that restrict its imports, which only the command line can give: --import-root=DIR allows local imports only inside the given folders (after resolving .. and symbolic links), --public-imports allows URL imports only from public addresses, and --import-base=URL resolves the imports of a model whose text was read from that URL. -v and --tooldir, which run tools, can only be given on the command line too: in //# OPTIONS, these options are an error.

See #100 for the design.

Unique names of clafers (UIDs)

Every clafer has a unique name, its UID, which the outputs use for it: the Alloy signatures, the Choco model, the explicit model (-m clafer), the JSON IR, the anchors of the HTML output, and the scope files (.cfr-scope). The UID of a clafer is its least-partially-qualified name, with __ between the names:

size          // root__size: another clafer named size exists
x
    size      // x__size
    color     // color: no other clafer is named so

An apostrophe in a name is _prime in the UID (a' is a_prime), and a UID that would be the same as one before it in the model gets __2, __3, .... A lookup by name, e.g., in a scope file or claferIG's i size 3, takes a UID or a qualified name, which names all the clafers whose paths end with it: size names both clafers above, x__size the one in x, and root__size the top-level one. The older form x::size and ::size is read too. A name with __ is a warning, since __ separates the names of a UID.

The outputs write the UIDs in the form their language allows: the Alloy output renames a clafer whose UID is an Alloy keyword or a name the Alloy output uses (e.g., sig is sig_1), and the variables of the Choco output are $ and the UID ($x__size).

Explicit models

-m clafer writes the explicit model of a static model to model.des.cfr: the model that chocosolver solves, with every name a UID, every card, group card, this, parent and dref written out, and nesting in braces; with --meta-data, also its scope file with every scope, model.des.cfr-scope. An explicit model is a Clafer model. Its first line, //# OPTIONS --explicit, marks it: for clafer, --explicit means -f -k -l --ss=none, so the model compiles to itself, and chocosolver reads such a model with its own parser, without the compiler.

Integer range of the Choco output

The options --minint and --maxint set the range of integers that the Choco output (-m choco) allows, for example, for a model whose attributes and their sums exceed the default range:

//# OPTIONS --minint=-1000 --maxint=1000

Without them, chocosolver chooses the range: -128..127. The options --minint and --maxint of chocosolver itself override the range of the model. A range that is too small silently restricts the instances, for example, the optimal instances of a multi-objective model; a range that is too large slows down the search. The options do not affect the Alloy output: ClaferIG sets the integer range of Alloy with its option --maxint (or --bitwidth).

Using compiler directives

Compiler directives are comments of the form

//# <directive name>

The following directives are markers of locations in the input files for different purposes. Each must appear alone on its own line, exactly as written (no leading or trailing whitespace):

• //# FRAGMENT - marks the beginning of the new module fragment.
• //# GRAPH - marks the insertion point for a graph rendering. The graph is only produced in HTML mode with the argument --add-graph.
• //# STATS - marks the insertion point for module statistics. The statistics can be omitted using the argument --no-stats.
• //# SUMMARY - shorthand for //# GRAPH and //# STATS

Developing Clafer

Here is some information about the development of the Clafer compiler.

Branching

We are following the simplified version of the successful Git branching model. The branch master is for releases and hot fixes only. The branch develop is for minor development and for integration of features from feature branches. For any substantial work, branch off from develop and create a pull request back into develop after the work is completed. We do testing and code review before merging into develop. If the develop is ahead, merge it into the feature branch and perform integration testing there. To make a release, we create a pull request from develop into master. We tag master with version numbers after each release merge.

Building

We have switched to Haskell Tool Stack. Install the tool first.

Testing

We have both automated tests and regression tests.

To run the automated tests (including both unit tests and doctests), execute

stack test

To only run unit tests, execute stack test test-suite.

To only run doctests, execute stack test doctests.

Note: it is still possible to run cabal test as previously; however, the Makefile uses stack by default.

For instructions for adding new modules to the doctest suite, see cabal integration.

To run all the automated tests and the regression tests, execute

make test

It fails if a test suite fails, or if an output of a model in test/positive differs from its regression in test/regression, has no regression, or a regression has no output. The outputs then become the new regressions: a missing regression is created, and a differing one is replaced, unless it has uncommitted changes. Review them with git diff test/regression, commit them (or restore the ones that are wrong), and run make test again.

We do test-driven development in the following way:

1. create a test case Clafer model in either test/positive or test/negative depending on whether a test case should compile successfully or return an error. For example, see a positive test case test/positive/redefinition.cfr.
2. produce the intended compiler output automatically if possible and manually fix the output. Save the intended output as a regression test case. For example, see test/regression/redefinition.cfr.reg.
3. implement the feature to reproduce the intended output: compiler the test case and execute

cd test
make diffRegressions

this will show you how the current output diverges from the intended output. A regression with uncommitted changes, such as an intended output written by hand, is kept.

Modifying the grammar

We are using a customized version of BNCF. Clone the repository and install a binary of bnfc so that it's visible in your PATH. After changing the grammar, execute

make grammar

Need help?

• Visit language's website.
• Report issues to issue tracker