claferIG 0.3.6.1 → 0.3.7
raw patch · 17 files changed
+264/−489 lines, 17 filesdep +tastydep +tasty-hunitdep +tasty-thdep −QuickCheckdep −test-frameworkdep −test-framework-hunitdep ~claferdep ~claferIGPVP ok
version bump matches the API change (PVP)
Dependencies added: tasty, tasty-hunit, tasty-th
Dependencies removed: QuickCheck, test-framework, test-framework-hunit, test-framework-quickcheck2, test-framework-th
Dependency ranges changed: clafer, claferIG
API changes (from Hackage documentation)
Files
- CHANGES.md +4/−0
- IDEs/claferIG-README.md +0/−46
- IDEs/sublime-text-2/Packages/SublimeREPL/config/ClaferIG/Default.sublime-commands +0/−10
- IDEs/sublime-text-2/Packages/SublimeREPL/config/ClaferIG/IGF.sublime-menu +0/−26
- IDEs/sublime-text-2/Packages/SublimeREPL/config/ClaferIG/IGS.sublime-menu +0/−26
- Makefile +17/−43
- README.md +13/−14
- alloyIG.jar binary
- claferIG.cabal +15/−50
- src-cmd/Main.hs +174/−0
- src/Language/Clafer/IG/AlloyIGInterface.hs +1/−8
- src/Language/Clafer/IG/ClaferIG.hs +3/−11
- src/Language/Clafer/IG/CommandLine.hs +1/−13
- src/Language/Clafer/IG/Constraints.hs +2/−58
- src/Main.hs +0/−174
- test/test-suite.hs +7/−7
- tools/Makefile +27/−3
CHANGES.md view
@@ -1,3 +1,7 @@+**ClaferIG Version 0.3.7 released on Oct 23, 2014** + +[Release](https://github.com/gsdlab/claferIG/pull/22) + **ClaferIG Version 0.3.6.1 released on Jul 08, 2014** [Release](https://github.com/gsdlab/claferIG/pull/20)
− IDEs/claferIG-README.md
@@ -1,46 +0,0 @@-IDE Integrations -================ - -Sublime Text 2 --------------- - -We provide a configuration for SublimeREPL for running ClaferIG inside Sublime as a REPL. - -### Usage - -Use `<CTRL>+i`, `g`, `s` to open a Clafer `.cfr` file with ClaferIG and `--ss=simple` setting. -Use `<CTRL>+i`, `g`, `f` to open a Clafer `.cfr` file with ClaferIG and `--ss=full` setting. -This commands assume that Clafer and ClaferIG executables are in system `PATH`. - -### Installation - -1. Install `SublimeREPL` plugin. - * You need to install `Package Control` first - see [installation](http://wbond.net/sublime_packages/package_control/installation). To open the Console, go to `View->Show Console`. - * Go to `Preferences->Package Control` - * type `Install`, `<Enter>` - * type `SublimeREPL`, `<Enter>` -2. Copy the folder `ClaferIG` from `IDEs\sublime-text-2\Packages\SublimeREPL\config\` to `Packages\SublimeREPL\config\` in Sublime Text 2 folder inside your home directory. -3. In Sublime, open `Preferences->Key Bindings - User` and add the following key bindings there (inside the `[ ]`, remember about commas `,` to have a proper list) - -``` - { - "keys": [ "ctrl+i", "g", "s" ], - "args": { - "id": "repl_claferIG", - "file": "config/ClaferIG/IGS.sublime-menu" - }, - "command": "run_existing_window_command" - }, - { - "keys": [ "ctrl+i", "g", "f" ], - "args": { - "id": "repl_claferIG", - "file": "config/ClaferIG/IGF.sublime-menu" - }, - "command": "run_existing_window_command" - } -``` - -> Note: -> on Windows 7 and 8, the folder is `<user name>\AppData\Roaming\Sublime Text 2\Packages`. -> on Mac, the folder is `~/Library/Application Support/Sublime Text 2/Packages`.
− IDEs/sublime-text-2/Packages/SublimeREPL/config/ClaferIG/Default.sublime-commands
@@ -1,10 +0,0 @@-[ - { - "caption": "SublimeREPL: ClaferIG", - "command": "run_existing_window_command", "args": - { - "id": "repl_claferIG", - "file": "config/ClaferIG/IGF.sublime-menu" - } - } -]
@@ -1,26 +0,0 @@-[ - { - "id": "tools", - "children": - [{ - "caption": "SublimeREPL", - "mnemonic": "r", - "id": "SublimeREPL", - "children": - [ - {"command": "repl_open", - "caption": "ClaferIG", - "id": "repl_claferIG", - "mnemonic": "i", - "args": { - "type": "subprocess", - "encoding": "utf8", - "cmd": ["claferIG", "$file", "--ss=full"], - "cwd": "$file_path", - "external_id": "claferIG" - } - } - ] - }] - } -]
@@ -1,26 +0,0 @@-[ - { - "id": "tools", - "children": - [{ - "caption": "SublimeREPL", - "mnemonic": "r", - "id": "SublimeREPL", - "children": - [ - {"command": "repl_open", - "caption": "ClaferIG", - "id": "repl_claferIG", - "mnemonic": "i", - "args": { - "type": "subprocess", - "encoding": "utf8", - "cmd": ["claferIG", "$file"], - "cwd": "$file_path", - "external_id": "claferIG" - } - } - ] - }] - } -]
Makefile view
@@ -1,30 +1,5 @@ TOOL_DIR = tools -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 - # Calling `make` should only build all: alloyIG.jar lib build @@ -34,12 +9,11 @@ mkdir -p $(to)/lib mkdir -p $(to)/tools cp -f lib/*minisatprover* $(to)/lib - cp -f tools/alloy4.jar $(to)/tools + cp -f tools/alloy4.2.jar $(to)/tools cp -f alloyIG.jar $(to) cp -f LICENSE $(to)/ cp -f CHANGES.md $(to)/claferIG-CHANGES.md - cp -f README.md $(to)/claferIG-README.md - cp -f -R IDEs $(to) + cp -f README.md $(to)/claferIG-README.mds cabal install --bindir=$(to) --ghc-option="-O" # Removes current build and makes a clean new one (Don't use if starting from scratch!) @@ -56,7 +30,7 @@ init: cabal sandbox init --sandbox=../.clafertools-cabal-sandbox - cabal install --only-dependencies + cabal install --only-dependencies --enable-tests # Build takes less time. For ease of development. build: alloyIG.jar @@ -66,14 +40,14 @@ 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 $(MAKE) -C $(TOOL_DIR) mkdir -p dist/javabuild - javac -source 1.6 -target 1.6 -cp "tools/alloy4.jar" -d dist/javabuild src/org/clafer/ig/AlloyIG.java src/org/clafer/ig/Util.java src/org/clafer/ig/AlloyIGException.java src/edu/mit/csail/sdg/alloy4compiler/parser/AlloyCompiler.java + javac -source 1.6 -target 1.6 -cp "tools/alloy4.2.jar" -d dist/javabuild src/org/clafer/ig/AlloyIG.java src/org/clafer/ig/Util.java src/org/clafer/ig/AlloyIGException.java src/edu/mit/csail/sdg/alloy4compiler/parser/AlloyCompiler.java jar cfm alloyIG.jar src/manifest -C dist/javabuild org/clafer/ig/ -C dist/javabuild edu lib: @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 \ - unzip tools/alloy4.jar $(LIB) -d lib; \ + unzip tools/alloy4.2.jar $(LIB) -d lib; \ chmod +x lib/$(LIB); \ cp lib/$(LIB) lib; \ fi @@ -82,21 +56,21 @@ # Only test a subset of the suite. The other cases do not work yet. cabal configure --enable-tests cabal build - mkdir dist/build/test-suite/lib - cp alloyIG.jar dist/build/test-suite/lib + # Install what's needed for running the tests + cp alloyIG.jar dist/build/test-suite/ + cp alloyIG.jar dist/build/claferIG/ + cp -r tools/ dist/build/test-suite/ + 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 - ./claferIG --all=4 -s dist/run test/suite/backquoted.cfr - ./claferIG --all=4 -s dist/run test/suite/BobsTeam.cfr - ./claferIG --all=4 -s dist/run test/suite/inconsistent.cfr - ./claferIG --all=4 -s dist/run test/suite/PersonFingers.cfr - ./claferIG --all=4 -s dist/run test/suite/waitingLine.cfr - ./claferIG --all=4 -s dist/run test/suite/subclaferCardinality.cfr clean: rm -rf dist rm -f alloyIG.jar rm -f claferIG - rm -rf lib/x86-linux - rm -rf lib/amd64-linux - rm -rf lib/x86-windows - rm -rf lib/x86-mac+ rm -rf tools/x86-linux + rm -rf tools/amd64-linux + rm -rf tools/x86-windows + rm -rf tools/x86-mac
README.md view
@@ -1,7 +1,7 @@ Clafer Instance Generator ========================= -v0.3.6.1 +v0.3.7 [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.6.1 +* [Clafer](https://github.com/gsdlab/clafer) v0.3.7 * [Java Platform (JDK)](http://www.oracle.com/technetwork/java/javase/downloads/index.html) v7+, 32bit -* [Alloy4.1](http://alloy.mit.edu/alloy/download.html) +* [Alloy4.2](http://alloy.mit.edu/alloy/download.html) ### Installation from binaries -Binary distributions of the release 0.3.6.1 of Clafer Tools for Windows, Mac, and Linux, +Binary distributions of the release 0.3.7 of Clafer Tools for Windows, Mac, and Linux, can be downloaded from [Clafer Tools - Binary Distributions](http://http://gsd.uwaterloo.ca/clafer-tools-binary-distributions). 1. download the binaries and unpack `<target directory>` of your choice @@ -42,12 +42,12 @@ * [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.6.1/) and it can be installed using +ClaferIG is now available on [Hackage](http://hackage.haskell.org/package/claferIG-0.3.7/) and it can be installed using 1. `cabal update` 2. `cabal install claferIG` -3. `cd <cabal's lib or share folder>` (`C:\Users\<user>\AppData\Roaming\cabal\i386-windows-ghc-7.6.3\claferIG-0.3.6.1` on Windows or `.cabal/share/x86_64-linux-ghc-7.6.3/claferIG-0.3.6.1/` on Linux) -3. to automatically download Alloy jars +3. `cd <cabal's lib or share folder>` (`C:\Users\<user>\AppData\Roaming\cabal\i386-windows-ghc-7.6.3\claferIG-0.3.7` on Windows or `.cabal/share/x86_64-linux-ghc-7.6.3/claferIG-0.3.7/` on Linux) +3. to automatically download Alloy4.2 jar * execute `make` in `tools` 4. To get the `minisatproover` library * execute `make lib` @@ -98,11 +98,10 @@ > On Windows, use `/` with the `make` command instead of `\`. -Integration with Sublime Text 2 +Integration with Sublime Text 2/3 ------------------------------- -See [IDEs/claferIG-README.md](IDEs/claferIG-README.md) - +See [ClaferToolsST](https://github.com/gsdlab/ClaferToolsST) Usage ===== @@ -113,7 +112,7 @@ (As printed by `claferIG --help`) -``` v0.3.6.1 +``` v0.3.7 igaONS] FILE @@ -164,9 +163,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 0.3.6.1 | --------------------- +------------------ +| ClaferIG 0.3.7 | +------------------ You can invoke the following commands as indicated by single quotes: [tab] - print the available commands
alloyIG.jar view
binary file changed (22360 → 22360 bytes)
claferIG.cabal view
@@ -1,5 +1,5 @@ Name: claferIG -Version: 0.3.6.1 +Version: 0.3.7 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 @@ -16,12 +16,7 @@ CHANGES.md, Makefile, lib/minisatprover.md, - tools/Makefile, - IDEs/claferIG-README.md, - IDEs/sublime-text-2/Packages/SublimeREPL/config/ClaferIG/Default.sublime-commands, - IDEs/sublime-text-2/Packages/SublimeREPL/config/ClaferIG/IGF.sublime-menu, - IDEs/sublime-text-2/Packages/SublimeREPL/config/ClaferIG/IGS.sublime-menu - + tools/Makefile source-repository head type: git location: git://github.com/gsdlab/claferIG.git @@ -33,30 +28,19 @@ Main-is: Main.hs Build-depends: base >= 4.6.0.1 && < 5, - clafer == 0.3.6.1, - claferIG == 0.3.6.1, - data-stringmap >= 1.0.1.1, + clafer == 0.3.7, + claferIG == 0.3.7, 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, - 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.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.6, - HUnit >= 1.2.5.2 + mtl >= 2.1.2, + transformers >= 0.3.0.0 other-modules: Paths_claferIG - Hs-Source-Dirs: src + Hs-Source-Dirs: src-cmd + ghc-options: -Wall -fno-warn-unused-do-bind -fno-warn-orphans -rtsopts library build-tools: ghc >= 7.6.3 @@ -69,27 +53,20 @@ filepath >= 1.3.0.1, process >= 1.1.0.2, - HUnit >= 1.2.5.2, mtl >= 2.1.2, parsec >= 3.1.3, - QuickCheck >= 2.6, transformers >= 0.3.0.0, data-stringmap >= 1.0.1.1, - cmdargs >= 0.10.7, executable-path >= 0.0.3, haskeline >= 0.7.1.2, HaXml >= 1.24, json-builder >= 0.3, 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.6.1 + clafer == 0.3.7 hs-source-dirs: src - ghc-options: -Wall -fno-warn-unused-do-bind -fno-warn-orphans + 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, @@ -108,30 +85,18 @@ hs-source-dirs: test 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, HUnit >= 1.2.5.2, - mtl >= 2.1.2, - parsec >= 3.1.3, - QuickCheck >= 2.6, transformers >= 0.3.0.0, - data-stringmap >= 1.0.1.1, cmdargs >= 0.10.7, - executable-path >= 0.0.3, - haskeline >= 0.7.1.2, - HaXml >= 1.24, - json-builder >= 0.3, - 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, + tasty >= 0.10, + tasty-hunit >= 0.9, + tasty-th >= 0.1.2, - clafer == 0.3.6.1, - claferIG == 0.3.6.1 + clafer == 0.3.7, + claferIG == 0.3.7 other-modules: Paths_claferIG ghc-options: -Wall -fno-warn-unused-do-bind -fno-warn-orphans
+ src-cmd/Main.hs view
@@ -0,0 +1,174 @@+{-# LANGUAGE DeriveDataTypeable #-} + +{- + Copyright (C) 2012-2014 Jimmy Liang, Michal Antkiewicz <http://gsd.uwaterloo.ca> + + Permission is hereby granted, free of charge, to any person obtaining a copy of + this software and associated documentation files (the "Software"), to deal in + the Software without restriction, including without limitation the rights to + use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies + of the Software, and to permit persons to whom the Software is furnished to do + so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all + copies or substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. +-} + +module Main where + +import Language.Clafer.IG.ClaferIG +import Language.Clafer.IG.ClaferModel +import Language.Clafer.IG.CommandLine +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) +import System.Console.CmdArgs +import System.Directory +import System.FilePath + +claferIGArgsDef :: IGArgs +claferIGArgsDef = IGArgs { + 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", + alloySolution = False &= help "Convert Alloy solution to a Clafer solution.", + 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.", + 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", + 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", + scope_strategy_comp = Simple &= help "Use scope computation strategy during compiling: none, simple (default), or full." &= name "ss" +} &= summary claferIGVersion &= program "claferig" + + +main :: IO () +main = + do + args' <- cmdArgs claferIGArgsDef + let + bw = bitwidth args' + mi = maxInt args' + -- maxInt overrides the bitwidth setting + args'' = if (mi > allowedMaxInt bw) + then args' {bitwidth = requiredBitwidth mi} + else args' + + if (alloySolution args'') + then + runAlloySolution args'' + else if (json args'') + then + tryClaferIG (args'' { useUids = True }) + else + tryClaferIG args'' + where + tryClaferIG args3 = + do + try <- runClaferIG args3 + case try of + Right r -> return r + Left l -> do + mapM putStrLn $ printError l + putStrLn "Press enter to retry." + void getLine + tryClaferIG args3 + +runClaferIG :: IGArgs -> IO (Either ClaferErrs ()) +runClaferIG args' = + runClaferIGT args' $ do + 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 + -- 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, scope2) -> ("this/"++uid, scope2)) 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 + +-- | Convert an Alloy XML file into an instance in Clafer +runAlloySolution :: IGArgs -> IO () +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 + +savePath :: FilePath -> IORef Int -> IO FilePath +savePath file' counterRef = + do + counter <- readIORef counterRef + writeIORef counterRef (counter + 1) + return $ file' ++ "." ++ (show counter) ++ ".data" + + +underDirectory :: FilePath -> FilePath -> IO FilePath +underDirectory dir file' = + do + createDirectoryIfMissing True dir + return $ joinPath [dir, file'] + + +saveAll :: IO FilePath -> ClaferIGT IO () +saveAll nextFile = + do + file' <- liftIO nextFile + liftIO $ createDirectoryIfMissing True $ takeDirectory file' + solution <- next + case solution of + Instance{modelInstance = modelInstance'} -> do + liftIO $ writeFile file' (show modelInstance') + saveAll nextFile + _ -> return ()
src/Language/Clafer/IG/AlloyIGInterface.hs view
@@ -224,16 +224,9 @@ do putMsg "removeConstraint" sendPosition from >> sendPosition to - (PosSpan _ from to) -> -- Should never happen - do - putMsg "removeConstraint" - sendPosition from >> sendPosition to where sendPosition (Pos line column) = - putMsg (show line) >> putMsg (show column) - sendPosition (PosPos _ line column) = - putMsg (show line) >> putMsg (show column) -- Should never happen - + putMsg (show line) >> putMsg (show column) -- | Tell alloyIG to return the unsat core of the previous operation sendUnsatCoreCommand :: MonadIO m => AlloyIGT m UnsatCore
src/Language/Clafer/IG/ClaferIG.hs view
@@ -197,15 +197,7 @@ editMap = fromList . removeConstraints . Data.List.foldr (\(num, ir) acc -> case (getIClafer ir) of Just (IClafer _ _ _ _ uid' _ _ _ _) -> (num, uid') : acc - _ -> acc) [] . tail . (Data.List.foldr (\x acc -> case x of - ((Span (Pos l1 _) (Pos l2 _)), irs) -> (zip [l1..l2] (replicate (fromIntegral $ l2 - l1 + 1) irs)) ++ acc - ((PosSpan _ (Pos l1 _) (Pos l2 _)), irs) -> (zip [l1..l2] (replicate (fromIntegral $ l2 - l1 + 1) irs)) ++ acc - ((Span (PosPos _ l1 _) (Pos l2 _)), irs) -> (zip [l1..l2] (replicate (fromIntegral $ l2 - l1 + 1) irs)) ++ acc - ((Span (Pos l1 _) (PosPos _ l2 _)), irs) -> (zip [l1..l2] (replicate (fromIntegral $ l2 - l1 + 1) irs)) ++ acc - ((Span (PosPos _ l1 _) (PosPos _ l2 _)), irs) -> (zip [l1..l2] (replicate (fromIntegral $ l2 - l1 + 1) irs)) ++ acc - ((PosSpan _ (PosPos _ l1 _) (Pos l2 _)), irs) -> (zip [l1..l2] (replicate (fromIntegral $ l2 - l1 + 1) irs)) ++ acc - ((PosSpan _ (Pos l1 _) (PosPos _ l2 _)), irs) -> (zip [l1..l2] (replicate (fromIntegral $ l2 - l1 + 1) irs)) ++ acc - ((PosSpan _ (PosPos _ l1 _) (PosPos _ l2 _)), irs) -> (zip [l1..l2] (replicate (fromIntegral $ l2 - l1 + 1) irs)) ++ acc) []) . toList + _ -> acc) [] . tail . (Data.List.foldr (\((Span (Pos l1 _) (Pos l2 _)), irs) acc -> (zip [l1..l2] (replicate (fromIntegral $ l2 - l1 + 1) irs)) ++ acc) []) . toList getIClafer :: [Ir] -> Maybe IClafer getIClafer [] = Nothing getIClafer ((IRClafer c):_) = Just c @@ -219,11 +211,11 @@ parse compile results <- generate - let (Just alloyResult) = Map.lookup Alloy results + let (Just alloyResult) = Map.lookup Alloy42 results return (claferEnv alloyResult, outputCode alloyResult, mappingToAlloy alloyResult, stringMap alloyResult) mapLeft f (Left l) = Left $ f l mapLeft _ (Right r) = Right r - claferArgs = defaultClaferArgs{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 = [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} claferFile' = claferModelFile igArgs bitwidth' = bitwidth igArgs
src/Language/Clafer/IG/CommandLine.hs view
@@ -419,15 +419,7 @@ addScopeVal scopesMap' (Just name) = "scope = " ++ (fromJustShow $ Map.lookup name scopesMap') getCommentLines :: String -> [Integer] - getCommentLines = foldr (\(s, _) acc -> case s of - (Span (Pos l1 _) (Pos l2 _)) -> [l1..l2] ++ acc - (PosSpan _ (Pos l1 _) (Pos l2 _)) -> [l1..l2] ++ acc - (Span (PosPos _ l1 _) (Pos l2 _)) -> [l1..l2] ++ acc --This one and bellow should not happen - (Span (Pos l1 _) (PosPos _ l2 _)) -> [l1..l2] ++ acc - (Span (PosPos _ l1 _) (PosPos _ l2 _)) -> [l1..l2] ++ acc - (PosSpan _ (PosPos _ l1 _) (Pos l2 _)) -> [l1..l2] ++ acc - (PosSpan _ (Pos l1 _) (PosPos _ l2 _)) -> [l1..l2] ++ acc - (PosSpan _ (PosPos _ l1 _) (PosPos _ l2 _)) -> [l1..l2] ++ acc) [] . getComments + getCommentLines = foldr (\((Span (Pos l1 _) (Pos l2 _)), _) acc -> [l1..l2] ++ acc) [] . getComments getConstraintInfo :: Constraint -> String getConstraintInfo (UserConstraint _ info) = show info @@ -624,10 +616,6 @@ "Parse error at line " ++ show l ++ ", column " ++ show c ++ ":\n " ++ msg printErr (SemanticErr (ErrPos _ _ (Pos l c)) msg) = "Error at line " ++ show l ++ ", column " ++ show c ++ ":\n " ++ msg - printErr (ParseErr (ErrPos _ _ (PosPos _ l c)) msg) = - "Parse error at line " ++ show l ++ ", column " ++ show c ++ ":\n " ++ msg --This should never happen - printErr (SemanticErr (ErrPos _ _ (PosPos _ l c)) msg) = - "Error at line " ++ show l ++ ", column " ++ show c ++ ":\n " ++ msg --This should never happen printErr (ClaferErr msg) = "Error:\n " ++ msg
src/Language/Clafer/IG/Constraints.hs view
@@ -64,12 +64,7 @@ instance Show ConstraintInfo where show ConstraintInfo{pos = Span (Pos l c) _, syntax} = syntax ++ " (line " ++ show l ++ ", column " ++ show c ++ ")" - show ConstraintInfo{pos = PosSpan _ (Pos l c) _, syntax} = syntax ++ " (line " ++ show l ++ ", column " ++ show c ++ ")" -- Should never happen - show ConstraintInfo{pos = Span (PosPos _ l c) _, syntax} = syntax ++ " (line " ++ show l ++ ", column " ++ show c ++ ")" -- Should never happen - show ConstraintInfo{pos = PosSpan _ (PosPos _ l c) _, syntax} = syntax ++ " (line " ++ show l ++ ", column " ++ show c ++ ")" -- Should never happen - - isLowerCardinalityConstraint :: Constraint -> Bool isLowerCardinalityConstraint LowerCardinalityConstraint{} = True isLowerCardinalityConstraint _ = False @@ -82,10 +77,8 @@ to :: Span -> Pos to (Span _ t) = t -to (PosSpan _ _ t) = t -- Should never happen {-from :: Span -> Pos -from (Span f _) = f -from (PosSpan _ f _) = f -- Should never happen-} +from (Span f _) = f -} lookupConstraint :: Span -> [Constraint] -> Constraint @@ -114,56 +107,7 @@ 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) - | otherwise = unlines $ f1 : fs ++ [fn] - where - f1 = drop (fromInteger $ c1 - 1) $ text !! (fromInteger $ l1 - 1) - fs = map (text !!) [(fromInteger $ l1) .. (fromInteger $ l2 - 2)] - fn = take (fromInteger $ c2 - 1) $ text !! (fromInteger $ l2 - 1) - extract (Span (PosPos _ l1 c1) (Pos l2 c2)) - | l1 == l2 = drop (fromInteger $ c1 - 1) $ take (fromInteger $ c2 - 1) $ text !! (fromInteger $ l1 - 1) - | otherwise = unlines $ f1 : fs ++ [fn] - where - f1 = drop (fromInteger $ c1 - 1) $ text !! (fromInteger $ l1 - 1) - fs = map (text !!) [(fromInteger $ l1) .. (fromInteger $ l2 - 2)] - fn = take (fromInteger $ c2 - 1) $ text !! (fromInteger $ l2 - 1) - extract (Span (Pos l1 c1) (PosPos _ l2 c2)) - | l1 == l2 = drop (fromInteger $ c1 - 1) $ take (fromInteger $ c2 - 1) $ text !! (fromInteger $ l1 - 1) - | otherwise = unlines $ f1 : fs ++ [fn] - where - f1 = drop (fromInteger $ c1 - 1) $ text !! (fromInteger $ l1 - 1) - fs = map (text !!) [(fromInteger $ l1) .. (fromInteger $ l2 - 2)] - fn = take (fromInteger $ c2 - 1) $ text !! (fromInteger $ l2 - 1) - extract (Span (PosPos _ l1 c1) (PosPos _ l2 c2)) - | l1 == l2 = drop (fromInteger $ c1 - 1) $ take (fromInteger $ c2 - 1) $ text !! (fromInteger $ l1 - 1) - | otherwise = unlines $ f1 : fs ++ [fn] - where - f1 = drop (fromInteger $ c1 - 1) $ text !! (fromInteger $ l1 - 1) - fs = map (text !!) [(fromInteger $ l1) .. (fromInteger $ l2 - 2)] - fn = take (fromInteger $ c2 - 1) $ text !! (fromInteger $ l2 - 1) - extract (PosSpan _ (Pos l1 c1) (Pos l2 c2)) - | l1 == l2 = drop (fromInteger $ c1 - 1) $ take (fromInteger $ c2 - 1) $ text !! (fromInteger $ l1 - 1) - | otherwise = unlines $ f1 : fs ++ [fn] - where - f1 = drop (fromInteger $ c1 - 1) $ text !! (fromInteger $ l1 - 1) - fs = map (text !!) [(fromInteger $ l1) .. (fromInteger $ l2 - 2)] - fn = take (fromInteger $ c2 - 1) $ text !! (fromInteger $ l2 - 1) - extract (PosSpan _ (PosPos _ l1 c1) (Pos l2 c2)) - | l1 == l2 = drop (fromInteger $ c1 - 1) $ take (fromInteger $ c2 - 1) $ text !! (fromInteger $ l1 - 1) - | otherwise = unlines $ f1 : fs ++ [fn] - where - f1 = drop (fromInteger $ c1 - 1) $ text !! (fromInteger $ l1 - 1) - fs = map (text !!) [(fromInteger $ l1) .. (fromInteger $ l2 - 2)] - fn = take (fromInteger $ c2 - 1) $ text !! (fromInteger $ l2 - 1) - extract (PosSpan _ (Pos l1 c1) (PosPos _ l2 c2)) - | l1 == l2 = drop (fromInteger $ c1 - 1) $ take (fromInteger $ c2 - 1) $ text !! (fromInteger $ l1 - 1) - | otherwise = unlines $ f1 : fs ++ [fn] - where - f1 = drop (fromInteger $ c1 - 1) $ text !! (fromInteger $ l1 - 1) - fs = map (text !!) [(fromInteger $ l1) .. (fromInteger $ l2 - 2)] - fn = take (fromInteger $ c2 - 1) $ text !! (fromInteger $ l2 - 1) - extract (PosSpan _ (PosPos _ l1 c1) (PosPos _ l2 c2)) + extract (Span (Pos l1 c1) (Pos l2 c2)) | l1 == l2 = drop (fromInteger $ c1 - 1) $ take (fromInteger $ c2 - 1) $ text !! (fromInteger $ l1 - 1) | otherwise = unlines $ f1 : fs ++ [fn] where
− src/Main.hs
@@ -1,174 +0,0 @@-{-# LANGUAGE DeriveDataTypeable #-} - -{- - Copyright (C) 2012-2014 Jimmy Liang, Michal Antkiewicz <http://gsd.uwaterloo.ca> - - Permission is hereby granted, free of charge, to any person obtaining a copy of - this software and associated documentation files (the "Software"), to deal in - the Software without restriction, including without limitation the rights to - use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies - of the Software, and to permit persons to whom the Software is furnished to do - so, subject to the following conditions: - - The above copyright notice and this permission notice shall be included in all - copies or substantial portions of the Software. - - THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR - IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, - FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE - AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER - LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, - OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE - SOFTWARE. --} - -module Main where - -import Language.Clafer.IG.ClaferIG -import Language.Clafer.IG.ClaferModel -import Language.Clafer.IG.CommandLine -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) -import System.Console.CmdArgs -import System.Directory -import System.FilePath - -claferIGArgsDef :: IGArgs -claferIGArgsDef = IGArgs { - 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", - alloySolution = False &= help "Convert Alloy solution to a Clafer solution.", - 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.", - 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", - 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", - scope_strategy_comp = Simple &= help "Use scope computation strategy during compiling: none, simple (default), or full." &= name "ss" -} &= summary claferIGVersion &= program "claferig" - - -main :: IO () -main = - do - args' <- cmdArgs claferIGArgsDef - let - bw = bitwidth args' - mi = maxInt args' - -- maxInt overrides the bitwidth setting - args'' = if (mi > allowedMaxInt bw) - then args' {bitwidth = requiredBitwidth mi} - else args' - - if (alloySolution args'') - then - runAlloySolution args'' - else if (json args'') - then - tryClaferIG (args'' { useUids = True }) - else - tryClaferIG args'' - where - tryClaferIG args3 = - do - try <- runClaferIG args3 - case try of - Right r -> return r - Left l -> do - mapM putStrLn $ printError l - putStrLn "Press enter to retry." - void getLine - tryClaferIG args3 - -runClaferIG :: IGArgs -> IO (Either ClaferErrs ()) -runClaferIG args' = - runClaferIGT args' $ do - 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 - -- 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 - --- | Convert an Alloy XML file into an instance in Clafer -runAlloySolution :: IGArgs -> IO () -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 - -savePath :: FilePath -> IORef Int -> IO FilePath -savePath file' counterRef = - do - counter <- readIORef counterRef - writeIORef counterRef (counter + 1) - return $ file' ++ "." ++ (show counter) ++ ".data" - - -underDirectory :: FilePath -> FilePath -> IO FilePath -underDirectory dir file' = - do - createDirectoryIfMissing True dir - return $ joinPath [dir, file'] - - -saveAll :: IO FilePath -> ClaferIGT IO () -saveAll nextFile = - do - file' <- liftIO nextFile - liftIO $ createDirectoryIfMissing True $ takeDirectory file' - solution <- next - case solution of - Instance{modelInstance = modelInstance'} -> do - liftIO $ writeFile file' (show modelInstance') - saveAll nextFile - _ -> return ()
test/test-suite.hs view
@@ -31,16 +31,15 @@ import System.FilePath import System.Console.CmdArgs import Prelude hiding (all) -import Test.Framework -import Test.Framework.TH -import Test.Framework.Providers.HUnit -import Test.HUnit +import Test.Tasty +import Test.Tasty.HUnit +import Test.Tasty.TH -tg_testsuite :: Test.Framework.Test +tg_testsuite :: TestTree tg_testsuite = $(testGroupGenerator) main :: IO () -main = defaultMain[tg_testsuite] +main = defaultMain $ testGroup "Tests" [ tg_testsuite ] claferIGArgsDef :: IGArgs claferIGArgsDef = IGArgs { @@ -67,7 +66,7 @@ --getModel :: MonadIO m => FilePath -> ClaferIGT m (Either Language.ClaferT.ClaferErrs Instance) getModel fPath = runClaferIGT (defaultIGArgs fPath) $ do - setGlobalScope (fromJust $ all $ defaultIGArgs fPath) + setGlobalScope (fromMaybe 1 $ all $ defaultIGArgs fPath) solve counterRef <- liftIO $ newIORef 1 let saveDirectory = fromMaybe return $ underDirectory `liftM` saveDir (defaultIGArgs fPath) @@ -90,6 +89,7 @@ fromRight (Right x) = x +fromRight _ = error "fromRight received Left _. Should never happen." case_strMapCheck :: Assertion
tools/Makefile view
@@ -1,18 +1,42 @@ 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 + UNAME := $(shell uname -s) + ifeq ($(UNAME),Darwin) + WGET_COMMAND := curl -O + endif +endif + all: - @if test ! -f "alloy4.jar"; then \ - echo "[WARNING] Missing alloy4.jar. Downloading..."; \ - $(WGET_COMMAND) http://alloy.mit.edu/alloy/downloads/alloy4.jar; \ + @if test ! -f "alloy4.2.jar"; then \ + 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