call-alloy 0.2.2.0 → 0.3

raw patch · 15 files changed

+137/−146 lines, 15 filesdep +extradep ~mtlbinary-addedPVP ok

version bump matches the API change (PVP)

Dependencies added: extra

Dependency ranges changed: mtl

API changes (from Hackage documentation)

Files

• ChangeLog.md +8/−0
• bin/commons-cli/commons-cli-1.4.jar binary
• bin/commons-cli/commons-cli-1.5.0.jar binary
• bin/org.alloytools.alloy.dist.jar too large to diff
• bin/slf4j/LICENSE +21/−0
• bin/slf4j/slf4j-simple-1.7.36.jar binary
• call-alloy.cabal +9/−7
• src/Language/Alloy/Debug.hs +2/−0
• src/Language/Alloy/Functions.hs +34/−79
• src/Language/Alloy/Internal/Call.hs +33/−50
• src/Language/Alloy/Parser.hs +13/−4
• src/Language/Alloy/RessourceNames.hs +5/−1
• src/Language/Alloy/Ressources.hs +5/−1
• src/Language/Alloy/Types.hs +6/−0
• test/Language/Alloy/CallSpec.hs +1/−4

@@ -4,6 +4,14 @@  ## Released changes +### 0.3++- upgrade to Alloy 6.0.0+- allow slashes in object names+- allow identity relations+- improve feedback on misspelled/missing relation and signature names+- remove 'relToMap'+ ### 0.2.2.0  - deprecate 'relToMap'

binary file changed (53820 → absent bytes)

binary file changed (absent → 58284 bytes)

file too large to diff

@@ -0,0 +1,21 @@+ Copyright (c) 2004-2017 QOS.ch+ All rights reserved.++ 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.

binary file changed (absent → 15333 bytes)

@@ -3,11 +3,9 @@ -- This file has been generated from package.yaml by hpack version 0.34.4. -- -- see: https://github.com/sol/hpack------ hash: 5c150629bcf8420718ec571afc36561ad329e6a349265b2719b219d59a96a022  name:           call-alloy-version:        0.2.2.0+version:        0.3 synopsis:       A simple library to call Alloy given a specification description:    Please see the README on GitHub at <https://github.com/marcellussiegburg/call-alloy#readme> category:       Language@@ -15,7 +13,7 @@ bug-reports:    https://github.com/marcellussiegburg/call-alloy/issues author:         Marcellus Siegburg maintainer:     marcellus.siegburg@uni-due.de-copyright:      2019-2020 Marcellus Siegburg+copyright:      2019-2022 Marcellus Siegburg license:        MIT license-file:   LICENSE build-type:     Simple@@ -25,9 +23,11 @@     ChangeLog.md     bin/alloy/RunAlloy.class     bin/org.alloytools.alloy.dist.jar-    bin/commons-cli/commons-cli-1.4.jar+    bin/commons-cli/commons-cli-1.5.0.jar     bin/commons-cli/NOTICE.txt     bin/commons-cli/LICENSE.txt+    bin/slf4j/slf4j-simple-1.7.36.jar+    bin/slf4j/LICENSE  source-repository head   type: git@@ -53,9 +53,10 @@     , bytestring >=0.10.4 && <0.12     , containers ==0.6.*     , directory ==1.3.*+    , extra ==1.7.*     , file-embed >=0.0.11 && <0.1     , filepath ==1.4.*-    , hashable >=1.2 && <1.4+    , hashable >=1.2 && <1.5     , mtl ==2.2.*     , process ==1.6.*     , split ==0.2.*@@ -93,9 +94,10 @@     , call-alloy     , containers ==0.6.*     , directory ==1.3.*+    , extra ==1.7.*     , file-embed >=0.0.11 && <0.1     , filepath ==1.4.*-    , hashable >=1.2 && <1.4+    , hashable >=1.2 && <1.5     , hspec     , mtl ==2.2.*     , process ==1.6.*

@@ -9,6 +9,8 @@ module Language.Alloy.Debug (   getRawInstances,   getRawInstancesWith,+  parseInstance,   ) where  import Language.Alloy.Internal.Call     (getRawInstances, getRawInstancesWith)+import Language.Alloy.Parser            (parseInstance)

@@ -10,21 +10,17 @@ Furthermore, it provides functions to handle these parsed instances. -} module Language.Alloy.Functions (-  getSingle, getDouble, getTriple,-  getSingleAs, getDoubleAs, getTripleAs,+  getIdentityAs, getSingleAs, getDoubleAs, getTripleAs,   int, object,   lookupSig,-  objectName,-  relToMap,   scoped, unscoped,   ) where -import qualified Data.Set                         as S (fromList, size, toList)-import qualified Data.Map                         as M (fromList, lookup)+import qualified Data.Set                         as S (fromList, toList)+import qualified Data.Map                         as M (lookup, keys)  import Control.Monad.Except             (MonadError, throwError)-import Data.Function                    (on)-import Data.List                        (groupBy)+import Data.List                        (intercalate) import Data.Map                         (Map) import Data.Set                         (Set) import Data.String                      (IsString, fromString)@@ -36,6 +32,7 @@   Object (..),   Relation (..),   Signature (..),+  showSignature,   )  {-|@@ -109,6 +106,23 @@     ++ "\nPlease open an issue at https://github.com/marcellussiegburg/call-alloy stating what you tried to attempt"  {-|+Retrieve a single value of a given 'AlloySig'.+The Value will be created by applying the given mapping function+from object name and 'Int' to value.+The mapping has to be injective (for all expected cases).+Successful if the signature's relation is a single value.+-}+getIdentityAs+  :: (MonadError s m, IsString s)+  => String+  -> (String -> Int -> m b)+  -> Entry Map a+  -> m b+getIdentityAs s f inst = do+  e <- lookupRel identity s inst+  specifyObject f e++{-| Retrieve a set of values of a given 'AlloySig'. Values will be created by applying the given mapping function from object Name and 'Int' to value.@@ -122,22 +136,10 @@   -> AlloySig   -> m (Set a) getSingleAs s f inst = do-  set <- getSingle s inst+  set <- lookupRel single s inst   traverseSet (specifyObject f) set -{-# DEPRECATED getSingle "use the typed version getSingleAs instead" #-} {-|-Retrieve a set of objects of a given 'AlloySig'.-Successful if the signature's relation is a set (or empty).--}-getSingle-  :: (IsString s, MonadError s m)-  => String-  -> AlloySig-  -> m (Set Object)-getSingle = lookupRel single--{-| Retrieve a binary relation of values of given 'AlloySig'. Values will be created by applying the given mapping functions from object Name and 'Int' to the value.@@ -152,26 +154,14 @@   -> AlloySig   -> m (Set (a, b)) getDoubleAs s f g inst = do-  set <- getDouble s inst+  set <- lookupRel double s inst   traverseSet applyMapping set   where     applyMapping (x, y) = (,)       <$> specifyObject f x       <*> specifyObject g y -{-# DEPRECATED getDouble "use the typed version getDoubleAs instead" #-} {-|-Retrieve a binary relation of objects of a given 'AlloySig'.-Successful if the signature's relation is binary (or empty).--}-getDouble-  :: (IsString s, MonadError s m)-  => String-  -> AlloySig-  -> m (Set (Object, Object))-getDouble = lookupRel double--{-| Retrieve a ternary relation of values of a given 'AlloySig'. Values will be created by applying the given mapping functions from object Name and 'Int' to the value.@@ -187,7 +177,7 @@   -> AlloySig   -> m (Set (a, b, c)) getTripleAs s f g h inst = do-  set <- getTriple s inst+  set <- lookupRel triple s inst   traverseSet applyMapping set   where     applyMapping (x, y, z) = (,,)@@ -195,40 +185,6 @@       <*> specifyObject g y       <*> specifyObject h z -{-# DEPRECATED getTriple "use the typed version getTripleAs instead" #-}-{-|-Retrieve a ternary relation of objects of a given 'AlloySig'.-Successful if the signature's relation is ternary (or empty).--}-getTriple-  :: (IsString s, MonadError s m)-  => String-  -> AlloySig-  -> m (Set (Object, Object, Object))-getTriple = lookupRel triple--{-|-Transforms a relation into a Mapping.--}-binaryToMap :: (Ord k, Ord v) => Set (k, v) -> Map k (Set v)-binaryToMap bin = M.fromList-  [(fst (head gs), S.fromList $ snd <$> gs)-  | gs <- groupBy ((==) `on` fst) $ S.toList bin]--{-# DEPRECATED relToMap "use binaryToMap instead" #-}-relToMap-  :: (IsString s, MonadError s m, Ord k, Ord v)-  => (a -> (k, v))-  -> Set a-  -> m (Map k (Set v))-relToMap f rel-  | S.size map' == length rel' = return $ binaryToMap map'-  | otherwise                  =-    throwError "relToMap: The performed transformation is not injective."-  where-    rel' = S.toList rel-    map' = S.fromList $ fmap f rel'- lookupRel   :: (IsString s, MonadError s m)   => (Relation a -> m b)@@ -238,6 +194,7 @@ lookupRel kind rel e = case M.lookup rel (relation e) of   Nothing -> throwError $ fromString $ "relation " ++ fromString rel     ++ " is missing in the Alloy instance"+    ++ " available are: " ++ intercalate ", " (M.keys $ relation e)   Just r  -> kind r  {-|@@ -249,19 +206,17 @@   -> AlloyInstance   -> m AlloySig lookupSig s insta = case M.lookup s insta of-  Nothing -> throwError $ fromString $ maybe "" (++ "/") (scope s) ++ sigName s+  Nothing -> throwError $ fromString $ showSignature s     ++ " is missing in the Alloy instance"+    ++ " available are: \"" ++ intercalate "\", " (showSignature <$> M.keys insta)   Just e   -> return e -{-# DEPRECATED objectName "use the typed versions of get... e.g. getSingleAs instead of getSingle" #-}-{-|-Retrieve an object's name.--}-objectName :: Object -> String-objectName o = case o of-  Object s n     -> s ++ '$' : show n-  NumberObject n -> show n-  NamedObject n  -> n+identity+  :: (IsString s, MonadError s m)+  => Relation a+  -> m Object+identity (Id r) = return r+identity _      = throwError "Relation is (unexpectedly) not exactly a single element"  single   :: (IsString s, MonadError s m, Monoid (a Object))

@@ -18,7 +18,7 @@   ) where  import qualified Data.ByteString                  as BS-  (hGetLine, intercalate, isSuffixOf, writeFile)+  (hGetLine, intercalate, isSuffixOf, stripPrefix, writeFile) import qualified Data.ByteString.Char8            as BS (unlines)  import Control.Concurrent (@@ -56,9 +56,14 @@ #endif  import Language.Alloy.RessourceNames (-  alloyJarName, className, classPackage, commonsCliJarName+  alloyJarName, className, classPackage, commonsCliJarName, slf4jJarName,   )-import Language.Alloy.Ressources        (alloyJar, classFile, commonsCliJar)+import Language.Alloy.Ressources (+  alloyJar,+  classFile,+  commonsCliJar,+  slf4jJar,+  )  {-| Configuration for calling alloy. These are:@@ -149,7 +154,8 @@   out <- getOutput pout   err <- getOutput perr   printContentOnError ph-  unless (null err) $ fail $ unpack $ BS.unlines err+  let err' = removeInfoPrefix err+  unless (null err') $ fail $ unpack $ BS.unlines err'   let instas = fmap (BS.intercalate "\n") $ drop 1 $ splitOn [begin] out   return $ filterLast (not . (partialInstance `BS.isSuffixOf`)) instas   where@@ -181,6 +187,25 @@       return output  {-|+Removes lines such as++@+[main] INFO kodkod.engine.config.Reporter - detecting symmetries ...+[main] INFO kodkod.engine.config.Reporter - detected 16 equivalence classes of atoms ...+[main] INFO kodkod.engine.config.Reporter - optimizing bounds and formula (breaking predicate symmetries, inlining, skolemizing) ...+[main] INFO kodkod.engine.config.Reporter - translating to boolean ...+[main] INFO kodkod.engine.config.Reporter - generating lex-leader symmetry breaking predicate ...+@++which seem to be appearing since Alloy-6.0.0+-}+removeInfoPrefix :: [ByteString] -> [ByteString]+removeInfoPrefix (x:xs)+  | Just _ <- BS.stripPrefix "[main] INFO" x+  = removeInfoPrefix xs+removeInfoPrefix xs = xs++{-| Start a new process that aborts execution by closing all handles and killing the processes after the given amount of time. -}@@ -212,51 +237,6 @@   mclassPath' <- readIORef mclassPath   maybe readClassPath return mclassPath' -{--{--data CallAlloyConfig = Config {-    alloyJarFile   :: FilePath,-    alloyClassFile :: FilePath,-    keepFiles      :: Bool-  }--}--jarFileEnv :: String-jarFileEnv = "ALLOY_JAR_FILE"--callAlloyEnv :: String-callAlloyEnv = "CALL_ALLOY_CLASS_FILE"--keepFilesEnv :: String-keepFilesEnv = "KEEP_ALLOY_FILES"--{-|-Lookup environment variables which are to prefer if present.--}-getEnvironmentInformation :: IO CallAlloyConfig-getEnvironmentInformation = do-  alloy     <- lookupEnv jarFileEnv-  callAlloy <- lookupEnv callAlloyEnv-  keep      <- lookupEnv keepFilesEnv-  let mconfig = Config <$> alloy <*> callAlloy <*> pure (isJust keep)-  case mconfig of-    Nothing -> do-      dataDir <- getXdgDirectory XdgData $ appName </> "dataDir"-    Just c  -> return c--}-{--getVersionFile :: IO FilePath-getVersionFile = do-  configDir <- getXdgDirectory XdgConfig appName-  let versionFile = configDir </> "version"-  exists <- doesFileExist versionFile-  if exists-    then do-    version <- read <$> readFile versionFile-    unless (version == versionHash) $ createVersionFile configDir versionFile-    else createVersionFile configDir versionFile--}- fallbackToTempDir :: IO FilePath -> IO FilePath fallbackToTempDir m = catch m $ \e ->   if isDoesNotExistError e@@ -291,6 +271,7 @@   dataDir <- getXdgDirectory XdgData $ appName </> "dataDir"   return $ dataDir ++ searchPathSeparator : dataDir </> alloyJarName     ++ searchPathSeparator : dataDir </> commonsCliJarName+    ++ searchPathSeparator : dataDir </> slf4jJarName  {-| Create all library files within the users 'XdgDirectory' by calling@@ -314,6 +295,7 @@   BS.writeFile (dataDir </> classPackage </> className <.> "class") classFile   BS.writeFile (dataDir </> alloyJarName) alloyJar   BS.writeFile (dataDir </> commonsCliJarName) commonsCliJar+  BS.writeFile (dataDir </> slf4jJarName) slf4jJar  {-| Creates user directories using the file permissions 700.@@ -343,8 +325,9 @@ versions of this library. -} versionHash :: Int-versionHash = hash $ alloyHash + commonsCliHash + classFileHash+versionHash = hash $ alloyHash + commonsCliHash + slf4jHash + classFileHash   where     alloyHash = hash alloyJar     commonsCliHash = hash commonsCliJar     classFileHash = hash classFile+    slf4jHash = hash slf4jJar

@@ -25,6 +25,9 @@ import Control.Monad.Except             (MonadError, throwError) import Data.ByteString                  (ByteString) import Data.Functor                     (($>))+import Data.List                        (intercalate)+import Data.List.Extra                  (unsnoc)+import Data.Maybe                       (fromJust) import Data.Set                         (Set) import Text.Trifecta @@ -69,13 +72,16 @@               <*> parseRelations <* (void newline <|> eof)))  sig :: Parser Signature-sig =-  try (Signature <$> (Just <$> word) <* char '/' <*> word)-  <|> Signature Nothing <$> word+sig = do+  xs' <- slashedWord+  return $ case fromJust $ unsnoc xs' of+    ([], x) -> Signature Nothing x+    (xs, x) -> Signature (Just $ intercalate "/" $ take (length xs') xs) x  parseRelations :: Parser (Relation Set) parseRelations = char '='   *> (try (string "{}" $> EmptyRelation)+      <|> (Id <$> try object)       <|> fmap Triple (try $ sep tripleRel)       <|> fmap Double (try $ sep doubleRel)       <|> fmap Single (sep singleRel))@@ -89,7 +95,7 @@  object :: Parser Object object =-  try (Object <$> word <* char '$' <*> (read <$> some digit))+  try (Object . intercalate "/" <$> slashedWord <* char '$' <*> (read <$> some digit))   <|> try (NumberObject <$> int)   <|> NamedObject <$> word @@ -97,6 +103,9 @@ int = fmap read $ (++)   <$> (try (string "-") <|> pure "")   <*> some digit++slashedWord :: Parser [String]+slashedWord = word `sepBy1` char '/'  word :: Parser String word = (:)

@@ -3,13 +3,17 @@   className,   classPackage,   commonsCliJarName,+  slf4jJarName,   ) where  alloyJarName :: String alloyJarName = "org.alloytools.alloy.dist.jar"  commonsCliJarName :: String-commonsCliJarName = "commons-cli-1.4.jar"+commonsCliJarName = "commons-cli-1.5.0.jar"++slf4jJarName :: String+slf4jJarName = "slf4j-simple-1.7.36.jar"  className :: String className = "RunAlloy"

@@ -3,6 +3,7 @@   alloyJar,   classFile,   commonsCliJar,+  slf4jJar,   ) where  import Data.ByteString                  (ByteString)@@ -10,7 +11,7 @@ import System.FilePath                  ((</>), (<.>))  import Language.Alloy.RessourceNames (-  alloyJarName, className, classPackage, commonsCliJarName+  alloyJarName, className, classPackage, commonsCliJarName, slf4jJarName,   )  alloyJar :: ByteString@@ -18,6 +19,9 @@  commonsCliJar :: ByteString commonsCliJar = $(embedFile $ "bin" </> "commons-cli" </> commonsCliJarName)++slf4jJar :: ByteString+slf4jJar = $(embedFile $ "bin" </> "slf4j" </> slf4jJarName)  classFile :: ByteString classFile = $(embedFile $ "bin" </> classPackage </> className <.> "class")

@@ -11,6 +11,7 @@ module Language.Alloy.Types (   AlloyInstance, AlloySig, Annotation (..),   Entries, Entry (..), Object (..), Relation (..), Signature (..),+  showSignature,   ) where  import Data.Map                         (Map)@@ -39,6 +40,10 @@     sigName  :: String   } deriving (Eq, Ord, Show) +showSignature :: Signature -> String+showSignature s =+  maybe "" (++ "/") (scope s) ++ sigName s+ {-| A concrete instance of an Alloy signature. -}@@ -60,6 +65,7 @@ -} data Relation a =     EmptyRelation+  | Id Object   | Single (a Object)   | Double (a (Object, Object))   | Triple (a (Object, Object, Object))

@@ -10,7 +10,6 @@ import Language.Alloy.Call              (existsInstance, getInstances) import Language.Alloy.Types             (Entry (..), Relation (..)) -import Language.Alloy.Call              (getInstancesWith, defaultCallAlloyConfig, CallAlloyConfig (..)) deriving instance Eq (Relation Set) deriving instance Eq (Entry Map Set) @@ -26,8 +25,6 @@       existsInstance "pred a (a: Int) { a > a }\nrun a" `shouldReturn` False   describe "getInstances" $ do     it "an empty spec returns a single trivial instance" $-      (show <$> getInstances (Just 2) "") `shouldReturn` "[fromList [(Signature {scope = Nothing, sigName = \"Int\"},Entry {annotation = Nothing, relation = fromList [(\"\",Single (fromList [NumberObject {number = -8},NumberObject {number = -7},NumberObject {number = -6},NumberObject {number = -5},NumberObject {number = -4},NumberObject {number = -3},NumberObject {number = -2},NumberObject {number = -1},NumberObject {number = 0},NumberObject {number = 1},NumberObject {number = 2},NumberObject {number = 3},NumberObject {number = 4},NumberObject {number = 5},NumberObject {number = 6},NumberObject {number = 7}]))]}),(Signature {scope = Nothing, sigName = \"String\"},Entry {annotation = Nothing, relation = fromList [(\"\",EmptyRelation)]}),(Signature {scope = Nothing, sigName = \"integers\"},Entry {annotation = Nothing, relation = fromList [(\"\",Single (fromList [NumberObject {number = -8},NumberObject {number = -7},NumberObject {number = -6},NumberObject {number = -5},NumberObject {number = -4},NumberObject {number = -3},NumberObject {number = -2},NumberObject {number = -1},NumberObject {number = 0},NumberObject {number = 1},NumberObject {number = 2},NumberObject {number = 3},NumberObject {number = 4},NumberObject {number = 5},NumberObject {number = 6},NumberObject {number = 7}]))]}),(Signature {scope = Nothing, sigName = \"none\"},Entry {annotation = Nothing, relation = fromList [(\"\",EmptyRelation)]}),(Signature {scope = Nothing, sigName = \"univ\"},Entry {annotation = Nothing, relation = fromList [(\"\",Single (fromList [NumberObject {number = -8},NumberObject {number = -7},NumberObject {number = -6},NumberObject {number = -5},NumberObject {number = -4},NumberObject {number = -3},NumberObject {number = -2},NumberObject {number = -1},NumberObject {number = 0},NumberObject {number = 1},NumberObject {number = 2},NumberObject {number = 3},NumberObject {number = 4},NumberObject {number = 5},NumberObject {number = 6},NumberObject {number = 7}]))]}),(Signature {scope = Just \"seq\", sigName = \"Int\"},Entry {annotation = Nothing, relation = fromList [(\"\",Single (fromList [NumberObject {number = 0},NumberObject {number = 1},NumberObject {number = 2},NumberObject {number = 3}]))]})]]"+      (show <$> getInstances (Just 2) "") `shouldReturn` "[fromList [(Signature {scope = Nothing, sigName = \"end\"},Entry {annotation = Nothing, relation = fromList [(\"\",Id (NumberObject {number = 0}))]}),(Signature {scope = Nothing, sigName = \"integers\"},Entry {annotation = Nothing, relation = fromList [(\"\",Single (fromList [NumberObject {number = -8},NumberObject {number = -7},NumberObject {number = -6},NumberObject {number = -5},NumberObject {number = -4},NumberObject {number = -3},NumberObject {number = -2},NumberObject {number = -1},NumberObject {number = 0},NumberObject {number = 1},NumberObject {number = 2},NumberObject {number = 3},NumberObject {number = 4},NumberObject {number = 5},NumberObject {number = 6},NumberObject {number = 7}]))]}),(Signature {scope = Nothing, sigName = \"loop\"},Entry {annotation = Nothing, relation = fromList [(\"\",Id (NumberObject {number = 0}))]})]]"     it "a conflicting spec returns no instance" $       getInstances (Just 1) "pred a (a: Int) { a > a }\nrun a" `shouldReturn` []-    it "a conflicting spec returns error" $-      getInstancesWith defaultCallAlloyConfig {maxInstances = Just 1, timeout = Just 1} "pred a (a: Int) { a > a }\nrun a" `shouldReturn` []