by Michał Antkiewicz, Nov 8, 2026
This release corrects the semantics of temporal models. Clafers now have stable, readable names in all outputs, the mode -m clafer outputs explicit form which does not change when compiled again (fix point), and the web tools run on current libraries. Binaries for Linux x86_64 are available from the Clafer tools binary distributions page.
Temporal obligations end with the parent. A constraint of a clafer holds for each of its instances while the instance exists, and its obligations (X, F, G, U) last while the instance's parent exists (#107). A transition nested in its source state, e.g., [ req=down --> movingDown ] in the state movingUp, as in the power window of Juodisius et al. (2019), now takes the machine to movingDown, while the pending obligations of nested states still lapse when their enclosing state is left. A negated obligation lapses with the parent too (#110): [ !(F error) ] means [ G !error ]. Two patterns now follow their scopes, and finaltarget fixes the set of targets while finalref fixes the reference of each instance.
A formal semantics. See the key proved properties, the explanation from structure to behavior, and the lessons of the compiler. The differences of the tools from the two Clafer papers are documented in the errata of the static and the temporal semantics.
Names instead of numbers. The identifier of a clafer is its name, qualified only where the name is not unique: size, or x__size for the size in x. It was c0_size, c1_size, ..., numbered in the order of the model, so it changed when a clafer with the same name was added before it. The names are the same in the Alloy and Choco outputs, the instances, the scope files and the web tools.
Explicit models. clafer -m clafer prints a model with everything written out: every name qualified, every multiplicity and group, this, parent and dref, and, for temporal models, the transitions and patterns as the formulas they stand for. An explicit model is Clafer: it compiles to itself and gives the same instances or traces as the original. chocosolver can now read explicit static models directly, without the compiler.
- clafer compiler, release pull request (0.5.7).
- temporal models: obligations bounded by the parent (#107), also when negated (#110);
final,finalrefandfinaltargeton a clafer that inherits its reference (#109); the patternsmust follow ... betweenandmust precede ... afterfollow their scopes - names after an explicit
drefare the children of the target, e.g.,this.dref.speed(#108), and a comparison of two references compares their targets (#87) parentof a top-level clafer is the syntheticroot(#112)- new:
noclafer, the empty set, andclafer, the set of all instances (static models) - an abstract clafer that nothing inherits from has the scope 0: the power window with abstract variants of its controller gives its first trace in 2 s instead of 223 s
- the TLS handshake model has traces again, and the temporal models have no Alloy warnings
- fixes: a reference to a union of targets with a nested clafer, e.g.,
u -> Hub.p ++ fast, gives valid Alloy
- temporal models: obligations bounded by the parent (#107), also when negated (#110);
- claferIG Alloy-based instance generator, release pull request (0.5.7).
- uses clafer-0.5.7, with the corrected temporal semantics and the clafers' names in its commands and scope files
- unsat cores include the constraints of abstract clafers (#46)
- the next trace no longer repeats a trace that differs only in the references of absent clafers (#48)
- the next trace,
forkandconfigno longer log the translation of the model, which took gigabytes for large models
- chocosolver Choco-based instance generator, release pull request (0.5.7).
- reads explicit models directly, with their scopes from a
.cfr-scopefile that can now give every scope and range - instances show the clafers' names as they are
- fixes: a crash on a join into a nested abstract clafer with two systems in one model; a wrong command line prints one line and exits with 1, instead of a stack trace
- reads explicit models directly, with their scopes from a
- claferwiki, release pull request (0.5.7).
- uses clafer-0.5.7
- Clafer for Visual Studio Code, release pull request (0.5.7).
- for Clafer 0.5.7; install the
.vsixfile from the GitHub release withcode --install-extension clafer-syntax-0.5.7.vsix
- for Clafer 0.5.7; install the
- Clafer Tools for Sublime Text, release pull request (0.5.7).
- for Clafer 0.5.7
- Clafer skills for Claude Code (new), release pull request (0.5.7).
- a skill for writing, fixing and checking static and temporal Clafer models with
clafer,claferIGandchocosolver - install it with
claude plugin marketplace add gsdlab/clafer-skillsandclaude plugin install clafer@clafer
- a skill for writing, fixing and checking static and temporal Clafer models with
- Web tools: ClaferIDE, ClaferConfigurator, and ClaferMooVisualizer 0.5.7, with the common platform (#14).
- ClaferIDE: the button TL sets the maximum trace length, and Results shows the explicit model, also of temporal models
- the editor is updated to Ace 1.45 and it highlights Clafer like the VS Code extension, including the temporal keywords
- jQuery 4, Express 5 and the other libraries are npm dependencies, so their vulnerabilities are reported; the unmaintained jQuery Form, Chosen, tipsy and lodash are removed
- fixes: removing a variant in the Feature and Quality Matrix no longer breaks the Spider Chart of ClaferMooVisualizer, and clicking a variant's heading in ClaferConfigurator no longer raises an error
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.7): the Clafer Model Wiki, the Railway Wiki, the Traffic Lights Wiki, ClaferIDE, ClaferConfigurator, and ClaferMooVisualizer.
Note: temporal models and check need the Alloy-based tools: the Choco-based tools, including ClaferConfigurator and ClaferMooVisualizer, work on static models.
