claferIG 0.4.2 → 0.4.2.1
raw patch · 9 files changed
+103/−99 lines, 9 filesdep ~claferdep ~claferIGbinary-addedPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: clafer, claferIG
API changes (from Hackage documentation)
Files
- CHANGES.md +30/−26
- README.md +62/−39
- alloyIG.jar binary
- claferIG.cabal +9/−7
- lib/libminisatprover.dylib binary
- lib/libminisatprover.so binary
- lib/minisatprover.dll binary
- lib/minisatprover.md +0/−25
- stack.yaml +2/−2
CHANGES.md view
@@ -1,53 +1,57 @@-# ClaferIG Version 0.4.2 released on Oct 16, 2015 +ClaferIG Version 0.4.2.1 released on Oct 19, 2015 -[Release](https://github.com/gsdlab/claferIG/pull/28) +* Fixed Java manifest file, added stack instructions to README -# ClaferIG Version 0.4.1 released on Sep 1, 2015 +ClaferIG Version 0.4.2 released on Oct 16, 2015 -[Release](https://github.com/gsdlab/claferIG/pull/27) +* [Release](https://github.com/gsdlab/claferIG/pull/28) -# ClaferIG Version 0.4.0 released on Jul 28, 2015 +ClaferIG Version 0.4.1 released on Sep 1, 2015 -[Release](https://github.com/gsdlab/claferIG/pull/26) +* [Release](https://github.com/gsdlab/claferIG/pull/27) -# ClaferIG Version 0.3.10 released on April 24, 2015 +ClaferIG Version 0.4.0 released on Jul 28, 2015 -[Release](https://github.com/gsdlab/claferIG/pull/25) +* [Release](https://github.com/gsdlab/claferIG/pull/26) -# ClaferIG Version 0.3.9 released on March 06, 2015 +ClaferIG Version 0.3.10 released on April 24, 2015 -[Release](https://github.com/gsdlab/claferIG/pull/24) +* [Release](https://github.com/gsdlab/claferIG/pull/25) -# ClaferIG Version 0.3.8 released on January 27, 2015 +ClaferIG Version 0.3.9 released on March 06, 2015 -[Release](https://github.com/gsdlab/claferIG/pull/23) +* [Release](https://github.com/gsdlab/claferIG/pull/24) -# ClaferIG Version 0.3.7 released on October 23, 2014 +ClaferIG Version 0.3.8 released on January 27, 2015 -[Release](https://github.com/gsdlab/claferIG/pull/22) +* [Release](https://github.com/gsdlab/claferIG/pull/23) -# ClaferIG Version 0.3.6.1 released on July 08, 2014 +ClaferIG Version 0.3.7 released on October 23, 2014 -[Release](https://github.com/gsdlab/claferIG/pull/20) +* [Release](https://github.com/gsdlab/claferIG/pull/22) -# ClaferIG Version 0.3.6 released on May 23, 2014 +ClaferIG Version 0.3.6.1 released on July 08, 2014 -[Release](https://github.com/gsdlab/claferIG/pull/19) +* [Release](https://github.com/gsdlab/claferIG/pull/20) -# ClaferIG Version 0.3.5 released on January 20, 2014 +ClaferIG Version 0.3.6 released on May 23, 2014 -[Release](https://github.com/gsdlab/claferIG/pull/17) +* [Release](https://github.com/gsdlab/claferIG/pull/19) -# ClaferIG Version 0.3.4 released on September 20, 2013 +ClaferIG Version 0.3.5 released on January 20, 2014 -# ClaferIG Version 0.3.3 released on August 14, 2013 +* [Release](https://github.com/gsdlab/claferIG/pull/17) -[Release](https://github.com/gsdlab/claferIG/pull/12) +ClaferIG Version 0.3.4 released on September 20, 2013 -# ClaferIG Version 0.3.2 released on April 11, 2013 +ClaferIG Version 0.3.3 released on August 14, 2013 -# ClaferIG Version 0.3.1 released on October 17, 2012 +* [Release](https://github.com/gsdlab/claferIG/pull/12) -# ClaferIG Version 0.3 released on July 17, 2012 +ClaferIG Version 0.3.2 released on April 11, 2013 + +ClaferIG Version 0.3.1 released on October 17, 2012 + +ClaferIG Version 0.3 released on July 17, 2012 This was the first release of Clafer Instance Generator and included all code since the beginning of the project.
README.md view
@@ -1,10 +1,11 @@ # Clafer Instance Generator -v0.4.2 +##### v0.4.2.1 -[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). +[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 @@ -21,37 +22,57 @@ Regardless of the installation method, the following are required: -* [Clafer](https://github.com/gsdlab/clafer) v0.4.2 +* [Clafer](https://github.com/gsdlab/clafer) v0.4.2.1 * [Java Platform (JDK)](http://www.oracle.com/technetwork/java/javase/downloads/index.html) v8+, 64bit * On Windows, Java must be 32bit because of Alloy, 64bit otherwise * [Alloy4.2](http://alloy.mit.edu/alloy/download.html) ### Installation from binaries -Binary distributions of the release 0.4.2 of Clafer Tools for Windows, Mac, and Linux, +Binary distributions of the release 0.4.2.1 of Clafer Tools for Windows, Mac, and Linux, can be downloaded from [Clafer Tools - Binary Distributions](http://gsd.uwaterloo.ca/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 +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 +Clafer is now available on [Hackage](http://hackage.haskell.org/package/claferIG-0.4.2.1/) and it can be installed using either [`stack`](https://github.com/commercialhaskell/stack) or [`cabal-install`](https://hackage.haskell.org/package/cabal-install). -* [GHC](https://www.haskell.org/downloads) v7.10.* +#### Installation using `stack` -ClaferIG is now available on [Hackage](http://hackage.haskell.org/package/claferIG-0.4.2/) and it can be installed using +Stack is the only requirement: no other Haskell tooling needs to be installed because stack will automatically install the needed Haskell build tools. -1. `cabal update` -2. `cabal install claferIG` -3. `cd <cabal's lib or share folder>` (`C:\Users\<user>\AppData\Roaming\cabal\i386-windows-ghc-7.10.2\claferIG-0.4.2` on Windows or `.cabal/share/x86_64-linux-ghc-7.10.2/claferIG-0.4.2/` on Linux) -3. to automatically download Alloy4.2 jar - * execute `make` in `tools` -4. To get the `minisatproover` library - * execute `make lib -B` -5. copy the following into the Cabal's `bin` folder +1. [install `stack`](https://github.com/commercialhaskell/stack#how-to-install) +2. execute + * `stack install claferIG` + * ``` cd `stack --local-bin-path` ``` + * `wget http://alloy.mit.edu/alloy/downloads/alloy4.2_2015-02-22.jar` + * `mv alloy4.2_2015-02-22.jar alloy4.2.jar` + * `wget https://github.com/gsdlab/claferIG/raw/master/alloyIG.jar` + * `mkdir lib` + * `cd lib` + * Depending on your OS: + * for Win, `wget https://github.com/gsdlab/claferIG/raw/master/lib/libminisatprover.dll` + * for Linux, `wget https://github.com/gsdlab/claferIG/raw/master/lib/libminisatprover.so` + * for Mac, `wget https://github.com/gsdlab/claferIG/raw/master/lib/libminisatprover.dylib` + +#### Installation using `cabal-install` + +Dependencies + +* [GHC](https://www.haskell.org/downloads) >= 7.8.3. 7.10.2 is recommended, +* `cabal-install` >= 1.18, should be installed together with a GHC distribution, + +1. Install GHC +2. `cabal update` +3. `cabal install claferIG` +4. `cd <cabal's lib or share folder>` (`C:\Users\<user>\AppData\Roaming\cabal\i386-windows-ghc-7.10.2\claferIG-0.4.2.1` on Windows or `.cabal/share/x86_64-linux-ghc-7.10.2/claferIG-0.4.2.1/` on Linux) +5. to automatically download alloy4.2.jar + * execute `make alloy4.2.jar` +7. copy the following into the Cabal's `bin` folder * the file `alloyIG.jar` - * the folder `tools` + * the file `alloy4.2.jar` * the folder `lib` ### Installation from the source code @@ -59,7 +80,7 @@ Dependencies * [GHC](https://www.haskell.org/downloads) v7.10.* -* [Clafer compiler](https://github.com/gsdlab/clafer) (to produce Alloy models (`.als`)). The version number of the compiler must match the version of the instance generator. +* [Clafer compiler](https://github.com/gsdlab/clafer) (to produce Alloy models (`.als`)). * On Linux, might need to manually install `zlib1g-dev` and `libncurses5-dev` to build one of Haskell packages on which ClaferIG depends * on Ubuntu, execute `sudo apt-get install zlib1g-dev libncurses5-dev` @@ -83,9 +104,16 @@ 1. install the [Clafer compiler](https://github.com/gsdlab/clafer) 2. in some `<source directory>`, execute `git clone git://github.com/gsdlab/claferIG.git` -3. in `<source directory>/claferIG`, execute - * `cabal update` - * `make init` +3. in `<source directory>/claferIG`, execute `stack setup`. This will install all dependencies, build tools, and MSYS2 (on Windows). +4. first time only on Windows + * open `MinGW64 Shell` using `C:\Users\<user>\AppData\Local\Programs\stack\i386-windows\msys2-20150512\mingw64_shell.bat` + * update MSYS2 following the [update procedure](http://sourceforge.net/p/msys2/wiki/MSYS2%20installation/): + * `pacman -Sy` + * `pacman --needed -S bash pacman pacman-mirrors msys2-runtime` + * restart shell if the runtime was updated + * `pacman -Su` + * `pacman -S make wget unzip diffutils` +5. `cd <source directory>/claferIG` * `make` ### Installation @@ -106,17 +134,16 @@ See [clafer-vim](https://github.com/wasowski/clafer-vim) -Usage -===== +# Usage Clafer Instance Generator can be used in interactive and batch modes, as well as, an API. -### Command-line Usage +## Command-line Usage (As printed by `claferIG --help`) ``` -ClaferIG v0.4.2 +ClaferIG v0.4.2.1 claferIG [OPTIONS] [FILE] @@ -163,13 +190,12 @@ - opens a non-interactive session and saves all instances up to the provided scope or a counterexample to files named `<model file name>.cfr.<instance number>.data`, one instance per file. -### 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 '': - -## ``` +## Interactive Session Usage -## | ClaferIG 0.4.2 | +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.4.2.1 You can invoke the following commands as indicated by single quotes: [tab] - print the available commands @@ -205,7 +231,6 @@ 'setUnsatCoreMinimization best' - best but slowest even for modest size cores ``` - ## Output format There are two output formats: native (plain text, default) and JSON (`--json`). @@ -229,7 +254,7 @@ For a model -```clafer +``` abstract A a ? b + @@ -248,7 +273,7 @@ A possible instance data looks as follows: -```clafer +``` === Instance 1 Begin === a1 @@ -279,7 +304,7 @@ For a model -```clafer +``` abstract A a ? b ? @@ -294,7 +319,7 @@ On possible near-miss instance: -```clafer +``` a1 a b @@ -321,7 +346,6 @@ ## How it works - The Clafer instance generator: * translates the input Clafer model (.cfr) to an Alloy4.2 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 @@ -331,7 +355,6 @@ * 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)
alloyIG.jar view
binary file changed (22364 → 22360 bytes)
claferIG.cabal view
@@ -1,5 +1,5 @@ Name: claferIG -Version: 0.4.2 +Version: 0.4.2.1 Synopsis: claferIG is an interactive tool that generates instances of Clafer models. Description: 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). Homepage: http://clafer.org @@ -19,7 +19,9 @@ , alloyIG.jar , CHANGES.md , Makefile - , lib/minisatprover.md + , lib/libminisatprover.dylib + , lib/libminisatprover.so + , lib/minisatprover.dll , stack.yaml source-repository head type: git @@ -42,8 +44,8 @@ , transformers-compat >= 0.3 && < 0.5 , mtl-compat >= 0.2.1 - , clafer == 0.4.2 - , claferIG == 0.4.2 + , clafer == 0.4.2.1 + , claferIG == 0.4.2.1 other-modules: Paths_claferIG Hs-Source-Dirs: src-cmd ghc-options: -Wall -fno-warn-orphans @@ -70,7 +72,7 @@ , transformers-compat >= 0.3 && < 0.5 , mtl-compat >= 0.2.1 - , clafer == 0.4.2 + , clafer == 0.4.2.1 if os(windows) build-depends: HaXml == 1.24 @@ -109,7 +111,7 @@ , tasty-th >= 0.1.3 , transformers-compat >= 0.3 && < 0.5 - , clafer == 0.4.2 - , claferIG == 0.4.2 + , clafer == 0.4.2.1 + , claferIG == 0.4.2.1 other-modules: Paths_claferIG ghc-options: -Wall -fno-warn-orphans
+ lib/libminisatprover.dylib view
binary file changed (absent → 74648 bytes)
+ lib/libminisatprover.so view
binary file changed (absent → 75650 bytes)
+ lib/minisatprover.dll view
binary file changed (absent → 142114 bytes)
− lib/minisatprover.md
@@ -1,25 +0,0 @@-ClaferIG uses Alloy which, in turn, requires a SAT solver. ClaferIG requires support for UnSAT core computation, which is provided by `minisatproover` library. - -In this folder, you need to have an appropriate `minisatproover` library for your operating system. -When building from source code, this gets created for you by the `tools/Makefile`. -When building from Hackage, you need to extract the library from `alloy.jar`. - -The taget folder structure should be - -1. for 32bit Linux - -`<cabal>/bin/lib/x86-linux/libminisatprover*` - -2. for 64bit Linux - -`<cabal>/bin/lib/amd64-linux/libminisatprover*` - -3. for Windows - -`<cabal>/bin/lib/x86-windows/minisatprover*` - -4. for Max - -`<cabal>/bin/lib/x86-mac/libminisatprover* - -
stack.yaml view
@@ -1,9 +1,9 @@ # for GHC-7.10.2 extra-deps: [ data-stringmap-1.0.1.1 - , HaXml-1.24 + , HaXml-1.24 # only for Windows, comment out for other OSs ] -resolver: lts-3.9 +resolver: lts-3.10 packages: - '../clafer'