diff --git a/CHANGES.md b/CHANGES.md new file mode 100644 --- /dev/null +++ b/CHANGES.md @@ -0,0 +1,36 @@ +**ClaferIG Version 0.3.5 released on January 20, 2014** + +[Release](https://github.com/gsdlab/claferIG/pull/17) + +[New features and bug fixes](http://gsd.uwaterloo.ca:8888/questions/scope:all/sort:activity-desc/tags:v0.3.5,claferig/page:1/) + +**ClaferIG Version 0.3.4 released on September 20, 2013** + +[New features and bug fixes](http://gsd.uwaterloo.ca:8888/questions/scope:all/sort:activity-desc/tags:v0.3.4,claferig/page:1/) + +**ClaferIG Version 0.3.3 released on August 14, 2013** + +[Release](https://github.com/gsdlab/claferIG/pull/12) + +[New features and bug fixes](http://gsd.uwaterloo.ca:8888/questions/scope:all/sort:activity-desc/tags:v0.3.3,claferig/page:1/) + +**ClaferIG Version 0.3.2 released on April 11, 2013** + +[New features and bug fixes](http://gsd.uwaterloo.ca:8888/questions/scope:all/sort:activity-desc/tags:v0.3.2,claferig/page:1/) + +**ClaferIG Version 0.3.1 released on October 17, 2012** + +[New features and bug fixes](http://gsd.uwaterloo.ca:8888/questions/scope:all/sort:activity-desc/tags:v0.3.1,claferig/page:1/) + +**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. + +[New features and bug fixes](http://gsd.uwaterloo.ca:8888/questions/scope:all/sort:activity-desc/tags:v0.3,claferig/page:1/) + +Undocumented features - See the `README.md`. + + + + + diff --git a/IDEs/claferIG-README.md b/IDEs/claferIG-README.md new file mode 100644 --- /dev/null +++ b/IDEs/claferIG-README.md @@ -0,0 +1,46 @@ +IDE Integrations +================ + +Sublime Text 2 +-------------- + +We provide a configuration for SublimeREPL for running ClaferIG inside Sublime as a REPL. + +### Usage + +Use `+i`, `g`, `s` to open a Clafer `.cfr` file with ClaferIG and `--ss=simple` setting. +Use `+i`, `g`, `f` to open a Clafer `.cfr` file with ClaferIG and `--ss=full` setting. +This commands assume that Clafer and ClaferIG executables are in system `PATH`. + +### Installation + +1. Install `SublimeREPL` plugin. + * You need to install `Package Control` first - see [installation](http://wbond.net/sublime_packages/package_control/installation). To open the Console, go to `View->Show Console`. + * Go to `Preferences->Package Control` + * type `Install`, `` + * type `SublimeREPL`, `` +2. Copy the folder `ClaferIG` from `IDEs\sublime-text-2\Packages\SublimeREPL\config\` to `Packages\SublimeREPL\config\` in Sublime Text 2 folder inside your home directory. +3. In Sublime, open `Preferences->Key Bindings - User` and add the following key bindings there (inside the `[ ]`, remember about commas `,` to have a proper list) + +``` + { + "keys": [ "ctrl+i", "g", "s" ], + "args": { + "id": "repl_claferIG", + "file": "config/ClaferIG/IGS.sublime-menu" + }, + "command": "run_existing_window_command" + }, + { + "keys": [ "ctrl+i", "g", "f" ], + "args": { + "id": "repl_claferIG", + "file": "config/ClaferIG/IGF.sublime-menu" + }, + "command": "run_existing_window_command" + } +``` + +> Note: +> on Windows 7 and 8, the folder is `\AppData\Roaming\Sublime Text 2\Packages`. +> on Mac, the folder is `~/Library/Application Support/Sublime Text 2/Packages`. diff --git a/IDEs/sublime-text-2/Packages/SublimeREPL/config/ClaferIG/Default.sublime-commands b/IDEs/sublime-text-2/Packages/SublimeREPL/config/ClaferIG/Default.sublime-commands new file mode 100644 --- /dev/null +++ b/IDEs/sublime-text-2/Packages/SublimeREPL/config/ClaferIG/Default.sublime-commands @@ -0,0 +1,10 @@ +[ + { + "caption": "SublimeREPL: ClaferIG", + "command": "run_existing_window_command", "args": + { + "id": "repl_claferIG", + "file": "config/ClaferIG/IGF.sublime-menu" + } + } +] diff --git a/IDEs/sublime-text-2/Packages/SublimeREPL/config/ClaferIG/IGF.sublime-menu b/IDEs/sublime-text-2/Packages/SublimeREPL/config/ClaferIG/IGF.sublime-menu new file mode 100644 --- /dev/null +++ b/IDEs/sublime-text-2/Packages/SublimeREPL/config/ClaferIG/IGF.sublime-menu @@ -0,0 +1,26 @@ +[ + { + "id": "tools", + "children": + [{ + "caption": "SublimeREPL", + "mnemonic": "r", + "id": "SublimeREPL", + "children": + [ + {"command": "repl_open", + "caption": "ClaferIG", + "id": "repl_claferIG", + "mnemonic": "i", + "args": { + "type": "subprocess", + "encoding": "utf8", + "cmd": ["claferIG", "$file", "--ss=full"], + "cwd": "$file_path", + "external_id": "claferIG" + } + } + ] + }] + } +] diff --git a/IDEs/sublime-text-2/Packages/SublimeREPL/config/ClaferIG/IGS.sublime-menu b/IDEs/sublime-text-2/Packages/SublimeREPL/config/ClaferIG/IGS.sublime-menu new file mode 100644 --- /dev/null +++ b/IDEs/sublime-text-2/Packages/SublimeREPL/config/ClaferIG/IGS.sublime-menu @@ -0,0 +1,26 @@ +[ + { + "id": "tools", + "children": + [{ + "caption": "SublimeREPL", + "mnemonic": "r", + "id": "SublimeREPL", + "children": + [ + {"command": "repl_open", + "caption": "ClaferIG", + "id": "repl_claferIG", + "mnemonic": "i", + "args": { + "type": "subprocess", + "encoding": "utf8", + "cmd": ["claferIG", "$file"], + "cwd": "$file_path", + "external_id": "claferIG" + } + } + ] + }] + } +] diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,17 @@ +Permission is hereby granted, free of charge, to any person obtaining a copy of +this software and associated documentation files (the "Software"), to deal in +the Software without restriction, including without limitation the rights to +use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies +of the Software, and to permit persons to whom the Software is furnished to do +so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. diff --git a/Makefile b/Makefile new file mode 100644 --- /dev/null +++ b/Makefile @@ -0,0 +1,133 @@ +TOOL_DIR = tools + +UNAME := $(shell uname | tr "A-Z" "a-z") + +ifeq ($(UNAME), darwin) + ONAME := $(shell uname -s | tr "A-Z" "a-z") +else + ONAME := $(shell uname -o | tr "A-Z" "a-z") +endif + +MNAME := $(shell uname -m | tr "A-Z" "a-z") + +ifeq ($(UNAME), linux) + ifeq ($(MNAME), i686) + LIB := x86-linux/libminisatprover* + endif + ifeq ($(MNAME), x86_64) + # amd64 is a nickname for x86_64 + LIB := amd64-linux/libminisatprover* + endif +endif +ifeq ($(UNAME), windows) + ifeq ($(MNAME), i686) + LIB := x86-windows/minisatprover* + endif + ifeq ($(MNAME), x86_64) + LIB := x86-windows/minisatprover* + endif +endif +ifeq ($(basename $(UNAME)), mingw32_nt-6) + ifeq ($(MNAME), i686) + LIB := x86-windows/minisatprover* + endif + ifeq ($(MNAME), x86_64) + LIB := x86-windows/minisatprover* + endif +endif +ifeq ($(ONAME), cygwin) + ifeq ($(MNAME), i686) + LIB := x86-windows/minisatprover* + endif + ifeq ($(MNAME), x86_64) + LIB := x86-windows/minisatprover* + endif +endif +ifeq ($(UNAME), darwin) + ifeq ($(MNAME), i686) + LIB := x86-mac/libminisatprover* + endif + ifeq ($(MNAME), x86_64) + LIB := x86-mac/libminisatprover* + endif + WGET_COMMAND := curl -O +else + WGET_COMMAND := wget +endif + +# Calling `make` should only build +all: alloyIG.jar lib build + +# Calling `make install to=` should only install +install: + mkdir -p $(to) + mkdir -p $(to)/lib + mkdir -p $(to)/tools + cp -f lib/*minisatprover* $(to)/lib + cp -f tools/alloy4.jar $(to)/tools + cp -f alloyIG.jar $(to) + cp -f LICENSE $(to)/ + cp -f CHANGES.md $(to)/claferIG-CHANGES.md + cp -f README.md $(to)/claferIG-README.md + cp -f -R IDEs $(to) + cabal install --bindir=$(to) --ghc-option="-O" + +# Removes current build and makes a clean new one (Don't use if starting from scratch!) +cleanEnv: + make clean + ghc-pkg unregister claferIG + rm `which claferIG` + make + +# this takes the version from the .cabal file. Need to run install first to produce Paths_claferIG.hs +newVersion: + ghc -isrc src/dateVer.hs dist/build/autogen/Paths_claferIG.hs -outputdir dist/build --make -o dateVer + ./dateVer > src/Language/Clafer/IG/Version.hs + + +# Build takes less time. For ease of development. +build: alloyIG.jar + cabal install --only-dependencies + cabal configure + cabal build + +alloyIG.jar: src/manifest src/org/clafer/ig/AlloyIG.java src/manifest src/org/clafer/ig/Util.java src/org/clafer/ig/AlloyIGException.java src/edu/mit/csail/sdg/alloy4compiler/parser/AlloyCompiler.java + $(MAKE) -C $(TOOL_DIR) + mkdir -p dist/javabuild + javac -source 1.6 -target 1.6 -cp "tools/alloy4.jar" -d dist/javabuild src/org/clafer/ig/AlloyIG.java src/org/clafer/ig/Util.java src/org/clafer/ig/AlloyIGException.java src/edu/mit/csail/sdg/alloy4compiler/parser/AlloyCompiler.java + jar cfm alloyIG.jar src/manifest -C dist/javabuild org/clafer/ig/ -C dist/javabuild edu + +lib: + + @if [[ "$(basename $(UNAME))"=="mingw32_nt-6" && -z "$(shell which unzip)" ]] ; then \ + mingw-get install msys-unzip-bin; \ + fi + + @if test -z $(LIB); then \ + echo "[WARNING] Did not find a minisat prover binary suitable for your system. You may need to build the binary yourself."; \ + else \ + unzip tools/alloy4.jar $(LIB) -d lib; \ + chmod +x lib/$(LIB); \ + cp lib/$(LIB) lib; \ + fi + +test: + # Only test a subset of the suite. The other cases do not work yet. + cabal configure --enable-tests + cabal build + mkdir dist/build/test-suite/lib + cp alloyIG.jar dist/build/test-suite/lib + cabal test + ./claferIG --all=4 -s dist/run test/suite/backquoted.cfr + ./claferIG --all=4 -s dist/run test/suite/BobsTeam.cfr + ./claferIG --all=4 -s dist/run test/suite/inconsistent.cfr + ./claferIG --all=4 -s dist/run test/suite/PersonFingers.cfr + ./claferIG --all=4 -s dist/run test/suite/waitingLine.cfr + ./claferIG --all=4 -s dist/run test/suite/subclaferCardinality.cfr + +clean: + rm -rf dist + rm -f alloyIG.jar + rm -f claferIG + rm -rf lib + rm -f dateVer* diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,309 @@ +Clafer Instance Generator +========================= + +v0.3.5.20-01-2014 + +[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 +------------ + +* [Jimmy Liang](http://gsd.uwaterloo.ca/jliang), MSc. Candidate. Main developer. +* [Michał Antkiewicz](http://gsd.uwaterloo.ca/mantkiew), Research Engineer. Requirements, development, architecture, testing, technology transfer. +* Luke Michael Brown, co-op student May-Aug 2013. Many improvements. + +Getting Clafer Tools +-------------------- + +Binary distributions of the release 0.3.5 of Clafer Tools for Windows, Mac, and Linux, +can be downloaded from [Clafer Tools - Binary Distributions](http://http://gsd.uwaterloo.ca/clafer-tools-binary-distributions). +Clafer Wiki requires Haskell Platform and MinGW to run on Windows. + +In case these binaries do not work on your particular machine configuration, the tools can be built from source code, as described below. + +### Dependencies for running + +* [Clafer](https://github.com/gsdlab/clafer) v0.3.5 +* [Java Platform (JDK)](http://www.oracle.com/technetwork/java/javase/downloads/index.html) v6+, 32bit +* [Alloy4.1](http://alloy.mit.edu/alloy/download.html) + +### Installation + +1. download the binaries and unpack `` of your choice +2. add the `` to your system path so that the executables can be found +3. copy Alloy 4.1's jar to the `/tools` folder + +Integration with Sublime Text 2 +------------------------------- + +See [IDEs/claferIG-README.md](IDEs/claferIG-README.md) + +Installation From Hackage +------------------------- + +Dependencies + +* [The Haskell Platform](http://hackage.haskell.org/platform/) v2013.2.0.0 + +ClaferIG is now available on [Hackage](http://hackage.haskell.org/package/claferIG-0.3.5/) and it can be installed using + +* `cabal update` +* `cabal install claferIG` +* To get the minisatproover library, execute `make lib` and copy the `lib` folder into the Cabal's `bin` folder +* To automatically download Alloy jars, execute `make` in `claferIG-0.3.5/tools` inside the Cabal's library folder and copy the `tools` folder into the Cabal's `bin` folder + +Building & Installation From Source Code +---------------------------------------- + +### Additional dependencies for building + +* [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. +* 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` + +On Windows + +* [MinGW+MSYS](http://mingw.org) + * since the Haskell Platform already contains MinGW, you may choose to install MinGW+MSYS to the same location, e.g., `c:\...\Haskell Platform\2013.2.0.0` + * add the `bin` folders of MinGW (`MinGW\bin`) and MSYS (`MinGW\MSYS\1.0\bin`) to your system path + * `unzip` will be automatically installed + +### 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. install the [Clafer compiler](https://github.com/gsdlab/clafer) into a `` of your choice + * Tip: it is advised to install both tools into the same `` +2. in some ``, execute `git clone git://github.com/gsdlab/claferIG.git` +3. in `/claferIG`, execute + * `cabal update` + * `make` + +### Installation + +1. execute `make install to=` +2. add the `` is on your command PATH + +#### Note: +> On Windows, use `/` with the `make` command instead of `\`. + +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 v0.3.5.20-01-2014 + +igargs [OPTIONS] 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 .cfr` + +- opens an interactive session and displays the minimal 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. + +### 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.20-01-2014 | +------------------------------ + +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 + .cfr..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 '.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 +'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: + +* no constraints +* no types and super types + * except when `--adduidsandtypes` parameter is 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 multipe 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 + +```clafer +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: + +```clafer +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 + +```clafer +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: + +```clafer +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: + +* translates the input Clafer model (.cfr) to an Alloy model (.als). The compiler's intermediate representation (IR) contains the mapping between Clafer names and Alloy names. The IR also contains the smallest scopes for each Alloy signature to ensure that a valid instance can be found if it exists +* invokes Alloy Analyzer 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? +========== +* See [language's website](http://clafer.org) for news, technical reports and more + * Check out a [Clafer tutorial](http://t3-necsis.cs.uwaterloo.ca:8091/Tutorial/Intro) + * Try a live instance of [ClaferWiki](http://t3-necsis.cs.uwaterloo.ca:8091) + * Try a live instance of [ClaferIDE](http://t3-necsis.cs.uwaterloo.ca:8094) + * Try a live instance of [ClaferConfigurator](http://t3-necsis.cs.uwaterloo.ca:8093) + * Try a live instance of [ClaferMooVisualizer](http://t3-necsis.cs.uwaterloo.ca:8092) +* Take a look at (incomplete) [Clafer wiki](https://github.com/gsdlab/clafer/wiki) +* Browse example models in the [test suite](https://github.com/gsdlab/clafer/tree/master/test/positive) and [MOO examples](https://github.com/gsdlab/clafer/tree/master/spl_configurator/dataset) +* Post questions, report bugs, suggest improvements [GSD Lab Bug Tracker](http://gsd.uwaterloo.ca:8888/questions/). Tag your entries with `claferig` (so that we know what they are related to) and with `jimmy-liang` or `michal` (so that Jimmy or Michał gets a notification). diff --git a/Setup.lhs b/Setup.lhs new file mode 100644 --- /dev/null +++ b/Setup.lhs @@ -0,0 +1,4 @@ +#! /usr/bin/env runhaskell + +> import Distribution.Simple +> main = defaultMain diff --git a/alloyIG.jar b/alloyIG.jar new file mode 100644 Binary files /dev/null and b/alloyIG.jar differ diff --git a/claferIG.cabal b/claferIG.cabal new file mode 100644 --- /dev/null +++ b/claferIG.cabal @@ -0,0 +1,135 @@ +Name: claferIG +Version: 0.3.5 +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: https://github.com/gsdlab/claferIG +License: MIT +License-file: LICENSE +Author: Jimmy Liang, Michal Antkiewicz, Luke Michael Brown +Maintainer: jliang@gsd.uwaterloo.ca +Stability: Experimental +Category: Model +Build-type: Simple +Cabal-version: >=1.16 +data-files: README.md + CHANGES.md, + Makefile, + tools/Makefile, + IDEs/claferIG-README.md, + IDEs/sublime-text-2/Packages/SublimeREPL/config/ClaferIG/Default.sublime-commands, + IDEs/sublime-text-2/Packages/SublimeREPL/config/ClaferIG/IGF.sublime-menu, + IDEs/sublime-text-2/Packages/SublimeREPL/config/ClaferIG/IGS.sublime-menu, + alloyIG.jar +source-repository head + type: git + location: git://github.com/gsdlab/claferIG.git +Executable claferIG + build-tools: ghc >= 7.6.3 + default-language: Haskell2010 + default-extensions: + DeriveDataTypeable + Main-is: Main.hs + Build-depends: + base >= 4.6.0.1 && < 5, + clafer == 0.3.5, + claferIG == 0.3.5, + data-stringmap >= 0.9.1, + cmdargs >= 0.10.5, + containers >= 0.4.2.1, + directory >= 1.2.0.1, + executable-path >= 0.0.3, + filepath >= 1.3.0.1, + haskeline >= 0.7.0.3, + HaXml >= 1.24, + mtl >= 2.1.2, + parsec >= 3.1.3, + process >= 1.1.0.2, + transformers >= 0.3.0.0, + json-builder >= 0.3, + 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, + QuickCheck >= 2.5.1.1, + HUnit >= 1.2.5.2 + other-modules: Paths_claferIG + Hs-Source-Dirs: src + +library + build-tools: ghc >= 7.6.3 + default-language: Haskell2010 + default-extensions: DeriveDataTypeable + build-depends: array >= 0.4.0.1, + base >= 4.6.0.1 && < 5, + containers >= 0.4.2.1, + directory >= 1.2.0.1, + filepath >= 1.3.0.1, + process >= 1.1.0.2, + + HUnit >= 1.2.5.2, + mtl >= 2.1.2, + parsec >= 3.1.3, + QuickCheck >= 2.5.1.1, + transformers >= 0.3.0.0, + + data-stringmap >= 0.9.1, + cmdargs >= 0.10.5, + executable-path >= 0.0.3, + haskeline >= 0.7.0.3, + HaXml >= 1.24, + json-builder >= 0.3, + 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, + + clafer == 0.3.5 + hs-source-dirs: src + ghc-options: -Wall -fno-warn-unused-do-bind -fno-warn-orphans + exposed-modules: Language.Clafer.IG.AlloyIGInterface, + Language.Clafer.IG.ClaferIG, + Language.Clafer.IG.ClaferModel, + Language.Clafer.IG.CommandLine, + Language.Clafer.IG.CommandLineParser, + Language.Clafer.IG.Constraints, + Language.Clafer.IG.JSONGenerator, + Language.Clafer.IG.Process, + Language.Clafer.IG.Solution, + Language.Clafer.IG.Sugarer + other-modules: Paths_claferIG +Test-Suite test-suite + type: exitcode-stdio-1.0 + default-language: Haskell2010 + main-is: test-suite.hs + hs-source-dirs: test + build-depends: array >= 0.4.0.1, + base >= 4.6.0.1 && < 5, + containers >= 0.4.2.1, + directory >= 1.2.0.1, + filepath >= 1.3.0.1, + process >= 1.1.0.2, + + HUnit >= 1.2.5.2, + mtl >= 2.1.2, + parsec >= 3.1.3, + QuickCheck >= 2.5.1.1, + transformers >= 0.3.0.0, + + data-stringmap >= 0.9.1, + cmdargs >= 0.10.5, + executable-path >= 0.0.3, + haskeline >= 0.7.0.3, + HaXml >= 1.24, + json-builder >= 0.3, + 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, + + clafer == 0.3.5, + claferIG == 0.3.5 + other-modules: Paths_claferIG + ghc-options: -Wall -fno-warn-unused-do-bind -fno-warn-orphans diff --git a/src/Language/Clafer/IG/AlloyIGInterface.hs b/src/Language/Clafer/IG/AlloyIGInterface.hs new file mode 100644 --- /dev/null +++ b/src/Language/Clafer/IG/AlloyIGInterface.hs @@ -0,0 +1,286 @@ +{-# LANGUAGE GeneralizedNewtypeDeriving, StandaloneDeriving #-} + +{- + Copyright (C) 2012-2013 Jimmy Liang + + Permission is hereby granted, free of charge, to any person obtaining a copy of + this software and associated documentation files (the "Software"), to deal in + the Software without restriction, including without limitation the rights to + use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies + of the Software, and to permit persons to whom the Software is furnished to do + so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all + copies or substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. +-} + +module Language.Clafer.IG.AlloyIGInterface where + +import Control.Applicative +import Control.Monad +import Control.Monad.IO.Class +import Control.Monad.Reader +import Control.Monad.Trans.State.Strict +import Data.Map as Map hiding (null) +import Data.Maybe +import Language.Clafer.Front.Absclafer (Span(..), Pos(..)) +import Language.Clafer.IG.Process +import System.Console.Haskeline.MonadException + +-- | An interface to the Alloy Analyzer + +newtype AlloyIGT m a = AlloyIGT (StateT (Maybe AlloyIGEnv) (ReaderT Process m) a) deriving (Applicative, Functor, Monad, MonadIO) + +instance MonadTrans AlloyIGT where + lift = AlloyIGT . lift . lift + +deriving instance MonadException m => MonadException (AlloyIGT m) + +fetch :: Monad m => AlloyIGT m AlloyIGEnv +fetch = fromMaybe (error "AlloyIG not loaded.") `liftM` AlloyIGT get + +fetches :: Monad m => (AlloyIGEnv -> a) -> AlloyIGT m a +fetches = (`liftM` fetch) + +set :: Monad m => AlloyIGEnv -> AlloyIGT m () +set = AlloyIGT . put . Just + +proc :: Monad m => AlloyIGT m Process +proc = AlloyIGT ask + +-- | Instance generator's environment +data AlloyIGEnv = AlloyIGEnv {alloyModel::String, sigMap::Map String Sig, scopes::Map String Integer, globalScope::Integer} + + +data Sig = Sig{s_name::String, s_multiplicity::Multiplicity, s_subset::Maybe String, s_startingScope::Maybe Integer} + + +data Multiplicity = One | Lone | Some | Any deriving (Eq, Read, Show) + + +data UnsatCore = UnsatCore{core::[Span]} deriving Show + + + +withinRange :: Integer -> Multiplicity -> Bool +withinRange scope One = scope == 1 +withinRange scope Lone = scope == 0 || scope == 1 +withinRange scope Some = scope >= 1 +withinRange _ Any = True + + +runAlloyIGT :: MonadIO m => AlloyIGT m a -> m a +runAlloyIGT run = + do + execPath <- liftIO $ executableDirectory + proce <- liftIO $ pipeProcess "java" ["-Djava.library.path=" ++ execPath ++ "lib" , "-jar", execPath ++ "alloyIG.jar"] + + runReaderT (evalStateT (unwrap run) Nothing) proce + where + unwrap (AlloyIGT a) = a + + +getAlloyModel :: MonadIO m => AlloyIGT m String +getAlloyModel = fetches alloyModel + + +getSigs :: MonadIO m => AlloyIGT m [String] +getSigs = keys `liftM` fetches sigMap + +-- | Call load before any other commands. +load :: Process -> String -> IO AlloyIGEnv +load proce alloyModel' = + do + putMessage proce "load" + putMessage proce alloyModel' + numberOfSigs <- readMessage proce + sigs <- replicateM numberOfSigs readSig + + let sigMap' = fromList [(s_name sig, sig) | sig <- sigs] + let scopes' = Map.empty + globalScope' <- readMessage proce + + return $ AlloyIGEnv alloyModel' sigMap' scopes' globalScope' + where + readSig = + do + sig <- getMessage proce + multiplicity <- readMessage proce + subset <- getMessage proce + hasStartingScope <- readMessage proce + startingScope <- + if hasStartingScope then Just <$> readMessage proce else return Nothing + return $ Sig sig multiplicity (if null subset then Nothing else Just subset) startingScope + + +sendLoadCommand :: MonadIO m => String -> AlloyIGT m () +sendLoadCommand alloyModel' = + do + proc' <- proc + env <- liftIO $ load proc' alloyModel' + set env + + sigs <- elems `liftM` fetches sigMap + mapM_ resetScope sigs + where + resetScope Sig{s_name = name, s_startingScope = startingScope} = + case startingScope of + Just scope -> sendSetScopeCommand name scope >> return () + Nothing -> sendSetScopeCommand name 1 >> return () + + +-- | Get the next solution from alloyIG +sendNextCommand :: MonadIO m => AlloyIGT m (Maybe String) +sendNextCommand = + do + putMsg "next" + status <- readMsg + case status of + True -> Just `liftM` getMsg + False -> return Nothing + + +getScope :: MonadIO m => String -> AlloyIGT m Integer +getScope sig = + do + rscopes <- fetches scopes + case Map.lookup sig rscopes of + Just scope -> return scope + Nothing -> getGlobalScope + + +getScopes :: MonadIO m => AlloyIGT m [(String, Integer)] +getScopes = toList `liftM` fetches scopes + + +-- | Tell alloyIG to change the scope of a sig +sendSetScopeCommand :: MonadIO m => String -> Integer -> AlloyIGT m (Maybe String) +sendSetScopeCommand sig scope = + do + sigMap' <- fetches sigMap + let Sig{s_multiplicity = multiplicity, s_subset = subset} = sigMap' ! sig + + -- Alloy has a fit when trying to set a scope outside its multiplicity + -- Don't send command if outside its multiplicity but continue the illusion that + -- the scope was set + case subset of + Nothing -> + do + when (withinRange scope multiplicity) $ + do + putMsg "setScope" + putMsg sig + putMsg $ show scope + rscopes <- fetches scopes + env <- fetch + set env {scopes = Map.insert sig scope rscopes} + return $ Nothing + Just sub -> + return $ Just sub + + +getGlobalScope :: MonadIO m => AlloyIGT m Integer +getGlobalScope = fetches globalScope + + +-- | Tell alloyIG to change the global scope +sendSetGlobalScopeCommand :: MonadIO m => Integer -> AlloyIGT m () +sendSetGlobalScopeCommand scope = + do + putMsg "setGlobalScope" + putMsg $ show scope + + env <- fetch + set env {globalScope = scope} + + +-- | Tell alloyIG to recalculate the solution +sendResolveCommand :: MonadIO m => AlloyIGT m () +sendResolveCommand = putMsg "resolve" + + +-- | Tell alloyIG to save the current state +sendSaveStateCommand :: MonadIO m => AlloyIGT m () +sendSaveStateCommand = putMsg "saveState" + + +-- | Tell alloyIG to restore the state +sendRestoreStateCommand :: MonadIO m => AlloyIGT m () +sendRestoreStateCommand = putMsg "restoreState" + + +-- | Tell alloyIG to remove the constraint +sendRemoveConstraintCommand :: MonadIO m => Span -> AlloyIGT m () +sendRemoveConstraintCommand s = case s of + (Span from to) -> + do + putMsg "removeConstraint" + sendPosition from >> sendPosition to + (PosSpan _ from to) -> -- Should never happen + do + putMsg "removeConstraint" + sendPosition from >> sendPosition to + where + sendPosition (Pos line column) = + putMsg (show line) >> putMsg (show column) + sendPosition (PosPos _ line column) = + putMsg (show line) >> putMsg (show column) -- Should never happen + + +-- | Tell alloyIG to return the unsat core of the previous operation +sendUnsatCoreCommand :: MonadIO m => AlloyIGT m UnsatCore +sendUnsatCoreCommand = + do + putMsg "unsatCore" + coreLength <- readMsg + core' <- replicateM coreLength readConstraint + return $ UnsatCore core' + where + readPosition = liftM2 Pos readMsg readMsg + readConstraint = liftM2 Span readPosition readPosition + + +-- | Tell alloyIG to change the unsat core minimization level. +-- 0 -> Fastest, +-- 1 -> Medium, +-- 2 -> Best +sendSetUnsatCoreMinimizationCommand :: MonadIO m => Integer -> AlloyIGT m () +sendSetUnsatCoreMinimizationCommand level = + do + putMsg "unsatCoreMinimization" + putMsg $ show level + + +-- | Tell alloyIG to change the bitwidth +sendSetBitwidthCommand :: MonadIO m => Integer -> AlloyIGT m () +sendSetBitwidthCommand bitwidth = + do + when (bitwidth < 0) $ fail (show bitwidth ++ " is not a valid bitwidth.") + putMsg "setBitwidth" + putMsg $ show bitwidth + + +-- | Tell alloyIG to quit +sendQuitCommand :: MonadIO m => AlloyIGT m () +sendQuitCommand = putMsg "quit" + + +getMsg :: MonadIO m => AlloyIGT m String +getMsg = getMessage =<< proc + +readMsg :: (MonadIO m, Read r) => AlloyIGT m r +readMsg = read `liftM` getMsg + +putMsg :: MonadIO m => String -> AlloyIGT m () +putMsg msg = + do + proc' <- proc + putMessage proc' msg diff --git a/src/Language/Clafer/IG/ClaferIG.hs b/src/Language/Clafer/IG/ClaferIG.hs new file mode 100644 --- /dev/null +++ b/src/Language/Clafer/IG/ClaferIG.hs @@ -0,0 +1,385 @@ +{-# LANGUAGE NamedFieldPuns, GeneralizedNewtypeDeriving, StandaloneDeriving, DeriveDataTypeable #-} + +{- + Copyright (C) 2012-2014 Jimmy Liang, Michal Antkiewicz + + Permission is hereby granted, free of charge, to any person obtaining a copy of + this software and associated documentation files (the "Software"), to deal in + the Software without restriction, including without limitation the rights to + use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies + of the Software, and to permit persons to whom the Software is furnished to do + so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all + copies or substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. +-} + +module Language.Clafer.IG.ClaferIG ( + claferIGVersion, + IGArgs(..), + ClaferIGEnv(..), + getClaferEnv, + getClaferIGArgs, + getConstraints, + getClaferModel, + getInfo, + getStrMap, + ClaferIGT(..), + Instance(..), + Counterexample(..), + runClaferIGT, + getAlloyModel, + solve, + getClafers, + getGlobalScope, + getBitwidth, + setGlobalScope, + getScopes, + getScope, + getQNameMaps, + valueOfScope, + increaseScope, + setScope, + setAlloyScope, + next, + setUnsatCoreMinimization, + setBitwidth, + quit, + reload, + findRemovable, + fst3, + getlineNumMap, + strictReadFile, + sigToClaferName) where + +import Language.Clafer +import Language.Clafer.QNameUID +import Language.ClaferT +import Language.Clafer.Intermediate.Intclafer +import qualified Language.Clafer.Intermediate.Analysis as Analysis +import Language.Clafer.IG.AlloyIGInterface (AlloyIGT) +import qualified Language.Clafer.IG.AlloyIGInterface as AlloyIG +import Language.Clafer.IG.ClaferModel +import Language.Clafer.IG.Constraints +import Language.Clafer.IG.Solution +import Language.Clafer.IG.Sugarer +import Control.Applicative +import Control.Monad +import Control.Monad.Error +import Control.Monad.Trans.State.Strict +import Data.List +import Data.Monoid +import Data.Tuple (swap) +import Data.Map as Map hiding (map, null) +import qualified Data.Sequence as Seq +import Data.Maybe +import Data.Data +import System.Console.Haskeline.MonadException +import Paths_claferIG (version) +import Data.Version (showVersion) + +claferIGVersion :: String +claferIGVersion = "ClaferIG " ++ showVersion Paths_claferIG.version + +data IGArgs = IGArgs { + all :: Maybe Integer, + saveDir :: Maybe FilePath, + claferModelFile :: FilePath, + alloySolution :: Bool, + bitwidth :: Integer, + maxInt :: Integer, + useUids :: Bool, + addTypes :: Bool, + json :: Bool, + flatten_inheritance_comp :: Bool, + no_layout_comp :: Bool, + check_duplicates_comp :: Bool, + skip_resolver_comp :: Bool, + scope_strategy_comp :: ScopeStrategy + +} deriving (Show, Data, Typeable) + +newtype ClaferIGT m a = ClaferIGT (StateT ClaferIGEnv (AlloyIGT m) a) + deriving (Applicative, Functor, Monad, MonadIO) + +deriving instance MonadException m => MonadException (ClaferIGT m) + +instance MonadTrans ClaferIGT where + lift = ClaferIGT . lift . lift + +fetch :: Monad m => ClaferIGT m ClaferIGEnv +fetch = ClaferIGT get + +fetches :: Monad m => (ClaferIGEnv -> a) -> ClaferIGT m a +fetches = ClaferIGT . gets + +set :: Monad m => ClaferIGEnv -> ClaferIGT m () +set = ClaferIGT . put + +runClaferIGT :: MonadIO m => IGArgs -> ClaferIGT m a -> m (Either ClaferErrs a) +runClaferIGT args run = + AlloyIG.runAlloyIGT $ runErrorT $ do + env <- (ErrorT $ load args) `catchError` (\x -> lift AlloyIG.sendQuitCommand >> throwError x) + lift $ evalStateT (unwrap run) env + where + unwrap (ClaferIGT c) = c + + +data ClaferIGEnv = ClaferIGEnv{ + claferEnv'::ClaferEnv, + claferIGArgs :: IGArgs, + constraints:: [Constraint], + claferModel:: String, + qNameMaps :: QNameMaps, + info :: Analysis.Info, + strMap :: Map Int String, + lineNumMap :: Map Integer String +} + +data Instance = + Instance {modelInstance::ClaferModel, alloyModelInstance::String} | + UnsatCore {unsatConstraints::[Constraint], counterexample::Maybe Counterexample} | + NoInstance + + +data Counterexample = Counterexample {removedConstraints::[Constraint], counterexampleInstance::ClaferModel, counterexampleAlloyInstance::String} + +getClaferEnv :: Monad m => ClaferIGT m ClaferEnv +getClaferEnv = fetches claferEnv' + +getlineNumMap :: Monad m => ClaferIGT m (Map Integer String) +getlineNumMap = fetches lineNumMap + +getClaferIGArgs :: Monad m => ClaferIGT m IGArgs +getClaferIGArgs = fetches claferIGArgs + +getConstraints :: Monad m => ClaferIGT m [ Constraint ] +getConstraints = fetches constraints + +getClaferModel :: Monad m => ClaferIGT m String +getClaferModel = fetches claferModel + +getStrMap :: Monad m => ClaferIGT m (Map Int String) +getStrMap = fetches strMap + +getInfo :: Monad m => ClaferIGT m Analysis.Info +getInfo = fetches info + +load :: MonadIO m => IGArgs -> AlloyIGT m (Either ClaferErrs ClaferIGEnv) +load igArgs = + runErrorT $ do + claferModel <- liftIO $ strictReadFile claferFile' + + (claferEnv', alloyModel, mapping, sMap) <- ErrorT $ return $ callClaferTranslator claferModel + + let ir = fst3 $ fromJust $ cIr claferEnv' + let constraints = parseConstraints claferModel ir mapping + + lift $ AlloyIG.sendLoadCommand alloyModel + lift $ AlloyIG.sendSetBitwidthCommand bitwidth' + + let qNameMaps = deriveQNameMaps ir + + let info = Analysis.gatherInfo ir + let irTrace = editMap $ irModuleTrace claferEnv' + + return $ ClaferIGEnv claferEnv' igArgs constraints claferModel qNameMaps info sMap irTrace + where + editMap :: (Map.Map Span [Ir]) -> (Map.Map Integer String) -- Map Line Number to Clafer Name + editMap = + fromList . removeConstraints . Data.List.foldr (\(num, ir) acc -> case (getIClafer ir) of + Just (IClafer _ _ _ _ uid' _ _ _ _) -> (num, uid') : acc + _ -> acc) [] . tail . (Data.List.foldr (\x acc -> case x of + ((Span (Pos l1 _) (Pos l2 _)), irs) -> (zip [l1..l2] (replicate (fromIntegral $ l2 - l1 + 1) irs)) ++ acc + ((PosSpan _ (Pos l1 _) (Pos l2 _)), irs) -> (zip [l1..l2] (replicate (fromIntegral $ l2 - l1 + 1) irs)) ++ acc + ((Span (PosPos _ l1 _) (Pos l2 _)), irs) -> (zip [l1..l2] (replicate (fromIntegral $ l2 - l1 + 1) irs)) ++ acc + ((Span (Pos l1 _) (PosPos _ l2 _)), irs) -> (zip [l1..l2] (replicate (fromIntegral $ l2 - l1 + 1) irs)) ++ acc + ((Span (PosPos _ l1 _) (PosPos _ l2 _)), irs) -> (zip [l1..l2] (replicate (fromIntegral $ l2 - l1 + 1) irs)) ++ acc + ((PosSpan _ (PosPos _ l1 _) (Pos l2 _)), irs) -> (zip [l1..l2] (replicate (fromIntegral $ l2 - l1 + 1) irs)) ++ acc + ((PosSpan _ (Pos l1 _) (PosPos _ l2 _)), irs) -> (zip [l1..l2] (replicate (fromIntegral $ l2 - l1 + 1) irs)) ++ acc + ((PosSpan _ (PosPos _ l1 _) (PosPos _ l2 _)), irs) -> (zip [l1..l2] (replicate (fromIntegral $ l2 - l1 + 1) irs)) ++ acc) []) . toList + getIClafer :: [Ir] -> Maybe IClafer + getIClafer [] = Nothing + getIClafer ((IRClafer c):_) = Just c + getIClafer (_:rs) = getIClafer rs + removeConstraints :: [(Integer, String)] -> [(Integer, String)] + removeConstraints = map swap . reverse . toList . fromList . reverse . map swap + + callClaferTranslator code = + mapLeft ClaferErrs $ runClafer claferArgs $ do + addModuleFragment code + parse + compile + results <- generate + let (Just alloyResult) = Map.lookup Alloy results + return (claferEnv alloyResult, outputCode alloyResult, mappingToAlloy alloyResult, stringMap alloyResult) + mapLeft f (Left l) = Left $ f l + mapLeft _ (Right r) = Right r + claferArgs = defaultClaferArgs{keep_unused = True, no_stats = True, skip_goals = True ,flatten_inheritance = flatten_inheritance_comp igArgs, no_layout = no_layout_comp igArgs, check_duplicates = check_duplicates_comp igArgs, skip_resolver = skip_resolver_comp igArgs, scope_strategy = scope_strategy_comp igArgs} + claferFile' = claferModelFile igArgs + bitwidth' = bitwidth igArgs + + +strictReadFile :: FilePath -> IO String +strictReadFile filePath = + do + contents <- readFile filePath + -- readFile is lazy. Force it to evaluate by mapping over everything doing nothing + mapM_ return contents + return contents + + +getAlloyModel :: MonadIO m => ClaferIGT m String +getAlloyModel = ClaferIGT $ lift AlloyIG.getAlloyModel + + +solve :: MonadIO m => ClaferIGT m () +solve = ClaferIGT $ lift AlloyIG.sendResolveCommand + + +getClafers :: MonadIO m => ClaferIGT m [String] +getClafers = + do + sigs <- ClaferIGT $ lift AlloyIG.getSigs + return $ map sigToClaferName sigs + + +getGlobalScope :: MonadIO m => ClaferIGT m Integer +getGlobalScope = ClaferIGT $ lift AlloyIG.getGlobalScope + +getBitwidth :: MonadIO m => ClaferIGT m Integer +getBitwidth = + do + claferIGArgs' <- getClaferIGArgs + return $ bitwidth claferIGArgs' + +setGlobalScope :: MonadIO m => Integer -> ClaferIGT m () +setGlobalScope scope = ClaferIGT $ lift $ AlloyIG.sendSetGlobalScopeCommand scope + + +getScopes :: MonadIO m => ClaferIGT m [ (String, Integer) ] +getScopes = ClaferIGT $ lift AlloyIG.getScopes + + +getScope :: MonadIO m => QName -> ClaferIGT m ([String]) +getScope qName = do + qNameMaps' <- fetches qNameMaps + return $ getUIDs qNameMaps' qName + +getQNameMaps :: MonadIO m => ClaferIGT m (QNameMaps) +getQNameMaps = fetches qNameMaps + +valueOfScope :: MonadIO m => String -> ClaferIGT m Integer +valueOfScope sigName = ClaferIGT $ lift $ AlloyIG.getScope sigName + + +increaseScope :: MonadIO m => Integer -> (String, Integer) -> ClaferIGT m (Either String ()) +increaseScope increment (sigName, value) = setAlloyScope (value + increment) sigName + +setScope :: MonadIO m => Integer -> (String, Integer) -> ClaferIGT m (Either String ()) +setScope value (sigName, _) = setAlloyScope value sigName + +setAlloyScope :: MonadIO m => Integer -> String -> ClaferIGT m (Either String ()) +setAlloyScope value sigName = + do + subset <- ClaferIGT $ lift $ AlloyIG.sendSetScopeCommand sigName value + runErrorT $ maybe (return ()) throwError $ sigToClaferName <$> subset + + +next :: MonadIO m => ClaferIGT m Instance +next = do + env <- getClaferEnv + claferIGArgs' <- getClaferIGArgs + let + useUids' = useUids claferIGArgs' + addTypes' = addTypes claferIGArgs' + constraints' <- getConstraints + info' <- getInfo + xmlSolution <- ClaferIGT $ lift AlloyIG.sendNextCommand + sMap <- getStrMap + case xmlSolution of + Just xml -> return $ Instance (xmlToModel useUids' addTypes' info' xml sMap) xml + Nothing -> do + ClaferIGT $ lift AlloyIG.sendSaveStateCommand + -- Generating counterexample modifies the state. If we ever want to + -- rerun the original model, we need to restore the state. + AlloyIG.UnsatCore core <- ClaferIGT $ lift AlloyIG.sendUnsatCoreCommand + c <- counterexample env core useUids' addTypes' info' constraints' sMap + ClaferIGT $ lift AlloyIG.sendRestoreStateCommand + return c + where + counterexample env' originalCore useUids'' addTypes'' info'' constraints' sMap = counterexample' env' originalCore [] useUids'' addTypes'' info'' constraints' sMap + where + counterexample' env'' core removed useUids''' addTypes''' info''' constraints'' sMap' = + case msum $ findRemovable env'' core constraints'' of + Just remove -> do + ClaferIGT $ lift $ AlloyIG.sendRemoveConstraintCommand $ range remove + ClaferIGT $ lift AlloyIG.sendResolveCommand + xmlSolution <- ClaferIGT $ lift AlloyIG.sendNextCommand + case xmlSolution of + Just xml -> return $ + UnsatCore (catMaybes $ findRemovable env'' core constraints'') (Just $ Counterexample (reverse $ remove : removed) (xmlToModel useUids''' addTypes''' info''' xml sMap') xml) + Nothing -> + do + AlloyIG.UnsatCore core' <- ClaferIGT $ lift AlloyIG.sendUnsatCoreCommand + counterexample' env'' core' (remove : removed) useUids''' addTypes''' info''' constraints' sMap' + Nothing -> -- It is possible that none of the constraints are removable + return NoInstance + + xmlToModel :: Bool -> Bool -> Analysis.Info -> String -> (Map Int String) -> ClaferModel + xmlToModel useUids' addTypes' info' xml sMap = (sugarClaferModel useUids' addTypes' (Just info') $ buildClaferModel $ parseSolution xml) sMap + +reload :: MonadIO m => ClaferIGT m (Either ClaferErrs ()) +reload = + runErrorT $ do + globalScope <- lift $ getGlobalScope + claferIGArgs' <- lift $ getClaferIGArgs + env <- ErrorT $ ClaferIGT $ lift $ load claferIGArgs' + lift $ set env + lift $ setGlobalScope globalScope + + +setUnsatCoreMinimization :: MonadIO m => Integer -> ClaferIGT m () +setUnsatCoreMinimization level = ClaferIGT $ lift $ AlloyIG.sendSetUnsatCoreMinimizationCommand level + + +setBitwidth :: MonadIO m => Integer -> ClaferIGT m () +setBitwidth bitwidth' = do + claferIGArgs' <- getClaferIGArgs + igEnv <- fetch + set igEnv{claferIGArgs = claferIGArgs'{bitwidth=bitwidth'}} + ClaferIGT $ lift $ AlloyIG.sendSetBitwidthCommand bitwidth' + + +quit :: MonadIO m => ClaferIGT m () +quit = ClaferIGT $ lift AlloyIG.sendQuitCommand + + +sigToClaferName :: String -> String +sigToClaferName n = + case snd $ break ('_' ==) n of + [] -> n + x -> tail x + +findRemovable :: ClaferEnv -> [Span] -> [Constraint] -> [Maybe Constraint] +findRemovable env core constraints' = + let absIDs = foldMapIR getId $ fst3 $ fromJust $ cIr env + in Data.List.filter (removeAbsZero absIDs ) $ map (\c -> find ((== c) . range) constraints') core + where + removeAbsZero :: (Seq.Seq String) -> Maybe Constraint -> Bool + removeAbsZero absIDs (Just (UpperCardinalityConstraint _ (ClaferInfo uID (Cardinality 0 (Just 0))))) = ((Seq.elemIndexL uID absIDs)==Nothing) + removeAbsZero _ _ = True + getId :: Ir -> (Seq.Seq String) + getId (IRClafer (IClafer _ True _ uID _ _ _ _ _)) = Seq.singleton uID + getId _ = mempty + +fst3 :: (IModule, GEnv, Bool) -> IModule +fst3 (imod, _, _) = imod diff --git a/src/Language/Clafer/IG/ClaferModel.hs b/src/Language/Clafer/IG/ClaferModel.hs new file mode 100644 --- /dev/null +++ b/src/Language/Clafer/IG/ClaferModel.hs @@ -0,0 +1,196 @@ +{- + Copyright (C) 2012-2013 Jimmy Liang + + Permission is hereby granted, free of charge, to any person obtaining a copy of + this software and associated documentation files (the "Software"), to deal in + the Software without restriction, including without limitation the rights to + use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies + of the Software, and to permit persons to whom the Software is furnished to do + so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all + copies or substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. +-} + +module Language.Clafer.IG.ClaferModel (ClaferModel(..), Clafer(..), Id(..), Value(..), c_name, buildClaferModel, traverse) where + +import Data.List +import Data.Either +import Data.Map as Map hiding (filter, map, foldr, singleton) +import Data.Maybe +import Language.Clafer.IG.Solution +import Prelude hiding (id) + +-- | Clafer model instance +data ClaferModel = ClaferModel {c_topLevel::[Clafer]} +data Clafer = Clafer {c_id::Id, c_value::Maybe Value, c_children::[Clafer]} +data Value = AliasValue {c_alias::Id} | IntValue {v_value::Int} | StringValue {v_str ::String} deriving Show + +c_name :: Clafer -> String +c_name = i_name . c_id + +-- | The tuple of name and ordinal must be globally unique +data Id = Id {i_name::String, i_ordinal::Int} deriving (Eq, Ord, Show) + +data FamilyTree = FamilyTree (Map Id Node) (Map Id [Node]) deriving Show +data Node = ClaferNode Id Int | ValueNode Id Int deriving (Eq, Ord, Show) + +roots :: FamilyTree -> (Map Id Node) +roots (FamilyTree r _) = r + +n_id :: Node -> Id +n_id (ClaferNode i _) = i +n_id (ValueNode i _) = i + +{-n_type :: Node -> Int +n_type (ClaferNode _ t) = t +n_type (ValueNode _ t) = t-} + +instance Show ClaferModel where + show (ClaferModel clafers) = concatMap show clafers + +instance Show Clafer where + show clafer = displayClafer "" clafer + where + displayClafer indent (Clafer id value children) = + indent ++ i_name id ++ maybe "" displayValue value ++ + "\n" ++ concatMap (displayClafer $ indent ++ " ") children + displayValue (AliasValue alias) = " = " ++ i_name alias + displayValue (IntValue value) = " = " ++ show value + displayValue (StringValue value) = " = " ++ value + + + +traverse :: ClaferModel -> [Clafer] +traverse (ClaferModel clafers) = + traverseClafers clafers + where + traverseClafers :: [Clafer] -> [Clafer] + traverseClafers clafs = concatMap traverseClafer clafs + traverseClafer :: Clafer -> [Clafer] + traverseClafer clafer = clafer : traverseClafers (c_children clafer) + + +addChild :: Id -> Node -> FamilyTree -> FamilyTree +addChild parent child (FamilyTree roots' descens) = + FamilyTree roots'' descens' + where + roots'' = + case child of + (ClaferNode id _) -> Map.delete id roots' + _ -> roots' + descens' = (insertWith (++) parent [child] descens) + + +getChildren :: Id -> FamilyTree -> [Node] +getChildren parent (FamilyTree _ descens) = findWithDefault [] parent descens + + +getRoots :: FamilyTree -> [Node] +getRoots = elems . roots + +{- +-- Renames the items in the solution so they are easier to work with +-- -> +-- -> +-- -> +renameSolution :: Solution -> Solution +renameSolution (Solution sigs fields) = + Solution (map renameSig sigs) (map renameField fields) + where + renameSig sig = sig{s_label = renameSigLabel $ s_label sig} + renameSigLabel label + | label `elem` ["univ", "Int", "seq/Int", "String"] = label + | otherwise = fromMaybe (error $ "Unexpected sig label " ++ label) $ dropDelimiter '/' label + + renameField field = field{f_label = renameFieldLabel $ f_label field} + renameFieldLabel "ref" = "ref" + renameFieldLabel label = fromMaybe (error $ "Unexpected field label " ++ label) $ dropDelimiter '_' label + + dropDelimiter char string = + case snd $ break (== char) string of + [] -> Nothing + x -> Just $ tail x +-} + +buildFamilyTree :: Solution -> FamilyTree +buildFamilyTree (Solution sigs fields) = + buildFields fields + where + asNodes :: Sig -> [Node] + asNodes Sig{s_id = id, s_atoms = atoms} = map (flip ClaferNode id) $ map (labelAsId . a_label) atoms + rootNodes :: [(Id, Node)] + rootNodes = [(n_id rootNode, rootNode) | rootNode <- concatMap asNodes sigs] + + buildFields fields' = foldr buildField (FamilyTree (fromList rootNodes) Map.empty) fields' + buildField field tree = foldr (uncurry buildTuple) tree (zip ([0,1..]::[Integer]) $ f_tuples field) + where + label = f_label field + {- + - + - + - + - + - + - + - If Met is an alias then add two alias nodes in the family tree. + - addChild (Id "Alice" 0) (AliasNode (Id "Met" 1) (Id "Bob" 0)) + - addChild (Id "Bob" 0) (AliasNode (Id "Met" 2) (Id "Alice" 0)) + - + - Otherwise add two Clafer nodes in the family tree. + - addChild (Id "Alice" 0) (ClaferNode $ Id "Bob" 0) + - addChild (Id "Bob" 0) (ClaferNode $ Id "Alice" 0) + -} + buildTuple _ Tuple{t_from = from, t_to = to, t_toType = toType} tree' = + addChild (labelAsId $ a_label from) (buildNode (labelAsId $ a_label to) toType) tree' + where + buildNode = if label == "ref" then ValueNode else ClaferNode + + labelAsId :: String -> Id + labelAsId label = + case e of + [] -> Id label 0 + _ -> Id s (read $ tail e) + where + (s, e) = break (== '$') label + + +-- | A map of label -> Sig +buildSigMap :: Solution -> Map String Sig +buildSigMap (Solution sigs _) = Map.fromList $ zip (map s_label sigs) sigs + + +buildClaferModel :: Solution -> ClaferModel +buildClaferModel solution = + ClaferModel $ lefts $ map buildClafer (getRoots ftree) + where + sigMap = buildSigMap solution + ftree = buildFamilyTree solution + + intType = s_id $ findWithDefault (error "Missing Int sig") "Int" sigMap + + singleton [] = Nothing + singleton [x] = Just x + singleton xs = error $ "Received more than one value " ++ show xs + + buildClafer :: Node -> Either Clafer Value + buildClafer (ClaferNode id _) = + Left $ Clafer id (singleton valueChildren) claferChildren + where + (claferChildren, valueChildren) = partitionEithers $ map buildClafer children + children = getChildren id ftree + buildClafer (ValueNode value ntype') = + if ntype' == intType then + Right $ IntValue (read name) + else + Right $ AliasValue value + where + name = i_name value diff --git a/src/Language/Clafer/IG/CommandLine.hs b/src/Language/Clafer/IG/CommandLine.hs new file mode 100644 --- /dev/null +++ b/src/Language/Clafer/IG/CommandLine.hs @@ -0,0 +1,658 @@ +{-# LANGUAGE NamedFieldPuns #-} + +{- + Copyright (C) 2012-2014 Jimmy Liang, Michal Antkiewicz + + Permission is hereby granted, free of charge, to any person obtaining a copy of + this software and associated documentation files (the "Software"), to deal in + the Software without restriction, including without limitation the rights to + use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies + of the Software, and to permit persons to whom the Software is furnished to do + so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all + copies or substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. +-} + +module Language.Clafer.IG.CommandLine (runCommandLine, printError, findNecessaryBitwidth, intToFloat, pickLargerScope, allowedMaxInt, requiredBitwidth) where + +import Language.Clafer +import Language.ClaferT +import Language.Clafer.Intermediate.Intclafer +import Language.Clafer.IG.ClaferIG +import Language.Clafer.IG.ClaferModel +import Language.Clafer.IG.CommandLineParser +import Language.Clafer.IG.Constraints +import Language.Clafer.IG.JSONGenerator +import Language.Clafer.Comments +import Language.Clafer.JSONMetaData +import Language.Clafer.QNameUID +import qualified Language.Clafer.IG.AlloyIGInterface as AlloyIG +import Control.Monad +import Control.Monad.Error +import Data.Char +import Data.IORef +import Data.List +import Data.Monoid +import Data.Foldable (foldMap) +import qualified Data.StringMap as SMap +import qualified Data.Map as Map +import Data.Maybe +import System.Console.Haskeline +import System.IO +import GHC.Float +import Prelude hiding (id) +import qualified Text.Parsec.Error as E + +data AutoComplete = Auto_Command | Auto_Clafer | Auto_ClaferInstance | Auto_UnsatCoreMinimization | Auto_Space | Auto_Digit | No_Auto deriving Show + +data AutoCompleteContext = AutoCompleteContext {clafers::IORef [String], claferInstances::IORef [String]} + +data Context = Context {currentAlloyInstance::Maybe String, saved::[ClaferModel], unsaved::[ClaferModel], autoCompleteContext::AutoCompleteContext} + +-- | Interactive session interface +runCommandLine :: ClaferIGT IO () +runCommandLine = + do + solve + clafers <- getClafers + + clafersRef <- liftIO $ newIORef clafers + claferInstancesRef <- liftIO $ newIORef [] + + let autoCompleteContext = AutoCompleteContext clafersRef claferInstancesRef + runInputT Settings { + complete = completeFunc autoCompleteContext, + historyFile = Nothing, + autoAddHistory = True + } $ loop Next (Context Nothing [] [] autoCompleteContext) + where + + + loop :: Command -> Context -> InputT (ClaferIGT IO) () + + loop Quit _ = return () + + loop Next context = + do + solution <- lift next + claferIGArgs' <- lift getClaferIGArgs + info <- lift getInfo + case solution of + Instance claferModel xml -> do + liftIO $ writeIORef (claferInstances $ autoCompleteContext context) $ map c_name (traverse claferModel) + + outputStrLn $ if json claferIGArgs' + then generateJSON info claferModel + else "=== Instance " ++ (show $ 1 + (length $ unsaved context)) ++ " ===\n\n" ++ (show claferModel) + nextLoop context{unsaved=claferModel:(unsaved context), currentAlloyInstance=Just xml} + UnsatCore core counterexample -> do + liftIO $ hPutStrLn stderr "No more instances found. Try increasing scope to get more instances." + liftIO $ hPutStrLn stderr "The following set of constraints cannot be satisfied in the current scope." + liftIO $ hPutStrLn stderr "(Hint: use the setUnsatCoreMinimization command to minimize the set of constraints below)" + printConstraints core + case counterexample of + Just (Counterexample removed claferModel _) -> do + liftIO $ hPutStrLn stderr "Altering the following constraints produced the following near-miss example:" + printTransformations removed + outputStrLn $ show claferModel + Nothing -> return () + nextLoop context + NoInstance -> do + liftIO $ hPutStrLn stderr "No more instances found. Try increasing scope to get more instances." + nextLoop context + where + printTransformation :: Constraint -> [Constraint] -> (String, [Constraint]) + printTransformation UserConstraint{constraintInfo = info} rest = ("removed " ++ syntax info, rest) + printTransformation ExactCardinalityConstraint{claferInfo = info} rest = + (show info ++ " changed to " ++ show (setUpper (setLower info 0) Nothing), rest) + printTransformation LowerCardinalityConstraint{claferInfo = info} rest = + case deleteUpper (uniqueId info) rest of + -- Deleted the lower and upper constraint + Just rest' -> (show info ++ " changed to " ++ show (setUpper (setLower info 0) Nothing), rest') + -- Only deleted the lower constraint + Nothing -> (show info ++ " changed to " ++ show (setLower info 0), rest) + printTransformation UpperCardinalityConstraint{claferInfo = info} rest = + case deleteLower (uniqueId info) rest of + -- Deleted the lower and upper constraint + Just rest' -> (show info ++ " changed to " ++ show (setUpper (setLower info 0) Nothing), rest') + -- Only deleted the upper constraint + Nothing -> (show info ++ " changed to " ++ show (setUpper info Nothing), rest) + + printConstraint UserConstraint{constraintInfo = info} = show info + printConstraint constraint = show $ claferInfo constraint + + printConstraints = printConstraints' (1::Integer) + printConstraints' _ [] = return () + printConstraints' i (c:cs) = + do + liftIO $ hPutStrLn stderr $ " " ++ show i ++ ") " ++ printConstraint c + printConstraints' (i + 1) cs + + printTransformations cs = printTransformations' (1::Integer) cs + printTransformations' _ [] = return () + printTransformations' i (c:cs) = + do + let (prnt, rest) = printTransformation c cs + liftIO $ hPutStrLn stderr $ " " ++ show i ++ ") " ++ prnt + printTransformations' (i + 1) rest + + setLower info@ClaferInfo{cardinality = c} lower = info{cardinality = c{lower = lower}} + + setUpper info@ClaferInfo{cardinality = c} upper = info{cardinality = c{upper = upper}} + + deleteLower :: String -> [Constraint] -> Maybe [Constraint] + deleteLower id ys = + findAndDelete id (filter isLowerCardinalityConstraint ys) + + deleteUpper :: String -> [Constraint] -> Maybe [Constraint] + deleteUpper id ys = + findAndDelete id (filter isUpperCardinalityConstraint ys) + + findAndDelete :: String -> [Constraint] -> Maybe [Constraint] + findAndDelete _ [] = Nothing + findAndDelete id (c:cs) + | id == uniqueId (claferInfo c) = Just cs + | otherwise = (c :) `fmap` findAndDelete id cs + + + loop Help context = + do + outputStrLn ( + "------------------\n" ++ + "| " ++ claferIGVersion ++ " |\n" ++ + "------------------\n\n" ++ + "You can invoke the following commands as indicated by single quotes:\n" ++ + "[tab] - print the available commands\n" ++ + " - auto-complete command name, a clafer name, or clafer instance name in a given context\n" ++ + "'n'ext, [enter] - to produce the next instance if available or to output a message that no more \n" ++ + " instances exist within the given scope\n" ++ + "'i'ncrease - to increase the maximum number of instances of a given clafer or all clafers (scope)\n" ++ + "'s'et - to set the maximum number of instances of a given clafer or all clafers (scope)\n" ++ + "'m'axint, 'maxint' - to set the bitwidth by providing the largest integer\n" ++ + "sa'v'e - to save all instances displayed so far or a counterexample to files named \n" ++ + " .cfr..data, one instance per file\n" ++ + "'q'uit - to quit the interactive session\n" ++ + "'r'eload - to reload your clafer model\n" ++ + "'h'elp - to display this menu options summary\n" ++ + "'scope' - to print out the values of the global scope and individual Clafer scopes\n" ++ + "'saveScopes' - to generate a '.cfr-scope' file with the current scopes\n" ++ + "'loadScopes' - to load scopes from a '.cfr-scope' file\n" ++ + "'setUnsatCoreMinimization' - to choose UnSAT core minimization strategy [fastest | medium | best]. Default: fastest\n" ++ + "'c', 'claferModel' - to print out the original Clafer model verbatim\n" ++ + "'a', 'alloyModel' - to print out the output of Clafer translator verbatim\n" ++ + "'alloyInstance' - to print out the Alloy xml document of the most recent solution\n" ++ + "'f'ind - to print a Clafer with given name found in the most recent solution\n\n" ++ + "Parameterized command usage:\n" ++ + "'i [enter]' - to increase for all clafers by 1\n" ++ + "'i [enter]' - to increase for the clafer by 1\n" ++ + "'i ' - to increase for the clafer by \n" ++ + "'s [enter]'- to set for the clafers to \n" ++ + "'s ' - to set for the clafer to \n" ++ + "'f ' - to display a clafer \n" ++ + "'setUnsatCoreMinimization fastest' - fastest but the worst\n" ++ + "'setUnsatCoreMinimization medium'\n" ++ + "'setUnsatCoreMinimization best' - best but slowest even for modest size cores" + ) + + nextLoop context + + loop Save context@Context{saved=saved, unsaved=unsaved} = + do + save unsaved (toInteger $ length saved) + nextLoop context{saved=unsaved ++ saved, unsaved=[]} + + loop Reload context = + do + oldScopes <- lift getScopes + oldBw <- lift getBitwidth + + runErrorT $ ErrorT (lift reload) `catchError` (liftIO . mapM_ (hPutStrLn stderr) . printError) + + env <- lift getClaferEnv + let ir = fst3 $ fromJust $ cIr env + tempScopes <- lift getScopes + lift $ mergeScopes oldScopes tempScopes + + newScopes <- lift getScopes + lift $ setBitwidth $ findNecessaryBitwidth ir oldBw $ snd $ unzip newScopes + newBw <- lift getBitwidth + printBitwidthWarning newBw + lift $ solve + nextLoop context + + loop (IncreaseGlobalScope inc') context = + do + globalScope <- lift getGlobalScope + bitwidth' <- lift getBitwidth + let newGlobalScope = max 1 $ globalScope+inc' + lift $ setGlobalScope newGlobalScope + when (newGlobalScope > allowedMaxInt bitwidth') $ do + outputStrLn $ "Warning! Requested global scope is larger than maximum allowed by bitwidth ... increasing bitwidth" + lift $ setBitwidth $ requiredBitwidth newGlobalScope + newBw <- lift getBitwidth + printBitwidthWarning newBw + + oldScopes <- lift getScopes + mapM ( \(sigName', val') -> setAlloyScopeAndBitwidth bitwidth' (max 1 $ val'+inc') (sigToClaferName sigName') sigName') oldScopes + lift solve + outputStrLn ("Global scope changed to " ++ show newGlobalScope) + nextLoop context + loop (SetGlobalScope newGlobalScope') context = + do + let newGlobalScope = max 1 newGlobalScope' + bitwidth' <- lift getBitwidth + lift $ setGlobalScope newGlobalScope + when (newGlobalScope > allowedMaxInt bitwidth') $ do + outputStrLn $ "Warning! Requested global scope is larger than maximum allowed by bitwidth ... increasing bitwidth" + lift $ setBitwidth $ requiredBitwidth newGlobalScope + newBw <- lift getBitwidth + printBitwidthWarning newBw + lift solve + outputStrLn ("Global scope set to " ++ show newGlobalScope) + nextLoop context + + loop (IncreaseScope fqName inc') context = + do + try $ do + qNameMaps' <- lift $ lift $ getQNameMaps + let uids = getUIDs qNameMaps' fqName + let sigs = map ("this/" ++) uids + bitwidth' <- lift $ lift getBitwidth + + lift $ mapM_ (incAlloyScopeAndBitwidth bitwidth' inc' fqName) sigs + + lift $ lift $ solve + nextLoop context + + loop (SetScope qName val') context = + do + try $ do + qNameMaps' <- lift $ lift $ getQNameMaps + let uids = getUIDs qNameMaps' qName + let sigs = map ((++) "this/") uids + bitwidth' <- lift $ lift getBitwidth + + lift $ mapM_ (setAlloyScopeAndBitwidth bitwidth' val' qName) sigs + + lift $ lift $ solve + nextLoop context + + loop (SetBitwidth newBitwidth) context = + do + when (newBitwidth >=4) $ do + lift $ setBitwidth newBitwidth + printBitwidthWarning newBitwidth + lift solve + printBitwidthIntRange newBitwidth + nextLoop context + + loop (SetMaxInt newMaxInt) context = + do + when (newMaxInt >= 7) $ do + let newBitwidth = requiredBitwidth newMaxInt + lift $ setBitwidth newBitwidth + printBitwidthWarning newBitwidth + lift solve + printBitwidthIntRange newBitwidth + nextLoop context + + loop ShowScopes context = + do + globalScope <- lift getGlobalScope + outputStrLn $ "Global scope = " ++ show globalScope + originalScopes <- lift getScopes + -- remove the "this/" prefix + mapM_ printScope originalScopes + nextLoop context + + where + printScope (sigName, value) = + outputStrLn $ " " ++ (drop 5 sigName) ++ " scope = " ++ show value + + loop SaveScopes context = + do + globalScope <- lift getGlobalScope + originalScopes <- lift getScopes + claferIGArgs' <- lift getClaferIGArgs + qNameMaps' <- lift getQNameMaps + let + globalScopeTuple = ("", globalScope) + -- remove the "this/" prefix + uidScopes = globalScopeTuple : (map (\(sigName, value) -> (drop 5 sigName, value)) originalScopes) + json = generateJSONScopes qNameMaps' uidScopes + claferModelFile' = claferModelFile claferIGArgs' + modelName = take (length claferModelFile' - 4) claferModelFile' + saveName = modelName ++ ".cfr-scope" + + liftIO $ writeFile saveName json + nextLoop context + + loop LoadScopes context = + do + outputStrLn "Not implemented yet." + nextLoop context + + loop (Find name) context = + do + case (unsaved context ++ saved context) of + model:_ -> + case find ((name ==) . c_name) $ traverse model of + Just clafer' -> outputStrLn $ show clafer' + Nothing -> outputStrLn $ "\"" ++ name ++ "\" not found in the model." + [] -> outputStrLn $ "No instance" + nextLoop context + + loop ShowClaferModel context = + do + bitwidth' <- lift getBitwidth + printBitwidthIntRange bitwidth' + originalScopes <- lift getScopes + -- remove the "this/" prefix + let + scopes = map ( \ (uid', val') -> (drop 5 uid', val') ) originalScopes + scopesMap = Map.fromList scopes + + globalScope' <- lift getGlobalScope + outputStrLn $ "Global scope = " ++ show globalScope' ++ "\n" + + env <- lift getClaferEnv + constraints' <- lift getConstraints + AlloyIG.UnsatCore core <- lift $ ClaferIGT $ lift AlloyIG.sendUnsatCoreCommand + let unSATs = map getConstraintInfo $ catMaybes $ findRemovable env core constraints' + + claferModel <- lift getClaferModel + let commentLines = getCommentLines claferModel + lineNumMap <- lift getlineNumMap + + + outputStrLn $ editModel claferModel commentLines unSATs lineNumMap scopesMap + nextLoop context + where + editModel :: String -> [Integer] -> [String] -> (Map.Map Integer String) -> (Map.Map String Integer) -> String + editModel model cLines unSATs lineNumMap scopesMap' = + let + claferLines = lines $ removeCommentsAndUnify model + maxLineLength = maximum $ map length claferLines + in unlines $ editLines cLines unSATs (numberOfDigits $ length claferLines) maxLineLength scopesMap' lineNumMap (zip [1..] claferLines) + + editLines :: [Integer] -> [String] -> Int -> Int -> (Map.Map String Integer) -> (Map.Map Integer String) -> [(Integer, String)] -> [String] + editLines _ _ _ _ _ _ [] = [] + editLines cLines unSATs m1 m2 scopesMap' lineNumMap ((num, l):rest) = + if (num `elem` cLines && isEmptyLine l) + then editLines cLines unSATs m1 m2 scopesMap' lineNumMap rest + else (show num ++ "." ++ (replicate (1 + m1 - (numberOfDigits $ fromIntegral num)) ' ') ++ (if (isUnSAT unSATs l num) then "> " else "| ") ++ l ++ (replicate (3 + m2 - (length l)) ' ') ++ (if (isUnSAT unSATs l num) then " String -> Integer -> Bool + isUnSAT us l ln = getAny $ foldMap (\u -> Any (((safehead $ words u) == (safehead $ words l) && (safehead $ reverse $ words u) == (safehead $ reverse $ words l)) || (u `isInfixOf` l) || ("column" `isInfixOf` u && "line" `isInfixOf` u && (init $ head $ tail $ tail $ reverse $ words u) == show ln))) us + safehead [] = [] + safehead x = head x + + addScopeVal :: (Map.Map String Integer) -> (Maybe String) ->String + addScopeVal _ Nothing = "" + addScopeVal scopesMap' (Just name) = "scope = " ++ (fromJustShow $ Map.lookup name scopesMap') + + getCommentLines :: String -> [Integer] + getCommentLines = foldr (\(s, _) acc -> case s of + (Span (Pos l1 _) (Pos l2 _)) -> [l1..l2] ++ acc + (PosSpan _ (Pos l1 _) (Pos l2 _)) -> [l1..l2] ++ acc + (Span (PosPos _ l1 _) (Pos l2 _)) -> [l1..l2] ++ acc --This one and bellow should not happen + (Span (Pos l1 _) (PosPos _ l2 _)) -> [l1..l2] ++ acc + (Span (PosPos _ l1 _) (PosPos _ l2 _)) -> [l1..l2] ++ acc + (PosSpan _ (PosPos _ l1 _) (Pos l2 _)) -> [l1..l2] ++ acc + (PosSpan _ (Pos l1 _) (PosPos _ l2 _)) -> [l1..l2] ++ acc + (PosSpan _ (PosPos _ l1 _) (PosPos _ l2 _)) -> [l1..l2] ++ acc) [] . getComments + + getConstraintInfo :: Constraint -> String + getConstraintInfo (UserConstraint _ info) = show info + getConstraintInfo x = show $ claferInfo x + + loop ShowAlloyModel context = + do + globalScope' <- lift getGlobalScope + alloyModel <- lift getAlloyModel + scopes <- lift getScopes + + outputStrLn $ editAlloyModel alloyModel scopes globalScope' + nextLoop context + where + editAlloyModel :: String -> [(String, Integer)] -> Integer -> String + editAlloyModel model s globalScope' = + let alloyLines = lines $ removeCommentsAndUnify model + splitNum = 1 + (length $ takeWhile (not . isEmptyLine) alloyLines) + (alloyInfo, alloyLines') = splitAt splitNum $ alloyLines + in unlines $ (("global scope = " ++ show globalScope' ++ "\n") :) $ alloyInfo ++ map (\(num, line) -> show num ++ ('.' : (replicate (1 + (numberOfDigits $ length alloyLines) - (numberOfDigits num)) ' ') ++ ('|' : ' ' : line))) (zip [(1 + splitNum)..] (addScopeVals alloyLines' s (maximum $ map length alloyLines'))) + addScopeVals :: [String] -> [(String, Integer)] -> Int -> [String] + addScopeVals [] _ _ = [] + addScopeVals (l:ls) ss m = + let val = Data.List.lookup (takeWhile (`notElem` [' ','\t','\n']) $ tail $ dropWhile (/='_') l) ss + in if ("sig" `notElem` words l) then ((l ++ (replicate (3 + m - (length l)) ' ') ++ " |") : addScopeVals ls ss m) + else (l ++ (replicate (3 + m - (length l)) ' ') ++ " | scope = " ++ (fromJustShow val)) : addScopeVals ls ss m + + loop ShowAlloyInstance context = + do + case currentAlloyInstance context of + Just alloyInstance -> outputStrLn alloyInstance + Nothing -> outputStrLn $ "No instance" + nextLoop context + + loop (SetUnsatCoreMinimization level) context = + do + let level' = + case level of + Fastest -> 2 + Medium -> 1 + Best -> 0 + lift $ setUnsatCoreMinimization level' >> solve + + nextLoop context + + nextLoop context = + do + minput <- getInputLine "claferIG> " + case minput of + Nothing -> loop Quit context + Just input -> + case parseCommandLine input of + Left msg -> outputStrLn (show msg) >> nextLoop context + Right command -> loop command context + + save :: MonadIO m => [ClaferModel] -> Integer -> InputT (ClaferIGT m) () + save [] _ = return () + save (c:cs) counter = do + claferIGArgs' <- lift $ getClaferIGArgs + let + claferModelFile' = claferModelFile claferIGArgs' + saveName = claferModelFile' ++ "." ++ (show counter) ++ ".data" + liftIO $ writeFile saveName (show c) + outputStrLn $ "Saved to " ++ saveName + save cs (counter + 1) + +try :: MonadIO m => ErrorT String (InputT m) a -> InputT m () +try e = either outputStrLn (void . return) =<< runErrorT e + +incAlloyScopeAndBitwidth :: MonadIO m => Integer -> Integer -> String -> UID -> InputT (ClaferIGT m) () +incAlloyScopeAndBitwidth bitwidth' inc' fqName' sigName' = do + scopeValue <- lift $ valueOfScope sigName' + setAlloyScopeAndBitwidth bitwidth' (max 1 $ scopeValue+inc') fqName' sigName' + +setAlloyScopeAndBitwidth :: MonadIO m => Integer -> Integer -> String -> UID -> InputT (ClaferIGT m) () +setAlloyScopeAndBitwidth bitwidth' newValue' fqName' sigName' = do + when (newValue' > allowedMaxInt bitwidth') $ do + lift $ setBitwidth $ requiredBitwidth $ newValue' + newBw <- lift $ getBitwidth + outputStrLn $ "Warning! Requested scope for " ++ fqName' ++ " is larger than maximum allowed by bitwidth ... increasing bitwidth" + printBitwidthWarning newBw + lift $ setAlloyScope newValue' sigName' + outputStrLn $ "Scope of " ++ fqName' ++ " (" ++ (drop 5 sigName') ++ ") changed to " ++ show newValue' + +mergeScopes :: MonadIO m => [(UID, Integer)] -> [(UID, Integer)] -> ClaferIGT m () +mergeScopes _ [] = return() +mergeScopes oldScopes newScopes = do + let mergedScopes = map (pickLargerScope oldScopes) newScopes + mapM_ (\(uid, val) -> setAlloyScope val uid) mergedScopes + +pickLargerScope :: [(String, Integer)] -> (String, Integer) -> (String, Integer) +pickLargerScope oldScopes (uid, val) = + let + oldScopesMap = SMap.fromList oldScopes + oldVal = SMap.findWithDefault val uid oldScopesMap + in (uid, max val oldVal) + +-- | bitwidth required to store the given integer +requiredBitwidth :: Integer -> Integer +requiredBitwidth n = ceiling $ logBase 2 $ (+1) $ (*2) $ intToFloat n + +-- | the largest integer allowed by the given bitwidth +allowedMaxInt :: Integer -> Integer +allowedMaxInt bw = (2 ^ (bw - 1)) - 1 + +-- | the smallest integer allowed by the given bitwidth +allowedMinInt :: Integer -> Integer +allowedMinInt bw = -((allowedMaxInt bw) + 1) + +printBitwidthIntRange :: MonadIO m => Integer -> InputT m () +printBitwidthIntRange bw = outputStrLn $ concat [ + "Integer range = ", + show $ allowedMinInt bw, + "..", + show $ allowedMaxInt bw, + " (", + "bitwidth = ", + show bw, + ")" ] + +printBitwidthWarning :: MonadIO m => Integer -> InputT m () +printBitwidthWarning bw = when (bw > 9) $ outputStrLn $ "Warning! This is a very large bitwidth for Alloy, which may cause slow down." + +-- i Ali|ce +-- If the cursor is at | then not open. The "ce" prevents autocomplete. +-- i Ali| ce +-- Is open, and autocomplete will kick in. +isOpen :: String -> [Char] -> Bool +isOpen _ [] = True +isOpen _ (x:_) = isSpace x + + +completeFunc :: MonadIO m => AutoCompleteContext -> CompletionFunc m +completeFunc context (prev, nxt) = + if isOpen prev nxt then + liftIO $ evalComplete context prev + else + return (prev, []) + + +completePrefix :: String -> [String] -> [Completion] +completePrefix prefix choices = map simpleCompletion $ filter (prefix `isPrefixOf`) choices + + +evalComplete :: AutoCompleteContext -> String -> IO (String, [Completion]) +evalComplete context prev = + do + completion <- autoComplete context word auto + return (reverseRest, completion) + where + input = reverse prev + (reverseWord, reverseRest) = break isSpace prev + word = reverse reverseWord + auto = autoCompleteDetect $ parseCommandLineAutoComplete input + + +autoComplete :: AutoCompleteContext -> String -> AutoComplete -> IO [Completion] +autoComplete _ word Auto_Command = return $ completePrefix word commandStrings +autoComplete context word Auto_Clafer = + do + c <- readIORef $ clafers context + return $ completePrefix word c +autoComplete context word Auto_ClaferInstance = + do + ci <- readIORef $ claferInstances context + return $ completePrefix word ci +autoComplete _ word Auto_UnsatCoreMinimization = return $ completePrefix word ["fastest", "medium", "best"] +autoComplete _ _ Auto_Digit = return [] -- Don't auto complete numbers. +autoComplete _ word Auto_Space = return [simpleCompletion $ word] +autoComplete _ _ No_Auto = return [] + +autoCompleteDetect :: E.ParseError -> AutoComplete +autoCompleteDetect error' + -- An unexpected message means that parsing failed before eof + | any (not . null) unexpectedMessages = No_Auto + | any (== "command") expectedMessages = Auto_Command + | any (== "clafer") expectedMessages = Auto_Clafer + | any (== "claferInstance") expectedMessages = Auto_ClaferInstance + | any (== "Unsat core minimization level") expectedMessages = Auto_UnsatCoreMinimization + | any (== "digit") expectedMessages = Auto_Digit + | any (== "space") expectedMessages = Auto_Space + | otherwise = No_Auto + where + messages = errorMessages error' + unexpectedMessages = mapMaybe unexpectedMessage messages + expectedMessages = mapMaybe expectedMessage messages + + +printError :: ClaferErrs -> [String] +printError (ClaferErrs errs) = + map printErr errs + where + printErr (ParseErr (ErrPos _ _ (Pos l c)) msg) = + "Parse error at line " ++ show l ++ ", column " ++ show c ++ ":\n " ++ msg + printErr (SemanticErr (ErrPos _ _ (Pos l c)) msg) = + "Error at line " ++ show l ++ ", column " ++ show c ++ ":\n " ++ msg + printErr (ParseErr (ErrPos _ _ (PosPos _ l c)) msg) = + "Parse error at line " ++ show l ++ ", column " ++ show c ++ ":\n " ++ msg --This should never happen + printErr (SemanticErr (ErrPos _ _ (PosPos _ l c)) msg) = + "Error at line " ++ show l ++ ", column " ++ show c ++ ":\n " ++ msg --This should never happen + printErr (ClaferErr msg) = + "Error:\n " ++ msg + +-- only remove the contents while preserving the empty lines +removeCommentsAndUnify :: String -> String +removeCommentsAndUnify [] = [] +removeCommentsAndUnify model@[_] = model +removeCommentsAndUnify ('\t':model) = ' ' : ' ' : ' ' : removeCommentsAndUnify model +removeCommentsAndUnify ('/':'/':model) = removeCommentsAndUnify $ dropWhile (/='\n') model +removeCommentsAndUnify ('/':'*':model) = removeBlock model + where + -- discard everything until "*/" is found or end of text while preserving new lines + removeBlock :: String -> String + removeBlock [] = [] + removeBlock [_] = [] + removeBlock ('\n':model') = '\n' : removeBlock model' + removeBlock ('*':'/':model') = removeCommentsAndUnify model' + -- discard contents of the block comment + removeBlock (_:model') = removeBlock model' +removeCommentsAndUnify (c:model) = c : removeCommentsAndUnify model + +isEmptyLine :: String -> Bool +isEmptyLine l = filter (`notElem` [' ', '\n', '\t', '\r']) l == [] + +numberOfDigits :: Int -> Int +numberOfDigits x = length $ show x + +findNecessaryBitwidth :: IModule -> Integer -> [ Integer ] -> Integer +findNecessaryBitwidth ir oldBw scopeValues = + if (newBw < oldBw) then oldBw else newBw + where + newBw = ceiling $ logBase 2 $ (+1) $ (*2) $ maxInModel ir + maxInModel :: IModule -> Float + maxInModel ir' = intToFloat $ max (maximum scopeValues) $ foldIR getMax 0 ir' + getMax :: Ir -> Integer -> Integer + getMax (IRIExp (IInt n)) m = max m $ abs n + getMax (IRClafer IClafer{card = Just (_, n)}) m = max m n + getMax _ m = m + +intToFloat :: Integer -> Float +intToFloat = fromInteger . toInteger + +fromJustShow :: (Maybe Integer) -> String +fromJustShow (Just x) = show x +fromJustShow Nothing = "Nothing" diff --git a/src/Language/Clafer/IG/CommandLineParser.hs b/src/Language/Clafer/IG/CommandLineParser.hs new file mode 100644 --- /dev/null +++ b/src/Language/Clafer/IG/CommandLineParser.hs @@ -0,0 +1,271 @@ +{- + Copyright (C) 2012-2014 Jimmy Liang, Michal Antkiewicz + + Permission is hereby granted, free of charge, to any person obtaining a copy of + this software and associated documentation files (the "Software"), to deal in + the Software without restriction, including without limitation the rights to + use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies + of the Software, and to permit persons to whom the Software is furnished to do + so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all + copies or substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. +-} + +module Language.Clafer.IG.CommandLineParser (Command(..), UnsatCoreMinimization(..), parseCommandLine, parseCommandLineAutoComplete, commandStrings, expectedMessage, unexpectedMessage, errorMessages) where + +import Control.Monad +import Data.List +import Text.ParserCombinators.Parsec +import Text.ParserCombinators.Parsec.Error +import Text.Parsec.Prim hiding (try) +import Data.Functor.Identity + + +-- | Interactive session commands +data Command = Next | + IncreaseGlobalScope Integer | + IncreaseScope String Integer | + SetGlobalScope Integer | + SetScope String Integer | + SetBitwidth Integer | + SetMaxInt Integer | + Save | + Quit | + Reload | + Help | + Find String | + ShowScopes | + SaveScopes | + LoadScopes | + ShowClaferModel | + ShowAlloyModel | + ShowAlloyInstance | + SetUnsatCoreMinimization UnsatCoreMinimization deriving Show + + +data UnsatCoreMinimization = Fastest | Medium | Best deriving Show + + +unexpectedMessage :: Message -> Maybe String +unexpectedMessage (SysUnExpect x) = Just x +unexpectedMessage (UnExpect x) = Just x +unexpectedMessage _ = Nothing + +expectedMessage :: Message -> Maybe String +expectedMessage (Expect x) = Just x +expectedMessage _ = Nothing + + +parseCommandLine :: String -> Either ParseError Command +parseCommandLine input = + if null input then Right Next + else parse doParse "claferIG" input + where + doParse = + do + skipMany (space "") + c <- commandLine + skipMany (space "") + eof + return c + + +-- | This function uses the expected/unexpected messages to understand what to autocomplete. +-- Any unexpected character means parse did not reach the end of the input, hence cannot autocomplete. +parseCommandLineAutoComplete :: String -> ParseError +parseCommandLineAutoComplete input = + case parse doParse "claferIG autocomplete" input of + Left e -> e + Right _ -> error "Failed at failing." + where + doParse = + do + skipMany (space "") + commandLine + -- Force the parse to fail to gather expected/unexpected messages + fail "reached end" + + +commandLine :: Parser Command +commandLine = + do + name <- command + case lookup name commandMap of + Just x -> x + Nothing -> + fail $ "Unknown command \"" ++ name ++ "\"" ++ hint didYouMean + where + quote x = '"' : x ++ "\"" + didYouMean = filter (name `isPrefixOf`) commandStrings + hint [] = "" + hint _ = ", did you mean " ++ intercalate " or " (map quote didYouMean) ++ "?" + + +command :: Parser String +command = many1 (letter "command") + + +-- Used by the autocomplete algorithm +commandStrings :: [String] +commandStrings = map fst commandMap + + +commandMap :: [(String, Parser Command)] +commandMap = + ("h", helpCommand): + ("i", increaseCommand): + ("s", setCommand): + ("b", setBitwidthCommand): + ("m", setMaxIntCommand): + ("maxint", setMaxIntCommand): + ("n", nextCommand): + ("f", findCommand): + ("q", quitCommand): + ("v", saveCommand): + ("r", reloadCommand): + ("scope", showScopesCommand): + ("saveScopes", saveScopesCommand): + ("loadScopes", loadScopesCommand): + ("claferModel", claferModelCommand): + ("c", claferModelCommand): + ("alloyModel", alloyModelCommand): + ("a", alloyModelCommand): + ("alloyInstance", alloyInstanceCommand): + ("setUnsatCoreMinimization", setUnsatCoreMinimization): + [] + + +helpCommand :: ParsecT String () Identity Command +helpCommand = return Help +increaseCommand :: Parser Command +increaseCommand = increaseGlobalScope +setCommand :: Parser Command +setCommand = setGlobalScope +setBitwidthCommand :: Parser Command +setBitwidthCommand = setBitwidth +setMaxIntCommand :: Parser Command +setMaxIntCommand = setMaxInt +nextCommand :: ParsecT String () Identity Command +nextCommand = return Next +quitCommand :: ParsecT String () Identity Command +quitCommand = return Quit +saveCommand :: ParsecT String () Identity Command +saveCommand = return Save +reloadCommand :: ParsecT String () Identity Command +reloadCommand = return Reload +findCommand :: ParsecT String () Identity Command +findCommand = Find `liftM` (gap >> claferInstance) +showScopesCommand :: ParsecT String () Identity Command +showScopesCommand = return ShowScopes +saveScopesCommand :: ParsecT String () Identity Command +saveScopesCommand = return SaveScopes +loadScopesCommand :: ParsecT String () Identity Command +loadScopesCommand = return LoadScopes +claferModelCommand :: ParsecT String () Identity Command +claferModelCommand = return ShowClaferModel +alloyModelCommand :: ParsecT String () Identity Command +alloyModelCommand = return ShowAlloyModel +alloyInstanceCommand :: ParsecT String () Identity Command +alloyInstanceCommand = return ShowAlloyInstance +setUnsatCoreMinimization :: ParsecT String () Identity Command +setUnsatCoreMinimization = SetUnsatCoreMinimization `liftM` (gap >> unsatCoreMinimization) + +gap :: ParsecT String () Identity () +gap = skipMany1 space + + +increaseGlobalScope :: Parser Command +increaseGlobalScope = + do + try (gap >> explicitIncreaseGlobalScope) + <|> + return (IncreaseGlobalScope 1) + +setGlobalScope :: Parser Command +setGlobalScope = + do + try (gap >> explicitSetGlobalScope) + <|> + do + try (gap >> explicitSetScope) + +explicitIncreaseGlobalScope :: Parser Command +explicitIncreaseGlobalScope = + fmap IncreaseGlobalScope signedNumber + <|> + increaseScope + +explicitSetGlobalScope :: Parser Command +explicitSetGlobalScope = fmap SetGlobalScope number + +increaseScope :: Parser Command +increaseScope = + do + name <- clafer + do + try (gap >> explicitIncreaseScope name) + <|> + return (IncreaseScope name 1) + +explicitIncreaseScope :: String -> Parser Command +explicitIncreaseScope name = fmap (IncreaseScope name) signedNumber + +explicitSetScope :: Parser Command +explicitSetScope = + do + name <- clafer + gap + i <- number + return (SetScope name i) + +setBitwidth :: Parser Command +setBitwidth = + do + gap + b <- number + return $ SetBitwidth b + +setMaxInt :: Parser Command +setMaxInt = + do + gap + b <- number + return $ SetMaxInt b + +number :: Parser Integer +number = do + n <- many1 digit + return $ read n + +signedNumber :: Parser Integer +signedNumber = do + s <- option "" $ string "-" + n <- many1 digit + return $ read $ s ++ n + +clafer :: Parser String +clafer = many1 ((alphaNum <|> char ':' <|> char '_') "clafer") + + +claferInstance :: Parser String +claferInstance = many1 (alphaNum "claferInstance") + + +unsatCoreMinimization :: Parser UnsatCoreMinimization +unsatCoreMinimization = + do + level <- many1 (letter "Unsat core minimization level") + case level of + "fastest" -> return Fastest + "medium" -> return Medium + "best" -> return Best + x -> fail $ x ++ " is not a valid unsat core minimization level" diff --git a/src/Language/Clafer/IG/Constraints.hs b/src/Language/Clafer/IG/Constraints.hs new file mode 100644 --- /dev/null +++ b/src/Language/Clafer/IG/Constraints.hs @@ -0,0 +1,196 @@ +{-# LANGUAGE NamedFieldPuns #-} + +{- + Copyright (C) 2012-2013 Jimmy Liang + + Permission is hereby granted, free of charge, to any person obtaining a copy of + this software and associated documentation files (the "Software"), to deal in + the Software without restriction, including without limitation the rights to + use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies + of the Software, and to permit persons to whom the Software is furnished to do + so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all + copies or substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. +-} + +module Language.Clafer.IG.Constraints (Constraint(..), Cardinality(..), ClaferInfo(..), ConstraintInfo(..), isLowerCardinalityConstraint, isUpperCardinalityConstraint, lookupConstraint, parseConstraints) where + +import Data.List +import Data.Maybe +import Data.Ord +import Language.Clafer +import Language.Clafer.Front.Absclafer (Span(..)) +import Language.Clafer.Intermediate.Intclafer +import qualified Language.Clafer.Intermediate.Intclafer as I + + + +data Constraint = + ExactCardinalityConstraint {range::Span, claferInfo::ClaferInfo} | + LowerCardinalityConstraint {range::Span, claferInfo::ClaferInfo} | + UpperCardinalityConstraint {range::Span, claferInfo::ClaferInfo} | + UserConstraint {range::Span, constraintInfo::ConstraintInfo} + deriving (Show, Eq) + + +data Cardinality = Cardinality {lower::Integer, upper::Maybe Integer} deriving Eq + +instance Show Cardinality where + show (Cardinality 0 Nothing) = "*" + show (Cardinality 1 Nothing) = "+" + show (Cardinality lower Nothing) = show lower ++ "..*" + show (Cardinality 0 (Just 1)) = "?" + show (Cardinality lower (Just upper)) + | lower == upper = show lower + | otherwise = show lower ++ ".." ++ show upper + + +data ClaferInfo = ClaferInfo {uniqueId::String, cardinality::Cardinality} deriving Eq + +instance Show ClaferInfo where + show (ClaferInfo uniqueId cardinality) = uniqueId ++ " " ++ show cardinality + + +data ConstraintInfo = ConstraintInfo {pId::String, pos::Span, syntax::String} deriving Eq + +instance Show ConstraintInfo where + show ConstraintInfo{pos = Span (Pos l c) _, syntax} = syntax ++ " (line " ++ show l ++ ", column " ++ show c ++ ")" + show ConstraintInfo{pos = PosSpan _ (Pos l c) _, syntax} = syntax ++ " (line " ++ show l ++ ", column " ++ show c ++ ")" -- Should never happen + show ConstraintInfo{pos = Span (PosPos _ l c) _, syntax} = syntax ++ " (line " ++ show l ++ ", column " ++ show c ++ ")" -- Should never happen + show ConstraintInfo{pos = PosSpan _ (PosPos _ l c) _, syntax} = syntax ++ " (line " ++ show l ++ ", column " ++ show c ++ ")" -- Should never happen + + + +isLowerCardinalityConstraint :: Constraint -> Bool +isLowerCardinalityConstraint LowerCardinalityConstraint{} = True +isLowerCardinalityConstraint _ = False + + +isUpperCardinalityConstraint :: Constraint -> Bool +isUpperCardinalityConstraint UpperCardinalityConstraint{} = True +isUpperCardinalityConstraint _ = False + + +to :: Span -> Pos +to (Span _ t) = t +to (PosSpan _ _ t) = t -- Should never happen +{-from :: Span -> Pos +from (Span f _) = f +from (PosSpan _ f _) = f -- Should never happen-} + + +lookupConstraint :: Span -> [Constraint] -> Constraint +lookupConstraint constraint' constraints = + case [x | x <- constraints, constraint' == range x] of + [] -> error $ show constraint' ++ " not equal to known constraints " ++ show constraints + cs -> minimumBy (comparing $ to . range) cs + + +parseConstraints :: String -> IModule -> [(Span, IrTrace)] -> [Constraint] +parseConstraints claferModel imodule mapping = + mapMaybe (uncurry convert) mapping + where + clafers = mDecls imodule >>= subclafers + pexps = (mapMaybe constraint $ mDecls imodule ++ concatMap elements clafers) >>= subexpressions + convert s IrPExp{pUid} = + Just $ UserConstraint s $ ConstraintInfo pUid (inPos $ findPExp pUid) $ extract $ inPos $ findPExp pUid + convert s LowerCard{pUid, isGroup = False} = + Just $ LowerCardinalityConstraint s $ claferInfo pUid + convert s UpperCard{pUid, isGroup = False} = + Just $ UpperCardinalityConstraint s $ claferInfo pUid + convert s ExactCard{pUid, isGroup = False} = + Just $ ExactCardinalityConstraint s $ claferInfo pUid + convert _ _ = Nothing + + findPExp pUid = fromMaybe (error $ "Unknown constraint " ++ pUid) $ find ((== pUid) . pid) pexps + findClafer pUid = fromMaybe (error $ "Unknown clafer " ++ pUid) $ find ((== pUid) . uid) clafers + text = lines claferModel + extract (Span (Pos l1 c1) (Pos l2 c2)) -- This one should occur the rest should not happen + | l1 == l2 = drop (fromInteger $ c1 - 1) $ take (fromInteger $ c2 - 1) $ text !! (fromInteger $ l1 - 1) + | otherwise = unlines $ f1 : fs ++ [fn] + where + f1 = drop (fromInteger $ c1 - 1) $ text !! (fromInteger $ l1 - 1) + fs = map (text !!) [(fromInteger $ l1) .. (fromInteger $ l2 - 2)] + fn = take (fromInteger $ c2 - 1) $ text !! (fromInteger $ l2 - 1) + extract (Span (PosPos _ l1 c1) (Pos l2 c2)) + | l1 == l2 = drop (fromInteger $ c1 - 1) $ take (fromInteger $ c2 - 1) $ text !! (fromInteger $ l1 - 1) + | otherwise = unlines $ f1 : fs ++ [fn] + where + f1 = drop (fromInteger $ c1 - 1) $ text !! (fromInteger $ l1 - 1) + fs = map (text !!) [(fromInteger $ l1) .. (fromInteger $ l2 - 2)] + fn = take (fromInteger $ c2 - 1) $ text !! (fromInteger $ l2 - 1) + extract (Span (Pos l1 c1) (PosPos _ l2 c2)) + | l1 == l2 = drop (fromInteger $ c1 - 1) $ take (fromInteger $ c2 - 1) $ text !! (fromInteger $ l1 - 1) + | otherwise = unlines $ f1 : fs ++ [fn] + where + f1 = drop (fromInteger $ c1 - 1) $ text !! (fromInteger $ l1 - 1) + fs = map (text !!) [(fromInteger $ l1) .. (fromInteger $ l2 - 2)] + fn = take (fromInteger $ c2 - 1) $ text !! (fromInteger $ l2 - 1) + extract (Span (PosPos _ l1 c1) (PosPos _ l2 c2)) + | l1 == l2 = drop (fromInteger $ c1 - 1) $ take (fromInteger $ c2 - 1) $ text !! (fromInteger $ l1 - 1) + | otherwise = unlines $ f1 : fs ++ [fn] + where + f1 = drop (fromInteger $ c1 - 1) $ text !! (fromInteger $ l1 - 1) + fs = map (text !!) [(fromInteger $ l1) .. (fromInteger $ l2 - 2)] + fn = take (fromInteger $ c2 - 1) $ text !! (fromInteger $ l2 - 1) + extract (PosSpan _ (Pos l1 c1) (Pos l2 c2)) + | l1 == l2 = drop (fromInteger $ c1 - 1) $ take (fromInteger $ c2 - 1) $ text !! (fromInteger $ l1 - 1) + | otherwise = unlines $ f1 : fs ++ [fn] + where + f1 = drop (fromInteger $ c1 - 1) $ text !! (fromInteger $ l1 - 1) + fs = map (text !!) [(fromInteger $ l1) .. (fromInteger $ l2 - 2)] + fn = take (fromInteger $ c2 - 1) $ text !! (fromInteger $ l2 - 1) + extract (PosSpan _ (PosPos _ l1 c1) (Pos l2 c2)) + | l1 == l2 = drop (fromInteger $ c1 - 1) $ take (fromInteger $ c2 - 1) $ text !! (fromInteger $ l1 - 1) + | otherwise = unlines $ f1 : fs ++ [fn] + where + f1 = drop (fromInteger $ c1 - 1) $ text !! (fromInteger $ l1 - 1) + fs = map (text !!) [(fromInteger $ l1) .. (fromInteger $ l2 - 2)] + fn = take (fromInteger $ c2 - 1) $ text !! (fromInteger $ l2 - 1) + extract (PosSpan _ (Pos l1 c1) (PosPos _ l2 c2)) + | l1 == l2 = drop (fromInteger $ c1 - 1) $ take (fromInteger $ c2 - 1) $ text !! (fromInteger $ l1 - 1) + | otherwise = unlines $ f1 : fs ++ [fn] + where + f1 = drop (fromInteger $ c1 - 1) $ text !! (fromInteger $ l1 - 1) + fs = map (text !!) [(fromInteger $ l1) .. (fromInteger $ l2 - 2)] + fn = take (fromInteger $ c2 - 1) $ text !! (fromInteger $ l2 - 1) + extract (PosSpan _ (PosPos _ l1 c1) (PosPos _ l2 c2)) + | l1 == l2 = drop (fromInteger $ c1 - 1) $ take (fromInteger $ c2 - 1) $ text !! (fromInteger $ l1 - 1) + | otherwise = unlines $ f1 : fs ++ [fn] + where + f1 = drop (fromInteger $ c1 - 1) $ text !! (fromInteger $ l1 - 1) + fs = map (text !!) [(fromInteger $ l1) .. (fromInteger $ l2 - 2)] + fn = take (fromInteger $ c2 - 1) $ text !! (fromInteger $ l2 - 1) + convertCard (l, -1) = Cardinality l Nothing + convertCard (l, h) = Cardinality l $ Just h + claferInfo pUid = + ClaferInfo (ident claf) $ convertCard $ fromJust $ card claf + where + claf = findClafer pUid + + +subclafers :: IElement -> [IClafer] +subclafers (IEClafer claf) = claf : (elements claf >>= subclafers) +subclafers _ = [] + +constraint :: IElement -> Maybe PExp +constraint (IEConstraint _ pexp) = Just pexp +constraint _ = Nothing + +subexpressions :: PExp -> [PExp] +subexpressions p@PExp{I.exp = exp'} = + p : subexpressions' exp' + where + subexpressions' IDeclPExp{oDecls, bpexp} = + concatMap (subexpressions . body) oDecls ++ subexpressions bpexp + subexpressions' IFunExp{exps} = concatMap subexpressions exps + subexpressions' _ = [] diff --git a/src/Language/Clafer/IG/JSONGenerator.hs b/src/Language/Clafer/IG/JSONGenerator.hs new file mode 100644 --- /dev/null +++ b/src/Language/Clafer/IG/JSONGenerator.hs @@ -0,0 +1,88 @@ +{- + Copyright (C) 2013 Michal Antkiewicz + + Permission is hereby granted, free of charge, to any person obtaining a copy of + this software and associated documentation files (the "Software"), to deal in + the Software without restriction, including without limitation the rights to + use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies + of the Software, and to permit persons to whom the Software is furnished to do + so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all + copies or substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. +-} + +module Language.Clafer.IG.JSONGenerator (generateJSON) where + +import qualified Language.Clafer.IG.ClaferModel as M +import qualified Language.Clafer.Intermediate.Analysis as A +import Data.Json.Builder +import Data.String.Conversions +import Prelude hiding (id) + +-- | Generate a representation of the instance in JSON format +generateJSON :: A.Info -> M.ClaferModel -> String +generateJSON info (M.ClaferModel topLevelClafers) = + convertString $ toJsonBS $ constructElements $ map (printClafer info) topLevelClafers + +printClafer :: A.Info -> M.Clafer -> Object +printClafer info (M.Clafer id value children) = + (map (printClafer info) children) `addElements` completeClaferObject + where + uid = M.i_name id + sclafer = A.runAnalysis (A.claferWithUid $ removeOrdinal uid) info + ident = A.uid sclafer + + getSuper :: Maybe A.SSuper -> (Bool, String) + getSuper Nothing = (False, "") + getSuper (Just (A.Ref s)) = (True, s) + getSuper (Just (A.Colon s)) = (False, s) + + (isOverlapping, super) = getSuper $ A.super sclafer + cardMin = A.low sclafer + cardMax = A.high sclafer + basicClaferObject = makeBasicClaferObject ident uid super isOverlapping cardMin cardMax + + addValue :: Maybe M.Value -> Object -> Object + addValue Nothing object = object + addValue (Just (M.IntValue i)) object = addIntValue i object + addValue (Just (M.AliasValue a)) object = addStringValue (M.i_name a) object + addValue (Just (M.StringValue _)) _ = error "Function addValue from JSONGenerator does not accept StringValues" -- Should never happen, string values are not generated yet + + completeClaferObject = addValue value basicClaferObject + + removeOrdinal :: String -> String + removeOrdinal = takeWhile (/= '$') + +makeBasicClaferObject :: String -> String -> String -> Bool -> Integer -> Integer -> Object +makeBasicClaferObject ident uid super isOverlapping cardMin cardMax = + mconcat [ row "ident" ident, + row "uid" uid, + row "super" super, + row "isOverlapping" isOverlapping, + row "cardMin" cardMin, + row "cardMax" cardMax ] + +addIntValue :: Int -> Object -> Object +addIntValue value claferObject = + claferObject `mappend` (row "value" value) + +addStringValue :: String -> Object -> Object +addStringValue value claferObject = + claferObject `mappend` (row "value" value) + +addElements :: [ Object ] -> Object -> Object +addElements elements claferObject = + claferObject `mappend` (constructElements elements) + +constructElements :: [ Object ] -> Object +constructElements elements = + row "elements" $ mconcat $ map element elements diff --git a/src/Language/Clafer/IG/Process.hs b/src/Language/Clafer/IG/Process.hs new file mode 100644 --- /dev/null +++ b/src/Language/Clafer/IG/Process.hs @@ -0,0 +1,82 @@ +{- + Copyright (C) 2012-2013 Jimmy Liang + + Permission is hereby granted, free of charge, to any person obtaining a copy of + this software and associated documentation files (the "Software"), to deal in + the Software without restriction, including without limitation the rights to + use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies + of the Software, and to permit persons to whom the Software is furnished to do + so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all + copies or substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. +-} + +module Language.Clafer.IG.Process (Process, executableDirectory, waitFor, getContentsVerbatim, getMessage, readMessage, putMessage, pipeProcess) where + +import Control.Monad +import Control.Monad.IO.Class +import System.Environment.Executable +import System.IO +import System.Process +import GHC.IO.Exception + +data Process = Process{stdIn::Handle, stdOut::Handle, procHandle::ProcessHandle} + + + +executableDirectory :: IO FilePath +executableDirectory = fst `liftM` splitExecutablePath + + +-- | Start another process and return the piped std_in, std_out stream +pipeProcess :: FilePath -> [String] -> IO Process +pipeProcess exec args = + do + let process = (proc exec args) { std_in = CreatePipe, std_out = CreatePipe } + (Just stdIn', Just stdOut', _, proceHandle) <- createProcess process + hSetNewlineMode stdIn' noNewlineTranslation + return $ Process stdIn' stdOut' proceHandle -- Pipe always has a handle according to docs + + +-- | Wait until the process terminates +waitFor :: Process -> IO ExitCode +waitFor proce = waitForProcess (procHandle proce) + + +-- | Reads the entire output verbatim +getContentsVerbatim :: Process -> IO String +getContentsVerbatim proce = + do + contents <- hGetContents $ stdOut proce + -- hGetContents is lazy. Force it to evaluate by mapping over everything doing nothing + mapM_ return contents + return contents + + +-- | Read the message +getMessage :: MonadIO m => Process -> m String +getMessage proce = + liftIO $ do + len <- read `liftM` hGetLine (stdOut proce) + mapM hGetChar $ replicate len (stdOut proce) + +readMessage :: (Read r, MonadIO m) => Process -> m r +readMessage proce = read `liftM` getMessage proce + +-- | Put the message +putMessage :: MonadIO m => Process -> String -> m () +putMessage proce message = + liftIO $ do + hPutStrLn (stdIn proce) (show $ length message) + hPutStr (stdIn proce) message + hFlush (stdIn proce) + diff --git a/src/Language/Clafer/IG/Solution.hs b/src/Language/Clafer/IG/Solution.hs new file mode 100644 --- /dev/null +++ b/src/Language/Clafer/IG/Solution.hs @@ -0,0 +1,104 @@ +{- + Copyright (C) 2012-2013 Jimmy Liang + + Permission is hereby granted, free of charge, to any person obtaining a copy of + this software and associated documentation files (the "Software"), to deal in + the Software without restriction, including without limitation the rights to + use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies + of the Software, and to permit persons to whom the Software is furnished to do + so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all + copies or substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. +-} + +module Language.Clafer.IG.Solution (Solution(..), Sig(..), Atom(..), Field(..), Tuple(..), parseSolution) where + +import Control.Monad +import Data.Maybe +import Text.XML.HaXml +import Text.XML.HaXml.Posn +import Prelude hiding (id) + +-- | Alloy solution +data Solution = Solution{s_sigs::[Sig], s_fields::[Field]} deriving Show + +-- | The univ sig does not have a parent +data Sig = Sig {s_label::String, s_id::Int, s_parentId::Maybe Int, s_atoms::[Atom]} deriving Show + +data Atom = Atom {a_label::String} deriving Show + +data Field = Field {f_label::String, f_id::Int, f_parentId::Int, f_tuples::[Tuple]} deriving Show + +data Tuple = Tuple {t_from::Atom, t_fromType::Int, t_to::Atom, t_toType::Int} deriving Show + + + +parseSolution :: String -> Solution +parseSolution xml = + let (Document _ _ root _) = xmlParse "claferIG" xml + rootElem = CElem root noPos + sigElems = tag "alloy" /> tag "instance" /> tag "sig" + fieldElems = tag "alloy" /> tag "instance" /> tag "field" + + sigs = map parseSig $ sigElems rootElem + fields = map parseField $ fieldElems rootElem + in + Solution sigs fields + + +parseSig :: Content i -> Sig +parseSig content' = + Sig label id parentId atoms + where + parentId = read `liftM` findOptAttr "parentID" content' + label = findAttr "label" content' + id = read $ findAttr "ID" content' + atoms = map parseAtom $ (keep /> tag "atom") content' + + +parseAtom :: Content i -> Atom +parseAtom = Atom . findAttr "label" + + +parseField :: Content i -> Field +parseField content' = + Field + (findAttr "label" content') + (read $ findAttr "ID" content') + (read $ findAttr "parentID" content') + (map parseTuple $ (keep /> tag "tuple") content') + where + + parseType :: Content i -> (Int, Int) + parseType content'' = + (toFromType !! 0, toFromType !! 1) + where toFromType = map (read . findAttr "ID") $ (keep /> tag "types" /> tag "type") content'' + + (fromType, toType) = parseType content' + + parseTuple :: Content i -> Tuple + parseTuple content''' = + Tuple (toFrom !! 0) fromType (toFrom !! 1) toType + where toFrom = map parseAtom $ (keep /> tag "atom") content''' + + +findOptAttr :: String -> Content i -> Maybe String +findOptAttr name ele = show `liftM` lookup (N name) (getAttrs ele) + + +findAttr :: String -> Content i -> String +findAttr name ele = fromJust $ show `fmap` lookup (N name) (getAttrs ele) + + +getAttrs :: Content i -> [Attribute] +getAttrs (CElem (Elem _ attributes _) _) = attributes +getAttrs _ = error "Function getAttrs from Solution was given an invliad argument expected of type (CElem (Elem _ attributes _) _)" -- This should never happen diff --git a/src/Language/Clafer/IG/Sugarer.hs b/src/Language/Clafer/IG/Sugarer.hs new file mode 100644 --- /dev/null +++ b/src/Language/Clafer/IG/Sugarer.hs @@ -0,0 +1,123 @@ +{- + Copyright (C) 2012-2014 Jimmy Liang, Michal Antkiewicz + + Permission is hereby granted, free of charge, to any person obtaining a copy of + this software and associated documentation files (the "Software"), to deal in + the Software without restriction, including without limitation the rights to + use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies + of the Software, and to permit persons to whom the Software is furnished to do + so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all + copies or substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. +-} + +module Language.Clafer.IG.Sugarer (sugarClaferModel) where + +import Language.Clafer.IG.ClaferModel +import qualified Language.Clafer.Intermediate.Analysis as Analysis +import Data.Maybe (fromJust) +import Data.List as List hiding (map) +import Data.Map as Map hiding (map, foldr, foldl) +import Prelude hiding (id) + + +-- | Sample: maps the id to the its simple name and the number of times its simple name appeared in the census before it +-- | Count: maps the simple name to the total count of the simple name +data Census = Census + (Map Id (Int, String)) -- Sample + (Map String Int) -- Counts + deriving Show + + +-- | Adds the full name to the census +poll :: Id -> Census -> Census +poll id (Census sample' counts') = + Census sample'' counts'' + where + fullName = i_name id + name = makeSimpleName fullName + counts'' = insertWith (+) name 1 counts' + ordinal' = findWithDefault (error $ "Did not find " ++ name ++ " in counts.") name counts'' + sample'' = insertWith (error $ "Polled " ++ fullName ++ " twice in the census.") id (ordinal', name) sample' + -- Transforms c2_name -> name + makeSimpleName :: String -> String + makeSimpleName name' = case dropWhile (/='_') name' of + "" -> error "Unexpected Clafer name " ++ name' + x -> tail x + +-- | Count the number of each clafer +claferModelCensus :: ClaferModel -> Census +claferModelCensus (ClaferModel topLevelClafers) = + clafersCensus (Census Map.empty Map.empty) topLevelClafers + where + clafersCensus = foldl claferCensus + claferCensus census Clafer{c_id=id, c_children=children} = poll id (clafersCensus census children) + + +-- | Rewrite the model into a human-friendlier format +sugarClaferModel:: Bool -> Bool -> Maybe Analysis.Info -> ClaferModel -> (Map Int String) -> ClaferModel +sugarClaferModel useUids addTypes info model@(ClaferModel topLevelClafers) sMap = + ClaferModel $ map sugarClafer topLevelClafers + where + sugarClafer (Clafer id value children) = + Clafer (sugarId useUids addTypes True id) (sugarValue (Clafer id value children)) (map sugarClafer children) + + sugarValue (Clafer _ (Just (AliasValue alias)) _) = Just $ AliasValue $ sugarId useUids addTypes False alias + sugarValue (Clafer _ Nothing _) = Nothing + sugarValue c = if (cType c) == "string" then (Just ((StringValue) (getString c))) else (c_value c) + + cType (Clafer id _ _) = + case (fromJust (Analysis.super (Analysis.runAnalysis (Analysis.claferWithUid (i_name id)) (fromJust info)))) of + (Analysis.Ref s) -> cTypeSolve s + (Analysis.Colon s) -> cTypeSolve s + + cTypeSolve "string" = "string" + cTypeSolve "integer" = "integer" + cTypeSolve "int" = "integer" + cTypeSolve "real" = "real" + cTypeSolve x = cType (Clafer (Id x 0) Nothing []) + + getString c = case (Map.lookup strNumber sMap) of + Nothing -> "\"\"" + Just s -> s + where strNumber = v_value $ fromJust $ c_value c + + + Census sample' counts' = claferModelCensus model + + sugarId :: Bool -> Bool -> Bool -> Id -> Id + sugarId useUids' addTypes' addRefDecl id = + if count == 1 + then Id (finalName ++ (refDecl addTypes' addRefDecl info)) 0 + else Id (finalName ++ "$" ++ show ordinal ++ (refDecl addTypes' addRefDecl info)) 0 + where + fullName = i_name id + + refDecl :: Bool -> Bool -> Maybe Analysis.Info -> String + refDecl True True (Just info') = retrieveSuper info' $ i_name id + refDecl _ _ _ = "" + + (ordinal, simpleName) = findWithDefault (error $ "Sample lookup " ++ show id ++ " failed.") id sample' + count = findWithDefault (error $ "Count lookup " ++ simpleName ++ " failed.") simpleName counts' + finalName = if useUids' then fullName else simpleName + +retrieveSuper :: Analysis.Info -> String -> String +retrieveSuper info uid = + if (Analysis.isBase sclafer) + then "" + else maybe "" sugarSuper (Analysis.super sclafer) + where + sclafer = Analysis.runAnalysis (Analysis.claferWithUid uid) info + + sugarSuper :: Analysis.SSuper -> String + sugarSuper (Analysis.Ref s) = " -> " ++ s + sugarSuper (Analysis.Colon s) = " : " ++ s diff --git a/src/Main.hs b/src/Main.hs new file mode 100644 --- /dev/null +++ b/src/Main.hs @@ -0,0 +1,156 @@ +{-# LANGUAGE DeriveDataTypeable #-} + +{- + Copyright (C) 2012-2014 Jimmy Liang, Michal Antkiewicz + + Permission is hereby granted, free of charge, to any person obtaining a copy of + this software and associated documentation files (the "Software"), to deal in + the Software without restriction, including without limitation the rights to + use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies + of the Software, and to permit persons to whom the Software is furnished to do + so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all + copies or substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. +-} + +module Main where + +import Language.Clafer.IG.ClaferIG +import Language.Clafer.IG.ClaferModel +import Language.Clafer.IG.CommandLine +import Language.Clafer.IG.Solution +import Language.Clafer.IG.Sugarer +import Language.Clafer.ClaferArgs +import Language.ClaferT +import Control.Monad +import Control.Monad.IO.Class +import Data.Either +import qualified Data.Map as Map +import Data.Maybe +import Data.IORef +import Prelude hiding (all) +import System.Console.CmdArgs +import System.Directory +import System.FilePath + +claferIGArgsDef :: IGArgs +claferIGArgsDef = IGArgs { + all = def &= help "Saves all instances up to the provided scope or a counterexample.", + saveDir = def &= help "Specify the directory for storing saved files." &= typ "FILE", + bitwidth = 4 &= help "Set the bitwidth for integers." &= typ "INTEGER", -- Default bitwidth is 4. + maxInt = 7 &= help "Set the bitwidth for integers based on the largest required number. Overrides --bitwidth argument." &= typ "INTEGER", + alloySolution = False &= help "Convert Alloy solution to a Clafer solution.", + claferModelFile = def &= argPos 0 &= typ "FILE", + useUids = False &= help "Use unique clafer names in the Clafer solution.", + addTypes = False &= help "Add colon/reference types to the Clafer solution.", + json = False &= help "Render solution as JSON (forces 'addUids').", + flatten_inheritance_comp = def &= help "Flatten inheritance during compiling ('alloy' and 'alloy42' modes only)" &= name "i", + no_layout_comp = def &= help "Don't resolve off-side rule layout during compiling" &= name "l", + check_duplicates_comp = def &= help "Check duplicated clafer names during compiling" &= name "c", + skip_resolver_comp = def &= help "Skip name resolution during compiling" &= name "f", + scope_strategy_comp = Simple &= help "Use scope computation strategy during compiling: none, simple (default), or full." &= name "ss" +} &= summary claferIGVersion &= program "claferig" + + +main :: IO () +main = + do + args' <- cmdArgs claferIGArgsDef + let + bw = bitwidth args' + mi = maxInt args' + -- maxInt overrides the bitwidth setting + args'' = if (mi > allowedMaxInt bw) + then args' {bitwidth = requiredBitwidth mi} + else args' + + if (alloySolution args'') + then + runAlloySolution args'' + else if (json args'') + then + tryClaferIG (args'' { useUids = True }) + else + tryClaferIG args'' + where + tryClaferIG args3 = + do + try <- runClaferIG args3 + case try of + Right r -> return r + Left l -> do + mapM putStrLn $ printError l + putStrLn "Press enter to retry." + void getLine + tryClaferIG args3 + +runClaferIG :: IGArgs -> IO (Either ClaferErrs ()) +runClaferIG args' = + runClaferIGT args' $ do + cModel <- liftIO $ strictReadFile $ claferModelFile args' + when (cModel == "") $ error "Cannot instantiate an empty model." + oldBw <- getBitwidth + env <- getClaferEnv + let ir = fst3 $ fromJust $ cIr env + scopes <- getScopes + setBitwidth $ findNecessaryBitwidth ir oldBw $ map snd scopes + solve + case all args' of + Just scope -> + do + setGlobalScope scope + solve + + let file' = claferModelFile args' + counterRef <- liftIO $ newIORef 1 + + let saveDirectory = fromMaybe return $ underDirectory `liftM` saveDir args' + saveAll (savePath file' counterRef >>= saveDirectory) + return () + Nothing -> runCommandLine + + quit + +-- | Convert an Alloy XML file into an instance in Clafer +runAlloySolution :: IGArgs -> IO () +runAlloySolution args' = + do + content <- readFile $ claferModelFile args' -- It's an Alloy XML file in this case + let sMap = Map.empty + putStrLn $ show $ (sugarClaferModel (useUids args') (addTypes args') Nothing $ buildClaferModel $ parseSolution content) $ sMap + +savePath :: FilePath -> IORef Int -> IO FilePath +savePath file' counterRef = + do + counter <- readIORef counterRef + writeIORef counterRef (counter + 1) + return $ file' ++ "." ++ (show counter) ++ ".data" + + +underDirectory :: FilePath -> FilePath -> IO FilePath +underDirectory dir file' = + do + createDirectoryIfMissing True dir + return $ joinPath [dir, file'] + + +saveAll :: IO FilePath -> ClaferIGT IO () +saveAll nextFile = + do + file' <- liftIO nextFile + liftIO $ createDirectoryIfMissing True $ takeDirectory file' + solution <- next + case solution of + Instance{modelInstance = modelInstance'} -> do + liftIO $ writeFile file' (show modelInstance') + saveAll nextFile + _ -> return () diff --git a/test/test-suite.hs b/test/test-suite.hs new file mode 100644 --- /dev/null +++ b/test/test-suite.hs @@ -0,0 +1,115 @@ +{-# OPTIONS_GHC -XTemplateHaskell #-} +{- + Copyright (C) 2012-2013 Luke Brown + + Permission is hereby granted, free of charge, to any person obtaining a copy of + this software and associated documentation files (the "Software"), to deal in + the Software without restriction, including without limitation the rights to + use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies + of the Software, and to permit persons to whom the Software is furnished to do + so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all + copies or substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. + -} +import Language.Clafer.IG.ClaferIG +import Language.Clafer.IG.ClaferModel +import Language.Clafer.IG.CommandLine +import Control.Monad +import Control.Monad.IO.Class +import Data.Maybe +import Data.IORef +import System.Directory +import System.FilePath +import System.Console.CmdArgs +import Prelude hiding (all) +import Test.Framework +import Test.Framework.TH +import Test.Framework.Providers.HUnit +import Test.HUnit + +tg_testsuite :: Test.Framework.Test +tg_testsuite = $(testGroupGenerator) + +main :: IO () +main = defaultMain[tg_testsuite] + +claferIGArgsDef :: IGArgs +claferIGArgsDef = IGArgs { + all = def, + saveDir = def, + claferModelFile = def, + alloySolution = False, + bitwidth = 4, + maxInt = 7, + useUids = False, + addTypes = False, + json = False, + flatten_inheritance_comp = False, + no_layout_comp = False, + check_duplicates_comp = False, + skip_resolver_comp = False, + scope_strategy_comp = def +} &= summary claferIGVersion + + +defaultIGArgs :: FilePath -> IGArgs +--defaultIGArgs fPath = IGArgs Nothing Nothing fPath False 4 False False False +defaultIGArgs fPath = claferIGArgsDef{claferModelFile = fPath} + +--getModel :: MonadIO m => FilePath -> ClaferIGT m (Either Language.ClaferT.ClaferErrs Instance) +getModel fPath = runClaferIGT (defaultIGArgs fPath) $ do + setGlobalScope (fromJust $ all $ defaultIGArgs fPath) + solve + counterRef <- liftIO $ newIORef 1 + let saveDirectory = fromMaybe return $ underDirectory `liftM` saveDir (defaultIGArgs fPath) + let nextFile = savePath fPath counterRef >>= saveDirectory + file <- liftIO nextFile + liftIO $ createDirectoryIfMissing True $ takeDirectory file + next + where + savePath :: FilePath -> IORef Int -> IO FilePath + savePath fPath' counterRef = + do + counter <- readIORef counterRef + writeIORef counterRef (counter + 1) + return $ fPath' ++ "." ++ (show counter) ++ ".data" + underDirectory :: FilePath -> FilePath -> IO FilePath + underDirectory dir file = + do + createDirectoryIfMissing True dir + return $ joinPath [dir, file] + + +fromRight (Right x) = x + + +case_strMapCheck :: Assertion +case_strMapCheck = do + --let claferModel = Right $ Instance (ClaferModel [(Clafer (Id "" 0) (Just (StringValue "")) [])]) "" + claferModel' <- getModel "test/positive/i220.cfr" + (valueCheck $ c_value $ head $ c_topLevel $ modelInstance $ fromRight $ claferModel') @? "Mapping Int back to String Failed!" + where + valueCheck Nothing = False + valueCheck (Just (AliasValue _)) = False + valueCheck (Just (IntValue _)) = False + valueCheck (Just (StringValue _)) = True + +case_pickLargerScope :: Assertion +case_pickLargerScope = do + let + oldScopes = [ ("c0_1", 1), ("c1_b", 2), ("c0_x", 5) ] + newScopes = [ ("c0_1", 2), ("c0_b", 2), ("c1_b", 1)] + mergedScopes = map (pickLargerScope oldScopes) newScopes + + mergedScopes @?= [ ("c0_1", 2), ("c0_b", 2), ("c1_b", 2)] + + diff --git a/tools/Makefile b/tools/Makefile new file mode 100644 --- /dev/null +++ b/tools/Makefile @@ -0,0 +1,16 @@ +UNAME := $(shell uname | tr "A-Z" "a-z") + + +ifeq ($(UNAME), darwin) + WGET_COMMAND := curl -O +else + WGET_COMMAND := wget +endif + + + +all: + @if test ! -f "alloy4.jar"; then \ + echo "[WARNING] Missing alloy4.jar. Downloading..."; \ + $(WGET_COMMAND) http://alloy.mit.edu/alloy/downloads/alloy4.jar; \ + fi