diff --git a/Makefile b/Makefile --- a/Makefile +++ b/Makefile @@ -1,58 +1,28 @@ TOOL_DIR = tools -UNAME := $(shell uname | tr "A-Z" "a-z") - -ifeq ($(UNAME), darwin) - ONAME := $(shell uname -s | tr "A-Z" "a-z") -else - ONAME := $(shell uname -o | tr "A-Z" "a-z") -endif - +WGET_COMMAND := wget MNAME := $(shell uname -m | tr "A-Z" "a-z") -ifeq ($(UNAME), linux) - ifeq ($(MNAME), i686) - LIB := x86-linux/libminisatprover* - endif - ifeq ($(MNAME), x86_64) - # amd64 is a nickname for x86_64 - LIB := amd64-linux/libminisatprover* - endif -endif -ifeq ($(UNAME), windows) - ifeq ($(MNAME), i686) - LIB := x86-windows/minisatprover* - endif - ifeq ($(MNAME), x86_64) - LIB := x86-windows/minisatprover* - endif -endif -ifeq ($(basename $(UNAME)), mingw32_nt-6) - ifeq ($(MNAME), i686) - LIB := x86-windows/minisatprover* - endif - ifeq ($(MNAME), x86_64) - LIB := x86-windows/minisatprover* - endif -endif -ifeq ($(ONAME), cygwin) - ifeq ($(MNAME), i686) - LIB := x86-windows/minisatprover* - endif - ifeq ($(MNAME), x86_64) - LIB := x86-windows/minisatprover* +ifeq ($(OS),Windows_NT) + ifeq ($(shell which wget), which: wget: unkown command) + mingw-get install msys-wget-bin endif -endif -ifeq ($(UNAME), darwin) - ifeq ($(MNAME), i686) - LIB := x86-mac/libminisatprover* + 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 ($(MNAME), x86_64) + ifeq ($(UNAME),Darwin) + WGET_COMMAND := curl -O LIB := x86-mac/libminisatprover* endif - WGET_COMMAND := curl -O -else - WGET_COMMAND := wget endif # Calling `make` should only build @@ -84,10 +54,12 @@ ghc -isrc src/dateVer.hs dist/build/autogen/Paths_claferIG.hs -outputdir dist/build --make -o dateVer ./dateVer > src/Language/Clafer/IG/Version.hs +init: + cabal sandbox init --sandbox=../.clafertools-cabal-sandbox + cabal install --only-dependencies # Build takes less time. For ease of development. build: alloyIG.jar - cabal install --only-dependencies cabal configure cabal build @@ -98,11 +70,6 @@ jar cfm alloyIG.jar src/manifest -C dist/javabuild org/clafer/ig/ -C dist/javabuild edu lib: - - @if [[ "$(basename $(UNAME))"=="mingw32_nt-6" && -z "$(shell which unzip)" ]] ; then \ - mingw-get install msys-unzip-bin; \ - fi - @if test -z $(LIB); then \ echo "[WARNING] Did not find a minisat prover binary suitable for your system. You may need to build the binary yourself."; \ else \ @@ -129,5 +96,7 @@ rm -rf dist rm -f alloyIG.jar rm -f claferIG - rm -rf lib - rm -f dateVer* + rm -rf lib/x86-linux + rm -rf lib/amd64-linux + rm -rf lib/x86-windows + rm -rf lib/x86-mac diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,7 +1,7 @@ Clafer Instance Generator ========================= -v0.3.5.1 +v0.3.6 [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.5.1 -* [Java Platform (JDK)](http://www.oracle.com/technetwork/java/javase/downloads/index.html) v6+, 32bit +* [Clafer](https://github.com/gsdlab/clafer) v0.3.6 +* [Java Platform (JDK)](http://www.oracle.com/technetwork/java/javase/downloads/index.html) v7+, 32bit * [Alloy4.1](http://alloy.mit.edu/alloy/download.html) ### Installation from binaries -Binary distributions of the release 0.3.5.1 of Clafer Tools for Windows, Mac, and Linux, +Binary distributions of the release 0.3.6 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 @@ -42,15 +42,15 @@ * [The Haskell Platform](http://hackage.haskell.org/platform/) v2013.2.0.0 -ClaferIG is now available on [Hackage](http://hackage.haskell.org/package/claferIG-0.3.5.1/) and it can be installed using +ClaferIG is now available on [Hackage](http://hackage.haskell.org/package/claferIG-0.3.6/) and it can be installed using 1. `cabal update` 2. `cabal install claferIG` -3. `cd ` (`lib` on Windows or `share` on Linux and Mac) +3. `cd ` (`C:\Users\\AppData\Roaming\cabal\i386-windows-ghc-7.6.3\claferIG-0.3.6` on Windows or `.cabal/share/x86_64-linux-ghc-7.6.3/claferIG-0.3.6/` on Linux) 3. to automatically download Alloy jars - * execute `make` in `clafer-0.3.5.1/tools` + * execute `make` in `tools` 4. To get the `minisatproover` library - * execute `make lib` in clafer-0.3.5.1` + * execute `make lib` 5. copy the following into the Cabal's `bin` folder * the file `alloyIG.jar` * the folder `tools` @@ -61,15 +61,18 @@ Dependencies * [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) - * since the Haskell Platform already contains MinGW, you may choose to install MinGW+MSYS to the same location, e.g., `c:\...\Haskell Platform\2013.2.0.0` - * add the `bin` folders of MinGW (`MinGW\bin`) and MSYS (`MinGW\MSYS\1.0\bin`) to your system path - * `unzip` will be automatically installed + * 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 ### Important: Branches must correspond @@ -80,17 +83,16 @@ Development versions from branches `develop` should work well together but this might not always be the case. ### Building -1. install the [Clafer compiler](https://github.com/gsdlab/clafer) into a `` of your choice - * Tip: it is advised to install both tools into the same `` +1. install the [Clafer compiler](https://github.com/gsdlab/clafer) 2. in some ``, execute `git clone git://github.com/gsdlab/claferIG.git` 3. in `/claferIG`, execute * `cabal update` + * `make init` * `make` ### Installation -1. execute `make install to=` -2. add the `` is on your command PATH +1. execute `make install to=/c/Users//AppData/Roaming/cabal/bin` #### Note: > On Windows, use `/` with the `make` command instead of `\`. @@ -111,7 +113,7 @@ (As printed by `claferIG --help`) -``` v0.3.5.1 +``` v0.3.6 igaONS] FILE @@ -162,9 +164,9 @@ In the interactive mode, the users can invoke the following commands by pressing a letter marked in the command name between '' or the whole command as marked by '': ``` ---------------------- -| ClaferIG v0.3.5.1 | ---------------------- +-------------------- +| ClaferIG 0.3.6 | +-------------------- You can invoke the following commands as indicated by single quotes: [tab] - print the available commands @@ -243,6 +245,8 @@ A possible instance data looks as follows: ```clafer +=== Instance 1 Begin === + a1 b$1 b$2 @@ -258,6 +262,8 @@ f$1 = 2 f$2 = 3 f$3 = 4 + +--- Instance 1 End --- ``` ### Near-miss instance @@ -306,7 +312,7 @@ ========== * See [language's website](http://clafer.org) for news, technical reports and more * Check out a [Clafer tutorial](http://t3-necsis.cs.uwaterloo.ca:8091/Tutorial/Intro) - * Try a live instance of [ClaferWiki](http://t3-necsis.cs.uwaterloo.ca:8091) + * Try a live instance of [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) diff --git a/claferIG.cabal b/claferIG.cabal --- a/claferIG.cabal +++ b/claferIG.cabal @@ -1,5 +1,5 @@ Name: claferIG -Version: 0.3.5.1 +Version: 0.3.6 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 @@ -10,12 +10,12 @@ Stability: Experimental Category: Model Build-type: Simple -Cabal-version: >=1.16 +Cabal-version: >=1.18 data-files: alloyIG.jar, README.md, CHANGES.md, Makefile, - lib/minisatproover.md, + lib/minisatprover.md, tools/Makefile, IDEs/claferIG-README.md, IDEs/sublime-text-2/Packages/SublimeREPL/config/ClaferIG/Default.sublime-commands, @@ -33,27 +33,27 @@ Main-is: Main.hs Build-depends: base >= 4.6.0.1 && < 5, - clafer == 0.3.5.1, - claferIG == 0.3.5.1, - data-stringmap >= 0.9.1, - cmdargs >= 0.10.5, - containers >= 0.4.2.1, + clafer == 0.3.6, + claferIG == 0.3.6, + data-stringmap >= 1.0.1.1, + 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.0.3, + haskeline >= 0.7.1.2, HaXml >= 1.24, mtl >= 2.1.2, parsec >= 3.1.3, process >= 1.1.0.2, transformers >= 0.3.0.0, json-builder >= 0.3, - string-conversions >= 0.3, - test-framework >= 0.8, - test-framework-hunit >= 0.3.0, - test-framework-quickcheck2 >= 0.3.0.1, + string-conversions >= 0.3.0.2, + test-framework >= 0.8.0.3, + test-framework-hunit >= 0.3.0.1, + test-framework-quickcheck2 >= 0.3.0.2, test-framework-th >= 0.2.4, - QuickCheck >= 2.5.1.1, + QuickCheck >= 2.6, HUnit >= 1.2.5.2 other-modules: Paths_claferIG Hs-Source-Dirs: src @@ -64,7 +64,7 @@ default-extensions: DeriveDataTypeable build-depends: array >= 0.4.0.1, base >= 4.6.0.1 && < 5, - containers >= 0.4.2.1, + containers >= 0.5.0.0, directory >= 1.2.0.1, filepath >= 1.3.0.1, process >= 1.1.0.2, @@ -72,22 +72,22 @@ HUnit >= 1.2.5.2, mtl >= 2.1.2, parsec >= 3.1.3, - QuickCheck >= 2.5.1.1, + QuickCheck >= 2.6, transformers >= 0.3.0.0, - data-stringmap >= 0.9.1, - cmdargs >= 0.10.5, + data-stringmap >= 1.0.1.1, + cmdargs >= 0.10.7, executable-path >= 0.0.3, - haskeline >= 0.7.0.3, + haskeline >= 0.7.1.2, HaXml >= 1.24, json-builder >= 0.3, - string-conversions >= 0.3, - test-framework >= 0.8, - test-framework-hunit >= 0.3.0, - test-framework-quickcheck2 >= 0.3.0.1, + string-conversions >= 0.3.0.2, + test-framework >= 0.8.0.3, + test-framework-hunit >= 0.3.0.1, + test-framework-quickcheck2 >= 0.3.0.2, test-framework-th >= 0.2.4, - clafer == 0.3.5.1 + clafer == 0.3.6 hs-source-dirs: src ghc-options: -Wall -fno-warn-unused-do-bind -fno-warn-orphans exposed-modules: Language.Clafer.IG.AlloyIGInterface, @@ -108,7 +108,7 @@ hs-source-dirs: test build-depends: array >= 0.4.0.1, base >= 4.6.0.1 && < 5, - containers >= 0.4.2.1, + containers >= 0.5.0.0, directory >= 1.2.0.1, filepath >= 1.3.0.1, process >= 1.1.0.2, @@ -116,22 +116,22 @@ HUnit >= 1.2.5.2, mtl >= 2.1.2, parsec >= 3.1.3, - QuickCheck >= 2.5.1.1, + QuickCheck >= 2.6, transformers >= 0.3.0.0, - data-stringmap >= 0.9.1, - cmdargs >= 0.10.5, + data-stringmap >= 1.0.1.1, + cmdargs >= 0.10.7, executable-path >= 0.0.3, - haskeline >= 0.7.0.3, + haskeline >= 0.7.1.2, HaXml >= 1.24, json-builder >= 0.3, - string-conversions >= 0.3, - test-framework >= 0.8, - test-framework-hunit >= 0.3.0, - test-framework-quickcheck2 >= 0.3.0.1, + string-conversions >= 0.3.0.2, + test-framework >= 0.8.0.3, + test-framework-hunit >= 0.3.0.1, + test-framework-quickcheck2 >= 0.3.0.2, test-framework-th >= 0.2.4, - clafer == 0.3.5.1, - claferIG == 0.3.5.1 + clafer == 0.3.6, + claferIG == 0.3.6 other-modules: Paths_claferIG ghc-options: -Wall -fno-warn-unused-do-bind -fno-warn-orphans diff --git a/lib/minisatproover.md b/lib/minisatproover.md deleted file mode 100644 --- a/lib/minisatproover.md +++ /dev/null @@ -1,25 +0,0 @@ -ClaferIG uses Alloy which, in turn, requires a SAT solver. ClaferIG requires support for UnSAT core computation, which is provided by `minisatproover` library. - -In this folder, you need to have an appropriate `minisatproover` library for your operating system. -When building from source code, this gets created for you by the `tools/Makefile`. -When building from Hackage, you need to extract the library from `alloy.jar`. - -The taget folder structure should be - -1. for 32bit Linux - -`/bin/lib/x86-linux/libminisatprover*` - -2. for 64bit Linux - -`/bin/lib/amd64-linux/libminisatprover*` - -3. for Windows - -`/bin/lib/x86-windows/minisatprover*` - -4. for Max - -`/bin/lib/x86-mac/libminisatprover* - - diff --git a/lib/minisatprover.md b/lib/minisatprover.md new file mode 100644 --- /dev/null +++ b/lib/minisatprover.md @@ -0,0 +1,25 @@ +ClaferIG uses Alloy which, in turn, requires a SAT solver. ClaferIG requires support for UnSAT core computation, which is provided by `minisatproover` library. + +In this folder, you need to have an appropriate `minisatproover` library for your operating system. +When building from source code, this gets created for you by the `tools/Makefile`. +When building from Hackage, you need to extract the library from `alloy.jar`. + +The taget folder structure should be + +1. for 32bit Linux + +`/bin/lib/x86-linux/libminisatprover*` + +2. for 64bit Linux + +`/bin/lib/amd64-linux/libminisatprover*` + +3. for Windows + +`/bin/lib/x86-windows/minisatprover*` + +4. for Max + +`/bin/lib/x86-mac/libminisatprover* + + 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 @@ -92,7 +92,12 @@ outputStrLn $ if json claferIGArgs' then generateJSON info claferModel - else "=== Instance " ++ (show $ 1 + (length $ unsaved context)) ++ " ===\n\n" ++ (show claferModel) + else let + iNumber = show $ 1 + (length $ unsaved context) + in + "=== Instance " ++ iNumber ++ " Begin ===\n\n" ++ + (show claferModel) ++ + "\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." @@ -328,19 +333,31 @@ globalScopeTuple = ("", globalScope) -- remove the "this/" prefix uidScopes = globalScopeTuple : (map (\(sigName, value) -> (drop 5 sigName, value)) originalScopes) - json = generateJSONScopes qNameMaps' uidScopes - claferModelFile' = claferModelFile claferIGArgs' - modelName = take (length claferModelFile' - 4) claferModelFile' - saveName = modelName ++ ".cfr-scope" - - liftIO $ writeFile saveName json + liftIO $ writeCfrScopeFile uidScopes qNameMaps' $ claferModelFile claferIGArgs' + outputStrLn "Scopes saved to the `.cfr-scope` file." nextLoop context loop LoadScopes context = do - outputStrLn "Not implemented yet." - nextLoop context - + claferIGArgs' <- lift getClaferIGArgs + qNameMaps' <- lift getQNameMaps + maybeUidScopes <- liftIO $ readCfrScopeFile qNameMaps' $ claferModelFile claferIGArgs' + case maybeUidScopes of + Nothing -> do + outputStrLn "The `.cfr-scope` file does not exist. Use the command `saveScopes` to create one." + nextLoop context + Just uidScopes -> do + let + (globalScopes, normalScopes) = partition (\(uid', _) -> null uid') uidScopes + -- from the globalScopes, take the maximum + globalScopeVals = map snd globalScopes + globalScope = maximum globalScopeVals + -- add the "this/" prefix + normalScopesAlloy = map (\(uid', scope) -> ("this/"++uid', scope)) normalScopes + lift $ setGlobalScope globalScope + lift $ mapM_ (\(uid', val) -> setAlloyScope val uid') normalScopesAlloy + outputStrLn "Scopes loaded from the `.cfr-scope` file." + loop ShowScopes context loop (Find name) context = do case (unsaved context ++ saved context) of @@ -499,14 +516,14 @@ mergeScopes _ [] = return() mergeScopes oldScopes newScopes = do let mergedScopes = map (pickLargerScope oldScopes) newScopes - mapM_ (\(uid, val) -> setAlloyScope val uid) mergedScopes + mapM_ (\(uid', val) -> setAlloyScope val uid') mergedScopes pickLargerScope :: [(String, Integer)] -> (String, Integer) -> (String, Integer) -pickLargerScope oldScopes (uid, val) = +pickLargerScope oldScopes (uid', val) = let oldScopesMap = SMap.fromList oldScopes - oldVal = SMap.findWithDefault val uid oldScopesMap - in (uid, max val oldVal) + oldVal = SMap.findWithDefault val uid' oldScopesMap + in (uid', max val oldVal) -- | bitwidth required to store the given integer requiredBitwidth :: Integer -> Integer @@ -647,7 +664,7 @@ maxInModel ir' = intToFloat $ max (maximum scopeValues) $ foldIR getMax 0 ir' getMax :: Ir -> Integer -> Integer getMax (IRIExp (IInt n)) m = max m $ abs n - getMax (IRClafer IClafer{card = Just (_, n)}) m = max m n + getMax (IRClafer IClafer{_card = Just (_, n)}) m = max m n getMax _ m = m intToFloat :: Integer -> Float 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 @@ -99,10 +99,10 @@ parseConstraints claferModel imodule mapping = mapMaybe (uncurry convert) mapping where - clafers = mDecls imodule >>= subclafers - pexps = (mapMaybe constraint $ mDecls imodule ++ concatMap elements clafers) >>= subexpressions + clafers = _mDecls imodule >>= subclafers + pexps = (mapMaybe constraint $ _mDecls imodule ++ concatMap _elements clafers) >>= subexpressions convert s IrPExp{pUid} = - Just $ UserConstraint s $ ConstraintInfo pUid (inPos $ findPExp pUid) $ extract $ inPos $ findPExp pUid + Just $ UserConstraint s $ ConstraintInfo pUid (_inPos $ findPExp pUid) $ extract $ _inPos $ findPExp pUid convert s LowerCard{pUid, isGroup = False} = Just $ LowerCardinalityConstraint s $ claferInfo pUid convert s UpperCard{pUid, isGroup = False} = @@ -111,8 +111,8 @@ Just $ ExactCardinalityConstraint s $ claferInfo pUid convert _ _ = Nothing - findPExp pUid = fromMaybe (error $ "Unknown constraint " ++ pUid) $ find ((== pUid) . pid) pexps - findClafer pUid = fromMaybe (error $ "Unknown clafer " ++ pUid) $ find ((== pUid) . uid) clafers + findPExp pUid = fromMaybe (error $ "Unknown constraint " ++ pUid) $ find ((== pUid) . _pid) pexps + findClafer pUid = fromMaybe (error $ "Unknown clafer " ++ pUid) $ find ((== pUid) . _uid) clafers text = lines claferModel extract (Span (Pos l1 c1) (Pos l2 c2)) -- This one should occur the rest should not happen | l1 == l2 = drop (fromInteger $ c1 - 1) $ take (fromInteger $ c2 - 1) $ text !! (fromInteger $ l1 - 1) @@ -173,24 +173,24 @@ convertCard (l, -1) = Cardinality l Nothing convertCard (l, h) = Cardinality l $ Just h claferInfo pUid = - ClaferInfo (ident claf) $ convertCard $ fromJust $ card claf + ClaferInfo (_ident claf) $ convertCard $ fromJust $ _card claf where claf = findClafer pUid subclafers :: IElement -> [IClafer] -subclafers (IEClafer claf) = claf : (elements claf >>= subclafers) +subclafers (IEClafer claf) = claf : (_elements claf >>= subclafers) subclafers _ = [] constraint :: IElement -> Maybe PExp -constraint (IEConstraint _ pexp) = Just pexp +constraint (IEConstraint _ pexp') = Just pexp' constraint _ = Nothing subexpressions :: PExp -> [PExp] -subexpressions p@PExp{I.exp = exp'} = +subexpressions p@PExp{I._exp = exp'} = p : subexpressions' exp' where - subexpressions' IDeclPExp{oDecls, bpexp} = - concatMap (subexpressions . body) oDecls ++ subexpressions bpexp - subexpressions' IFunExp{exps} = concatMap subexpressions exps + subexpressions' IDeclPExp{_oDecls, _bpexp} = + concatMap (subexpressions . _body) _oDecls ++ subexpressions _bpexp + subexpressions' IFunExp{_exps} = concatMap subexpressions _exps subexpressions' _ = [] 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 @@ -96,11 +96,12 @@ sugarId :: Bool -> Bool -> Bool -> Id -> Id sugarId useUids' addTypes' addRefDecl id = - if count == 1 - then Id (finalName ++ (refDecl addTypes' addRefDecl info)) 0 - else Id (finalName ++ "$" ++ show ordinal ++ (refDecl addTypes' addRefDecl info)) 0 + Id (finalName ++ ordinalDisplay ++ (refDecl addTypes' addRefDecl info)) 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 diff --git a/src/Main.hs b/src/Main.hs --- a/src/Main.hs +++ b/src/Main.hs @@ -30,11 +30,13 @@ import Language.Clafer.IG.Solution import Language.Clafer.IG.Sugarer import Language.Clafer.ClaferArgs +import Language.Clafer.JSONMetaData import Language.ClaferT import Control.Monad import Control.Monad.IO.Class import Data.Either import qualified Data.Map as Map +import Data.List (partition) import Data.Maybe import Data.IORef import Prelude hiding (all) @@ -44,7 +46,7 @@ claferIGArgsDef :: IGArgs claferIGArgsDef = IGArgs { - all = def &= help "Saves all instances up to the provided scope or a counterexample.", + all = def &= opt "1" &= help "Saves all instances or a counterexample. Reads scopes from a `.cfr.scope` file or uses the provided global scope." &= typ "INTEGER", 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", @@ -96,29 +98,45 @@ runClaferIG :: IGArgs -> IO (Either ClaferErrs ()) runClaferIG args' = runClaferIGT args' $ do - cModel <- liftIO $ strictReadFile $ claferModelFile args' + let claferModelFileName = claferModelFile args' + cModel <- liftIO $ strictReadFile claferModelFileName when (cModel == "") $ error "Cannot instantiate an empty model." oldBw <- getBitwidth env <- getClaferEnv let ir = fst3 $ fromJust $ cIr env scopes <- getScopes setBitwidth $ findNecessaryBitwidth ir oldBw $ map snd scopes + solve case all args' of - Just scope -> - do - setGlobalScope scope - solve - - let file' = claferModelFile args' - counterRef <- liftIO $ newIORef 1 - - let saveDirectory = fromMaybe return $ underDirectory `liftM` saveDir args' - saveAll (savePath file' counterRef >>= saveDirectory) - return () + Just scope -> do + -- copied from CommandLine LoadScopes command + qNameMaps' <- getQNameMaps + maybeUidScopes <- liftIO $ readCfrScopeFile qNameMaps' claferModelFileName + case maybeUidScopes of + 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 + (globalScopes, normalScopes) = partition (\(uid, _) -> null uid) uidScopes + -- from the globalScopes, take the maximum + globalScopeVals = map snd globalScopes + globalScope = maximum globalScopeVals + -- add the "this/" prefix + normalScopesAlloy = map (\(uid, scope) -> ("this/"++uid, scope)) normalScopes + setGlobalScope globalScope + mapM_ (\(uid, val) -> setAlloyScope val uid) normalScopesAlloy + -- end copied + + solve + + counterRef <- liftIO $ newIORef 1 + + let saveDirectory = fromMaybe return $ underDirectory `liftM` saveDir args' + saveAll (savePath claferModelFileName counterRef >>= saveDirectory) + quit Nothing -> runCommandLine - - quit -- | Convert an Alloy XML file into an instance in Clafer runAlloySolution :: IGArgs -> IO () diff --git a/test/test-suite.hs b/test/test-suite.hs --- a/test/test-suite.hs +++ b/test/test-suite.hs @@ -1,4 +1,4 @@ -{-# OPTIONS_GHC -XTemplateHaskell #-} +{-# LANGUAGE TemplateHaskell #-} {- Copyright (C) 2012-2013 Luke Brown diff --git a/tools/Makefile b/tools/Makefile --- a/tools/Makefile +++ b/tools/Makefile @@ -1,13 +1,15 @@ -UNAME := $(shell uname | tr "A-Z" "a-z") - +WGET_COMMAND := wget -ifeq ($(UNAME), darwin) - WGET_COMMAND := curl -O +ifeq ($(OS),Windows_NT) + ifeq ($(shell which wget), which: wget: unkown command) + mingw-get install msys-wget-bin + endif else - WGET_COMMAND := wget + UNAME := $(shell uname -s) + ifeq ($(UNAME),Darwin) + WGET_COMMAND := curl -O + endif endif - - all: @if test ! -f "alloy4.jar"; then \