[![Hackage](https://img.shields.io/hackage/v/clafer.svg)](https://hackage.haskell.org/package/clafer) [![Build Status](https://secure.travis-ci.org/gsdlab/clafer.svg)](http://travis-ci.org/gsdlab/clafer) # Clafer, the language ##### v0.5.8 [Clafer](http://clafer.org) is a general-purpose lightweight structural and behavioral modeling language developed by [GSD Lab](http://gsd.uwaterloo.ca/), [University of Waterloo](http://uwaterloo.ca), and [MODELS](http://www.itu.dk/research/models/) group at [IT University of Copenhagen](http://www.itu.dk/). 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](http://www.clafer.org/2016/06/technical-report-case-studies-on-ee.html). For examples of behavior modeling, see [Behavioral Modeling](https://wiselab.uwaterloo.ca/modelwiki/#behavioral-modeling) section on the wiki. Behavior models compile to the temporal logic of Alloy 6: [ClaferIG](https://github.com/gsdlab/claferIG) generates their traces and checks their assertions. The Choco backend supports only static models. ### Resources * [Learning Clafer](https://wiselab.uwaterloo.ca/modelwiki/#learning-clafer) * [Cheat Sheet](doc/CheatSheet.md) * [Syntax Documentation](doc/clafer.pdf) * [Grammar](src/clafer.cf) # 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](https://github.com/gsdlab/claferIG)), * Choco3-based Instance Generator and Multi-Objective Optimizer ([chocosolver](https://github.com/gsdlab/chocosolver). * Web Frontends * Clafer Integrated Development Environment ([ClaferIDE](https://github.com/gsdlab/claferIDE)), * Clafer Configurator ([ClaferConfigurator](https://github.com/gsdlab/ClaferConfigurator)), * Multi-Objective [Visualizer and Explorer](https://github.com/gsdlab/ClaferMooVisualizer), and * Clafer Wiki ([ClaferWiki](https://github.com/gsdlab/claferwiki)). ## Contributors * [Michał Antkiewicz](https://uwaterloo.ca/wise-lab/profiles/michal-antkiewicz), Main developer. * [Kacper Bak](http://gsd.uwaterloo.ca/kbak), Original developer. * [Jimmy Liang](http://gsd.uwaterloo.ca/jliang), Developer. * Luke Michael Brown, co-op student May-Aug 2013. Many improvements. * Paulius Juodisius, [customized BNFC generator](https://github.com/juodaspaulius/bnfc) and layout resolver. * [Rafael Olaechea](http://gsd.uwaterloo.ca/rolaechea), 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](https://adoptium.net) 17 or newer, 64-bit (a runtime is enough) * only needed for validating the outputs (`--validate`) and for `--ecore2clafer` * [Alloy 6.2.0](https://github.com/AlloyTools/org.alloytools.alloy/releases/tag/v6.2.0) (`alloy6.2.0.jar`) * only needed for validating the Alloy output (`--validate`) * `chocosolver.jar` from [chocosolver](https://github.com/gsdlab/chocosolver) * only needed for validating the Choco output (`--validate`) * `ecore2clafer.jar` (in this repository) * only needed for `--ecore2clafer` * [GraphViz](http://graphviz.org/) * 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=`. ### 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](https://wiselab.uwaterloo.ca/clafer-tools-binary-distributions/). 1. Download the binaries and unpack them into a `` of your choice. 2. Add the `` 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=` for `--validate` and `--ecore2clafer`. ### Installation from Hackage Clafer is available on [Hackage](https://hackage.haskell.org/package/clafer) and it can be installed using either [`cabal-install`](https://hackage.haskell.org/package/cabal-install) or [`stack`](https://haskellstack.org). #### Installation using `cabal-install` Dependencies * `ghc-9.6.7` or `ghc-9.12.4` * `cabal-install-3.10.3` or newer 1. Use [`ghcup`](https://www.haskell.org/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`](https://docs.haskellstack.org/en/stable/install_and_upgrade/) 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=`. In a checkout of this repository, `make alloy6.2.0.jar` downloads the Alloy jar. ### Installation from the source code Dependencies * [`stack`](https://github.com/commercialhaskell/stack#how-to-install) * [Git](http://git-scm.com/) On Windows * [MSYS2](http://msys2.sourceforge.net/) * it is installed automatically by `stack setup` * update MSYS2 following the [update procedure](http://sourceforge.net/p/msys2/wiki/MSYS2%20installation/): * `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 'master` are guaranteed to work well together. Development versions from branches `develop` should work well together but this might not always be the case. #### Building 1. in some `` of your choice, execute * `git clone https://github.com/gsdlab/clafer.git` 2. in `/clafer`, execute `stack setup`. This will install all dependencies, build tools, and MSYS2 (on Windows). 3. `cd ` * `make` on Linux/Mac * `stack exec make` on Windows ### Installation 1. Execute * `make install to=` on Linux/Mac * `stack exec make install to=` 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](https://github.com/gsdlab/clafer-vscode) * Sublime Text 4: [ClaferToolsST](https://github.com/gsdlab/ClaferToolsST) * VIM: [clafer-vim](https://github.com/wasowski/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 '/alloy6.2.0.jar' for Alloy models, '/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](https://wiselab.uwaterloo.ca/modelwiki/ClaferTools/CommandLineArguments). 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](https://github.com/gsdlab/clafer/issues/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 ``` //# ``` 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](http://gsd.uwaterloo.ca:8888/question/463/multi-fragment-modules). * `//# 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](http://nvie.com/posts/a-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](https://haskellstack.org/). Install the tool first. ## Testing We have both automated tests and regression tests. To run the automated tests (including both unit tests and [doctests](https://github.com/sol/doctest#readme)), 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](https://github.com/sol/doctest#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](https://github.com/gsdlab/clafer/blob/namedDrefs/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](https://github.com/gsdlab/clafer/blob/namedDrefs/test/regression/redefinition.als.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](https://github.com/juodaspaulius/bnfc). 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](http://clafer.org). * Report issues to [issue tracker](https://github.com/gsdlab/clafer/issues)