by Michał Antkiewicz, Nov 1, 2026
This release brings support for temporal models. Behavioural Clafer compiles to the temporal logic of Alloy 6.2, and claferIG and ClaferIDE now run these models and let you explore their traces. Assertions can be checked with counterexamples, for static and temporal models. Solutions can be shown as graphs, and the editors get an outline and temporal snippets. Binaries for Linux x86_64 are available from the Clafer tools binary distributions page.
Temporal models. A model with temporal operators, or with the modifiers initial and final, is dynamic: its solutions are traces, sequences of states that change over time, each of which is an instance. A trace ends with a loop back to an earlier state, and repeats from there forever. The semantics follows Juodisius et al., Clafer: Lightweight Modeling of Structure, Behaviour, and Variability (2019). Try the coffee machine example in ClaferIDE, which shows three modeling styles: transitions, temporal logic and specification patterns. The traffic light in the Clafer Model Wiki is another example. See the Clafer Cheat Sheet for details. Temporal models are supported by the Alloy-based tools only.
Exploring traces. In claferIG and ClaferIDE, the next solution is a different trace, from the shortest up to the maximum trace length. Diff shows each state as its changes from the previous one. Fork gives another trace with the same first states: what else can happen from there? Next Config gives a trace with another configuration, for example, other final features of a product line.
Checking assertions. Until now, claferIG ignored assertions. The command check of claferIG and the button Check of ClaferIDE now check all the assertions of a model, or those on one line, also the nested ones, and give a counterexample of each one that fails. The check is bounded: no counterexample means that the assertion holds within the scopes and the maximum trace length, not in general.
- clafer compiler, release pull request (0.5.6).
- temporal models compile to the temporal logic of Alloy 6.2: mutable relations (
var) and the operatorsalways,after,eventuallyanduntil - a chain of transitions is a sequence:
a --> b --> cisa => X (b && X c), e.g., the scenario[ initially (green --> yellow --> red) ] - assertions nested in a clafer hold for each of its instances, and a line can have several assertions
- the constraints and cardinalities of temporal models are facts of their own, so that unsat cores can name them
- enumerations are final in dynamic models (#92)
- fixes:
parentof a quantified variable, partially qualified names match whole names, and the HTML and graph outputs show expressions with the parentheses that the grammar requires
- temporal models compile to the temporal logic of Alloy 6.2: mutable relations (
- claferIG Alloy-based instance generator, release pull request (0.5.6), and #45.
- uses clafer-0.5.6: runs temporal models, with
--tland the commandtlfor the maximum trace length - the commands
d(diff),fork <state>andconfig;configalso gives a static model's instance with another structure - the command
checkorcheck <line>checks assertions (#30) - the command
dotand the option--dotgive solutions as Graphviz graphs: for a trace, its states and transitions - unsat cores and near-miss examples, also for dynamic models with no traces
-nlimits the number of instances saved by--all(#43)- each session keeps Alloy's temporary files in its own folder, which is removed when it ends; the logs of large models used to fill the temporary folder of the system
- uses clafer-0.5.6: runs temporal models, with
- chocosolver Choco-based instance generator, release pull request (0.5.6).
- claferwiki, release pull request (0.5.6).
- uses clafer-0.5.6: models and their graphs show expressions with the required parentheses
- Clafer for Visual Studio Code, release pull request (0.5.6).
- outline of the clafers of a model: the Outline view, breadcrumbs and Go to Symbol in Editor
- snippets for temporal models, e.g.,
statemachine,transitionandscenario - Clafer: Instances (Alloy) also runs temporal models, and a new run replaces the terminal of the previous run of that model
- install the
.vsixfile from the GitHub release withcode --install-extension clafer-syntax-0.5.6.vsix
- Clafer Tools for Sublime Text, release pull request (0.5.6).
- for Clafer 0.5.6: the Alloy instance generator also runs temporal models
- Web tools: ClaferIDE, ClaferConfigurator, and ClaferMooVisualizer 0.5.6, with the common platform (#12, #13).
- ClaferIDE runs temporal models with the Alloy-based generator, with the buttons Diff (on by default), Fork, Next Config and Check, and the new coffee machine example
- ClaferIDE: the view Compiled Formats is now Results, with a Solution Graph of the latest instance or trace, and a Model Graph
- ClaferMooVisualizer: a click on a bubble or a line of the parallel coordinates selects its variant every time
- fixed: the help pages have their styles and images again
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.6): 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.
