diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -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) diff --git a/Makefile b/Makefile --- a/Makefile +++ b/Makefile @@ -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: diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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 `` 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 ` (`C:\Users\\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 ` (`C:\Users\\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//AppData/Roaming/cabal/bin` +1. execute `make install to=` #### 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 .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 .cfr -all ` @@ -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) diff --git a/alloyIG.jar b/alloyIG.jar Binary files a/alloyIG.jar and b/alloyIG.jar differ diff --git a/claferIG.cabal b/claferIG.cabal --- a/claferIG.cabal +++ b/claferIG.cabal @@ -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 -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 +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 diff --git a/src-cmd/Main.hs b/src-cmd/Main.hs --- a/src-cmd/Main.hs +++ b/src-cmd/Main.hs @@ -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] --alloy-solution=\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] --alloy-solution=\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 () diff --git a/src/Language/Clafer/IG/AlloyIGInterface.hs b/src/Language/Clafer/IG/AlloyIGInterface.hs --- a/src/Language/Clafer/IG/AlloyIGInterface.hs +++ b/src/Language/Clafer/IG/AlloyIGInterface.hs @@ -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 diff --git a/src/Language/Clafer/IG/ClaferIG.hs b/src/Language/Clafer/IG/ClaferIG.hs --- a/src/Language/Clafer/IG/ClaferIG.hs +++ b/src/Language/Clafer/IG/ClaferIG.hs @@ -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 diff --git a/src/Language/Clafer/IG/CommandLine.hs b/src/Language/Clafer/IG/CommandLine.hs --- a/src/Language/Clafer/IG/CommandLine.hs +++ b/src/Language/Clafer/IG/CommandLine.hs @@ -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 diff --git a/src/Language/Clafer/IG/Constraints.hs b/src/Language/Clafer/IG/Constraints.hs --- a/src/Language/Clafer/IG/Constraints.hs +++ b/src/Language/Clafer/IG/Constraints.hs @@ -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 diff --git a/src/Language/Clafer/IG/JSONGenerator.hs b/src/Language/Clafer/IG/JSONGenerator.hs --- a/src/Language/Clafer/IG/JSONGenerator.hs +++ b/src/Language/Clafer/IG/JSONGenerator.hs @@ -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' diff --git a/src/Language/Clafer/IG/Sugarer.hs b/src/Language/Clafer/IG/Sugarer.hs --- a/src/Language/Clafer/IG/Sugarer.hs +++ b/src/Language/Clafer/IG/Sugarer.hs @@ -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 -> "\"\"" 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 _ = "" diff --git a/test/test-suite.hs b/test/test-suite.hs --- a/test/test-suite.hs +++ b/test/test-suite.hs @@ -46,7 +46,7 @@ all = def, saveDir = def, claferModelFile = def, - alloySolution = False, + alloySolution = def, bitwidth = 4, maxInt = 7, useUids = False, diff --git a/tools/Makefile b/tools/Makefile --- a/tools/Makefile +++ b/tools/Makefile @@ -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