diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,3 +1,7 @@ +**ClaferIG Version 0.3.10 released on April 24, 2015** + +[Release](https://github.com/gsdlab/claferIG/pull/25) + **ClaferIG Version 0.3.9 released on March 06, 2015** [Release](https://github.com/gsdlab/claferIG/pull/24) diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,7 +1,7 @@ Clafer Instance Generator ========================= -v0.3.9 +v0.3.10 [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,14 +24,15 @@ Regardless of the installation method, the following are required: -* [Clafer](https://github.com/gsdlab/clafer) v0.3.9 -* [Java Platform (JDK)](http://www.oracle.com/technetwork/java/javase/downloads/index.html) v8+, 32bit +* [Clafer](https://github.com/gsdlab/clafer) v0.3.10 +* [Java Platform (JDK)](http://www.oracle.com/technetwork/java/javase/downloads/index.html) v8+, 64bit + * On Windows, Java must be 32bit because of Alloy * [Alloy4.2](http://alloy.mit.edu/alloy/download.html) ### Installation from binaries -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). +Binary distributions of the release 0.3.10 of Clafer Tools for Windows, Mac, and Linux, +can be downloaded from [Clafer Tools - Binary Distributions](http://gsd.uwaterloo.ca/clafer-tools-binary-distributions). 1. download the binaries and unpack `` of your choice 2. add the `` to your system path so that the executables can be found @@ -40,45 +41,45 @@ Dependencies -* [The Haskell Platform](http://hackage.haskell.org/platform/) v2014.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.9/) and it can be installed using +ClaferIG is now available on [Hackage](http://hackage.haskell.org/package/claferIG-0.3.10/) and it can be installed using 1. `cabal update` 2. `cabal install claferIG` -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. `cd ` (`C:\Users\\AppData\Roaming\cabal\i386-windows-ghc-7.8.3\claferIG-0.3.10` on Windows or `.cabal/share/x86_64-linux-ghc-7.8.3/claferIG-0.3.10/` on Linux) 3. to automatically download Alloy4.2 jar - * execute `make` in `tools` + * execute `make` in `tools` 4. To get the `minisatproover` library - * execute `make lib` + * execute `make lib -B` 5. copy the following into the Cabal's `bin` folder * the file `alloyIG.jar` * the folder `tools` - * the folder `lib` + * the folder `lib` ### Installation from the source code Dependencies -* [The Haskell Platform](http://hackage.haskell.org/platform/) v2014.2.0.0 +* [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. * 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 +On Windows -* [MSYS2](http://msys2.sourceforge.net/) +* [MSYS2](http://msys2.sourceforge.net/) * download MSYS2 installer * in MSYS2 console, execute - * `pacman -Syu` + * `pacman -Syu` * `pacman -S make wget unzip diffutils` ### Important: Branches must correspond -All related projects are following the *simultaneous release model*. -The branch `master` contains releases, whereas the branch `develop` contains code under development. +All related projects are following the *simultaneous release model*. +The branch `master` contains releases, whereas the branch `develop` contains code under development. 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. @@ -96,7 +97,7 @@ 1. execute `make install to=` -#### Note: +#### Note: > On Windows, use `/` with the `make` command instead of `\`. @@ -119,8 +120,8 @@ (As printed by `claferIG --help`) -``` -ClaferIG v0.3.9 +``` +ClaferIG v0.3.10 claferIG [OPTIONS] [FILE] @@ -172,7 +173,7 @@ ``` ------------------ -| ClaferIG 0.3.9 | +| ClaferIG 0.3.10 | ------------------ You can invoke the following commands as indicated by single quotes: @@ -228,7 +229,7 @@ ### Note: > The instance data models could be read by the Clafer translator if the translator had simple type inference support. -#### Example +#### Example For a model @@ -259,17 +260,17 @@ b$2 c = 10 d$1 = e1 - d$2 = e2 - g1 = e1 - h$1 = 5 + d$2 = e2 + g1 = e1 + h$1 = 5 g2 = e2 h$2 = 2 e1 f$1 = 2 f$2 = 3 - f$3 = 4 - f$4 = 2 + f$3 = 4 + f$4 = 2 --- Instance 1 End --- ``` @@ -278,7 +279,7 @@ Near-miss instance notation is the same as the instance data notation. Additionally, it indicates which constraints belong to the UnSAT Core. -#### Example +#### Example For a model @@ -293,7 +294,7 @@ [ b ] // C3 ``` -Constraints C1, C2, and C3 form an UnSAT Core. Removal of any of them will make the model satisfiable. The constraint C1 is part of the model and cannot be removed (part of domain knowledge). Therefore, either C2 or C3 must be removed to remove the inconsistency. +Constraints C1, C2, and C3 form an UnSAT Core. Removal of any of them will make the model satisfiable. The constraint C1 is part of the model and cannot be removed (part of domain knowledge). Therefore, either C2 or C3 must be removed to remove the inconsistency. On possible near-miss instance: @@ -304,6 +305,23 @@ ``` Here, `C1` and `C3` are satisfied but `C2` is not. To resolve the conflict and assuming that the counter example is actually a correct instance data, the user has to modify the model by removing `C2`. However, should the counter example actually represent incorrect instance data, the user can remove `C3` to resolve the inconsistency. + +Troubleshooting +--------------- + +If you get an error: + +``` +Exception in thread "main" java.lang.UnsatisfiedLinkError: no minisatproverx1 in java.library.path + at java.lang.ClassLoader.loadLibrary(Unknown Source) + at java.lang.Runtime.loadLibrary0(Unknown Source) + at java.lang.System.loadLibrary(Unknown Source) + at org.clafer.ig.AlloyIG.main(AlloyIG.java:275) +``` + +it means that you have a 64bit Java on Windows instead of the required 32bit one. +On Windows, Alloy only supports Minisat with UnSAT core on 32bit Java. +There's nothing we can do. How it works ------------ 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,5 +1,5 @@ Name: claferIG -Version: 0.3.9 +Version: 0.3.10 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 @@ -23,7 +23,6 @@ Executable claferIG 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 @@ -37,16 +36,15 @@ , executable-path >= 0.0.3 , haskeline >= 0.7.1.2 - , clafer == 0.3.9 - , claferIG == 0.3.9 + , clafer == 0.3.10 + , claferIG == 0.3.10 other-modules: Paths_claferIG Hs-Source-Dirs: src-cmd - ghc-options: -Wall -fno-warn-unused-do-bind -fno-warn-orphans -rtsopts + ghc-options: -Wall -fno-warn-orphans library build-tools: ghc >= 7.8.3 default-language: Haskell2010 - default-extensions: DeriveDataTypeable build-depends: array >= 0.5.0 , base >= 4.7.0.1 && < 5 , containers >= 0.5.5.1 @@ -65,9 +63,9 @@ , json-builder >= 0.3 , string-conversions >= 0.3.0.2 - , clafer == 0.3.9 + , clafer == 0.3.10 hs-source-dirs: src - ghc-options: -Wall -fno-warn-unused-do-bind -fno-warn-orphans -rtsopts + ghc-options: -Wall -fno-warn-orphans exposed-modules: Language.Clafer.IG.AlloyIGInterface , Language.Clafer.IG.ClaferIG , Language.Clafer.IG.ClaferModel @@ -97,7 +95,7 @@ , tasty-hunit >= 0.9 , tasty-th >= 0.1.2 - , clafer == 0.3.9 - , claferIG == 0.3.9 + , clafer == 0.3.10 + , claferIG == 0.3.10 other-modules: Paths_claferIG - ghc-options: -Wall -fno-warn-unused-do-bind -fno-warn-orphans + ghc-options: -Wall -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 @@ -92,7 +92,7 @@ case try of Right r -> return r Left l -> do - mapM putStrLn $ printError l + mapM_ putStrLn $ printError l putStrLn "Press enter to retry." void getLine tryClaferIG args3 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 @@ -34,6 +34,7 @@ import Language.Clafer.Front.AbsClafer (Span(..), Pos(..)) import Language.Clafer.IG.Process import System.Console.Haskeline.MonadException +import Prelude -- | An interface to the Alloy Analyzer 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 @@ -73,7 +73,7 @@ import Language.Clafer.IG.Sugarer import Control.Applicative import Control.Monad -import Control.Monad.Error +import Control.Monad.Except import Control.Monad.Trans.State.Strict import Data.List import Data.Monoid @@ -85,6 +85,7 @@ import System.Console.Haskeline.MonadException import Paths_claferIG (version) import Data.Version (showVersion) +import Prelude claferIGVersion :: String claferIGVersion = "ClaferIG " ++ showVersion Paths_claferIG.version @@ -129,8 +130,8 @@ runClaferIGT :: MonadIO m => IGArgs -> ClaferIGT m a -> m (Either ClaferErrs a) runClaferIGT args run = - AlloyIG.runAlloyIGT $ runErrorT $ do - env <- (ErrorT $ load args) `catchError` (\x -> lift AlloyIG.sendQuitCommand >> throwError x) + AlloyIG.runAlloyIGT $ runExceptT $ do + env <- (ExceptT $ load args) `catchError` (\x -> lift AlloyIG.sendQuitCommand >> throwError x) lift $ evalStateT (unwrap run) env where unwrap (ClaferIGT c) = c @@ -175,10 +176,10 @@ load :: MonadIO m => IGArgs -> AlloyIGT m (Either ClaferErrs ClaferIGEnv) load igArgs = - runErrorT $ do + runExceptT $ do claferModel <- liftIO $ strictReadFile claferFile' - (claferEnv', alloyModel, mapping, sMap) <- ErrorT $ return $ callClaferTranslator claferModel + (claferEnv', alloyModel, mapping, sMap) <- ExceptT $ return $ callClaferTranslator claferModel let (ir, genv', _) = fromJust $ cIr claferEnv' @@ -285,7 +286,7 @@ setAlloyScope value sigName = do subset <- ClaferIGT $ lift $ AlloyIG.sendSetScopeCommand sigName value - runErrorT $ maybe (return ()) throwError $ sigToClaferName <$> subset + runExceptT $ maybe (return ()) throwError $ sigToClaferName <$> subset next :: MonadIO m => ClaferIGT m Instance @@ -333,10 +334,10 @@ reload :: MonadIO m => ClaferIGT m (Either ClaferErrs ()) reload = - runErrorT $ do + runExceptT $ do globalScope <- lift $ getGlobalScope claferIGArgs' <- lift $ getClaferIGArgs - env <- ErrorT $ ClaferIGT $ lift $ load claferIGArgs' + env <- ExceptT $ ClaferIGT $ lift $ load claferIGArgs' lift $ set env lift $ setGlobalScope globalScope diff --git a/src/Language/Clafer/IG/ClaferModel.hs b/src/Language/Clafer/IG/ClaferModel.hs --- a/src/Language/Clafer/IG/ClaferModel.hs +++ b/src/Language/Clafer/IG/ClaferModel.hs @@ -1,5 +1,5 @@ {- - Copyright (C) 2012-2013 Jimmy Liang + Copyright (C) 2012-2015 Jimmy Liang, Michal Antkiewicz, Luke Michael Brown 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 @@ -20,7 +20,7 @@ SOFTWARE. -} -module Language.Clafer.IG.ClaferModel (ClaferModel(..), Clafer(..), Id(..), Value(..), c_name, buildClaferModel, traverse) where +module Language.Clafer.IG.ClaferModel (ClaferModel(..), Clafer(..), Id(..), Value(..), c_name, buildClaferModel, traverseModel) where import Data.List import Data.Either @@ -31,8 +31,8 @@ -- | Clafer model instance data ClaferModel = ClaferModel {c_topLevel::[Clafer]} -data Clafer = Clafer {c_id::Id, c_value::Maybe Value, c_children::[Clafer]} -data Value = AliasValue {c_alias::Id} | IntValue {v_value::Int} | StringValue {v_str ::String} deriving Show +data Clafer = Clafer {c_id::Id, c_value::Maybe Value, c_children::[Clafer]} deriving Eq +data Value = AliasValue {c_alias::Id} | IntValue {v_value::Int} | StringValue {v_str ::String} deriving (Show, Eq) c_name :: Clafer -> String c_name = i_name . c_id @@ -69,8 +69,8 @@ -traverse :: ClaferModel -> [Clafer] -traverse (ClaferModel clafers) = +traverseModel :: ClaferModel -> [Clafer] +traverseModel (ClaferModel clafers) = traverseClafers clafers where traverseClafers :: [Clafer] -> [Clafer] @@ -170,10 +170,15 @@ buildClaferModel :: Solution -> ClaferModel buildClaferModel solution = - ClaferModel $ lefts $ map buildClafer (getRoots ftree) + ClaferModel $ removeDups [] $ lefts $ map buildClafer (getRoots ftree) where sigMap = buildSigMap solution ftree = buildFamilyTree solution + + removeDups :: [Clafer] -> [Clafer] -> [Clafer] + removeDups acc [] = acc + removeDups acc (m:ms) = if (m `elem` ms) then removeDups acc ms + else removeDups (m{c_children = (removeDups [] $ c_children m)} : acc) ms intType = s_id $ findWithDefault (error "Missing Int sig") "Int" sigMap 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 @@ -36,21 +36,20 @@ import Language.Clafer.JSONMetaData import Language.Clafer.QNameUID import qualified Language.Clafer.IG.AlloyIGInterface as AlloyIG -import Control.Monad -import Control.Monad.Error +import Control.Monad.Except import Data.Char import Data.IORef import Data.List import Data.Monoid -import Data.Foldable (foldMap) +import Data.Foldable hiding (mapM_, maximum, find, elem, notElem, foldr, any, concat) import qualified Data.StringMap as SMap import qualified Data.Map as Map import Data.Maybe import System.Console.Haskeline import System.IO import GHC.Float -import Prelude hiding (id) import qualified Text.Parsec.Error as E +import Prelude data AutoComplete = Auto_Command | Auto_Clafer | Auto_ClaferInstance | Auto_UnsatCoreMinimization | Auto_Space | Auto_Digit | No_Auto deriving Show @@ -88,7 +87,7 @@ uidIClaferMap' <- lift $ getUIDIClaferMap case solution of Instance claferModel xml -> do - liftIO $ writeIORef (claferInstances $ autoCompleteContext context) $ map c_name (traverse claferModel) + liftIO $ writeIORef (claferInstances $ autoCompleteContext context) $ map c_name (traverseModel claferModel) outputStrLn $ if json claferIGArgs' then generateJSON uidIClaferMap' claferModel @@ -155,18 +154,18 @@ setUpper info@ClaferInfo{cardinality = c} upper = info{cardinality = c{upper = upper}} deleteLower :: String -> [Constraint] -> Maybe [Constraint] - deleteLower id ys = - findAndDelete id (filter isLowerCardinalityConstraint ys) + deleteLower id' ys = + findAndDelete id' (filter isLowerCardinalityConstraint ys) deleteUpper :: String -> [Constraint] -> Maybe [Constraint] - deleteUpper id ys = - findAndDelete id (filter isUpperCardinalityConstraint ys) + deleteUpper id' ys = + findAndDelete id' (filter isUpperCardinalityConstraint ys) findAndDelete :: String -> [Constraint] -> Maybe [Constraint] findAndDelete _ [] = Nothing - findAndDelete id (c:cs) - | id == uniqueId (claferInfo c) = Just cs - | otherwise = (c :) `fmap` findAndDelete id cs + findAndDelete id' (c:cs) + | id' == uniqueId (claferInfo c) = Just cs + | otherwise = (c :) `fmap` findAndDelete id' cs loop Help context = @@ -220,7 +219,7 @@ oldScopes <- lift getScopes oldBw <- lift getBitwidth - runErrorT $ ErrorT (lift reload) `catchError` (liftIO . mapM_ (hPutStrLn stderr) . printError) + _ <- runExceptT $ ExceptT (lift reload) `catchError` (liftIO . mapM_ (hPutStrLn stderr) . printError) env <- lift getClaferEnv let ir = fst3 $ fromJust $ cIr env @@ -247,7 +246,7 @@ printBitwidthWarning newBw oldScopes <- lift getScopes - mapM ( \(sigName', val') -> setAlloyScopeAndBitwidth bitwidth' (max 1 $ val'+inc') (sigToClaferName sigName') sigName') oldScopes + mapM_ ( \(sigName', val') -> setAlloyScopeAndBitwidth bitwidth' (max 1 $ val'+inc') (sigToClaferName sigName') sigName') oldScopes lift solve outputStrLn ("Global scope changed to " ++ show newGlobalScope) nextLoop context @@ -362,7 +361,7 @@ do case (unsaved context ++ saved context) of model:_ -> - case find ((name ==) . c_name) $ traverse model of + case find ((name ==) . c_name) $ traverseModel model of Just clafer' -> outputStrLn $ show clafer' Nothing -> outputStrLn $ "\"" ++ name ++ "\" not found in the model." [] -> outputStrLn $ "No instance" @@ -486,8 +485,8 @@ outputStrLn $ "Saved to " ++ saveName save cs (counter + 1) -try :: MonadIO m => ErrorT String (InputT m) a -> InputT m () -try e = either outputStrLn (void . return) =<< runErrorT e +try :: MonadIO m => ExceptT String (InputT m) a -> InputT m () +try e = either outputStrLn (void . return) =<< runExceptT e incAlloyScopeAndBitwidth :: MonadIO m => Integer -> Integer -> String -> UID -> InputT (ClaferIGT m) () incAlloyScopeAndBitwidth bitwidth' inc' fqName' sigName' = do @@ -501,7 +500,7 @@ newBw <- lift $ getBitwidth outputStrLn $ "Warning! Requested scope for " ++ fqName' ++ " is larger than maximum allowed by bitwidth ... increasing bitwidth" printBitwidthWarning newBw - lift $ setAlloyScope newValue' sigName' + _ <- lift $ setAlloyScope newValue' sigName' outputStrLn $ "Scope of " ++ fqName' ++ " (" ++ (drop 5 sigName') ++ ") changed to " ++ show newValue' mergeScopes :: MonadIO m => [(UID, Integer)] -> [(UID, Integer)] -> ClaferIGT m () diff --git a/src/Language/Clafer/IG/CommandLineParser.hs b/src/Language/Clafer/IG/CommandLineParser.hs --- a/src/Language/Clafer/IG/CommandLineParser.hs +++ b/src/Language/Clafer/IG/CommandLineParser.hs @@ -90,7 +90,7 @@ doParse = do skipMany (space "") - commandLine + _ <-commandLine -- Force the parse to fail to gather expected/unexpected messages fail "reached end" diff --git a/tools/Makefile b/tools/Makefile --- a/tools/Makefile +++ b/tools/Makefile @@ -11,6 +11,6 @@ all: @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; \ + $(WGET_COMMAND) http://alloy.mit.edu/alloy/downloads/alloy4.2_2015-02-22.jar; \ + mv alloy4.2_2015-02-22.jar alloy4.2.jar; \ fi