claferIG 0.4.2.1 → 0.4.3
raw patch · 9 files changed
+91/−83 lines, 9 filesdep ~claferdep ~claferIGPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: clafer, claferIG
API changes (from Hackage documentation)
Files
- CHANGES.md +20/−16
- README.md +29/−35
- alloyIG.jar binary
- claferIG.cabal +7/−6
- src-cmd/Main.hs +7/−2
- src/Language/Clafer/IG/ClaferModel.hs +3/−3
- src/Language/Clafer/IG/CommandLine.hs +8/−5
- src/Language/Clafer/IG/Sugarer.hs +15/−14
- stack.yaml +2/−2
CHANGES.md view
@@ -1,57 +1,61 @@-ClaferIG Version 0.4.2.1 released on Oct 19, 2015 +##### ClaferIG Version 0.4.3 released on Dec 22, 2015 +* [Release](https://github.com/gsdlab/claferIG/pull/31) + +##### ClaferIG Version 0.4.2.1 released on Oct 19, 2015 + * Fixed Java manifest file, added stack instructions to README -ClaferIG Version 0.4.2 released on Oct 16, 2015 +##### ClaferIG Version 0.4.2 released on Oct 16, 2015 * [Release](https://github.com/gsdlab/claferIG/pull/28) -ClaferIG Version 0.4.1 released on Sep 1, 2015 +##### ClaferIG Version 0.4.1 released on Sep 1, 2015 * [Release](https://github.com/gsdlab/claferIG/pull/27) -ClaferIG Version 0.4.0 released on Jul 28, 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 +##### 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.
README.md view
@@ -1,6 +1,6 @@ # Clafer Instance Generator -##### v0.4.2.1 +##### v0.4.3 [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. @@ -22,14 +22,14 @@ Regardless of the installation method, the following are required: -* [Clafer](https://github.com/gsdlab/clafer) v0.4.2.1 +* [Clafer](https://github.com/gsdlab/clafer) v0.4.3 * [Java Platform (JDK)](http://www.oracle.com/technetwork/java/javase/downloads/index.html) v8+, 64bit * On Windows, Java must be 32bit because of Alloy, 64bit otherwise * [Alloy4.2](http://alloy.mit.edu/alloy/download.html) ### Installation from binaries -Binary distributions of the release 0.4.2.1 of Clafer Tools for Windows, Mac, and Linux, +Binary distributions of the release 0.4.3 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, @@ -37,7 +37,7 @@ ### Installation From Hackage -Clafer is now available on [Hackage](http://hackage.haskell.org/package/claferIG-0.4.2.1/) and it can be installed using either [`stack`](https://github.com/commercialhaskell/stack) or [`cabal-install`](https://hackage.haskell.org/package/cabal-install). +Clafer is now available on [Hackage](http://hackage.haskell.org/package/claferIG-0.4.3/) and it can be installed using either [`stack`](https://github.com/commercialhaskell/stack) or [`cabal-install`](https://hackage.haskell.org/package/cabal-install). #### Installation using `stack` @@ -67,7 +67,7 @@ 1. Install GHC 2. `cabal update` 3. `cabal install claferIG` -4. `cd <cabal's lib or share folder>` (`C:\Users\<user>\AppData\Roaming\cabal\i386-windows-ghc-7.10.2\claferIG-0.4.2.1` on Windows or `.cabal/share/x86_64-linux-ghc-7.10.2/claferIG-0.4.2.1/` on Linux) +4. `cd <cabal's lib or share folder>` (`C:\Users\<user>\AppData\Roaming\cabal\i386-windows-ghc-7.10.2\claferIG-0.4.3` on Windows or `.cabal/share/x86_64-linux-ghc-7.10.2/claferIG-0.4.3/` on Linux) 5. to automatically download alloy4.2.jar * execute `make alloy4.2.jar` 7. copy the following into the Cabal's `bin` folder @@ -87,12 +87,14 @@ On Windows * [MSYS2](http://msys2.sourceforge.net/) - * download MSYS2 installer - * in MSYS2 console, execute - * `pacman -Syu` - * `pacman -S make wget unzip diffutils` +* it is installed automatically by `stack setup` (see Building below) +* to open MinGW64 shell, execute `mingw64_shell.bat` in `C:\Users\<user>\AppData\Local\Programs\stack\x86_64-windows\msys2-<date>`, where `<date>` is the release date of your MSYS installation +* update MSYS2 packages + * follow [III. Updating packages](http://sourceforge.net/p/msys2/wiki/MSYS2%20installation/) +* execute + * `pacman -S make wget unzip diffutils` -### Important: Branches must correspond +### 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. @@ -105,15 +107,7 @@ 1. install the [Clafer compiler](https://github.com/gsdlab/clafer) 2. in some `<source directory>`, execute `git clone git://github.com/gsdlab/claferIG.git` 3. in `<source directory>/claferIG`, execute `stack setup`. This will install all dependencies, build tools, and MSYS2 (on Windows). -4. first time only on Windows - * open `MinGW64 Shell` using `C:\Users\<user>\AppData\Local\Programs\stack\i386-windows\msys2-20150512\mingw64_shell.bat` - * update MSYS2 following the [update procedure](http://sourceforge.net/p/msys2/wiki/MSYS2%20installation/): - * `pacman -Sy` - * `pacman --needed -S bash pacman pacman-mirrors msys2-runtime` - * restart shell if the runtime was updated - * `pacman -Su` - * `pacman -S make wget unzip diffutils` -5. `cd <source directory>/claferIG` +4. `cd <source directory>/claferIG` * `make` ### Installation @@ -121,7 +115,7 @@ 1. execute `make install to=<target directory>` #### Note: -> On Windows, use `/` with the `make` command instead of `\`. +> On Windows, use `/` with the `make` command instead of `\`, e.g., `make install to=/c/clafer-tools-0.4.3/` ## Integration with Sublime Text 2/3 @@ -143,7 +137,7 @@ (As printed by `claferIG --help`) ``` -ClaferIG v0.4.2.1 +ClaferIG v0.4.3 claferIG [OPTIONS] [FILE] @@ -195,7 +189,7 @@ In the interactive mode, the users can invoke the following commands by pressing a letter marked in the command name between '' or the whole command as marked by '': ``` -ClaferIG v0.4.2.1 +ClaferIG v0.4.3 You can invoke the following commands as indicated by single quotes: [tab] - print the available commands @@ -241,11 +235,11 @@ * no constraints * no types and super types - * except when `--adduidsandtypes` parameter is used + * except when `--useuids --addtypes` parameters are 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. +Additionally, the data notation contains concrete values of the clafers and suffix numbers to distinguish among multiple 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. @@ -279,19 +273,19 @@ a1 b$1 b$2 - c = 10 - d$1 = e1 - d$2 = e2 - g1 = e1 - h$1 = 5 - g2 = e2 - h$2 = 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 - f$4 = 2 + f$1 -> 2 + f$2 -> 3 + f$3 -> 4 + f$4 -> 2 --- Instance 1 End --- ```
alloyIG.jar view
binary file changed (22360 → 22360 bytes)
claferIG.cabal view
@@ -1,5 +1,5 @@ Name: claferIG -Version: 0.4.2.1 +Version: 0.4.3 Synopsis: claferIG is an interactive tool that generates instances of Clafer models. Description: Clafer is a powerful (equivalent to first-order predicate logic) yet lightweight structural modeling language. Despite simplicity and conciseness of Clafer, writing correct models remains challenging due to hard-to-predict interactions among all constraints expressed in the model. Clafer instance generator (ClaferIG) is an interactive tool that generates instances and counter examples of concrete clafers in a Clafer model. If the concrete clafers do not have contradicting constraints, the generator produces valid instance data. Otherwise, the generator produces an unsatisfiable core which included all contradicting constraints and generates a counter example by removing one constraint from the core. The generator can potentially produce many instances if the concrete clafers are not fully specialized. The generator produces different instances on-demand. With these capabilities, the instance generator can be used for debugging models: checking the consistency of the model and detecting under- and overconstraining of the model. The instance generator can also be used programmatically via API (the command line and interactive session interfaces only use the API). Homepage: http://clafer.org @@ -14,6 +14,7 @@ , GHC == 7.8.4 , GHC == 7.10.1 , GHC == 7.10.2 + , GHC == 7.10.3 Cabal-version: >= 1.18 data-files: README.md , alloyIG.jar @@ -44,8 +45,8 @@ , transformers-compat >= 0.3 && < 0.5 , mtl-compat >= 0.2.1 - , clafer == 0.4.2.1 - , claferIG == 0.4.2.1 + , clafer == 0.4.3 + , claferIG == 0.4.3 other-modules: Paths_claferIG Hs-Source-Dirs: src-cmd ghc-options: -Wall -fno-warn-orphans @@ -72,7 +73,7 @@ , transformers-compat >= 0.3 && < 0.5 , mtl-compat >= 0.2.1 - , clafer == 0.4.2.1 + , clafer == 0.4.3 if os(windows) build-depends: HaXml == 1.24 @@ -111,7 +112,7 @@ , tasty-th >= 0.1.3 , transformers-compat >= 0.3 && < 0.5 - , clafer == 0.4.2.1 - , claferIG == 0.4.2.1 + , clafer == 0.4.3 + , claferIG == 0.4.3 other-modules: Paths_claferIG ghc-options: -Wall -fno-warn-orphans
src-cmd/Main.hs view
@@ -102,7 +102,10 @@ runClaferIGT args' $ do let claferModelFileName = claferModelFile args' cModel <- liftIO $ strictReadFile claferModelFileName - when (cModel == "") $ error "Cannot instantiate an empty model." + if null cModel + then error "Cannot instantiate an empty model." + else liftIO $ putStrLn "Compiling the Clafer model..." + oldBw <- getBitwidth env <- getClaferEnv let ir = fst3 $ fromJust $ cIr env @@ -138,7 +141,9 @@ let saveDirectory = fromMaybe return $ underDirectory `liftM` saveDir args' saveAll (savePath claferModelFileName counterRef >>= saveDirectory) quit - Nothing -> runCommandLine + Nothing -> do + liftIO $ putStrLn "Type 'h' for the list of available REPL commands\n" + runCommandLine -- | Convert an Alloy XML file into an instance in Clafer
src/Language/Clafer/IG/ClaferModel.hs view
@@ -63,9 +63,9 @@ 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 + displayValue (AliasValue alias) = " -> " ++ i_name alias + displayValue (IntValue value) = " -> " ++ show value + displayValue (StringValue value) = " -> " ++ value
src/Language/Clafer/IG/CommandLine.hs view
@@ -99,9 +99,12 @@ "\n--- Instance " ++ iNumber ++ " End ---\n\n" 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 "No instances found." 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)" + liftIO $ hPutStrLn stderr "Consider removing one of the constraints from the model." + liftIO $ hPutStrLn stderr "Use the setUnsatCoreMinimization command to minimize the set of constraints below." + liftIO $ hPutStrLn stderr "Try increasing the scopes to get an instance (type 'h' for help)." + printConstraints core case counterexample of Just (Counterexample removed claferModel _) -> do @@ -111,7 +114,7 @@ Nothing -> return () nextLoop context NoInstance -> do - liftIO $ hPutStrLn stderr "No more instances found. Try increasing scope to get more instances." + liftIO $ hPutStrLn stderr "No more instances found. Try increasing the scopes to get more instances (type 'h' for help)." nextLoop context where printTransformation :: Constraint -> [Constraint] -> (String, [Constraint]) @@ -171,9 +174,9 @@ loop Help context = do outputStrLn ( - "--------------------\n" ++ + "------------------\n" ++ "| " ++ claferIGVersion ++ " |\n" ++ - "--------------------\n\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" ++
src/Language/Clafer/IG/Sugarer.hs view
@@ -48,12 +48,13 @@ 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 +-- 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) = @@ -104,24 +105,24 @@ else "" refDecl :: Bool -> Bool -> UIDIClaferMap -> String - refDecl True True uidIClaferMap'' = retrieveSuper uidIClaferMap'' $ i_name id + refDecl True True uidIClaferMap'' = retrieveSuper useUids' 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 :: UIDIClaferMap -> String -> String -retrieveSuper uidIClaferMap' uid = +retrieveSuper :: Bool -> UIDIClaferMap -> String -> String +retrieveSuper useUids' uidIClaferMap' uid = sugarSuper (getSuper iclafer) - ++ - sugarReference (getReference iclafer) + -- ++ + -- sugarReference (getReference iclafer) where iclafer = fromJust $ findIClafer uidIClaferMap' uid sugarSuper :: [String] -> String - sugarSuper [s] = " : " ++ s + sugarSuper [s] = " : " ++ if useUids' then s else makeSimpleName s sugarSuper _ = "" - sugarReference :: [String] -> String - sugarReference [s] = " -> " ++ s - sugarReference _ = "" + -- sugarReference :: [String] -> String + -- sugarReference [s] = " -> " ++ s + -- sugarReference _ = ""
stack.yaml view
@@ -2,9 +2,9 @@ extra-deps: [ data-stringmap-1.0.1.1 , HaXml-1.24 # only for Windows, comment out for other OSs + , clafer-0.4.3 ] -resolver: lts-3.10 +resolver: lts-3.19 packages: -- '../clafer' - '.'