diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -2,6 +2,10 @@ ## Unreleased changes +- upgrade to Alloy 6.2.0 +- document Alloy version +- improve documentation + ## Released changes ### 0.5 diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -4,6 +4,8 @@ This package installs a simple Java Library to make an API call to the Alloy Library. Alloy is installed (as JAR file) alongside this library as well. +The currently used Alloy version is 6.2.0. + ## Requirements - Java Runtime Environment: @@ -107,39 +109,6 @@ Entry { annotation = Nothing, relation = fromList [("", EmptyRelation)] - }), - ( 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 = -4}, - NumberObject {number = -3}, - NumberObject {number = -2}, - NumberObject {number = -1}, - NumberObject {number = 0}, - NumberObject {number = 1}, - NumberObject {number = 2}, - NumberObject {number = 3} - ])) - ] - }), - ( Signature {scope = Nothing, sigName = "loop"}, - Entry { - annotation = Nothing, - relation = fromList [ - ( "", - Id (NumberObject {number = 0})) - ] }), ( Signature {scope = Nothing, sigName = "none"}, Entry { diff --git a/call-alloy.cabal b/call-alloy.cabal --- a/call-alloy.cabal +++ b/call-alloy.cabal @@ -1,11 +1,11 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.36.0. +-- This file has been generated from package.yaml by hpack version 0.37.0. -- -- see: https://github.com/sol/hpack name: call-alloy -version: 0.5.0.1 +version: 0.6 synopsis: A simple library to call Alloy given a specification description: Please see the README on GitHub at category: Language @@ -13,10 +13,19 @@ bug-reports: https://github.com/marcellussiegburg/call-alloy/issues author: Marcellus Siegburg maintainer: marcellus.siegburg@uni-due.de -copyright: 2019-2024 Marcellus Siegburg +copyright: 2019-2025 Marcellus Siegburg license: MIT license-file: LICENSE build-type: Simple +tested-with: + GHC == 9.12.2 + , GHC == 9.10.1 + , GHC == 9.8.4 + , GHC == 9.6.6 + , GHC == 9.4.8 + , GHC == 9.2.8 + , GHC == 9.0.2 + , GHC == 8.10.7 extra-source-files: README.md LICENSE @@ -26,13 +35,10 @@ test/unit/readmeExampleSpecification.als data-files: alloy/RunAlloy.class - alloy/SATSolver.class org.alloytools.alloy.dist.jar commons-cli/commons-cli-1.5.0.jar commons-cli/NOTICE.txt commons-cli/LICENSE.txt - slf4j/slf4j-simple-1.7.36.jar - slf4j/LICENSE data-dir: data source-repository head @@ -64,11 +70,11 @@ async >=2.2.1 && <2.3 , base >=4.12 && <5 , bytestring >=0.10.4 && <0.13 - , containers >=0.6 && <0.8 + , containers >=0.6 && <0.9 , directory ==1.3.* , exceptions >=0.8.1 && <0.11 - , extra ==1.7.* - , filepath ==1.4.* + , extra >=1.7 && <1.9 + , filepath >=1.4 && <1.6 , process ==1.6.* , split ==0.2.* , transformers >=0.5.0.0 && <0.7 @@ -108,12 +114,12 @@ , base >=4.12 && <5 , bytestring >=0.10.4 && <0.13 , call-alloy - , containers >=0.6 && <0.8 + , containers >=0.6 && <0.9 , directory ==1.3.* , exceptions >=0.8.1 && <0.11 - , extra ==1.7.* + , extra >=1.7 && <1.9 , file-embed - , filepath ==1.4.* + , filepath >=1.4 && <1.6 , hspec , process ==1.6.* , split ==0.2.* diff --git a/data/alloy/RunAlloy.class b/data/alloy/RunAlloy.class Binary files a/data/alloy/RunAlloy.class and b/data/alloy/RunAlloy.class differ diff --git a/data/alloy/SATSolver.class b/data/alloy/SATSolver.class deleted file mode 100644 Binary files a/data/alloy/SATSolver.class and /dev/null differ diff --git a/data/org.alloytools.alloy.dist.jar b/data/org.alloytools.alloy.dist.jar # file too large to diff: data/org.alloytools.alloy.dist.jar diff --git a/data/slf4j/LICENSE b/data/slf4j/LICENSE deleted file mode 100644 --- a/data/slf4j/LICENSE +++ /dev/null @@ -1,21 +0,0 @@ - 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/data/slf4j/slf4j-simple-1.7.36.jar b/data/slf4j/slf4j-simple-1.7.36.jar deleted file mode 100644 Binary files a/data/slf4j/slf4j-simple-1.7.36.jar and /dev/null differ diff --git a/src/Language/Alloy/Call.hs b/src/Language/Alloy/Call.hs --- a/src/Language/Alloy/Call.hs +++ b/src/Language/Alloy/Call.hs @@ -1,7 +1,7 @@ {-| Module : Language.Alloy.Call Description : A simple library to call Alloy given a specification -Copyright : (c) Marcellus Siegburg, 2019 - 2021 +Copyright : (c) Marcellus Siegburg, 2019 - 2025 License : MIT Maintainer : marcellus.siegburg@uni-due.de @@ -12,7 +12,8 @@ (as it is required by Alloy). -} module Language.Alloy.Call ( - CallAlloyConfig (maxInstances, noOverflow, satSolver, timeout), + alloyVersion, + CallAlloyConfig (..), SatSolver (..), defaultCallAlloyConfig, existsInstance, @@ -32,6 +33,17 @@ import Control.Monad.IO.Class (MonadIO (liftIO)) {-| +The currently used Alloy version. + +>>> alloyVersion +"6.2.0" + +@since 0.6 +-} +alloyVersion :: String +alloyVersion = "6.2.0" + +{-| This function may be used to get all model instances for a given Alloy specification. It calls Alloy via a Java interface and parses the raw instance answers before returning the resulting list of 'AlloyInstance's. @@ -51,7 +63,7 @@ This function may be used to get all model instances for a given Alloy specification. It calls Alloy via a Java interface and parses the raw instance answers before returning the resulting list of 'AlloyInstance's. -Parameters are set using a 'CallAlloyConfig'. +Parameters are set using a t'CallAlloyConfig'. -} getInstancesWith :: (MonadIO m, MonadThrow m) diff --git a/src/Language/Alloy/Exceptions.hs b/src/Language/Alloy/Exceptions.hs --- a/src/Language/Alloy/Exceptions.hs +++ b/src/Language/Alloy/Exceptions.hs @@ -28,6 +28,9 @@ ) import Text.Trifecta.Result (ErrInfo) +{-| +Any exception that might be raised by @call-alloy@. +-} data CallAlloyException where CallAlloyException :: Exception e => e -> CallAlloyException @@ -44,6 +47,14 @@ CallAlloyException a <- fromException x cast a +{-| +An unexpected Alloy response. + +This would usually happen when @call-alloy@ does not know how to interpret a +response that was received from Alloy. +In this case an issue should be opened, describing in detail what was tried +and the received error response. +-} newtype AlloyResponseFailure = ParsingAlloyResponseFailed ErrInfo deriving Show @@ -52,9 +63,19 @@ toException = alloyExceptionToException fromException = alloyExceptionFromException +{-| +Containing an expectation. +-} newtype Expected = Expected {unExpected :: String} + +{-| +Containing what we actually got. +-} newtype Got = Got {unGot :: String} +{-| +An object name does not match an expectation. +-} data AlloyObjectNameMismatch = AlloyObjectNameMismatch !Expected !Got @@ -68,9 +89,19 @@ toException = alloyExceptionToException fromException = alloyExceptionFromException +{-| +How to refer to a specific relation. +-} newtype RelationName = RelationName {unRelationName :: String} + +{-| +Possible alternatives. +-} newtype Alternatives a = Alternatives {unAlternatives :: [a]} +{-| +A lookup within an 'AlloyInstance' failed. +-} data AlloyLookupFailed = LookupAlloySignatureFailed !Signature !AlloyInstance | LookupAlloyRelationFailed !RelationName !(Alternatives RelationName) @@ -91,6 +122,9 @@ toException = alloyExceptionToException fromException = alloyExceptionFromException +{-| +A relation type does not match. +-} data UnexpectedAlloyRelation = ExpectedIdenticalRelationship | ExpectedSingleRelationship 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 @@ -42,13 +42,13 @@ ) {-| -Create a 'Signature' given its scope and name. +Create a t'Signature' given its scope and name. -} scoped :: String -> String -> Signature scoped = Signature . Just {-| -Create an unscoped 'Signature' given its name. +Create an unscoped t'Signature' given its name. -} unscoped :: String -> Signature unscoped = Signature Nothing 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 @@ -4,7 +4,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-| Module : Language.Alloy.Internal.Call -Copyright : (c) Marcellus Siegburg, 2019 - 2021 +Copyright : (c) Marcellus Siegburg, 2019 - 2025 License : MIT This module provides the basic internal functionality to retrieve the raw @@ -12,7 +12,7 @@ It provides data types and functions to interact with Alloy. -} module Language.Alloy.Internal.Call ( - CallAlloyConfig (maxInstances, noOverflow, satSolver, timeout), + CallAlloyConfig (..), SatSolver (..), defaultCallAlloyConfig, getRawInstances, @@ -91,12 +91,16 @@ {-| Available SAT solvers. + +Note: solvers marked as not supported by default were supported +in earlier versions of Alloy, but got removed. +There might be a way of integrating those manually, but this has net been tried. -} data SatSolver = BerkMin -- ^ BerkMin -- - -- * not tested + -- * not supported by default | Glucose -- ^ Glucose -- @@ -104,7 +108,7 @@ | Glucose41 -- ^ Glucose41 -- - -- * incremental + -- * not supported by default | Lingeling -- ^ Lingeling -- @@ -120,38 +124,47 @@ | PLingeling -- ^ PLingeling -- - -- * not incremental + -- * not supported by default | SAT4J -- ^ SAT4J -- -- * incremental + | SAT4JLight + -- ^ SAT4J Light + -- + -- * incremental + | SAT4JPMax + -- ^ SAT4Ji PMax + -- + -- * incremental | Spear -- ^ Spear -- - -- * not tested + -- * not supported by default deriving (Bounded, Enum, Eq, Read, Show) toParameter :: SatSolver -> String toParameter = \case - BerkMin -> "BERKMIN" - Glucose -> "GLUCOSE" - Glucose41 -> "GLUCOSE41" - Lingeling -> "LINGELING" - MiniSat -> "MINISAT" - MiniSatProver -> "MINISAT_PROVER" - PLingeling -> "PLINGELING" - SAT4J -> "SAT4J" - Spear -> "SPEAR" + BerkMin -> "berkmin" + Glucose -> "glucose" + Glucose41 -> "glucose41" + Lingeling -> "lingeling.parallel" + MiniSat -> "minisat" + MiniSatProver -> "minisat.prover" + PLingeling -> "plingeling" + SAT4J -> "sat4j" + SAT4JLight -> "sat4j.light" + SAT4JPMax -> "sat4j.pmax" + Spear -> "spear" {-| -Configuration for calling alloy. These are: - - * maximal number of instances to retrieve ('Nothing' for all) - * whether to not overflow when calculating numbers within Alloy - * an timeout after which to forcibly kill Alloy - (retrieving only instances that were returned before killing the process) +Configuration for calling alloy. -} -data CallAlloyConfig = CallAlloyConfig { +data CallAlloyConfig = + -- | you should use 'defaultCallAlloyConfig' instead of this constructor + -- as additional configuration parameters might be introduced in later + -- releases. + CallAlloyConfig { -- | maximal number of instances to retrieve ('Nothing' for all) maxInstances :: !(Maybe Integer), -- | whether to not overflow when calculating numbers within Alloy @@ -227,7 +240,7 @@ This function may be used to get all raw model instances for a given Alloy specification. It calls Alloy via a Java interface and splits the raw instance answers before returning the resulting list of raw instances. -Parameters are set using a 'CallAlloyConfig'. +Parameters are set using a t'CallAlloyConfig'. -} getRawInstancesWith :: CallAlloyConfig @@ -265,7 +278,7 @@ $ drop 1 $ splitOn [begin] out where begin :: ByteString - begin = "---INSTANCE---" + begin = "---Trace---" filterLast _ [] = [] filterLast p x@[_] = filter p x filterLast p (x:xs) = x:filterLast p xs 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 @@ -70,16 +70,29 @@ crlf :: Parser Char crlf = char '\r' *> char '\n' +eof' :: Parser () +eof' = optional (char '\r') *> eof + endOfLine :: Parser Char endOfLine = newline <|> crlf alloyInstance :: Parser [Entries (,)] -alloyInstance = (++) - <$> entrySection "---INSTANCE---" - <*> entrySection "------State 0-------" +alloyInstance = + entrySection "------State 0 (loop)-------" where - entrySection x = (try (void $ string x *> endOfLine) <|> return ()) - *> many entry + entrySection x = + string x + *> endOfLine + *> many (try entry) + <* many alloyInfo + <* eof' + alloyInfo = + string "c last restart ## conflicts : " + *> many digit + *> space + *> many digit + *> space + *> (void (try endOfLine) <|> eof') entry :: Parser (Entries (,)) entry = do @@ -87,7 +100,7 @@ entrySignature <- sig (entrySignature,) . Entry entryAnnotation <$> ((,) <$> ((string "<:" *> word) <|> pure "") - <*> parseRelations <* (void endOfLine <|> eof)) + <*> parseRelations <* (void (try endOfLine) <|> eof')) sig :: Parser Signature sig = do 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 @@ -60,7 +60,7 @@ } deriving (Eq, Ord, Show) {-| -An Alloy relation, i.e. a collection of a tuple of 'Object's. +An Alloy relation, i.e. a collection of a tuple of t'Object's. The collection may be a singleton, a set, a list, ... -} data Relation a = 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 @@ -42,14 +42,14 @@ 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 = \"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}))]}),(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 = \"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 = \"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}]))]})]]" it "a conflicting spec returns no instance" $ getInstances (Just 1) "pred a (a: Int) { a > a }\nrun a" `shouldReturn` [] it "giving not enough time should return no result" $ getInstancesWith cfg "pred a (a: Int) { a >= a }\nrun a" `shouldReturn` [] #if TEST_DIFFERENT_SOLVERS - let untested = [BerkMin, Spear] - solvers = [minBound ..] \\ untested + let unsupported = [BerkMin, Glucose41, PLingeling, Spear] + solvers = [minBound ..] \\ unsupported for_ solvers $ \solver -> it ("using solver " ++ show solver ++ " generates an instance") $ do xs <- length <$> getInstancesWith diff --git a/test/unit/readmeExampleInstance.hs b/test/unit/readmeExampleInstance.hs --- a/test/unit/readmeExampleInstance.hs +++ b/test/unit/readmeExampleInstance.hs @@ -41,39 +41,6 @@ annotation = Nothing, relation = fromList [("", EmptyRelation)] }), - ( 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 = -4}, - NumberObject {number = -3}, - NumberObject {number = -2}, - NumberObject {number = -1}, - NumberObject {number = 0}, - NumberObject {number = 1}, - NumberObject {number = 2}, - NumberObject {number = 3} - ])) - ] - }), - ( Signature {scope = Nothing, sigName = "loop"}, - Entry { - annotation = Nothing, - relation = fromList [ - ( "", - Id (NumberObject {number = 0})) - ] - }), ( Signature {scope = Nothing, sigName = "none"}, Entry { annotation = Nothing,