by Michał Antkiewicz, Oct 27, 2026

Release 0.5.5 adds decimals, improved scope inference, and for web tools, improved UI and URLs without port numbers. Binaries for Linux x86_64 are available from the Clafer tools binary distributions page.

Decimals. The new primitive type decimal holds numbers with a fixed number of fractional digits. The bike example in ClaferMooVisualizer shows a bike whose optional features have decimal costs and weights, and the trade-off between its price and its weight. Decimals are supported by the Choco-based tools only. See the Clafer Cheat Sheet for details.

Scopes. References with unbounded multiplicities get correct scopes, and the compiler warns about large ones; partial scope files are now supported in both chocosolver and claferIG.

• clafer compiler
  • decimals (#102), also in clafer-mode.el (#103)
  • scopes of references and warnings about large scopes (#104)
• chocosolver, the Choco-based instance generator
  • uses choco-solver 6.0.2 (#38)
  • decimals (#39)
  • reads scope files (#40)
• claferIG, the Alloy-based instance generator
  • uses clafer-0.5.5 and explains why it cannot run models with decimals (#39)
  • shows its errors in ClaferIDE (#40)
  • reads partial scope files without the global scope (#41)
• claferwiki
  • uses clafer-0.5.5 (#23)
  • links to the web tools without port numbers (#24)
• VS Code extension
  • highlights decimals (#3)
  • install clafer-syntax-0.5.5.vsix from the 0.5.5 release with code --install-extension clafer-syntax-0.5.5.vsix
• Sublime Text 4 plugin
  • highlights decimals (#6)
• web tools ClaferIDE, ClaferConfigurator, and ClaferMooVisualizer
  • decimals and the bike example (common platform #9, ClaferIDE#20, ClaferConfigurator#12, ClaferMooVisualizer#29)
  • buttons to copy the URL of an example, to import it into another model (common platform #10, ClaferIDE#21, ClaferConfigurator#13, ClaferMooVisualizer#30)
  • available via URLs without port numbers (common platform #11, ClaferIDE#22, ClaferConfigurator#14, ClaferMooVisualizer#31)
• ClaferCaseStudies, made compatible with 0.5.5 and published results can be reproduced (ClaferCaseStudies#1).

The binary bundle contains clafer, claferIG, chocosolver and Alloy 6.2.0. It runs on Linux x86_64 with glibc 2.39 or newer and needs Java 21 or newer; on Windows, use it through WSL.

Live demos, now available via URLs without port numbers: the Clafer Model Wiki, the Railway Wiki, the Traffic Lights Wiki, ClaferIDE, ClaferConfigurator and ClaferMooVisualizer.

Clafer tools and web tools 0.5.4 released: models in several files

  by Michał Antkiewicz, Oct 25, 2026

This release lets a Clafer model import other models, so that a model can be split into several files, for example, a design space and one file for each system that configures it (#100). All tools report errors with the file and the position in it, the editors for Visual Studio Code and Sublime Text 4 compile models and show the errors in place, and the compiler and chocosolver get several fixes. Binaries for Linux x86_64 are available from the Clafer tools binary distributions page.

Models in several files. A model imports other files in its first line, //# OPTIONS --import=design-space.cfr, or on the command line, clafer SystemA.cfr --import=design-space.cfr. The files are compiled together as one model, with one namespace; imports are followed transitively, each file once. A model and its imports can also be URLs, so a model can import a design space published on a server. Errors are given as file.cfr:line:column, in the file in which they are. See the Clafer Cheat Sheet for the details.

• clafer compiler, release pull request (0.5.4).
  • --import, also with http:// and https:// URLs; the options of all files are combined (e.g., the largest --maxint)
  • positions as file.cfr:line:column everywhere, also in a model of one file (previously line 3 column 5); the JSON output has the source positions of clafers and expressions, with their file, and the HTML output shows each file under its name
  • options that restrict imports for models that may come from anyone, as in the web tools: --import-root, --public-imports and --import-base; an imported file must be a .cfr file
  • group cardinality opt makes its children optional again, as in the language's definition
  • a group cardinality whose lower bound the children cannot reach (e.g., xor over no children) is an error instead of being silently unconstrained
  • fixes: comments no longer count in the indentation, clafer names with apostrophes (same') work with Alloy and Choco, comments are escaped in the HTML output, and unknown options in //# OPTIONS are an error instead of being ignored
• claferIG Alloy-based instance generator, release pull request (0.5.4).
  • uses clafer-0.5.4: --import, and the options in the model's //# OPTIONS apply
  • errors and the constraints of UnSAT cores give their file and position; the command c shows each file under its name, with the scope of the first clafer
  • instances show the clafers' names from the model
• chocosolver Choco-based instance generator, release pull request (0.5.4).
  • compiles a .cfr model with its imports, and shows the compiler's errors when it does not compile
  • fixes: references refined in subclafers of an abstract clafer (a model could have no instances), and a crash with parent.parent of an optional child of a nested abstract clafer
• claferwiki, release pull request (0.5.4).
  • uses clafer-0.5.4
  • fixes the model graphs behind HTTPS proxies and the syntax highlighting of code blocks
• Clafer for Visual Studio Code, release pull request (0.5.4).
  • compiles the model when it is saved, or with Clafer: Compile, and shows the errors in the model and in the Problems panel, also in imported files
  • Clafer: Instances (Alloy) and Clafer: Instances (Choco) run claferIG and chocosolver in a terminal
  • install the .vsix file from the GitHub release with code --install-extension clafer-syntax-0.5.4.vsix
• Clafer Tools for Sublime Text, release pull request (0.5.4), now for Sublime Text 4.
  • syntax highlighting that follows the Clafer grammar, and the compiler's errors shown in the model; double-click an error's position, or press F4, to open its file
  • the instance generators run in a Terminus tab; the tools are found on PATH
  • install or update Clafer Tools with Package Control
• Web tools: ClaferIDE, ClaferConfigurator, and ClaferMooVisualizer 0.5.4, with the common platform.
  • models can import other models: the tool's examples (--import=Examples/<file>.cfr) and .cfr files on public servers; a model opened from a wiki imports relative to its URL
  • messages give positions as model.cfr:line:column
  • fixed: the welcome window appears again, and the page no longer stays grayed out on the first visit

The Linux binary bundle contains clafer, claferIG with the optimized MiniSat solver, chocosolver.jar with a chocosolver launcher, and the Alloy jars. It runs on Linux x86_64 with glibc 2.39 or newer (Ubuntu 24.04, Debian 13, Arch Linux, Fedora) and needs Java 21 or newer. On Windows, use it through WSL.

Live demos (0.5.4): the Clafer Model Wiki, the Railway Wiki, the Traffic Lights Wiki, ClaferIDE, ClaferConfigurator, and ClaferMooVisualizer.

Note: a claferwiki page cannot import other models yet; it is compiled from its own code blocks. As before, reasoning (instance generation, configuration, optimization) works for the static subset of Clafer; behavioral models can be compiled to HTML.

Clafer semantics in Lean 4

by Kacper Bąk, Oct 20, 2026

The clafer-semantics repository provides a Lean 4 formalization of Clafer’s structural semantics, based on our paper Clafer: unifying class and feature modeling. It includes reusable graph and class-diagram libraries, machine-checked proofs, and worked examples, including the paper’s telematics model. Explore the code and documentation on GitHub, or browse the repository and ask questions through DeepWiki. Contributions and feedback are welcome!

Clafer tools and web tools 0.5.3 released, migration to wiselab.uwaterloo.ca server

 by Michał Antkiewicz, Oct 16, 2026

This release moves the Clafer tools to Alloy 6.2.0 and choco-solver 4.10.18, fixes compiler bugs found with larger example models, and brings the Clafer web tools, ClaferIDE, ClaferConfigurator and ClaferMooVisualizer, back to life with live demos. Binaries for Linux x86_64 are available from the Clafer tools binary distributions page.

• clafer compiler, release pull request (0.5.3).
  • Alloy 6.2.0 replaces Alloy 4.2; the generated Alloy models are unchanged, and --validate runs all Alloy commands headlessly
  • new options --minint and --maxint (also in //# OPTIONS) set the integer range of the Choco output
  • fixes in the type checker, the Alloy and Choco outputs, references, and scope inference, among them #84, #86, and #89
• claferIG Alloy-based instance generator, release pull request (0.5.3).
  • uses clafer-0.5.3 and Alloy 6.2.0
  • comes with an optimized build of the MiniSat solver with UnSAT cores, several times faster than the one in Alloy 6.2.0
  • works around an Alloy 6.2.0 bug that made every UnSAT core empty
• claferwiki, release pull request (0.5.3).
  • uses clafer-0.5.3
  • the buttons for ClaferIDE, ClaferConfigurator, and ClaferMooVisualizer link to the host the browser used to reach the wiki
• chocosolver Choco-based instance generator, release pull request (0.5.3).
  • choco-solver 4.10.18
  • uses the integer range of the model, set with clafer's --minint and --maxint
  • time limits apply to the whole search, including the restarts of optimization
  • fixes in integer arithmetic (multiplication beyond 46340, overflow) and in the scope analysis of mutually recursive clafers
• Clafer for Visual Studio Code, release pull request (0.5.3).
  • highlighting of Clafer in Markdown fenced code blocks, as used by ClaferWiki pages
  • a snippet for the integer range of the Choco output
  • install the .vsix file from the GitHub release with code --install-extension clafer-syntax-0.5.3.vsix
• Web tools: ClaferIDE, ClaferConfigurator, and ClaferMooVisualizer 0.5.3, with the common platform, first releases since 0.4.4.
  • work with Clafer 0.5.3 and its JSON output; the web tools and the other Clafer tools now share one version
  • ClaferConfigurator and ClaferMooVisualizer report that models with temporal (behavioral) constraints are not supported; ClaferIDE edits and compiles them
  • run on current Node.js (tested with v26) and Express 4
  • upgraded browser libraries (jQuery 3.7, lodash 4.18, d3 3.5), fixing their known vulnerabilities, and hardened servers

The Linux binary bundle contains clafer, claferIG with the optimized MiniSat solver, chocosolver.jar with a chocosolver launcher, and the Alloy jars. It runs on Linux x86_64 with glibc 2.39 or newer (Ubuntu 24.04, Debian 13, Arch Linux, Fedora) and needs Java 21 or newer. On Windows, use it through WSL.

Live demos (0.5.3) have moved from t3-necsis.cs.uwaterloo.ca, which is being retired, to wiselab.uwaterloo.ca, now over HTTPS. Please update your bookmarks and links; the wikis have their pages and models as before:

• Clafer Model Wiki (formerly t3-necsis.cs.uwaterloo.ca:8091)
• Railway Wiki (formerly :8099)
• Traffic Lights Wiki (formerly :8098)
• ClaferIDE, ClaferConfigurator, and ClaferMooVisualizer, on the same ports as before

The buttons under a model in the wikis open it in the web tools.

Known issue: in the web tools, the welcome window does not appear on the first visit, and the page stays grayed out until you click it. This will be fixed in the next release.

Note: while the compiler can compile behavioral Clafer models to html, reasoning (instance generation, configuration, optimization) is currently not supported. Reasoning works for the static subset of Clafer as for 0.4.5.

Clafer compiler, IG, wiki, chocosolver, and VS Code extension 0.5.2 released

by Michał Antkiewicz, Oct 9, 2026

This is mostly a maintenance release bringing compatibility with the current Haskell compiler, Java, tools, and dependencies. It also brings the first release of Clafer support for Visual Studio Code. Binaries for Linux x86_64 are available from the Clafer tools binary distributions page.

• clafer compiler, release pull request (0.5.2).
  • compatibility with GHC 9.6.7 (Stackage LTS-22.44).
• claferIG Alloy-based instance generator, release pull request (0.5.2).
  • uses clafer-0.5.2
  • compatibility with GHC 9.6.7.
• claferwiki, release pull request (0.5.2).
  • uses clafer-0.5.2
  • compatibility with GHC 9.6.7.
  • gitit-0.16.0.2
• chocosolver Choco-based instance generator, release pull request (0.5.2).
• version aligned with the other Clafer tools (previous release: 0.4.4)
• requires Java 21 or newer
• updated build plugins and dependencies, fixing known vulnerabilities in Rhino and JUnit
• Clafer for Visual Studio Code 0.5.2, first release.
• syntax highlighting for .cfr files following the Clafer 0.5.2 grammar, including embedded Alloy and Choco blocks
• comment toggling, bracket matching, folding of nested clafers, and snippets
• ported from Clafer Tools for Sublime Text
• install the .vsix file from the GitHub release with code --install-extension clafer-syntax-0.5.2.vsix

The Linux binary bundle contains clafer, claferIG, chocosolver.jar and the Alloy jars. It runs on Linux x86_64 with glibc 2.39 or newer (Ubuntu 24.04, Debian 13, Arch Linux, Fedora) and needs Java 21 or newer. On Windows, use it through WSL.

Note: while the compiler can compile behavioral Clafer models to html, reasoning (instance generation, optimization) is currently not supported. Reasoning works for the static subset of Clafer as for 0.4.5.

Clafer compiler, IG, and wiki 0.5.1 released

 by Michał Antkiewicz, Sep 12, 2023

This is mostly a maintenance release bringing compatibility with the current Haskell compiler, tools, and dependencies.

Clafer compiler, release pull request (0.5.1).

• compatibility with GHC 9.4.6.

Clafer instance generator, release pull request (0.5.1).

• uses clafer-0.5.1
• compatibility with GHC 9.4.6.
• respect --json when using --all

Clafer wiki, release pull request (0.5.1).

• uses clafer-0.5.1
• compatibility with GHC 9.4.6.
• gitit-0.15.1.1

The Clafer model wiki, "Traffic Lights" Domain Model Example wiki, and Train Station Layout Case Study wiki are currently running clafer 0.5.1 and claferwiki-0.5.1.

New paper "Clafer: Lightweight Modeling of Structure, Behaviour, and Variability"

by Michał Antkiewicz, Jan 6, 2019

Our new paper "Clafer: Lightweight Modeling of Structure, Behaviour, and Variability" has been published in the journal The Art, Science, and Engineering of Programming.

Abstract

Embedded software is growing fast in size and complexity, leading to intimate mixture of complex architectures and complex control. Consequently, software specification requires modeling both structures and behaviour of systems. Unfortunately, existing languages do not integrate these aspects well, usually prioritizing one of them. It is common to develop a separate language for each of these facets

In this paper, we contribute Clafer: a small language that attempts to tackle this challenge. It combines rich structural modeling with state of the art behavioural formalisms. We are not aware of any other modeling language that seamlessly combines these facets common to system and software modeling.

We show how Clafer, in a single unified syntax and semantics, allows capturing feature models (variability), component models, discrete control models (automata) and variability encompassing all these aspects. The language is built on top of first order logic with quantifiers over basic entities (for modeling structures) combined with linear temporal logic (for modeling behaviour). On top of this semantic foundation we build a simple but expressive syntax, enriched with carefully selected syntactic expansions that cover hierarchical modeling, associations, automata, scenarios, and Dwyer’s property patterns.

We evaluate Clafer using a power window case study, and comparing it against other notations that substantially overlap with its scope (SysML, AADL, Temporal OCL and Live Sequence Charts), discussing benefits and perils of using a single notation for the purpose.


NOTE: Behavioral Clafer does not currently have reasoning capabilities. The compiler implements the syntax of the language and it can desugar the syntactic sugar and produce HTML rendering. For the instance generation and multi-objective optimization capabilities, it's best to use the static Clafer 0.4.5, which works best with all instance generators and web tools.

"Clafer: unifying class and feature modeling" available publicly on Springer's SharedIt

by Michał Antkiewicz, Sep 18, 2018

Our paper  "Clafer: unifying class and feature modeling" can now be accessed freely via Springer's SharedIt initiative using the following link:

https://rdcu.be/6eU3

Enjoy!

Behavioral Model Set

by Michał Antkiewicz, May 08, 2018

Clafer Model Wiki contains a few example models showcasing behavioral Clafer.

1. TrafficLight. A simple state machine model for traffic light transitions.
2. PowerWindow. Our main case study from the behavioral Clafer paper.
3. WebSocketProtocol.
4. TLS Handshake.

Clafer Compiler 0.5.0 Released

by Michał Antkiewicz, Jan 31, 2018

This release contains only the Clafer compiler 0.5.0, which now includes support for modeling behavior. The release does not include reasoning capability; for structural modeling and reasoning keep using the previous release 0.4.5.

Binary builds are available from Clafer Tools - Binary Distributions.

Clafer compiler, release pull request (0.5.0).

• support for behavioral modeling,
• ability to compile, desugar, and render to HTML behavioral models,
• test suite of behavioral models,
• experimental Alloy code generator,
• compatibility with GHC 8.2.2.

The Clafer model wiki is currently running Clafer 0.5.0.