call-alloy 0.6.0.2 → 0.6.0.3

raw patch · 15 files changed

+211/−100 lines, 15 filesdep +pretty-showPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: pretty-show

API changes (from Hackage documentation)

Files

• ChangeLog.md +5/−1
• README.md +13/−8
• call-alloy.cabal +11/−8
• data/alloy/RunAlloy.class binary
• src/Language/Alloy/Exceptions.hs +2/−2
• src/Language/Alloy/Functions.hs +7/−4
• src/Language/Alloy/Internal/Call.hs +14/−19
• src/Language/Alloy/Parser.hs +9/−2
• src/Language/Alloy/ResourceNames.hs +22/−0
• src/Language/Alloy/Resources.hs +25/−0
• src/Language/Alloy/RessourceNames.hs +0/−22
• src/Language/Alloy/Ressources.hs +0/−25
• test/Language/Alloy/CallSpec.hs +9/−5
• test/ReadmeExample.hs +4/−4
• test/unit/emptySpecInstance.hs +90/−0

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

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

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

binary file changed (3874 → 3969 bytes)

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

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

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

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

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

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

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

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

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

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

@@ -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 }+                         ])+                  )+                ]+          }+      )+    ]+]