claferIG 0.3.10 → 0.4.0

raw patch · 9 files changed

+109/−99 lines, 9 filesdep ~HaXmldep ~arraydep ~basePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: HaXml, array, base, clafer, claferIG, cmdargs, containers, directory, filepath, haskeline, mtl, parsec, process, string-conversions, tasty, tasty-hunit, tasty-th, transformers

API changes (from Hackage documentation)

Files

• CHANGES.md +16/−12
• Makefile +11/−6
• README.md +34/−37
• alloyIG.jar binary
• claferIG.cabal +42/−37
• src-cmd/Main.hs +1/−1
• src/Language/Clafer/IG/ClaferIG.hs +3/−3
• src/Language/Clafer/IG/ClaferModel.hs +2/−2
• tools/Makefile +0/−1

@@ -1,41 +1,45 @@-**ClaferIG Version 0.3.10 released on April 24, 2015**
+# ClaferIG Version 0.4.0 released on Jul 28, 2015
 
+[Release](https://github.com/gsdlab/claferIG/pull/26)
+
+# ClaferIG Version 0.3.10 released on April 24, 2015
+
 [Release](https://github.com/gsdlab/claferIG/pull/25)
 
-**ClaferIG Version 0.3.9 released on March 06, 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**
+# 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 October 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 July 08, 2014**
+# ClaferIG Version 0.3.6.1 released on July 08, 2014
 
 [Release](https://github.com/gsdlab/claferIG/pull/20)
 
-**ClaferIG Version 0.3.6 released on May 23, 2014**
+# ClaferIG Version 0.3.6 released on May 23, 2014
 
 [Release](https://github.com/gsdlab/claferIG/pull/19)
 
-**ClaferIG Version 0.3.5 released on January 20, 2014**
+# ClaferIG Version 0.3.5 released on January 20, 2014
 
 [Release](https://github.com/gsdlab/claferIG/pull/17)
 
-**ClaferIG Version 0.3.4 released on September 20, 2013**
+# ClaferIG Version 0.3.4 released on September 20, 2013
 
-**ClaferIG Version 0.3.3 released on August 14, 2013**
+# ClaferIG Version 0.3.3 released on August 14, 2013
 
 [Release](https://github.com/gsdlab/claferIG/pull/12)
 
-**ClaferIG Version 0.3.2 released on April 11, 2013**
+# ClaferIG Version 0.3.2 released on April 11, 2013
 
-**ClaferIG Version 0.3.1 released on October 17, 2012**
+# ClaferIG Version 0.3.1 released on October 17, 2012
 
-**ClaferIG Version 0.3 released on July 17, 2012**
+# ClaferIG Version 0.3 released on July 17, 2012
 
 This was the first release of Clafer Instance Generator and included all code since the beginning of the project.

@@ -5,6 +5,7 @@ else
 	UNAME := $(shell uname -s)
 	ifeq ($(UNAME), Linux)
+		MNAME := $(shell uname -m | tr "A-Z" "a-z")
 		ifeq ($(MNAME), i686)
 			LIB := x86-linux/libminisatprover*
 		endif
@@ -32,8 +33,8 @@ 	cp -f alloyIG.jar $(to)
 	cp -f LICENSE $(to)/
 	cp -f CHANGES.md $(to)/claferIG-CHANGES.md
-	cp -f README.md $(to)/claferIG-README.mds
-	cabal install --bindir=$(to) --ghc-option="-O"
+	cp -f README.md $(to)/claferIG-README.md
+	cabal install --bindir=$(to)
 
 # Removes current build and makes a clean new one (Don't use if starting from scratch!)
 cleanEnv:
@@ -53,7 +54,7 @@ 
 # Build takes less time. For ease of development.
 build: alloyIG.jar
-	cabal configure
+	cabal configure --enable-tests
 	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
@@ -72,9 +73,6 @@ 	fi
 
 test:
-	# Only test a subset of the suite. The other cases do not work yet.
-	cabal configure --enable-tests
-	cabal build
 	# Install what's needed for running the tests
 	cp alloyIG.jar dist/build/test-suite/
 	cp alloyIG.jar dist/build/claferIG/
@@ -92,3 +90,10 @@ 	rm -rf tools/amd64-linux
 	rm -rf tools/x86-windows
 	rm -rf tools/x86-mac
+
+tags:
+	hasktags --ctags --extendedctag .
+
+codex:
+	codex update
+	mv codex.tags tags

@@ -1,22 +1,19 @@-Clafer Instance Generator
-=========================
+# Clafer Instance Generator
 
-v0.3.10
+v0.4.0
 
 [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
-------------
+## Contributors
 
-* [Jimmy Liang](http://gsd.uwaterloo.ca/jliang), Main developer.
-* [Michał Antkiewicz](http://gsd.uwaterloo.ca/mantkiew), Requirements, development, architecture, testing, technology transfer.
+* [Michał Antkiewicz](http://gsd.uwaterloo.ca/mantkiew), Main developer.
+* [Jimmy Liang](http://gsd.uwaterloo.ca/jliang), Original developer.
 * Luke Michael Brown, co-op student May-Aug 2013. Many improvements.
 
-Getting the Clafer Instance Generator
--------------------------------------
+## Getting the Clafer Instance Generator
 
 Clafer can be installed from a binary distribution (preferred), from Hackage, and from the source code.
 
@@ -24,14 +21,14 @@ 
 Regardless of the installation method, the following are required:
 
-* [Clafer](https://github.com/gsdlab/clafer) v0.3.10
+* [Clafer](https://github.com/gsdlab/clafer) v0.4.0
 * [Java Platform (JDK)](http://www.oracle.com/technetwork/java/javase/downloads/index.html) v8+, 64bit
-  * On Windows, Java must be 32bit because of Alloy
+  * On Windows, Java must be 32bit because of Alloy, 64bit otherwise
 * [Alloy4.2](http://alloy.mit.edu/alloy/download.html)
 
 ### Installation from binaries
 
-Binary distributions of the release 0.3.10 of Clafer Tools for Windows, Mac, and Linux,
+Binary distributions of the release 0.4.0 of Clafer Tools for Windows, Mac, and Linux,
 can be downloaded from [Clafer Tools - Binary Distributions](http://gsd.uwaterloo.ca/clafer-tools-binary-distributions).
 
 1. download the binaries and unpack `<target directory>` of your choice
@@ -41,14 +38,13 @@ 
 Dependencies
 
-* [The Haskell Platform](http://hackage.haskell.org/platform/) v2014.2.0.0
-  * Alternatively GHC >= 7.8.3 and Cabal >= 1.18
+* [GHC](https://www.haskell.org/downloads) v7.10.*
 
-ClaferIG is now available on [Hackage](http://hackage.haskell.org/package/claferIG-0.3.10/) and it can be installed using
+ClaferIG is now available on [Hackage](http://hackage.haskell.org/package/claferIG-0.4.0/) 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.8.3\claferIG-0.3.10` on Windows or `.cabal/share/x86_64-linux-ghc-7.8.3/claferIG-0.3.10/` on Linux)
+3. `cd <cabal's lib or share folder>`  (`C:\Users\<user>\AppData\Roaming\cabal\i386-windows-ghc-7.10.1\claferIG-0.4.0` on Windows or `.cabal/share/x86_64-linux-ghc-7.10.1/claferIG-0.4.0/` on Linux)
 3. to automatically download Alloy4.2 jar
   * execute `make` in `tools`
 4. To get the `minisatproover` library
@@ -62,8 +58,7 @@ 
 Dependencies
 
-* [The Haskell Platform](http://hackage.haskell.org/platform/) v2014.2.0.0
-  * Alternatively GHC >= 7.8.3 and Cabal >= 1.18
+* [GHC](https://www.haskell.org/downloads) v7.10.*
 * [Clafer compiler](https://github.com/gsdlab/clafer) (to produce Alloy models (`.als`)). The version number of the compiler must match the version of the instance generator.
 * 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`
@@ -101,14 +96,14 @@ > On Windows, use `/` with the `make` command instead of `\`.
 
 
-Integration with Sublime Text 2/3
--------------------------------
+## Integration with Sublime Text 2/3
 
+
 See [ClaferToolsST](https://github.com/gsdlab/ClaferToolsST)
 
-Integration with VIM
---------------------
+## Integration with VIM
 
+
 See [clafer-vim](https://github.com/wasowski/clafer-vim)
 
 Usage
@@ -121,7 +116,7 @@ (As printed by `claferIG --help`)
 
 ```
-ClaferIG v0.3.10
+ClaferIG v0.4.0
 
 claferIG [OPTIONS] [FILE]
 
@@ -145,7 +140,7 @@   -j --json                                    Render solution as JSON
                                                (forces 'addUids').
   -i --flatten-inheritance-comp                Flatten inheritance during
-                                               compiling ('alloy' and 'alloy42'
+                                               compiling ('alloy' and 'Alloy'
                                                modes only)
   -l --no-layout-comp                          Don't resolve off-side rule
                                                layout during compiling
@@ -171,11 +166,11 @@ ### 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 0.3.10 |
-------------------
+## ```
 
+## | ClaferIG 0.4.0 |
+
+
 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
@@ -211,11 +206,12 @@ ```
 
 
-Output format
--------------
+## Output format
 
-### Instance data
+There are two output formats: native (plain text, default) and JSON (`--json`).
 
+### Instance data (native)
+
 The instance data notation is very similar to a regular Clafer notation for concrete clafers with a few differences:
 
 * no constraints
@@ -306,9 +302,9 @@ 
 Here, `C1` and `C3` are satisfied but `C2` is not. To resolve the conflict and assuming that the counter example is actually a correct instance data, the user has to modify the model by removing `C2`. However, should the counter example actually represent incorrect instance data, the user can remove `C3` to resolve the inconsistency.
 
-Troubleshooting
----------------
+## Troubleshooting
 
+
 If you get an error:
 
 ```
@@ -323,9 +319,9 @@ On Windows, Alloy only supports Minisat with UnSAT core on 32bit Java.
 There's nothing we can do.
 
-How it works
-------------
+## How it works
 
+
 The Clafer instance generator:
 
 * translates the input Clafer model (.cfr) to an Alloy4.2 model (.als). The compiler's intermediate representation (IR) contains the mapping between Clafer names and Alloy names. The IR also contains the scopes for each Alloy signature to ensure that a valid instance can be found if it exists
@@ -334,7 +330,8 @@ * 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?
-==========
+# Need help?
+
+
 * 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,5 +1,5 @@ Name:                   claferIG
-Version:                0.3.10
+Version:                0.4.0
 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
@@ -21,49 +21,54 @@     type:               git
     location:           git://github.com/gsdlab/claferIG.git
 Executable claferIG
-    build-tools:        ghc >= 7.8.3
+    build-tools:        ghc >= 7.10.1
     default-language:   Haskell2010
     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
+    Build-depends:      base >= 4.8.0.0 && < 5
+                      , containers >= 0.5.6.2
+                      , directory >= 1.2.2.0
+                      , filepath >= 1.4.0.0
+                      , transformers >= 0.4.2.0
 
-                      , mtl >= 2.1.3.1
+                      , mtl >= 2.2.1
 
-                      , cmdargs >= 0.10.7
+                      , cmdargs >= 0.10.13
                       , executable-path >= 0.0.3
-                      , haskeline >= 0.7.1.2
+                      , haskeline >= 0.7.2.1
 
-                      , clafer == 0.3.10
-                      , claferIG == 0.3.10
+                      , clafer == 0.4.0
+                      , claferIG == 0.4.0
     other-modules:      Paths_claferIG
     Hs-Source-Dirs:     src-cmd
     ghc-options:        -Wall -fno-warn-orphans
 
 library
-    build-tools:        ghc >= 7.8.3
+    build-tools:        ghc >= 7.10.1
     default-language:   Haskell2010
-    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
+    build-depends:      array >= 0.5.1.0
+                      , base >= 4.8.0.0 && < 5
+                      , containers >= 0.5.6.2
+                      , directory >= 1.2.2.0
+                      , filepath >= 1.4.0.0
+                      , process >= 1.2.3.0
+                      , transformers >= 0.4.2.0
 
-                      , mtl >= 2.1.3.1
-                      , parsec >= 3.1.5
+                      , mtl >= 2.2.1
+                      , parsec >= 3.1.9
 
                       , data-stringmap >= 1.0.1.1
                       , executable-path >= 0.0.3
-                      , haskeline >= 0.7.1.2
-                      , HaXml >= 1.24
+                      , haskeline >= 0.7.2.1
                       , json-builder >= 0.3
-                      , string-conversions >= 0.3.0.2
+                      , string-conversions >= 0.4
 
-                      , clafer == 0.3.10
+                      , clafer == 0.4.0
+
+    if os(windows)
+      build-depends:  HaXml == 1.24
+    else
+      build-depends:  HaXml >= 1.25.3
+
     hs-source-dirs:     src
     ghc-options:        -Wall -fno-warn-orphans
     exposed-modules:    Language.Clafer.IG.AlloyIGInterface
@@ -82,20 +87,20 @@     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
+    build-depends:      array >= 0.5.1.0
+                      , base >= 4.8.0.0 && < 5
+                      , directory >= 1.2.2.0
+                      , filepath >= 1.4.0.0
+                      , transformers >= 0.4.2.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.13
+                      , tasty >= 0.10.1.2
+                      , tasty-hunit >= 0.9.2
+                      , tasty-th >= 0.1.3
 
-                      , clafer == 0.3.10
-                      , claferIG == 0.3.10
+                      , clafer == 0.4.0
+                      , claferIG == 0.4.0
     other-modules:      Paths_claferIG
     ghc-options:        -Wall -fno-warn-orphans

@@ -56,7 +56,7 @@     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",
+    flatten_inheritance_comp    = def &= help "Flatten inheritance during compiling ('alloy' mode 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",

@@ -85,7 +85,7 @@ import System.Console.Haskeline.MonadException
 import Paths_claferIG (version)
 import Data.Version (showVersion)
-import Prelude 
+import Prelude
 
 claferIGVersion :: String
 claferIGVersion = "ClaferIG " ++ showVersion Paths_claferIG.version
@@ -214,11 +214,11 @@             iModule <- desugar Nothing
             compile iModule
             results <- generate
-            let (Just alloyResult) = Map.lookup Alloy42 results
+            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{mode = [Alloy42], 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}
+    claferArgs = defaultClaferArgs{mode = [Alloy], keep_unused = True, no_stats = 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
 

@@ -152,7 +152,7 @@         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
+            buildNode = if "_ref" `isSuffixOf` label then ValueNode else ClaferNode
 
     labelAsId :: String -> Id
     labelAsId label =
@@ -188,7 +188,7 @@ 
     buildClafer :: Node -> Either Clafer Value
     buildClafer (ClaferNode id _) =
-        Left $ Clafer id (singleton valueChildren) claferChildren
+        Left $ Clafer id (singleton $ nub valueChildren) claferChildren
         where
         (claferChildren, valueChildren) = partitionEithers $ map buildClafer children
         children = getChildren id ftree

@@ -1,5 +1,4 @@ WGET_COMMAND := wget
-MNAME := $(shell uname -m | tr "A-Z" "a-z")
 
 ifneq ($(OS),Windows_NT)
 	UNAME := $(shell uname -s)