claferIG 0.3.8 → 0.3.9

raw patch · 14 files changed

+276/−254 lines, 14 filesdep ~arraydep ~basedep ~claferPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: array, base, clafer, claferIG, containers, directory, filepath, mtl, parsec, process

API changes (from Hackage documentation)

Files

• CHANGES.md +7/−3
• Makefile +19/−1
• README.md +36/−34
• alloyIG.jar binary
• claferIG.cabal +91/−90
• src-cmd/Main.hs +31/−18
• src/Language/Clafer/IG/AlloyIGInterface.hs +1/−1
• src/Language/Clafer/IG/ClaferIG.hs +23/−22
• src/Language/Clafer/IG/CommandLine.hs +2/−2
• src/Language/Clafer/IG/Constraints.hs +1/−1
• src/Language/Clafer/IG/JSONGenerator.hs +34/−26
• src/Language/Clafer/IG/Sugarer.hs +28/−27
• test/test-suite.hs +1/−1
• tools/Makefile +2/−28

@@ -1,12 +1,16 @@-**ClaferIG Version 0.3.8 released on Jan 27, 2015**
+**ClaferIG Version 0.3.9 released on March 06, 2015**
 
+[Release](https://github.com/gsdlab/claferIG/pull/24)
+
+**ClaferIG Version 0.3.8 released on January 27, 2015**
+
 [Release](https://github.com/gsdlab/claferIG/pull/23)
 
-**ClaferIG Version 0.3.7 released on Oct 23, 2014**
+**ClaferIG Version 0.3.7 released on October 23, 2014**
 
 [Release](https://github.com/gsdlab/claferIG/pull/22)
 
-**ClaferIG Version 0.3.6.1 released on Jul 08, 2014**
+**ClaferIG Version 0.3.6.1 released on July 08, 2014**
 
 [Release](https://github.com/gsdlab/claferIG/pull/20)
 

@@ -1,5 +1,24 @@ TOOL_DIR = tools
 
+ifeq ($(OS),Windows_NT)
+	LIB := x86-windows/minisatprover*
+else
+	UNAME := $(shell uname -s)
+	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),Darwin)
+		WGET_COMMAND := curl -O
+		LIB := x86-mac/libminisatprover*
+	endif
+endif
+
 # Calling `make` should only build
 all: alloyIG.jar lib build
 
@@ -63,7 +82,6 @@ 	cp -r tools/ dist/build/claferIG/
 	cp -r lib/ dist/build/test-suite/
 	cp -r lib/ dist/build/claferIG/
-	# On Windows, also need to manually copy glpk_4_52.dll to dist/build/test-suite/
 	cabal test
 
 clean:

@@ -1,7 +1,7 @@ Clafer Instance Generator
 =========================
 
-v0.3.8
+v0.3.9
 
 [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).
@@ -24,13 +24,13 @@ 
 Regardless of the installation method, the following are required:
 
-* [Clafer](https://github.com/gsdlab/clafer) v0.3.8
-* [Java Platform (JDK)](http://www.oracle.com/technetwork/java/javase/downloads/index.html) v7+, 32bit
+* [Clafer](https://github.com/gsdlab/clafer) v0.3.9
+* [Java Platform (JDK)](http://www.oracle.com/technetwork/java/javase/downloads/index.html) v8+, 32bit
 * [Alloy4.2](http://alloy.mit.edu/alloy/download.html)
 
 ### Installation from binaries
 
-Binary distributions of the release 0.3.8 of Clafer Tools for Windows, Mac, and Linux, 
+Binary distributions of the release 0.3.9 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). 
 
 1. download the binaries and unpack `<target directory>` of your choice
@@ -40,13 +40,14 @@ 
 Dependencies
 
-* [The Haskell Platform](http://hackage.haskell.org/platform/) v2013.2.0.0
+* [The Haskell Platform](http://hackage.haskell.org/platform/) v2014.2.0.0 
+  * Alternatively GHC >= 7.8.3 and Cabal >= 1.18
 
-ClaferIG is now available on [Hackage](http://hackage.haskell.org/package/claferIG-0.3.8/) and it can be installed using
+ClaferIG is now available on [Hackage](http://hackage.haskell.org/package/claferIG-0.3.9/) and it can be installed using
 
 1. `cabal update`
 2. `cabal install claferIG`
-3. `cd <cabal's lib or share folder>`  (`C:\Users\<user>\AppData\Roaming\cabal\i386-windows-ghc-7.6.3\claferIG-0.3.8` on Windows or `.cabal/share/x86_64-linux-ghc-7.6.3/claferIG-0.3.8/` on Linux)
+3. `cd <cabal's lib or share folder>`  (`C:\Users\<user>\AppData\Roaming\cabal\i386-windows-ghc-7.8.3\claferIG-0.3.9` on Windows or `.cabal/share/x86_64-linux-ghc-7.8.3/claferIG-0.3.9/` on Linux)
 3. to automatically download Alloy4.2 jar
   * execute `make` in `tools` 
 4. To get the `minisatproover` library
@@ -60,19 +61,19 @@ 
 Dependencies
 
+* [The Haskell Platform](http://hackage.haskell.org/platform/) v2014.2.0.0 
+  * Alternatively GHC >= 7.8.3 and Cabal >= 1.18
 * [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.
-* Cabal >= 1.18
 * 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) 
-  * download [mingw-get-setup.exe](http://sourceforge.net/projects/mingw/files/Installer/mingw-get/)
-  * since the Haskell Platform already contains MinGW, only install MSYS. Installing another MinGW causes problems as it contains different versions of tools as compared to the MinGW in the Haskell Platform
-  * choose the existing MinGW location, e.g., `c:\...\HaskellPlatform\2013.2.0.0\MinGw`
-  * ensure `wget` and `unzip` are selected to be installed 
-  * add the `bin` folder of MSYS (`MinGW\MSYS\1.0\bin`) to your system path
+* [MSYS2](http://msys2.sourceforge.net/) 
+  * download MSYS2 installer
+  * in MSYS2 console, execute
+     * `pacman -Syu` 
+     * `pacman -S make wget unzip diffutils`
 
 ### Important: Branches must correspond
 
@@ -81,6 +82,7 @@ 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)
@@ -92,7 +94,7 @@ 
 ### Installation
 
-1. execute `make install to=/c/Users/<your user name>/AppData/Roaming/cabal/bin`
+1. execute `make install to=<target directory>`
 
 #### Note: 
 > On Windows, use `/` with the `make` command instead of `\`.
@@ -103,6 +105,11 @@ 
 See [ClaferToolsST](https://github.com/gsdlab/ClaferToolsST)
 
+Integration with VIM
+--------------------
+
+See [clafer-vim](https://github.com/wasowski/clafer-vim)
+
 Usage
 =====
 
@@ -112,9 +119,10 @@ 
 (As printed by `claferIG --help`)
 
-``` v0.3.8
+``` 
+ClaferIG v0.3.9
 
-igaONS] FILE
+claferIG [OPTIONS] [FILE]
 
 Common flags:
      --all=INT                                 Saves all instances up to the
@@ -145,15 +153,15 @@   -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.
+                                               during compiling: none or simple
+                                               (default).
   -? --help                                    Display help message
   -V --version                                 Print version information
 ```
 
 `claferIG <model file name>.cfr`
 
-- opens an interactive session and displays the minimal instance or a counterexample
+- opens an interactive session and displays an instance or a counterexample.
 
 `claferIG <model file name>.cfr -all <scope>`
 
@@ -164,7 +172,7 @@ 
 ```
 ------------------
-| ClaferIG 0.3.8 |
+| ClaferIG 0.3.9 |
 ------------------
 
 You can invoke the following commands as indicated by single quotes:
@@ -228,13 +236,13 @@ abstract A
     a ?
     b +
-    c : integer ?
+    c -> integer ?
     d -> E 2
     g -> E 2
-        h : integer
+        h -> integer
 
 abstract E
-    f : integer +
+    f ->> integer +
 
 a1 : A
 e1 : E
@@ -261,6 +269,7 @@     f$1 = 2
     f$2 = 3
     f$3 = 4 
+    f$4 = 2 
 
 --- Instance 1 End ---
 ```
@@ -301,7 +310,7 @@ 
 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
+* translates the input Clafer model (.cfr) to an Alloy4.2 model (.als). The compiler's intermediate representation (IR) contains the mapping between Clafer names and Alloy names. The IR also contains the scopes for each Alloy signature to ensure that a valid instance can be found if it exists
 * 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,
@@ -309,12 +318,5 @@ 
 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) which contains a repository of models for various applications
-  * 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 by examples 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 `clafer` (so that we know what they are related to) and with `jimmy-liang` or `michal` (so that Jimmy or Michał gets a notification).
+* Visit [language's website](http://clafer.org).
+* Report issues to [issue tracker](https://github.com/gsdlab/claferIG/issues)

binary file changed (22370 → 22370 bytes)

@@ -1,102 +1,103 @@-Name:               claferIG
-Version:            0.3.8
-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, Michał Antkiewicz, Luke Michael Brown
-Maintainer:         Jimmy Liang <jliang@gsd.uwaterloo.ca>
-Stability:          Experimental
-Category:           Model
-Build-type:         Simple
-Cabal-version:      >=1.18
-data-files:         alloyIG.jar,
-                    README.md,
-                    CHANGES.md,
-                    Makefile,
-                    lib/minisatprover.md,
-                    tools/Makefile
+Name:                   claferIG
+Version:                0.3.9
+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:             Michal Antkiewicz <mantkiew@gsd.uwaterloo.ca>
+Stability:              Experimental
+Category:               Model
+Build-type:             Simple
+Cabal-version:          >= 1.18
+data-files:             alloyIG.jar,
+                        README.md,
+                        CHANGES.md,
+                        Makefile,
+                        lib/minisatprover.md,
+                        tools/Makefile
 source-repository head
-    type:           git
-    location:       git://github.com/gsdlab/claferIG.git
+    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.8,
-                    claferIG == 0.3.8,
-                    cmdargs >= 0.10.7,
-                    containers >= 0.5.0.0,
-                    directory >= 1.2.0.1,
-                    executable-path >= 0.0.3,
-                    filepath >= 1.3.0.1,
-                    haskeline >= 0.7.1.2,
-                    mtl >= 2.1.2,
-                    transformers >= 0.3.0.0
-    other-modules:  Paths_claferIG
-    Hs-Source-Dirs: src-cmd
-    ghc-options:     -Wall -fno-warn-unused-do-bind -fno-warn-orphans -rtsopts
+    build-tools:        ghc >= 7.8.3
+    default-language:   Haskell2010
+    default-extensions: DeriveDataTypeable
+    Main-is:            Main.hs
+    Build-depends:      base >= 4.7.0.1 && < 5
+                      , containers >= 0.5.5.1
+                      , directory >= 1.2.1.0
+                      , filepath >= 1.3.0.2
+                      , transformers >= 0.3.0.0
 
+                      , mtl >= 2.1.3.1
+
+                      , cmdargs >= 0.10.7
+                      , executable-path >= 0.0.3
+                      , haskeline >= 0.7.1.2
+
+                      , clafer == 0.3.9
+                      , claferIG == 0.3.9
+    other-modules:      Paths_claferIG
+    Hs-Source-Dirs:     src-cmd
+    ghc-options:        -Wall -fno-warn-unused-do-bind -fno-warn-orphans -rtsopts
+
 library
-    build-tools:    ghc >= 7.6.3
-    default-language: Haskell2010
+    build-tools:        ghc >= 7.8.3
+    default-language:   Haskell2010
     default-extensions: DeriveDataTypeable
-    build-depends:  array >= 0.4.0.1,
-                    base >= 4.6.0.1 && < 5,
-                    containers >= 0.5.0.0,
-                    directory >= 1.2.0.1,
-                    filepath >= 1.3.0.1,
-                    process >= 1.1.0.2,
+    build-depends:      array >= 0.5.0
+                      , base >= 4.7.0.1 && < 5
+                      , containers >= 0.5.5.1
+                      , directory >= 1.2.1.0
+                      , filepath >= 1.3.0.2
+                      , process >= 1.2.0.0
+                      , transformers >= 0.3.0.0
 
-                    mtl >= 2.1.2,
-                    parsec >= 3.1.3,
-                    transformers >= 0.3.0.0,
+                      , mtl >= 2.1.3.1
+                      , parsec >= 3.1.5
 
-                    data-stringmap >= 1.0.1.1,
-                    executable-path >= 0.0.3,
-                    haskeline >= 0.7.1.2,
-                    HaXml >= 1.24,
-                    json-builder >= 0.3,
-                    string-conversions >= 0.3.0.2,
+                      , data-stringmap >= 1.0.1.1
+                      , executable-path >= 0.0.3
+                      , haskeline >= 0.7.1.2
+                      , HaXml >= 1.24
+                      , json-builder >= 0.3
+                      , string-conversions >= 0.3.0.2
 
-                    clafer == 0.3.8
-    hs-source-dirs: src
-    ghc-options:     -Wall -fno-warn-unused-do-bind -fno-warn-orphans -rtsopts
-    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
+                      , clafer == 0.3.9
+    hs-source-dirs:     src
+    ghc-options:        -Wall -fno-warn-unused-do-bind -fno-warn-orphans -rtsopts
+    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,
-                    directory >= 1.2.0.1,
-                    filepath >= 1.3.0.1,
+    type:               exitcode-stdio-1.0
+    default-language:   Haskell2010
+    main-is:            test-suite.hs
+    hs-source-dirs:     test
+    build-depends:      array >= 0.5.0
+                      , base >= 4.7.0.1 && < 5
+                      , directory >= 1.2.1.0
+                      , filepath >= 1.3.0.2
+                      , transformers >= 0.3.0.0
 
-                    HUnit >= 1.2.5.2,
-                    transformers >= 0.3.0.0,
+                      , HUnit >= 1.2.5.2
 
-                    cmdargs >= 0.10.7,
-                    tasty >= 0.10,
-                    tasty-hunit >= 0.9,
-                    tasty-th >= 0.1.2,
+                      , cmdargs >= 0.10.7
+                      , tasty >= 0.10
+                      , tasty-hunit >= 0.9
+                      , tasty-th >= 0.1.2
 
-                    clafer == 0.3.8,
-                    claferIG == 0.3.8
-    other-modules:  Paths_claferIG
-    ghc-options:    -Wall -fno-warn-unused-do-bind -fno-warn-orphans
+                      , clafer == 0.3.9
+                      , claferIG == 0.3.9
+    other-modules:      Paths_claferIG
+    ghc-options:        -Wall -fno-warn-unused-do-bind -fno-warn-orphans

@@ -24,7 +24,7 @@ 
 module Main where
 
-import Language.Clafer.IG.ClaferIG 
+import Language.Clafer.IG.ClaferIG
 import Language.Clafer.IG.ClaferModel
 import Language.Clafer.IG.CommandLine
 import Language.Clafer.IG.Solution
@@ -32,6 +32,7 @@ import Language.Clafer.ClaferArgs
 import Language.Clafer.JSONMetaData
 import Language.ClaferT
+import Language.Clafer.Common
 import Control.Monad
 import Control.Monad.IO.Class
 import Data.Either
@@ -50,7 +51,7 @@     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.",
+    alloySolution               = def &= help "Convert Alloy solution to a Clafer solution." &= typ "FILE",
     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.",
@@ -75,11 +76,12 @@                         then args' {bitwidth = requiredBitwidth mi}
                         else args'
 
-        if (alloySolution args'')
-            then
-                runAlloySolution args''
+        if (not $ null $ alloySolution args'')
+            then do
+                _ <- runAlloySolution args''
+                return ()
             else if (json args'')
-                then 
+                then
                     tryClaferIG (args'' { useUids = True })
                 else
                     tryClaferIG args''
@@ -95,7 +97,7 @@                     void getLine
                     tryClaferIG args3
 
-runClaferIG :: IGArgs -> IO (Either ClaferErrs ())    
+runClaferIG :: IGArgs -> IO (Either ClaferErrs ())
 runClaferIG args' =
     runClaferIGT args' $ do
         let claferModelFileName = claferModelFile args'
@@ -106,7 +108,7 @@         let ir = fst3 $ fromJust $ cIr env
         scopes <- getScopes
         setBitwidth $ findNecessaryBitwidth ir oldBw $ map snd scopes
-        
+
         solve
         case all args' of
             Just scope -> do
@@ -117,8 +119,8 @@                     Nothing -> do
                         liftIO $ putStrLn "Using the provided global scope as a `.cfr-scope` file does not exist. Use the command `saveScopes` to create one."
                         setGlobalScope scope
-                    Just uidScopes -> do 
-                        let 
+                    Just uidScopes -> do
+                        let
                             (globalScopes, normalScopes) = partition (\(uid, _) -> null uid) uidScopes
                             -- from the globalScopes, take the maximum
                             globalScopeVals = map snd globalScopes
@@ -132,19 +134,30 @@                 solve
 
                 counterRef <- liftIO $ newIORef 1
-                
+
                 let saveDirectory = fromMaybe return $ underDirectory `liftM` saveDir args'
                 saveAll (savePath claferModelFileName counterRef >>= saveDirectory)
                 quit
             Nothing    -> runCommandLine
 
+
 -- | Convert an Alloy XML file into an instance in Clafer
-runAlloySolution :: IGArgs -> IO () 
+runAlloySolution :: IGArgs -> IO (Either ClaferErrs ())
 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
+    runClaferIGT args' $ do
+        let claferModelFileName = claferModelFile args'
+        cModel <- liftIO $ strictReadFile claferModelFileName
+        when (cModel == "") $ error $ "Cannot convert Alloy solution without the Clafer model from which the instance was created.\n"
+                                   ++ "Usage: claferIG [OPTIONS] <model.cfr> --alloy-solution=<instance.xml>\n"
+        alloyInstance <- liftIO $ strictReadFile $ alloySolution args' -- It's an Alloy XML file in this case
+        when (null alloyInstance) $ error $ "Provide an Alloy solution Alloy file name.\n"
+                                         ++ "Usage: claferIG [OPTIONS] <model.cfr> --alloy-solution=<instance.xml>\n"
+        env <- getClaferEnv
+        let (_, genv', _) = fromJust $ cIr env
+        let
+            sMap = Map.empty
+            uidIClaferMap' = uidClaferMap genv'
+        liftIO $ putStrLn $ show $ (sugarClaferModel (useUids args') (addTypes args') uidIClaferMap' $ buildClaferModel $ parseSolution alloyInstance) $ sMap
 
 savePath :: FilePath -> IORef Int -> IO FilePath
 savePath file' counterRef =
@@ -152,8 +165,8 @@         counter <- readIORef counterRef
         writeIORef counterRef (counter + 1)
         return $ file' ++ "." ++ (show counter) ++ ".data"
-        
 
+
 underDirectory :: FilePath -> FilePath -> IO FilePath
 underDirectory dir file' =
     do
@@ -171,4 +184,4 @@             Instance{modelInstance = modelInstance'} -> do
                 liftIO $ writeFile file' (show modelInstance')
                 saveAll nextFile
-            _ -> return ()  
+            _ -> return ()

@@ -31,7 +31,7 @@ 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.Front.AbsClafer (Span(..), Pos(..))
 import Language.Clafer.IG.Process
 import System.Console.Haskeline.MonadException
 

@@ -30,8 +30,8 @@     getClaferIGArgs,
     getConstraints,
     getClaferModel,
-    getInfo,
     getStrMap,
+    getUIDIClaferMap,
     ClaferIGT(..),
     Instance(..),
     Counterexample(..),
@@ -61,10 +61,10 @@     sigToClaferName) where
 
 import Language.Clafer
+import Language.Clafer.Common
 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
@@ -93,7 +93,7 @@     all :: Maybe Integer,
     saveDir :: Maybe FilePath,
     claferModelFile :: FilePath,
-    alloySolution :: Bool,
+    alloySolution :: FilePath,
     bitwidth :: Integer,
     maxInt :: Integer,
     useUids :: Bool,
@@ -121,6 +121,9 @@ fetches :: Monad m => (ClaferIGEnv -> a) -> ClaferIGT m a
 fetches = ClaferIGT . gets
 
+getUIDIClaferMap :: Monad m => ClaferIGT m UIDIClaferMap
+getUIDIClaferMap = fetches info
+
 set :: Monad m => ClaferIGEnv -> ClaferIGT m ()
 set = ClaferIGT . put
 
@@ -139,7 +142,7 @@     constraints:: [Constraint],
     claferModel:: String,
     qNameMaps :: QNameMaps,
-    info :: Analysis.Info,
+    info :: UIDIClaferMap,
     strMap :: Map Int String,
     lineNumMap :: Map Integer String
 }
@@ -170,9 +173,6 @@ 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
@@ -180,7 +180,8 @@ 
         (claferEnv', alloyModel, mapping, sMap) <- ErrorT $ return $ callClaferTranslator claferModel
 
-        let ir = fst3 $ fromJust $ cIr claferEnv'
+        let
+            (ir, genv', _) = fromJust $ cIr claferEnv'
         let constraints = parseConstraints claferModel ir mapping
 
         lift $ AlloyIG.sendLoadCommand alloyModel
@@ -188,10 +189,10 @@ 
         let qNameMaps = deriveQNameMaps ir
 
-        let info = Analysis.gatherInfo ir
+        let uidIClaferMap' = uidClaferMap genv'
         let irTrace = editMap $ irModuleTrace claferEnv'
 
-        return $ ClaferIGEnv claferEnv' igArgs constraints claferModel qNameMaps info sMap irTrace
+        return $ ClaferIGEnv claferEnv' igArgs constraints claferModel qNameMaps uidIClaferMap' sMap irTrace
     where
     editMap :: (Map.Map Span [Ir]) -> (Map.Map Integer String) -- Map Line Number to Clafer Name
     editMap =
@@ -291,27 +292,27 @@ next = do
     env <- getClaferEnv
     claferIGArgs' <- getClaferIGArgs
+    uidIClaferMap' <- getUIDIClaferMap
     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
+        Just xml -> return $ Instance (xmlToModel useUids' addTypes' uidIClaferMap' 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
+            c <- counterexample env core useUids' addTypes' uidIClaferMap' 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
+    counterexample env' originalCore useUids'' addTypes'' uidIClaferMap'' constraints' sMap = counterexample' env' originalCore [] useUids'' addTypes'' uidIClaferMap'' constraints' sMap
         where
-        counterexample' env'' core removed useUids''' addTypes''' info''' constraints'' sMap' =
+        counterexample' env'' core removed useUids''' addTypes''' uidIClaferMap''' constraints'' sMap' =
             case msum $ findRemovable env'' core constraints'' of
                 Just remove -> do
                     ClaferIGT $ lift $ AlloyIG.sendRemoveConstraintCommand $ range remove
@@ -319,16 +320,16 @@                     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)
+                            UnsatCore (catMaybes $ findRemovable env'' core constraints'') (Just $ Counterexample (reverse $ remove : removed) (xmlToModel useUids''' addTypes''' uidIClaferMap''' xml sMap') xml)
                         Nothing ->
                             do
                                 AlloyIG.UnsatCore core' <- ClaferIGT $ lift AlloyIG.sendUnsatCoreCommand
-                                counterexample' env'' core' (remove : removed) useUids''' addTypes''' info''' constraints' sMap'
+                                counterexample' env'' core' (remove : removed) useUids''' addTypes''' uidIClaferMap''' 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
+    xmlToModel :: Bool -> Bool -> UIDIClaferMap -> String -> (Map Int String) -> ClaferModel
+    xmlToModel  useUids' addTypes' uidIClaferMap' xml sMap = (sugarClaferModel useUids' addTypes' uidIClaferMap' $ buildClaferModel $ parseSolution xml) sMap
 
 reload :: MonadIO m => ClaferIGT m (Either ClaferErrs ())
 reload  =
@@ -364,7 +365,7 @@ 
 findRemovable :: ClaferEnv -> [Span] -> [Constraint] -> [Maybe Constraint]
 findRemovable env core constraints' =
-    let absIDs = foldMapIR getId $ fst3 $ fromJust $ cIr env
+    let absIDs = foldMapIR getId $ getIMod $ fromJust $ cIr env
     in  Data.List.filter (removeAbsZero absIDs ) $ map (\c -> find ((== c) . range) constraints') core
     where
         removeAbsZero :: (Seq.Seq String) -> Maybe Constraint -> Bool
@@ -374,5 +375,5 @@         getId (IRClafer (IClafer _ True _ uID _ _ _ _ _ _ _)) = Seq.singleton uID
         getId _ = mempty
 
-fst3 :: (IModule, GEnv, Bool) -> IModule
-fst3 (imod, _, _) = imod
+getIMod :: (IModule, GEnv, Bool) -> IModule
+getIMod (imod, _, _) = imod

@@ -85,13 +85,13 @@         do
             solution <- lift next
             claferIGArgs' <- lift getClaferIGArgs
-            info <- lift getInfo
+            uidIClaferMap' <- lift $ getUIDIClaferMap
             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
+                        then generateJSON uidIClaferMap' claferModel
                         else let
                                 iNumber = show $ 1 + (length $ unsaved context)
                              in

@@ -28,7 +28,7 @@ import Data.Maybe
 import Data.Ord
 import Language.Clafer
-import Language.Clafer.Front.Absclafer (Span(..))
+import Language.Clafer.Front.AbsClafer (Span(..))
 import Language.Clafer.Intermediate.Intclafer
 import qualified Language.Clafer.Intermediate.Intclafer as I
 

@@ -22,31 +22,32 @@ 
 module Language.Clafer.IG.JSONGenerator (generateJSON) where
 
+import Language.Clafer.Common
+import Language.Clafer.Intermediate.Intclafer
 import qualified Language.Clafer.IG.ClaferModel as M
-import qualified Language.Clafer.Intermediate.Analysis as A
-import Data.Maybe (fromMaybe)
+import Data.Maybe (fromJust)
 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
+generateJSON :: UIDIClaferMap -> M.ClaferModel                  -> String
+generateJSON    uidIClaferMap'   (M.ClaferModel topLevelClafers) =
+    convertString $ toJsonBS $ constructElements $ map (printClafer uidIClaferMap') topLevelClafers
 
-printClafer :: A.Info -> M.Clafer                           -> Object
-printClafer    info      (M.Clafer id value children) =
-    (map (printClafer info) children) `addElements` completeClaferObject
+printClafer :: UIDIClaferMap -> M.Clafer                           -> Object
+printClafer    uidIClaferMap'      (M.Clafer id value children) =
+    (map (printClafer uidIClaferMap') children) `addElements` completeClaferObject
     where
-        uid = M.i_name id
-        sclafer = A.runAnalysis (A.claferWithUid $ removeOrdinal uid) info
-        ident = A.uid sclafer
+        uid' = M.i_name id
+        iclafer = fromJust $ findIClafer uidIClaferMap' $ removeOrdinal uid'
+        ident' = _ident iclafer
 
-        super = fromMaybe "" $ A.super sclafer
-        reference = fromMaybe "" $ A.reference sclafer
-        cardMin = A.low sclafer
-        cardMax = A.high sclafer
-        basicClaferObject = makeBasicClaferObject ident uid super reference cardMin cardMax
+        super' = getSuper iclafer
+        reference' = getReference iclafer
+        (Just (cardMin, _)) = _card iclafer
+        (Just (_, cardMax)) = _card iclafer
+        basicClaferObject = makeBasicClaferObject ident' uid' super' reference' cardMin cardMax
 
         addValue :: Maybe M.Value         -> Object -> Object
         addValue    Nothing                  object = object
@@ -59,14 +60,21 @@         removeOrdinal :: String -> String
         removeOrdinal = takeWhile (/= '$')
 
-makeBasicClaferObject :: String -> String -> String -> String       -> Integer -> Integer    -> Object
-makeBasicClaferObject    ident     uid       super     reference       cardMin    cardMax =
-    mconcat [ row "ident" ident,
-              row "uid" uid,
-              row "super" super,
-              row "reference" reference,
+makeBasicClaferObject :: String -> String -> [String] -> [String] -> Integer -> Integer -> Object
+makeBasicClaferObject    ident'    uid'      super'      reference'   cardMin    cardMax  =
+    mconcat [ row "ident" ident',
+              row "uid" uid',
+              superRow,
+              refRow,
               row "cardMin" cardMin,
               row "cardMax" cardMax ]
+    where
+        superRow = case super' of
+            [s] -> row "super" s
+            _   -> mempty
+        refRow = case reference' of
+            [r] -> row "reference" r
+            _   -> mempty
 
 addIntValue :: Int -> Object      -> Object
 addIntValue    value  claferObject =
@@ -77,9 +85,9 @@     claferObject `mappend` (row "value" value)
 
 addElements :: [ Object ] -> Object      -> Object
-addElements    elements      claferObject =
-    claferObject `mappend` (constructElements elements)
+addElements    elements'      claferObject =
+    claferObject `mappend` (constructElements elements')
 
 constructElements :: [ Object ] -> Object
-constructElements    elements    =
-    row "elements" $ mconcat $ map element elements
+constructElements    elements'    =
+    row "elements" $ mconcat $ map element elements'

@@ -22,8 +22,8 @@ 
 module Language.Clafer.IG.Sugarer (sugarClaferModel) where
 
+import Language.Clafer.Common
 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)
@@ -64,8 +64,8 @@ 
 
 -- | 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 =
+sugarClaferModel:: Bool -> Bool  -> UIDIClaferMap -> ClaferModel                      -> (Map Int String) -> ClaferModel
+sugarClaferModel   useUids addTypes uidIClaferMap'   model@(ClaferModel topLevelClafers) sMap              =
     ClaferModel $ map sugarClafer topLevelClafers
     where
     sugarClafer (Clafer id value children) =
@@ -75,15 +75,17 @@     sugarValue (Clafer _ Nothing _) = Nothing
     sugarValue c  = if (cType c) == "string" then (Just ((StringValue) (getString c))) else (c_value c)
 
-    cType (Clafer id _ _) = cTypeSolve $ (Analysis.super (Analysis.runAnalysis (Analysis.claferWithUid (i_name id)) (fromJust info)))
 
-    cTypeSolve Nothing = ""
-    cTypeSolve (Just "string") = "string"
-    cTypeSolve (Just "integer") = "integer"
-    cTypeSolve (Just "int") = "integer"
-    cTypeSolve (Just "real") = "real"
-    cTypeSolve (Just x) = cType (Clafer (Id x 0) Nothing [])
+    cType (Clafer id _ _) = cTypeSolve $ getReference iclafer
+      where
+        iclafer = fromJust $ findIClafer uidIClaferMap' $ i_name id
 
+    cTypeSolve ["string"]  = "string"
+    cTypeSolve ["integer"] = "integer"
+    cTypeSolve ["int"]     = "integer"
+    cTypeSolve ["real"]    = "real"
+    cTypeSolve _           = ""
+
     getString c = case (Map.lookup strNumber sMap) of
         Nothing -> "\"<text " ++ show strNumber ++ ">\""
         Just s -> s
@@ -94,33 +96,32 @@ 
     sugarId :: Bool -> Bool  -> Bool    -> Id -> Id
     sugarId    useUids' addTypes' addRefDecl id  =
-        Id (finalName ++ ordinalDisplay ++ (refDecl addTypes' addRefDecl info)) 0
+        Id (finalName ++ ordinalDisplay ++ (refDecl addTypes' addRefDecl uidIClaferMap')) 0
         where
         fullName = i_name id
         ordinalDisplay = if (useUids || count > 1)
                          then "$" ++ show ordinal
                          else ""
 
-        refDecl :: Bool -> Bool -> Maybe Analysis.Info -> String
-        refDecl    True    True    (Just info')          = retrieveSuper info' $ i_name id
-        refDecl    _       _       _                    = ""
+        refDecl :: Bool -> Bool ->  UIDIClaferMap -> String
+        refDecl    True    True    uidIClaferMap'' = retrieveSuper uidIClaferMap'' $ 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 sugarSuper (Analysis.super sclafer))
-    ++ sugarReference  (Analysis.reference sclafer)
+retrieveSuper :: UIDIClaferMap -> String -> String
+retrieveSuper uidIClaferMap'      uid =
+    sugarSuper (getSuper iclafer)
+    ++
+    sugarReference  (getReference iclafer)
     where
-        sclafer = Analysis.runAnalysis (Analysis.claferWithUid uid) info
+        iclafer = fromJust $ findIClafer uidIClaferMap' uid
 
-        sugarSuper :: Maybe String -> String
-        sugarSuper (Just s) = " : " ++ s
-        sugarSuper Nothing = ""
-        sugarReference :: Maybe String -> String
-        sugarReference (Just s) = " -> " ++ s
-        sugarReference Nothing = ""
+        sugarSuper :: [String] -> String
+        sugarSuper [s] = " : " ++ s
+        sugarSuper _   = ""
+        sugarReference :: [String] -> String
+        sugarReference [s] = " -> " ++ s
+        sugarReference _   = ""

@@ -46,7 +46,7 @@     all             = def,
     saveDir         = def,
     claferModelFile = def,
-    alloySolution   = False,
+    alloySolution   = def,
     bitwidth        = 4,
     maxInt          = 7,
     useUids         = False,

@@ -1,33 +1,7 @@ WGET_COMMAND := wget
 MNAME := $(shell uname -m | tr "A-Z" "a-z")
 
-ifeq ($(OS),Windows_NT)
-	ifeq ($(shell which wget), which: wget: unkown command)
-		mingw-get install msys-wget-bin
-	endif
-	LIB := x86-windows/minisatprover*
-else
-	UNAME := $(shell uname -s)
-	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),Darwin)
-		WGET_COMMAND := curl -O
-		LIB := x86-mac/libminisatprover*
-	endif
-endif
-
-ifeq ($(OS),Windows_NT)
-	ifeq ($(shell which wget), which: wget: unkown command)
-		mingw-get install msys-wget-bin
-	endif
-else
+ifneq ($(OS),Windows_NT)
 	UNAME := $(shell uname -s)
 	ifeq ($(UNAME),Darwin)
 		WGET_COMMAND := curl -O
@@ -39,4 +13,4 @@ 		echo "[WARNING] Missing alloy4.2.jar. Downloading...";  \
 		$(WGET_COMMAND) http://alloy.mit.edu/alloy/downloads/alloy4.2_2014-05-16.jar; \
 		mv alloy4.2_2014-05-16.jar alloy4.2.jar; \
-	fi+	fi