The claferIG package

[maintain]

Clafer 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).


[Skip to ReadMe]

Properties

Versions0.3.5, 0.3.5.1, 0.3.5.1, 0.3.6, 0.3.6.1, 0.3.7, 0.3.8, 0.3.9, 0.3.10, 0.4.0
Dependenciesarray (>=0.4.0.1), base (>=4.6.0.1 && <5), clafer (==0.3.5.1), claferIG (==0.3.5.1), cmdargs (>=0.10.5), containers (>=0.4.2.1), data-stringmap (>=0.9.1), directory (>=1.2.0.1), executable-path (>=0.0.3), filepath (>=1.3.0.1), haskeline (>=0.7.0.3), HaXml (>=1.24), HUnit (>=1.2.5.2), json-builder (>=0.3), mtl (>=2.1.2), parsec (>=3.1.3), process (>=1.1.0.2), QuickCheck (>=2.5.1.1), string-conversions (>=0.3), test-framework (>=0.8), test-framework-hunit (>=0.3.0), test-framework-quickcheck2 (>=0.3.0.1), test-framework-th (>=0.2.4), transformers (>=0.3.0.0) [details]
LicenseMIT
AuthorJimmy Liang, Michał Antkiewicz, Luke Michael Brown
MaintainerJimmy Liang <jliang@gsd.uwaterloo.ca>
StabilityExperimental
CategoryModel
Home pagehttps://github.com/gsdlab/claferIG
Source repositoryhead: git clone git://github.com/gsdlab/claferIG.git
ExecutablesclaferIG
UploadedFri Jan 31 18:54:06 UTC 2014 by mantkiew

Modules

Downloads

Maintainers' corner

For package maintainers and hackage trustees

Readme for claferIG-0.3.5.1

Clafer Instance Generator ========================= v0.3.5.1 Clafer 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. Contributors ------------

Dependencies for running

Regardless of the installation method, the following are required:

Installation from binaries

Binary distributions of the release 0.3.5.1 of Clafer Tools for Windows, Mac, and Linux, can be downloaded from Clafer Tools - Binary Distributions.

  1. download the binaries and unpack <target directory> of your choice
  2. add the <target directory> to your system path so that the executables can be found

Installation From Hackage

Dependencies

  1. cabal update
  2. cabal install claferIG
  3. cd <cabal's lib or share folder> (lib on Windows or share on Linux and Mac)
  4. to automatically download Alloy jars
    • execute make in clafer-0.3.5.1/tools
  5. To get the minisatproover library
    • execute make lib in clafer-0.3.5.1`
  6. copy the following into the Cabal's bin folder
    • the file alloyIG.jar
    • the folder tools
    • the folder lib

Installation from the source code

Dependencies

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 'masterare guaranteed to work well together. Development versions from branchesdevelop` should work well together but this might not always be the case.

Building

  1. install the Clafer compiler into a <target directory> of your choice
    • Tip: it is advised to install both tools into the same <target directory>
  2. in some <source directory>, execute git clone git://github.com/gsdlab/claferIG.git
  3. in <source directory>/claferIG, execute
    • cabal update
    • make

Installation

  1. execute make install to=<target directory>
  2. add the <target directory> is on your command PATH

Note:

On Windows, use / with the make command instead of \. Integration with Sublime Text 2 ------------------------------- See IDEs/claferIG-README.md 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)


igaONS] FILE

Common flags:
     --all=INT                                 Saves all instances up to the
                                               provided scope or a
                                               counterexample.
     --savedir=FILE                            Specify the directory for
                                               storing saved files.
     --alloysolution                           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').
  -i --flatten-inheritance-comp                Flatten inheritance during
                                               compiling ('alloy' and 'alloy42'
                                               modes 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

claferIG <model file name>.cfr

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.3.5.1 |
---------------------

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 instance if available or to output a message that no more
                     instances 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
sa'v'e             - to save all instances displayed so far or a counterexample to files named
                     <model file name>.cfr.<instance number>.data, one instance per file
'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 '<model>.cfr-scope' file with the current scopes
'loadScopes'       - to load scopes from a '<model>.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 <name> [enter]'  - to increase for the clafer <name> by 1
'i <name> <number>' - to increase for the clafer <name> by <number>
's <number> [enter]'- to set for the clafers to <number>
's <name> <number>' - to set for the clafer <name> to <number>
'f <name>'          - to display a clafer <name>
'setUnsatCoreMinimization fastest' - fastest but the worst
'setUnsatCoreMinimization medium'
'setUnsatCoreMinimization best' - best but slowest even for modest size cores

Output format -------------

Instance data

The instance data notation is very similar to a regular Clafer notation for concrete clafers with a few differences:

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:

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 

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. How it works ------------ The Clafer instance generator: