# Clafer Instance Generator ##### v0.5.8 [Clafer](http://clafer.org) is a powerful (equivalent to first-order predicate logic) yet lightweight structural modeling language. Despite simplicity and conciseness of Clafer, writing correct models remains challenging due to hard-to-predict interactions among all constraints expressed in the model. **Clafer instance generator** (ClaferIG) is an interactive tool that generates instances and counter examples of concrete clafers in a Clafer model. If the concrete clafers do not have contradicting constraints, the generator produces valid instance data. Otherwise, the generator produces an unsatisfiable core which included all contradicting constraints and generates a counter example by removing one constraint from the core. The generator can potentially produce many instances if the concrete clafers are not fully specialized. The generator produces different instances on-demand. With these capabilities, the instance generator can be used for debugging models: checking the consistency of the model and detecting under- and overconstraining of the model. The instance generator can also be used programmatically via API (the command line and interactive session interfaces only use the API). For more information, see [technical report](http://gsd.uwaterloo.ca/node/462). ## Contributors * [Michał Antkiewicz](https://uwaterloo.ca/wise-lab/profiles/michal-antkiewicz), Main developer. * [Jimmy Liang](http://gsd.uwaterloo.ca/jliang), Original developer. * Luke Michael Brown, co-op student May-Aug 2013. Many improvements. ## Getting the Clafer Instance Generator ClaferIG can be installed from a binary distribution (preferred), from Hackage, and from the source code. ### Dependencies for running Regardless of the installation method, the following are required: * [Java](https://adoptium.net) 17 or newer, 64-bit (a runtime is enough) * `alloyIG.jar` (in this repository) and [Alloy 6.2.0](https://github.com/AlloyTools/org.alloytools.alloy/releases/tag/v6.2.0) (`alloy6.2.0.jar`), in the directory of the `claferIG` executable * Alloy includes the MiniSat solver with UnSAT cores for Linux and macOS; on Windows, ClaferIG generates instances but cannot compute UnSAT cores and near-miss instances * the MiniSat build in Alloy 6.2.0 is several times slower than the one in Alloy 4.2 because it is compiled without optimization ([AlloyTools/org.alloytools.alloy#352](https://github.com/AlloyTools/org.alloytools.alloy/issues/352)); ClaferIG uses `lib/libminisatprover.so` (`.dylib` on macOS) in the directory of its executable instead, if present. `make` builds it from source. The Clafer compiler is part of `claferIG`: the executable `clafer` is not needed. ClaferIG looks for the jars and `lib/` in the directory of its executable, after following symbolic links: put them next to the file itself, not next to a link to it. ### Installation from binaries Binary distributions of Clafer Tools (`clafer`, `claferIG`, and `chocosolver` with the jars they need; Linux x86-64 for the recent releases) can be downloaded from [Clafer Tools - Binary Distributions](https://wiselab.uwaterloo.ca/clafer-tools-binary-distributions/). They include `alloyIG.jar`, `alloy6.2.0.jar`, and the optimized `lib/libminisatprover.so`. 1. Download the binaries and unpack them into a `` of your choice. 2. Add the `` to your system path so that the executables can be found. ### Installation from Hackage ClaferIG is available on [Hackage](https://hackage.haskell.org/package/claferIG) and it can be installed using either [`cabal-install`](https://hackage.haskell.org/package/cabal-install) or [`stack`](https://haskellstack.org). Either way, the jars are installed separately, into the directory of the executable. #### Installation using `cabal-install` Dependencies * `ghc-9.6.7` or `ghc-9.12.4` * `cabal-install-3.10.3` or newer 1. Use [`ghcup`](https://www.haskell.org/ghcup/) to install `ghc` and `cabal` 2. `cabal update` 3. `cabal install claferIG --install-method=copy --installdir=` 4. In the ``, execute * `curl -fsSL -o alloy6.2.0.jar https://github.com/AlloyTools/org.alloytools.alloy/releases/download/v6.2.0/org.alloytools.alloy.dist.jar` * `curl -fsSL -O https://github.com/gsdlab/claferIG/raw/master/alloyIG.jar` 5. Add the `` to your system path. `--install-method=copy` is needed: by default, `cabal install` puts a symbolic link into its `bin` directory, and ClaferIG would look for the jars in cabal's package store, where the link points. #### Installation using `stack` ClaferIG is not part of Stackage snapshots, so give the versions of both packages; their dependencies come from the snapshot. This release is tested with the snapshot `nightly-2026-11-11`: 1. [Install `stack`](https://docs.haskellstack.org/en/stable/install_and_upgrade/) 2. `stack install claferIG-0.5.8 clafer-0.5.8 --resolver nightly-2026-11-11` 3. In `~/.local/bin` (``stack path --local-bin``), where the executable is copied, download the jars as in step 4 above. ### Installation from the source code Dependencies * [`stack`](https://haskellstack.org) * the source code of the [Clafer compiler](https://github.com/gsdlab/clafer) in a sibling directory `clafer` (`stack.yaml` builds it from `../clafer`) * On Linux, the development files of `gmp`, `ncurses` and `zlib`, needed to build ClaferIG and its dependencies * on Ubuntu, execute `sudo apt install libgmp-dev libncurses-dev zlib1g-dev` On Windows * [MSYS2](http://msys2.sourceforge.net/) * it is installed automatically by `stack setup` (see Building below) * update MSYS2 packages * follow [III. Updating packages](http://sourceforge.net/p/msys2/wiki/MSYS2%20installation/) but always execute `stack exec pacman -- ` * execute * `stack exec pacman -- -S make diffutils` ### Important: branches must correspond 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 'master` are guaranteed to work well together. Development versions from branches `develop` should work well together but this might not always be the case. ### Building 1. in some ``, execute `git clone https://github.com/gsdlab/clafer.git` (check out the same branch as ClaferIG) 2. in the same ``, execute `git clone https://github.com/gsdlab/claferIG.git` 3. in `/claferIG`, execute `stack setup`. This will install all dependencies, build tools, and MSYS2 (on Windows). 4. `cd /claferIG` * `make` * this also builds the optimized MiniSat solver with UnSAT cores in `lib/`, which needs `git`, `cmake`, a C++ compiler and a JDK ### Installation 1. execute `make install to=` #### Note: > On Windows, use `/` with the `make` command instead of `\`, e.g., `make install to=/c/clafer-tools-0.5.4/` ## Integration with text editors * VS Code: [clafer-vscode](https://github.com/gsdlab/clafer-vscode) * Sublime Text 4: [ClaferToolsST](https://github.com/gsdlab/ClaferToolsST) * VIM: [clafer-vim](https://github.com/wasowski/clafer-vim) # Usage Clafer Instance Generator can be used in interactive and batch modes, as well as, an API. ## Command-line Usage (As printed by `claferIG --help`) ``` ClaferIG 0.5.8 claferig [OPTIONS] FILE Common flags: --all[=INTEGER] Saves all instances or a counterexample. Reads scopes from a `.cfr.scope` file or uses the provided global scope. -n=INTEGER Specify the maximum number of instances saved by --all. --savedir=FILE Specify the directory for storing saved files. --import=FILE Compile the model together with the given file or URL, which is relative to the current directory. A model also imports files with --import in its //# OPTIONS directive, relative to its own folder or URL. --import-root=DIR Allow only local imports inside DIR, after resolving '..' and symbolic links (command line only). Can be repeated. --public-imports Allow only URL imports from public addresses (command line only). --import-base=URL The URL from which the model's text was read: its imports are relative to the URL (command line only). --alloysolution=FILE Convert Alloy solution to a Clafer solution. -b --bitwidth=INTEGER Set the bitwidth for integers. -m --maxint=INTEGER Set the bitwidth for integers based on the largest required number. Overrides --bitwidth argument. -u --useuids Use unique clafer names in the Clafer solution. --addtypes Add colon/reference types to the Clafer solution. -j --json Render solution as JSON (forces 'addUids'). -d --diff Show each next instance, or state of a trace, as its changes from the previous one. --dot Render solution as a Graphviz graph: for a trace, its states and transitions. --tl=INTEGER Set the maximum length of the traces of a dynamic model (default: 10). -i --flatten-inheritance-comp Flatten inheritance during compiling ('alloy' mode only) -l --no-layout-comp Don't resolve off-side rule layout during compiling -c --check-duplicates-comp Check duplicated clafer names during compiling -f --skip-resolver-comp Skip name resolution during compiling --ss=SCOPESTRATEGY --scope-strategy-comp Use scope computation strategy during compiling: none, simple (default), or full. -? --help Display help message -V --version Print version information --numeric-version Print just the version number ``` `claferIG .cfr` - opens an interactive session and displays an instance or a counterexample. `claferIG .cfr -all ` - opens a non-interactive session and saves all instances up to the provided scope or a counterexample to files named `.cfr..data`, one instance per file. ### Models in several files A model can import other files, as with the Clafer compiler: `--import=FILE` in the model's `//# OPTIONS` directive, relative to the model's folder, or on the command line, relative to the current directory. The files and their imports are compiled together as one model. A model and its imports can also be URLs (`http://`, `https://`). See [Models in several files](https://github.com/gsdlab/clafer#models-in-several-files) in the compiler's README. ``` //# OPTIONS --import=products.cfr MyPhone : Phone ``` `claferIG MyPhone.cfr` generates the instances of `MyPhone.cfr` with the clafers of `products.cfr`. The other options of the directives (e.g., `--maxint`, `--no-layout`) apply too, and an error names the file in which it is (`products.cfr:3:11`). ### Dynamic models A dynamic model, with temporal operators (e.g., `X`, `U`, `initially`) or the temporal modifiers `initial` and `final`, describes how its instances change over time. Its solutions are traces: each `n`ext gives a trace, and the trace is a sequence of states, each an instance of the model. Alloy's traces are lassos: after the last state, the trace loops back to an earlier state, and repeats the states from there forever. ``` //# OPTIONS --import=TrafficLight.cfr tl : TrafficLight [ initially (green --> yellow --> red --> green --> yellow_on --> yellow_off --> off) ] ``` ``` === Trace 1 Begin === --- State 0 --- tl on normal green --- State 1 --- tl on normal yellow ... --- State 6 --- tl off --- Loop back to state 3 --- --- Trace 1 End --- ``` `--tl=INTEGER` and the command `tl ` set the maximum length of the traces (by default, 10 states). The traces are given from the shortest, and each trace is different from the traces given before, as the states in which the instances are, regardless of the names of their atoms. `--all` saves each trace to its own file, and `--json` gives a trace as `{"states": [...], "loop": 3}`. Two commands explore other traces than the next one: * `fork ` gives another trace with the same states as the last trace before the state ``: what else can happen from there. E.g., `fork 2` keeps the states 0 and 1. * `config` gives a trace with another configuration: the clafers that do not change over time, e.g., the features of a product line declared `final`, differ from those of the traces given so far. `config` also works on static models, whose next instances often differ only in a value: it gives an instance whose structure, its clafers without the values of their references, differs from those of the instances given so far. Each `config` gives, e.g., another selection of features of a product line. The next instances then continue from it, without the structures given so far. The command `check` checks the assertions of the model, also the nested ones and those of temporal models, one by one. An assertion holds for all the solutions within the scopes and the maximum trace length, so `No counterexample` does not prove it for larger scopes or longer traces. A counterexample is shown like any other solution, and the next solution of the model stays as it is. Checking a large model can take much longer than generating a solution; lower the maximum trace length (`tl`) to get a faster answer. `check ` checks only the assertions on that line, or all of them if the number is not positive. ``` claferIG> check No counterexample: tl.off => X tl.on (TrafficLight.cfr:13:10) Counterexample of: never tl.off (TrafficLight.cfr:12:10) === Trace 3 Begin === ... 2 assertion(s) checked within the scopes and the maximum trace length: 1 with a counterexample. ``` The command `dot` saves the most recent solution as a Graphviz graph: a node for each state, with the instance as its label and the name of the state (`S0`, `S1`, ...) outside it, an edge to the next state, and a dashed edge back to the loop state. In the diff view, the first state is in full and each next state shows its changes, which keeps the graph of a large model readable. With `--dot`, solutions are given as such graphs, and `--all` saves them to `.dot` files. To render one: ```bash dot -Tsvg TrafficLight.cfr.1.dot -o trace.svg ``` A dynamic model, or a scenario, with no traces has an unsat core: the constraints that contradict each other, e.g., a scenario and the transition it does not follow, and a near-miss trace without one of them, as for a static model. ``` 1) green --> yellow (TrafficLight.cfr:6:33) 2) initially (green --> red) (scenario.cfr:3:7) ``` With `--diff`, or after the command `d`, the first state, whose clafers all appear, is shown with `+` on each line, and each next state as its changes from the previous state: the clafers that appear (`+`), with their children, the clafers that disappear (`-`), and the values that change (`~`). Each change is indented as the clafer in the tree, and has the least-partially-qualified name of the clafer, which is qualified only as much as needed to tell it from the other clafers with the same name, e.g., `normal.yellow` if `flashing` also had a `yellow`. An instance has the same name in all the states of a trace, so a clafer that disappears and appears again is the same instance. ``` --- State 0 --- + tl + on + normal + green ... --- State 3 --- - red + green --- State 4 --- - normal + flashing + yellow_on ``` In a static model, the diff view shows the first instance with `+` on each line, and each next instance as its differences from the previous instance, by their structure: the names of the instances of different solutions are unrelated, so the numbers of the instances are left out. ## Interactive Session Usage In the interactive mode, the users can invoke the following commands by pressing a letter marked in the command name between '' or the whole command as marked by '': ``` ClaferIG v0.5.8 You can invoke the following commands as indicated by single quotes: [tab] - print the available commands - auto-complete command name, a clafer name, or clafer instance name in a given context 'n'ext, [enter] - to produce the next solution if available, an instance of a static model or a trace of a dynamic model, or to output a message that no more solutions exist within the given scope 'i'ncrease - to increase the maximum number of instances of a given clafer or all clafers (scope) 's'et - to set the maximum number of instances of a given clafer or all clafers (scope) 'm'axint, 'maxint' - to set the bitwidth by providing the largest integer 'tl' - to set the maximum length of the traces of a dynamic model 'd'iff - to show each next instance or state as its changes from the previous one, or in full (+ appears, - disappears, ~ changes its value) 'fork' - to produce another trace with the same first states as the last trace 'config' - to produce a trace of a dynamic model whose clafers that do not change over time differ from those of the traces so far, or an instance of a static model whose clafers, without the values of their references, differ from those so far sa'v'e - to save all instances displayed so far or a counterexample to files named .cfr..data, one instance per file 'check' - to check the assertions of the model within the scopes and the maximum trace length, and to give a counterexample of each one that fails 'dot' - to save the most recent solution as a Graphviz graph, for a trace its states and transitions, to .cfr..dot 'q'uit - to quit the interactive session 'r'eload - to reload your clafer model 'h'elp - to display this menu options summary 'scope' - to print out the values of the global scope and individual Clafer scopes 'saveScopes' - to generate a '.cfr-scope' file with the current scopes 'loadScopes' - to load scopes from a '.cfr-scope' file 'setUnsatCoreMinimization' - to choose UnSAT core minimization strategy [fastest | medium | best]. Default: fastest 'c', 'claferModel' - to print out the original Clafer model verbatim 'a', 'alloyModel' - to print out the output of Clafer translator verbatim 'alloyInstance' - to print out the Alloy xml document of the most recent solution 'f'ind - to print a Clafer with given name found in the most recent solution Parameterized command usage: 'i [enter]' - to increase for all clafers by 1 'i [enter]' - to increase for the clafer by 1 'i ' - to increase for the clafer by 's [enter]'- to set for the clafers to 's ' - to set for the clafer to 'f ' - to display a clafer 'tl ' - to set the maximum trace length to 'fork ' - to produce another trace with the states of the last trace before state 'check ' - to check only the assertions on line , or all of them if it is not positive 'setUnsatCoreMinimization fastest' - fastest but the worst 'setUnsatCoreMinimization medium' 'setUnsatCoreMinimization best' - best but slowest even for modest size cores ``` ## Output format There are two output formats: native (plain text, default) and JSON (`--json`). ### Instance data (native) The instance data notation is very similar to a regular Clafer notation for concrete clafers with a few differences: * no constraints * no types and super types * except when `--useuids --addtypes` parameters are used * no clafer and group cardinalities (each clafer has the default group `(0..*)` and clafer `(1..1)` cardinality) * no clafers not present in the instance Additionally, the data notation contains concrete values of the clafers and suffix numbers to distinguish among multiple instances of the same clafer. ### Note: > The instance data models could be read by the Clafer translator if the translator had simple type inference support. #### Example For a model ``` abstract A a ? b + c -> integer ? d -> E 2 g -> E 2 h -> integer abstract E f ->> integer + a1 : A e1 : E e2 : E ``` A possible instance data looks as follows: ``` === Instance 1 Begin === a1 b$1 b$2 c -> 10 d$1 -> e1 d$2 -> e2 g1 -> e1 h$1 -> 5 g2 -> e2 h$2 -> 2 e1 f$1 -> 2 f$2 -> 3 f$3 -> 4 f$4 -> 2 --- Instance 1 End --- ``` ### Near-miss instance Near-miss instance notation is the same as the instance data notation. Additionally, it indicates which constraints belong to the UnSAT Core. #### Example For a model ``` abstract A a ? b ? [ a ] // C1 a1 : A [ no a ] // C2 [ b ] // C3 ``` Constraints C1, C2, and C3 form an UnSAT Core. Removal of any of them will make the model satisfiable. The constraint C1 is part of the model and cannot be removed (part of domain knowledge). Therefore, either C2 or C3 must be removed to remove the inconsistency. On possible near-miss instance: ``` a1 a b ``` Here, `C1` and `C3` are satisfied but `C2` is not. To resolve the conflict and assuming that the counter example is actually a correct instance data, the user has to modify the model by removing `C2`. However, should the counter example actually represent incorrect instance data, the user can remove `C3` to resolve the inconsistency. ## Troubleshooting If ClaferIG reports `No more instances found` for an inconsistent model instead of an UnSAT core, the MiniSat solver with UnSAT cores is not available on your platform (Windows); see the dependencies above. ## How it works The Clafer instance generator: * translates the input Clafer model (.cfr) to an Alloy 6 model (.als). The compiler's intermediate representation (IR) contains the mapping between Clafer names and Alloy names. The IR also contains the scopes for each Alloy signature to ensure that a valid instance can be found if it exists * invokes Alloy Analyzer with the MiniSat solver with UnSAT cores to produce an instance or find an UnSAT core ** given an UnSAT core, removes constraints from the core until an instance is found - that instance represents the counterexample which violates the removed constraints * translates the instance or the counterexample data produced by Alloy Analyzer to Clafer instance data format using the name map from IR in a reverse direction, * for a counterexample, translates the counter example in Alloy to Claefr instance data and constraint violations in Alloy into constraint violations in Clafer model # Need help? * Visit [language's website](http://clafer.org). * Report issues to [issue tracker](https://github.com/gsdlab/claferIG/issues)