diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -4,6 +4,10 @@ ## Released changes +### 0.6.0.3 + +- fix native-access bug with recent Java versions + ### 0.6.0.2 - ignore finalizer warnings @@ -21,7 +25,7 @@ ### 0.5 - use MonadThrow instead of MonadError -- add Readme eample to test cases +- add readme example to test cases ### 0.4.1.1 diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -10,7 +10,8 @@ - Java Runtime Environment: There is currently no warning if you have not set up any Java Runtime Environment. - However, you will get runtime errors if it is not available when a call to Alloy happens. + However, you will get runtime errors if it is not available + when a call to Alloy happens. If you want to force a check, perform the test cases. ## Please note @@ -53,10 +54,14 @@ ``` -The graph is consisting of `Node`s, which might have some goods `stored` and may deliver them to other `Node`s (via `flow`). +The graph is consisting of `Node`s, which might have some goods `stored` +and may deliver them to other `Node`s (via `flow`). `Node`s do not have `flow` to themselves. -The `currentFlow` is the minimum between the flow from the starting `Node` to the end `Node` and the currently `stored` goods at the starting `Node` (note: intermediate `Node`s are not allowed). -We call two `Nodes` `x` and `y` `withFlow` if `currentFlow` from `x` to `y` is greater than `0`. +The `currentFlow` is the minimum between the flow +from the starting `Node` to the end `Node` and the currently `stored` goods +at the starting `Node` (note: intermediate `Node`s are not allowed). +We call two `Nodes` `x` and `y` `withFlow` if `currentFlow` from `x` to `y` +is greater than `0`. We restrict our search to `3`-Bit signed `Int` values and `2` `Nodes`. ### An instance example @@ -210,15 +215,15 @@ :: MonadThrow m => AlloyInstance -> m (Set Node, Set (Node, Int), Set (Node, Node, Int), Set Node, Set Node) -instanceToNames insta = do +instanceToNames model = do let node :: MonadThrow m => String -> Int -> m Node node = object "Node" Node - n <- lookupSig (scoped "this" "Node") insta + n <- lookupSig (scoped "this" "Node") model nodes <- getSingleAs "" node n store <- getDoubleAs "stored" node int n flow <- getTripleAs "flow" node node int n - x <- lookupSig (unscoped "$withFlow_x") insta >>= getSingleAs "" node - y <- lookupSig (unscoped "$withFlow_y") insta >>= getSingleAs "" node + x <- lookupSig (unscoped "$withFlow_x") model >>= getSingleAs "" node + y <- lookupSig (unscoped "$withFlow_y") model >>= getSingleAs "" node return (nodes, store, flow, x, y) ``` 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.37.0. +-- This file has been generated from package.yaml by hpack version 0.38.1. -- -- see: https://github.com/sol/hpack name: call-alloy -version: 0.6.0.2 +version: 0.6.0.3 synopsis: A simple library to call Alloy given a specification description: Please see the README on GitHub at category: Language @@ -19,9 +19,9 @@ build-type: Simple tested-with: GHC == 9.12.2 - , GHC == 9.10.1 + , GHC == 9.10.3 , GHC == 9.8.4 - , GHC == 9.6.6 + , GHC == 9.6.7 , GHC == 9.4.8 , GHC == 9.2.8 , GHC == 9.0.2 @@ -30,6 +30,7 @@ README.md LICENSE ChangeLog.md + test/unit/emptySpecInstance.hs test/unit/readmeExampleInstance.hs test/unit/readmeExampleResult.hs test/unit/readmeExampleSpecification.als @@ -47,6 +48,7 @@ flag test-different-solvers description: During tests different solvers are called to test if they are working on the current system + manual: True default: False @@ -59,8 +61,8 @@ Language.Alloy.Functions Language.Alloy.Internal.Call Language.Alloy.Parser - Language.Alloy.RessourceNames - Language.Alloy.Ressources + Language.Alloy.ResourceNames + Language.Alloy.Resources Language.Alloy.Types Paths_call_alloy hs-source-dirs: @@ -98,8 +100,8 @@ Language.Alloy.Functions Language.Alloy.Internal.Call Language.Alloy.Parser - Language.Alloy.RessourceNames - Language.Alloy.Ressources + Language.Alloy.ResourceNames + Language.Alloy.Resources Language.Alloy.Types Language.Alloy.CallSpec ReadmeExample @@ -121,6 +123,7 @@ , file-embed , filepath >=1.4 && <1.6 , hspec + , pretty-show , process ==1.6.* , split ==0.2.* , string-interpolate 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/src/Language/Alloy/Exceptions.hs b/src/Language/Alloy/Exceptions.hs --- a/src/Language/Alloy/Exceptions.hs +++ b/src/Language/Alloy/Exceptions.hs @@ -107,11 +107,11 @@ | LookupAlloyRelationFailed !RelationName !(Alternatives RelationName) instance Show AlloyLookupFailed where - show (LookupAlloySignatureFailed s insta) = "LookupAlloySignatureFailed: " + show (LookupAlloySignatureFailed s model) = "LookupAlloySignatureFailed: " <> showSignature s <> " is missing in the Alloy instance" <> "; available are: \"" - <> intercalate "\", " (showSignature <$> M.keys insta) + <> intercalate "\", " (showSignature <$> M.keys model) show (LookupAlloyRelationFailed rel xs) = "LookupAlloyRelationFailed: " <> "relation " ++ unRelationName rel <> " is missing in the Alloy instance" 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 @@ -83,7 +83,8 @@ For retrieval of an unmixed type of values using a get... function (should be the case for uniformly base named values; this is usually never true for the universe (@lookupSig (unscoped "univ")@)) -I.e. setting and checking the 'String' for the base name of the value to look for, +I.e. setting and checking the 'String' for the base name +of the value to look for, but failing in case anything different appears (unexpectedly). -} object @@ -107,7 +108,9 @@ Object n i -> f n i NamedObject g -> error $ "there is no way of converting Object " ++ g - ++ "\nPlease open an issue at https://github.com/marcellussiegburg/call-alloy stating what you tried to attempt" + ++ "\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'. @@ -209,8 +212,8 @@ => Signature -> AlloyInstance -> m AlloySig -lookupSig s insta = case M.lookup s insta of - Nothing -> throwM $ LookupAlloySignatureFailed s insta +lookupSig s model = case M.lookup s model of + Nothing -> throwM $ LookupAlloySignatureFailed s model Just e -> return e identity 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 @@ -78,11 +78,11 @@ createProcess, proc, terminateProcess, waitForProcess, ) -import Language.Alloy.RessourceNames ( +import Language.Alloy.ResourceNames ( className, classPackage, ) -import Language.Alloy.Ressources ( +import Language.Alloy.Resources ( alloyJar, commonsCliJar, slf4jJar, @@ -134,7 +134,7 @@ -- -- * incremental | SAT4JPMax - -- ^ SAT4Ji PMax + -- ^ SAT4J with Partial Maximum Satisfiability -- -- * incremental | Spear @@ -226,8 +226,11 @@ callAlloyWith config = do classPath <- getClassPath let callAlloy = proc "java" - $ ["-cp", classPath, classPackage ++ '.' : className, - "-i", show $ fromMaybe (-1) $ maxInstances config] + $ [ + "--enable-native-access=ALL-UNNAMED", + "-cp", classPath, classPackage ++ '.' : className, + "-i", show $ fromMaybe (-1) $ maxInstances config + ] ++ ["-o" | not $ noOverflow config] ++ ["-s", toParameter (satSolver config)] createProcess callAlloy { @@ -302,26 +305,18 @@ partialInstance = "---PARTIAL_INSTANCE---" {-| -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 ... -@ - -and +Removes lines starting with any of @ -[main] WARN kodkod.engine.config.Reporter - Temporal formula: will be reduced to possibly unsound static version. +[main] INFO +[main] WARN +[Finalizer] WARN @ -and +and partial instances @ -PARTIAL_INSTANCE +---PARTIAL_INSTANCE--- @ which seem to be appearing since Alloy-6.0.0 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 @@ -66,7 +66,9 @@ where createOrInsert (s, e) = M.alter (Just . alterSig e) s alterSig e Nothing = e { relation = uncurry M.singleton $ relation e} - alterSig e (Just y) = y { relation = uncurry M.insert (relation e) (relation y) } + alterSig e (Just y) = y { + relation = uncurry M.insert (relation e) (relation y) + } crlf :: Parser Char crlf = char '\r' *> char '\n' @@ -135,7 +137,12 @@ object :: Parser Object object = - try (Object . intercalate "/" <$> slashedWord <* char '$' <*> (read <$> some digit)) + try ( + Object . intercalate "/" + <$> slashedWord + <* char '$' + <*> (read <$> some digit) + ) <|> try (NumberObject <$> int) <|> NamedObject <$> word diff --git a/src/Language/Alloy/ResourceNames.hs b/src/Language/Alloy/ResourceNames.hs new file mode 100644 --- /dev/null +++ b/src/Language/Alloy/ResourceNames.hs @@ -0,0 +1,22 @@ +module Language.Alloy.ResourceNames ( + alloyJarName, + className, + classPackage, + commonsCliJarName, + slf4jJarName, + ) where + +alloyJarName :: String +alloyJarName = "org.alloytools.alloy.dist.jar" + +commonsCliJarName :: String +commonsCliJarName = "commons-cli-1.5.0.jar" + +slf4jJarName :: String +slf4jJarName = "slf4j-simple-1.7.36.jar" + +className :: String +className = "RunAlloy" + +classPackage :: String +classPackage = "alloy" diff --git a/src/Language/Alloy/Resources.hs b/src/Language/Alloy/Resources.hs new file mode 100644 --- /dev/null +++ b/src/Language/Alloy/Resources.hs @@ -0,0 +1,25 @@ +module Language.Alloy.Resources ( + alloyJar, + commonsCliJar, + slf4jJar, + ) where + +import Data.Functor ((<&>)) +import System.FilePath (()) + +import Language.Alloy.ResourceNames ( + alloyJarName, commonsCliJarName, slf4jJarName, + ) +import Paths_call_alloy (getDataDir) + +prependDataDir :: FilePath -> IO FilePath +prependDataDir xs = getDataDir <&> ( xs) + +alloyJar :: IO FilePath +alloyJar = prependDataDir alloyJarName + +commonsCliJar :: IO FilePath +commonsCliJar = prependDataDir ("commons-cli" commonsCliJarName) + +slf4jJar :: IO FilePath +slf4jJar = prependDataDir ("slf4j" slf4jJarName) diff --git a/src/Language/Alloy/RessourceNames.hs b/src/Language/Alloy/RessourceNames.hs deleted file mode 100644 --- a/src/Language/Alloy/RessourceNames.hs +++ /dev/null @@ -1,22 +0,0 @@ -module Language.Alloy.RessourceNames ( - alloyJarName, - className, - classPackage, - commonsCliJarName, - slf4jJarName, - ) where - -alloyJarName :: String -alloyJarName = "org.alloytools.alloy.dist.jar" - -commonsCliJarName :: String -commonsCliJarName = "commons-cli-1.5.0.jar" - -slf4jJarName :: String -slf4jJarName = "slf4j-simple-1.7.36.jar" - -className :: String -className = "RunAlloy" - -classPackage :: String -classPackage = "alloy" diff --git a/src/Language/Alloy/Ressources.hs b/src/Language/Alloy/Ressources.hs deleted file mode 100644 --- a/src/Language/Alloy/Ressources.hs +++ /dev/null @@ -1,25 +0,0 @@ -module Language.Alloy.Ressources ( - alloyJar, - commonsCliJar, - slf4jJar, - ) where - -import Data.Functor ((<&>)) -import System.FilePath (()) - -import Language.Alloy.RessourceNames ( - alloyJarName, commonsCliJarName, slf4jJarName, - ) -import Paths_call_alloy (getDataDir) - -prependDataDir :: FilePath -> IO FilePath -prependDataDir xs = getDataDir <&> ( xs) - -alloyJar :: IO FilePath -alloyJar = prependDataDir alloyJarName - -commonsCliJar :: IO FilePath -commonsCliJar = prependDataDir ("commons-cli" commonsCliJarName) - -slf4jJar :: IO FilePath -slf4jJar = prependDataDir ("slf4j" slf4jJarName) 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 @@ -14,6 +14,7 @@ import Data.Set (Set) import Data.String.Interpolate (i) import Test.Hspec +import Text.Show.Pretty (ppShow) import Language.Alloy.Call ( CallAlloyConfig (..), @@ -39,14 +40,15 @@ it "an empty spec has an instance" $ existsInstance "" `shouldReturn` True it "a conflicting spec has no instance" $ - existsInstance "pred a (a: Int) { a > a }\nrun a" `shouldReturn` False + existsInstance (runPredicate "a > 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 = \"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 "an empty spec returns a single trivial instance" $ do + expected <- readFile "test/unit/emptySpecInstance.hs" + (ppShow <$> getInstances (Just 2) "") `shouldReturn` init expected it "a conflicting spec returns no instance" $ - getInstances (Just 1) "pred a (a: Int) { a > a }\nrun a" `shouldReturn` [] + getInstances (Just 1) (runPredicate "a > a") `shouldReturn` [] it "giving not enough time should return no result" $ - getInstancesWith cfg "pred a (a: Int) { a >= a }\nrun a" `shouldReturn` [] + getInstancesWith cfg (runPredicate "a >= a") `shouldReturn` [] #if TEST_DIFFERENT_SOLVERS let unsupported = [BerkMin, Glucose41, PLingeling, Spear] solvers = [minBound ..] \\ unsupported @@ -71,6 +73,8 @@ length <$> getInstancesWith cfg (graph x) xs `shouldBe` replicate (fromInteger n) 0 where + runPredicate property = + "pred a (a: Int) { " ++ property ++ " }\n" ++ "run a" cfg = defaultCallAlloyConfig { maxInstances = Nothing, timeout = Just 0 diff --git a/test/ReadmeExample.hs b/test/ReadmeExample.hs --- a/test/ReadmeExample.hs +++ b/test/ReadmeExample.hs @@ -23,13 +23,13 @@ :: MonadThrow m => AlloyInstance -> m (Set Node, Set (Node, Int), Set (Node, Node, Int), Set Node, Set Node) -instanceToNames insta = do +instanceToNames model = do let node :: MonadThrow m => String -> Int -> m Node node = object "Node" Node - n <- lookupSig (scoped "this" "Node") insta + n <- lookupSig (scoped "this" "Node") model nodes <- getSingleAs "" node n store <- getDoubleAs "stored" node int n flow <- getTripleAs "flow" node node int n - x <- lookupSig (unscoped "$withFlow_x") insta >>= getSingleAs "" node - y <- lookupSig (unscoped "$withFlow_y") insta >>= getSingleAs "" node + x <- lookupSig (unscoped "$withFlow_x") model >>= getSingleAs "" node + y <- lookupSig (unscoped "$withFlow_y") model >>= getSingleAs "" node return (nodes, store, flow, x, y) diff --git a/test/unit/emptySpecInstance.hs b/test/unit/emptySpecInstance.hs new file mode 100644 --- /dev/null +++ b/test/unit/emptySpecInstance.hs @@ -0,0 +1,90 @@ +[ 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 } + ]) + ) + ] + } + ) + ] +]