Clafer is a general-purpose lightweight structural and behavioral modeling language developed by GSD Lab, University of Waterloo, and MODELS group at IT University of Copenhagen. Clafer can be used for modeling of static hierarchical structures and for modeling the change of the structures over time (behavior). Clafer allows for naturally expressing variability in both the structure and behavior. The main goal of Clafer is to make modeling more accessible to a wider range of users and domains.
There are many possible applications of Clafer; however, three are prominent:
-
Product-Line Architecture Modeling - aims at representing and managing commonality and variability of assets in product lines and creating and verifying product configurations. Clafer naturally supports multi-staged configuration. By applying modeling patterns, Clafer can be used for feature modeling, architecture modeling (e.g., by applying EAST-ADL), and behavior modeling (e.g., hierarchical state transition systems). All these aspects naturally include variability.
-
Multi-Objective Product Optimization - aims at finding a set of products in a given product line that are optimal with respect to a set of objectives. Clafer multi-objective optimizer generates a Pareto front of optimal product configurations.
-
Domain Modeling - aims at improving the understanding of the problem domain in the early stages of software development and determining the requirements with fewer defects. This is also known as Concept Modeling or Ontology Modeling.
-
Concept Behavior Modeling - aims at eliciting how a structure of a concept evolved over time and checking properties of possible behaviors.
May applications actually combine the three. For example, see Technical Report: Case Studies on E/E Architectures for Power Window and Central Door Locks Systems.
For examples of behavior modeling, see Behavioral Modeling section on the wiki. Behavior models compile to the temporal logic of Alloy 6: ClaferIG generates their traces and checks their assertions. The Choco backend supports only static models.
Clafer compiler provides a reference implementation of Clafer, the language. It translates models in Clafer to other formats (e.g., Alloy, JSON, JS, HTML, DOT) to allow for reasoning and processing with existing tools (Alloy Analyzer, Choco3, and GraphViz).
Currently, the compiler is used by
- Backends
- Alloy-based Instance Generator (ClaferIG),
- Choco3-based Instance Generator and Multi-Objective Optimizer (chocosolver.
- Web Frontends
- Clafer Integrated Development Environment (ClaferIDE),
- Clafer Configurator (ClaferConfigurator),
- Multi-Objective Visualizer and Explorer, and
- Clafer Wiki (ClaferWiki).
- Michał Antkiewicz, Main developer.
- Kacper Bak, Original developer.
- Jimmy Liang, Developer.
- Luke Michael Brown, co-op student May-Aug 2013. Many improvements.
- Paulius Juodisius, customized BNFC generator and layout resolver.
- Rafael Olaechea, Multi-Objective Optimization extensions.
Clafer can be installed from a binary distribution (preferred), from Hackage, and from the source code.
Regardless of the installation method, the following are
Optional:
- Java Platform (JDK) v17+, 64bit
- only needed for running Alloy validation
- Alloy 6.2.0 (
alloy6.2.0.jar)- only needed for Alloy output validation
- GraphViz
- the program
dotis needed only in thehtmlmode for SVG graph generation
- the program
Binary distributions of the release 0.5.4 of Clafer Tools for Windows, Mac, and Linux, can be downloaded from Clafer Tools - Binary Distributions.
- Download the binaries and unpack
<target directory>of your choice. - Add the
<target directory>to your system path so that the executables can be found.
Clafer is available on Hackage and it can be installed using either stack or cabal-install.
Stack is the only requirement: no other Haskell tooling needs to be installed because stack will automatically install everything that's needed.
- Install
stack- (first time only) Execute
stack setup.
- (first time only) Execute
- Execute
stack install clafer.
Dependencies
- Use
ghcupto installghc,cabal, andstack cabal updatecabal install alex happycabal install exe:clafer- on Windows
cd C:\Users\<user>\AppData\Roaming\cabal\x86_64-windows-ghc-9.6.7\clafer-0.5.4 - on Linux
cd ~/.cabal/bin/ - to automatically download the Alloy jar, execute
make alloy6.2.0.jar,- move
alloy6.2.0.jarto the location of the clafer executable.
Dependencies
On Windows
- MSYS2
- it is installed automatically by
stack setup - update MSYS2 following the update procedure:
stack exec pacman -- -Systack exec pacman -- --needed -S bash pacman pacman-mirrors msys2-runtime- restart shell if the runtime was updated
stack exec pacman -- -Su
stack exec pacman -- -S make wget unzip diffutils
- it is installed automatically by
All related projects are following the simultaneous release model.
The branch master contains releases, whereas the branch develop contains code under development.
When building the tools, the branches should match.
Releases from branches 'masterare guaranteed to work well together. Development versions from branchesdevelop` should work well together but this might not always be the case.
- in some
<source directory>of your choice, execute
git clone git://github.com/gsdlab/clafer.git
- in
<source directory>/clafer, executestack setup. This will install all dependencies, build tools, and MSYS2 (on Windows). cd <source directory>
makeon Linux/Macstack exec makeon Windows
- Execute
make install to=<target directory>on Linux/Macstack exec make install to=<target directory>on Windows
On Windows, use
/with themakecommand instead of\, e.g.,make install to=/c/clafer-tools-0.5.4/
- VS Code: clafer-vscode
- Sublime Text 4: ClaferToolsST
- VIM: clafer-vim
(As printed by clafer --help)
Clafer 0.5.7
clafer [OPTIONS] [FILE]
Common flags:
-m --mode=CLAFERMODE Generated output type. Available
CLAFERMODEs are: 'alloy' (default,
Alloy 6); 'json' (intermediate
representation of Clafer model);
'clafer' (the explicit model, with
everything written out, as Choco
solves it; a temporal model with its
temporal modifiers and operators,
which only Alloy solves);
'html' (original model in HTML);
'graph' (graphical representation
written in DOT language); 'cvlgraph'
(cvl notation representation written
in DOT language); 'choco' (Choco
constraint programming solver).
Multiple modes can be specified at
the same time, e.g., '-m alloy -m
html'.
-o --console-output Output code on console.
-i --flatten-inheritance Flatten inheritance ('alloy' mode
only).
--timeout-analysis=INT Timeout for analysis.
-l --no-layout Don't resolve off-side rule layout.
-n --nl --new-layout Use new fast layout resolver
(experimental).
-c --check-duplicates Check duplicated clafer names in
the entire model.
-f --skip-resolver The names of the clafers are their
UIDs, as in an explicit model: skip
renaming them. Names must be unique;
they are still resolved and checked.
--explicit The model is an explicit model, as
'clafer -m clafer' prints it, with
every name a UID and every card
written out, and its scopes in its
scope file. Shorthand for -f -k -l
--ss=none.
-k --keep-unused Keep uninstantated abstract clafers
('alloy' mode only).
-s --no-stats Don't print statistics.
-v --validate Validate outputs of all modes, and
exit with 1 if a tool rejects one.
Uses '<tooldir>/alloy6.2.0.jar' for
Alloy models,
'<tooldir>/chocosolver.jar' for Choco
models, dot for graphs, and clafer
itself for explicit models, which
must compile to themselves. Use
'--tooldir' to override the default
location ('.') of these tools.
--tooldir=DIR Specify the tools directory
('validate' only). Default: '.'
(current directory).
-a --alloy-mapping Generate mapping to Alloy source
code ('alloy' mode only).
--self-contained Generate a self-contained html
document ('html' mode only).
--add-graph Add a graph to the generated html
model ('html' mode only). Requires
the "dot" executable to be on the
system path.
--sr --show-references Whether the links for references
should be rendered. ('html' and
'graph' modes only).
--add-comments Include comments from the source
file in the html output ('html' mode
only).
-e --ecore2clafer Translate an ECore model into
Clafer.
--tl=INT --trace-len Define the maximum trace length.
--ss=SCOPESTRATEGY --scope-strategy Use scope computation strategy:
none or simple (default).
--check-afm --afm Throws an error if the cardinality
of any of the clafers is above 1.
--meta-data Generate a 'fully qualified
name'-'least-partially-qualified
name'-'unique ID' map ('.cfr-map').
In Alloy and Choco modes, generate
the scopes map ('.cfr-scope'); in
Clafer mode, the explicit model's
scope file with every scope
('.des.cfr-scope').
--minint=INT Smallest integer value ('choco'
mode only). Default: -128, chosen by
chocosolver.
--maxint=INT Largest integer value ('choco' mode
only). Default: 127, chosen by
chocosolver.
--decimal-digits=INT Number of fractional digits of
decimals ('choco' mode only).
Default: the most fractional digits
of the model's decimal literals.
--import=FILE Compile the model with the model in
FILE (a path or an http/https URL),
which is compiled before it (and only
once, if imported by several files).
In '//# OPTIONS', FILE is relative to
the model's folder or URL; options of
the imported files are combined with
the model's. Can be repeated.
--import-root=DIR Allow only local imports inside
DIR, after resolving '..' and
symbolic links (command line only).
Can be repeated; without it, any
local file can be imported.
--public-imports Allow only URL imports from public
addresses, not from loopback,
private, or link-local ones, without
a proxy (command line only).
--import-base=URL The URL from which the model's text
was read: its imports are relative to
the URL, and can only be URLs
(command line only).
-? --help Display help message
-V --version Print version information
--numeric-version Print just the version number
The dependencies among the command line arguments are described on the model wiki.
Multiple modes can be used at the same time. For example,
clafer model.cfr -m alloy -m json -m html -m graph --self-contained --show-references --no-stats
The mode -m alloy is only the default mode if no other modes are given. When other modes are given, the mode -m alloy must be added explicitly if needed.
Additionally, [OPTIONS] can also be specified directly in the model file by inserting the following compiler directive as the first line of the file:
//# OPTIONS [OPTIONS]
for example
//# OPTIONS --keep-unused -m=alloy
The directive is only recognized on the very first line of the file and must start exactly with //# OPTIONS (no leading whitespace).
Options given at command line override the options given in the file using //# OPTIONS which, in turn, override the defaults.
An option that the compiler does not know is an error.
A model can import other files, which are compiled together with it as one model: --import=FILE, in its //# OPTIONS or on the command line, for example, a model of one system that imports the model of a design space:
//# OPTIONS --import=design-space.cfr
System : DesignSpace
or clafer System.cfr --import=design-space.cfr. The option can be repeated.
-
In
//# OPTIONS, the path is relative to the file containing the directive; on the command line, to the current directory. -
The model and the imported files can be URLs (
http://,https://):clafer https://example.org/models/System.cfr. An import in a model read from a URL is relative to its URL (e.g.,--import=design-space.cfrreadshttps://example.org/models/design-space.cfr), and such a model can only import URLs, not local files. A local model can import a URL, e.g., a design space published on a server://# OPTIONS --import=https://example.org/models/design-space.cfr. Afile://URL is a local path. -
An imported file must be a
.cfrfile: a URL's path, without its query, must end with.cfr, also after a redirect, and a URL served as HTML, JSON or XML (by itsContent-Type) is refused. A model cannot read other files or web pages, whose text the errors would show. -
The imports are followed transitively: an imported file may import other files. Each file is compiled only once, even if several files import it, and before the files importing it. An import cycle is an error.
-
All files share one namespace, as if they were concatenated: a clafer defined in one file can be used in the others, and the same top-level name in two files is an error. There are no qualified names or separate compilation.
-
The outputs are named after the compiled model (
System.als,System.js, ...), in the current directory for a model read from a URL. Errors give the file in which they are, as in a model of one file:Compile error at design-space.cfr:12:5.... The spans of the JSON IR name their file ({"file": "design-space.cfr", "start": …, "end": …}), and the HTML output shows each file under its name. -
The options of all files are combined: the largest
--maxint,--decimal-digits,--tland--timeout-analysis, the smallest--minint, all modes and imports;-k,-c,--check-afmand-iif any file has them,-fonly if all files have it. The layout (-l,--nl) and the scope strategy (--ss) must be the same in all files. Options of the compilation rather than of the model (-o,-s,-v,--tooldir,-a,--self-contained,--add-graph,--sr,--add-comments,--meta-data) are only allowed in the compiled model and on the command line. -
A model that may come from anyone, e.g., in a web tool, is compiled with options that restrict its imports, which only the command line can give:
--import-root=DIRallows local imports only inside the given folders (after resolving..and symbolic links),--public-importsallows URL imports only from public addresses, and--import-base=URLresolves the imports of a model whose text was read from that URL.-vand--tooldir, which run tools, can only be given on the command line too: in//# OPTIONS, these options are an error.
See #100 for the design.
Every clafer has a unique name, its UID, which the outputs use for it: the Alloy signatures, the Choco model, the explicit model (-m clafer), the JSON IR, the anchors of the HTML output, and the scope files (.cfr-scope). The UID of a clafer is its least-partially-qualified name, with __ between the names:
size // root__size: another clafer named size exists
x
size // x__size
color // color: no other clafer is named so
An apostrophe in a name is _prime in the UID (a' is a_prime), and a UID that would be the same as one before it in the model gets __2, __3, .... A lookup by name, e.g., in a scope file or claferIG's i size 3, takes a UID or a qualified name, which names all the clafers whose paths end with it: size names both clafers above, x__size the one in x, and root__size the top-level one. The older form x::size and ::size is read too. A name with __ is a warning, since __ separates the names of a UID.
The outputs write the UIDs in the form their language allows: the Alloy output renames a clafer whose UID is an Alloy keyword or a name the Alloy output uses (e.g., sig is sig_1), and the variables of the Choco output are $ and the UID ($x__size).
-m clafer writes the explicit model of a static model to model.des.cfr: the model that chocosolver solves, with every name a UID, every card, group card, this, parent and dref written out, and nesting in braces; with --meta-data, also its scope file with every scope, model.des.cfr-scope. An explicit model is a Clafer model. Its first line, //# OPTIONS --explicit, marks it: for clafer, --explicit means -f -k -l --ss=none, so the model compiles to itself, and chocosolver reads such a model with its own parser, without the compiler.
The options --minint and --maxint set the range of integers that the Choco output (-m choco) allows, for example, for a model whose attributes and their sums exceed the default range:
//# OPTIONS --minint=-1000 --maxint=1000
Without them, chocosolver chooses the range: -128..127. The options --minint and --maxint of chocosolver itself override the range of the model. A range that is too small silently restricts the instances, for example, the optimal instances of a multi-objective model; a range that is too large slows down the search. The options do not affect the Alloy output: ClaferIG sets the integer range of Alloy with its option --maxint (or --bitwidth).
Compiler directives are comments of the form
//# <directive name>
The following directives are markers of locations in the input files for different purposes. Each must appear alone on its own line, exactly as written (no leading or trailing whitespace):
//# FRAGMENT- marks the beginning of the new module fragment.//# GRAPH- marks the insertion point for a graph rendering. The graph is only produced in HTML mode with the argument--add-graph.//# STATS- marks the insertion point for module statistics. The statistics can be omitted using the argument--no-stats.//# SUMMARY- shorthand for//# GRAPHand//# STATS
Here is some information about the development of the Clafer compiler.
We are following the simplified version of the successful Git branching model.
The branch master is for releases and hot fixes only.
The branch develop is for minor development and for integration of features from feature branches.
For any substantial work, branch off from develop and create a pull request back into develop after the work is completed.
We do testing and code review before merging into develop.
If the develop is ahead, merge it into the feature branch and perform integration testing there.
To make a release, we create a pull request from develop into master.
We tag master with version numbers after each release merge.
We have switched to Haskell Tool Stack. Install the tool first.
We have both automated tests and regression tests.
To run the automated tests (including both unit tests and doctests), execute
stack test
To only run unit tests, execute stack test test-suite.
To only run doctests, execute stack test doctests.
Note: it is still possible to run
cabal testas previously; however, theMakefileusesstackby default.
For instructions for adding new modules to the doctest suite, see cabal integration.
To run all the automated tests and the regression tests, execute
make test
It fails if a test suite fails, or if an output of a model in test/positive differs from its regression in test/regression, has no regression, or a regression has no output.
The outputs then become the new regressions: a missing regression is created, and a differing one is replaced, unless it has uncommitted changes.
Review them with git diff test/regression, commit them (or restore the ones that are wrong), and run make test again.
We do test-driven development in the following way:
- create a test case Clafer model in either
test/positiveortest/negativedepending on whether a test case should compile successfully or return an error. For example, see a positive test case test/positive/redefinition.cfr. - produce the intended compiler output automatically if possible and manually fix the output. Save the intended output as a regression test case. For example, see test/regression/redefinition.cfr.reg.
- implement the feature to reproduce the intended output: compiler the test case and execute
cd test
make diffRegressions
this will show you how the current output diverges from the intended output. A regression with uncommitted changes, such as an intended output written by hand, is kept.
We are using a customized version of BNCF.
Clone the repository and install a binary of bnfc so that it's visible in your PATH.
After changing the grammar, execute
make grammar
- Visit language's website.
- Report issues to issue tracker