Clafer is a lightweight structural modeling language.
This is the old project website. More more up-to-date information, visit the new official website: clafer.org:
Complete documentation will be developed incrementally. For now, you can look at the following documents:
Important information: Models on this page do not work with the current Clafer Tools because of the changes to Clafer syntax:
~ should be changed to !== should be changed to =a => b else c should be changed to if a then b else c-- should be changed to //{- -} should be changed to /* */_ anymoreisSubstring are not supported in the compiler; however, the Choco3-based backend implements themThese models should be regenerated after the translators to Clafer are fixed to support the current syntax. We invite contributors to help update the tooling.
The current version of the Linux kernel model in Clafer can be found on Kacper's Thesis Page
Please consult Clafer documentation if you want to learn more about the language.
| eCos | eCos is a configurable real-time operating system. The zip file provides 116 Clafer models intended for various architectures. |
| Linux Kernel v2.6.32 | The archive contains Boolean feature model of the Linux Kernel v2.6.32 for the i386 architecture |
See the Feature Models in the Wild project for more information on these models.
Binaries for the Clafer compiler (clafer), Alloy-based instance generator (ClaferIG), and Choco-based instance generator and multi-objective optimizer (chocosolver). The web tools (IDE, wiki, configurator, MOO visualizer) need to be installed from sources. Additionally, Clafer, ClaferIG, and ClaferWiki can now be installed directly from Hackage using Cabal or Stack. See the respective READMEs for instructions.
For best experience on desktop, we recommend using Sublime Text 3 and installing the ClaferToolsST.
This release includes the compiler and ClaferIG 0.4.5, and chocosolver 0.4.4.
See the release announcement.
This release includes the compiler, ClaferIG, and chocosolver. See the release announcement.
This release includes the compiler, ClaferIG, and chocosolver. See the release announcement.
This release includes the compiler, ClaferIG, and chocosolver. ClaferChocoIG is merged into chocosolver and discontinued. See the release announcement.
This release includes the compiler and ClaferIG. ClaferChocoIG is the same as in 0.4.0. See the release announcement.
This major release includes the compiler, ClaferIG, and ClaferChocoIG. See the release announcement.
(updated on May 13)
This release includes the compiler, ClaferIG, and ClaferChocoIG. See the release announcement. The binaries include a HotFix release 0.3.10.1 of the Choco-based backend.
(updated on Mar 30)
This release includes the compiler, ClaferIG, and ClaferChocoIG. See the release announcement.
This release includes the compiler, ClaferIG, and ClaferChocoIG.
We will no longer provide the portable build since Clafer Tools is now an official Sublime Text package.
We also provide a VIM integration.
See the release announcement.
We are moving to a staged release model. First, Haskell-based tools, including the compiler, IG, and the wiki, followed by backends Choco3-based and Z3-based, finally followed by the web tools. The 0.3.6.1 release includes the compiler, all backends, and the wiki.
Important Notice: The zip file includes a distribution of Z3 SMT solver. In order to use it for commercial applications, a separate license must by purchased. It is; however, free for research and academic purposes. See Z3 license.
Additionally, we created w wiki page Guidelines for feature modeling using Clafer.
Installation and Running - see the included README files. If the READMEs don't help or you need a build for Mac or 32 bit linux, email Michał Antkiewicz.
Older binaries are available from ClaferIG Downloads Page.
A presentation introducing Clafer, comparing concept modeling in OWL and Clafer, and presenting the details of a translation of the tutorial Pizza example from OWL to Clafer is available for viewing here.
To view, hoover mouse over the lower-right corner of the presentation More and select Fullscreen. Use right arrow to advance, left arrow to go back. Click on an element to zoom in. Click on empty space to zoom out. Use mouse wheel to zoom in and out. Use drag & drop to pan.
The translation of the Pizza example into Clafer is attached below (pizza.cfr). The translation is almost complete: it is missing IceCream and other inconsistent parts, and a few minor details.
The file pizza-only-Veneziana.als is a translation of the Clafer model to alloy which can be run using Alloy 4 analyzer (it gives semantics to the Clafer model in terms of alloy). The translation omits all unused abstract pizza types except for Veneziana which is instantiated.
To analyze and instantiate the model, open the file in Alloy 4 analyzer, press the buttons execute and, after analysis is completed, show. This will visualize an instance of the model found by Alloy that conforms to all constraints. The Alloy model represents a lower bound of the space of instances, that is, Alloy may create more instances than necessary to satisfy the constraints.
Instead of the standard graph visualization, the instance can also be viewed as a tree by clicking on the button Tree in the instance viewer. Subsequent instances can be generated by pressing Next.
| Attachment | Size |
|---|---|
| pizza-only-Veneziana.als | 21.68 KB |
| pizza.cfr | 7.95 KB |
The purpose of the attached document is to demonstrate how a complex family of concepts can be modeled using Clafer. The document presents an exact record of the actual analysis performed by the author and shows a typical evolution of the concept definitions when using the “concrete-to-abstract” modeling approach.
Basic knowledge of Clafer is assumed. Refer to Concept Modeling Using Clafer - Tutorial for a thorough introduction.
| Attachment | Size |
|---|---|
| 2011.08.24 Scotiabank mortgages in Clafer v.3.pdf | 973.56 KB |
We have evaluated Clafer on hundreds realistic examples of feature models, meta-models, feature-based templates, and domain models. For each model, we performed instance finding analysis, since many other analyses can be reduced to this problem. For slices of meta-models and feature-based templates element liveness was verified, because it is another example of a non-trivial analysis. We consider our results promising, since we obtained acceptable timings (within seconds) without fully exploiting the potential of Alloy.
The attached archive contains Clafer (*.cfr files) and corresponding Alloy (*.als files) models.
| Attachment | Size |
|---|---|
| models.zip | 1.42 MB |
We have evaluated Clafer on over 60 realistic examples of feature models, meta-models, and feature-based templates. For each model, we performed instance finding analysis, since many other analyses can be reduced to this problem. For slices of meta-models and feature-based templates element liveness was verified, because it is another example of a non-trivial analysis. We consider our results promising, since we obtained acceptable timings (within seconds) without fully exploiting the potential of Alloy.
The attached files contain Clafer (*.cfr files) and corresponding Alloy (*.als files) models.
Language documentation is available here.
| Attachment | Size |
|---|---|
| fm-splot.tar.gz | 304.26 KB |
| meta-models.tar.gz | 15.73 KB |
| fbmts.tar.gz | 17.63 KB |
This page contains the telematics example introduced in our technical report Feature and Class Models in Clafer: Mixed, Specialized, and Coupled.
The example is also available on the Clafer Model Wiki.
| Attachment | Size |
|---|---|
| telematics.tar.gz | 151.05 KB |