diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -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' diff --git a/bin/commons-cli/commons-cli-1.4.jar b/bin/commons-cli/commons-cli-1.4.jar deleted file mode 100644 Binary files a/bin/commons-cli/commons-cli-1.4.jar and /dev/null differ diff --git a/bin/commons-cli/commons-cli-1.5.0.jar b/bin/commons-cli/commons-cli-1.5.0.jar new file mode 100644 Binary files /dev/null and b/bin/commons-cli/commons-cli-1.5.0.jar differ diff --git a/bin/org.alloytools.alloy.dist.jar b/bin/org.alloytools.alloy.dist.jar # file too large to diff: bin/org.alloytools.alloy.dist.jar diff --git a/bin/slf4j/LICENSE b/bin/slf4j/LICENSE new file mode 100644 --- /dev/null +++ b/bin/slf4j/LICENSE @@ -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. diff --git a/bin/slf4j/slf4j-simple-1.7.36.jar b/bin/slf4j/slf4j-simple-1.7.36.jar new file mode 100644 Binary files /dev/null and b/bin/slf4j/slf4j-simple-1.7.36.jar differ diff --git a/call-alloy.cabal b/call-alloy.cabal --- a/call-alloy.cabal +++ b/call-alloy.cabal @@ -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 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.* diff --git a/src/Language/Alloy/Debug.hs b/src/Language/Alloy/Debug.hs --- a/src/Language/Alloy/Debug.hs +++ b/src/Language/Alloy/Debug.hs @@ -9,6 +9,8 @@ module Language.Alloy.Debug ( getRawInstances, getRawInstancesWith, + parseInstance, ) where import Language.Alloy.Internal.Call (getRawInstances, getRawInstancesWith) +import Language.Alloy.Parser (parseInstance) diff --git a/src/Language/Alloy/Functions.hs b/src/Language/Alloy/Functions.hs --- a/src/Language/Alloy/Functions.hs +++ b/src/Language/Alloy/Functions.hs @@ -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)) diff --git a/src/Language/Alloy/Internal/Call.hs b/src/Language/Alloy/Internal/Call.hs --- a/src/Language/Alloy/Internal/Call.hs +++ b/src/Language/Alloy/Internal/Call.hs @@ -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 diff --git a/src/Language/Alloy/Parser.hs b/src/Language/Alloy/Parser.hs --- a/src/Language/Alloy/Parser.hs +++ b/src/Language/Alloy/Parser.hs @@ -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 = (:) diff --git a/src/Language/Alloy/RessourceNames.hs b/src/Language/Alloy/RessourceNames.hs --- a/src/Language/Alloy/RessourceNames.hs +++ b/src/Language/Alloy/RessourceNames.hs @@ -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" diff --git a/src/Language/Alloy/Ressources.hs b/src/Language/Alloy/Ressources.hs --- a/src/Language/Alloy/Ressources.hs +++ b/src/Language/Alloy/Ressources.hs @@ -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") diff --git a/src/Language/Alloy/Types.hs b/src/Language/Alloy/Types.hs --- a/src/Language/Alloy/Types.hs +++ b/src/Language/Alloy/Types.hs @@ -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)) diff --git a/test/Language/Alloy/CallSpec.hs b/test/Language/Alloy/CallSpec.hs --- a/test/Language/Alloy/CallSpec.hs +++ b/test/Language/Alloy/CallSpec.hs @@ -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` []