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.

Best paper award for SoSyM 2017

by Michał Antkiewicz, Sep 22, 2017

Our paper "Synthesis and exploration of multi-level, multi-perspective architectures of automotive embedded systems" published in the Software and Systems Modeling journal has won one of the six best paper awards for year 2017.

Congratulations to our students Jordan Ross, Jimmy Liang, and Alexandr Murashkin!

The work presented in the paper was Jordan's master's thesis work based on previous master's thesis work by Alexandr. Jimmy made it all possible by contributing chocosolver, the scalable Clafer backend.

Clafer Tutorial at CBSOFT'17

by Michał Antkiewicz, Sep 18, 2017

Today, prof. Andrzej Wąsowski (IT University of Copenhagen) delivered a 3.5h tutorial entitled "Domain Modeling and Variability Modeling in Clafer" at CBSOFT'17, Fortaleza, Brazil.

The tutorial introduced the Clafer language and the participants used the online Clafer tools to write and analyze their models.

Abstract

Variability Modeling is a key activity in implementing Software Product Lines and highly configurable systems. Clafer is a small language for domain modeling with excellent support for variability modeling.  In this tutorial, we will introduce the basics of variability modeling and the basics of the  Clafer language.  Most of the tutorial will be interactive. The participants will use online Clafer tools to create basic models and analyze them, including consistency checking of models, and finding optimal configurations. Time permitting, we will discuss extensions of Clafer beyond structural domain modeling.

Behavioral Clafer

by Michał Antkiewicz, Mar 21, 2017

Behavioral Clafer was finally merged into develop, which means it will be part of the next release: 0.5.0.

That is a huge step for Clafer because it adds capability of modeling how the structures evolve over time. In that context, all possible instances of a static Clafer model can be considered as all possible snapshots (statespace) of a dynamic model. Also, the constraints in a static model can be considered as global invariants in a dynamic model.

The Clafer Model Wiki and the Clafer Tools (Visualizer, Configurator, and IDE) have been updated to use the 0.5.0 version; however, there is currently no reasoning support for the behavioral constructs. The models can only be compiled, desugared, and rendered to HTML.

We added two example models to showcase the behavioural modeling style:

• Simplified Web Socket Protocol - a simple model showcasing state modeling, trace specification, and the intended traces.
• Power Window - a complex model showcasing modeling structure and behaviour with variability: feature modeling, component modeling, statemachine modeling, variability in behaviour using alphabet variability, inheritance, and strategy pattern, and (safety) properties.