call-alloy 0.5.0.1 → 0.6

raw patch · 16 files changed

+135/−138 lines, 16 filesdep ~containersPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: containers

API changes (from Hackage documentation)

Files

• ChangeLog.md +4/−0
• README.md +2/−33
• call-alloy.cabal +18/−12
• data/alloy/RunAlloy.class binary
• data/alloy/SATSolver.class binary
• data/org.alloytools.alloy.dist.jar too large to diff
• data/slf4j/LICENSE +0/−21
• data/slf4j/slf4j-simple-1.7.36.jar binary
• src/Language/Alloy/Call.hs +15/−3
• src/Language/Alloy/Exceptions.hs +34/−0
• src/Language/Alloy/Functions.hs +2/−2
• src/Language/Alloy/Internal/Call.hs +37/−24
• src/Language/Alloy/Parser.hs +19/−6
• src/Language/Alloy/Types.hs +1/−1
• test/Language/Alloy/CallSpec.hs +3/−3
• test/unit/readmeExampleInstance.hs +0/−33

@@ -2,6 +2,10 @@  ## Unreleased changes +- upgrade to Alloy 6.2.0+- document Alloy version+- improve documentation+ ## Released changes  ### 0.5

@@ -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 {

@@ -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 <https://github.com/marcellussiegburg/call-alloy#readme> 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.*

binary file changed (4238 → 3874 bytes)

binary file changed (2046 → absent bytes)

file too large to diff

@@ -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.

binary file changed (15333 → absent bytes)

@@ -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)

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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 =

@@ -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

@@ -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,