call-alloy 0.4.0.3 → 0.4.1

raw patch · 7 files changed

+105/−16 lines, 7 filesdep ~Win32binary-addedPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: Win32

API changes (from Hackage documentation)

Files

• ChangeLog.md +4/−0
• call-alloy.cabal +9/−8
• data/alloy/RunAlloy.class binary
• data/alloy/SATSolver.class binary
• src/Language/Alloy/Call.hs +2/−1
• src/Language/Alloy/Internal/Call.hs +75/−7
• test/Language/Alloy/CallSpec.hs +15/−0

@@ -4,6 +4,10 @@  ## Released changes +### 0.4.1++- add support for different SAT solvers+ ### 0.4.0.3  - fix terminal spamming due to process abortion on Windows

@@ -1,11 +1,11 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.35.0.+-- This file has been generated from package.yaml by hpack version 0.36.0. -- -- see: https://github.com/sol/hpack  name:           call-alloy-version:        0.4.0.3+version:        0.4.1 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@@ -23,6 +23,7 @@     ChangeLog.md 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@@ -53,8 +54,8 @@   build-depends:       async >=2.2.1 && <2.3     , base >=4.12 && <5-    , bytestring >=0.10.4 && <0.12-    , containers ==0.6.*+    , bytestring >=0.10.4 && <0.13+    , containers >=0.6 && <0.8     , directory ==1.3.*     , extra ==1.7.*     , filepath ==1.4.*@@ -67,7 +68,7 @@   if os(windows)     cpp-options: -DWINDOWS     build-depends:-        Win32 >=2.5 && <2.14+        Win32 >=2.5 && <2.15   else     build-depends:         unix >=2.7 && <2.9@@ -93,9 +94,9 @@   build-depends:       async >=2.2.1 && <2.3     , base >=4.12 && <5-    , bytestring >=0.10.4 && <0.12+    , bytestring >=0.10.4 && <0.13     , call-alloy-    , containers ==0.6.*+    , containers >=0.6 && <0.8     , directory ==1.3.*     , extra ==1.7.*     , filepath ==1.4.*@@ -110,7 +111,7 @@   if os(windows)     cpp-options: -DWINDOWS     build-depends:-        Win32 >=2.5 && <2.14+        Win32 >=2.5 && <2.15   else     build-depends:         unix >=2.7 && <2.9

binary file changed (3575 → 4238 bytes)

binary file changed (absent → 2046 bytes)

@@ -12,7 +12,8 @@ (as it is required by Alloy). -} module Language.Alloy.Call (-  CallAlloyConfig (maxInstances, noOverflow, timeout),+  CallAlloyConfig (maxInstances, noOverflow, satSolver, timeout),+  SatSolver (..),   defaultCallAlloyConfig,   existsInstance,   getInstances,

@@ -1,4 +1,5 @@ {-# LANGUAGE CPP #-}+{-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} {-|@@ -11,18 +12,22 @@ It provides data types and functions to interact with Alloy. -} module Language.Alloy.Internal.Call (-  CallAlloyConfig (maxInstances, noOverflow, timeout),+  CallAlloyConfig (maxInstances, noOverflow, satSolver, timeout),+  SatSolver (..),   defaultCallAlloyConfig,   getRawInstances,   getRawInstancesWith,   ) where  import qualified Data.ByteString                  as BS (-  hGetLine,   intercalate,   stripPrefix,   )-import qualified Data.ByteString.Char8            as BS (unlines)+import qualified Data.ByteString.Char8            as BS (+  hGetLine,+  putStrLn,+  unlines,+  )  import Control.Concurrent (   threadDelay,@@ -74,7 +79,8 @@   )  import Language.Alloy.RessourceNames (-  className, classPackage,+  className,+  classPackage,   ) import Language.Alloy.Ressources (   alloyJar,@@ -84,6 +90,60 @@ import Paths_call_alloy                 (getDataDir)  {-|+Available SAT solvers.+-}+data SatSolver+  = BerkMin+  -- ^ BerkMin+  --+  -- * not tested+  | Glucose+  -- ^ Glucose+  --+  -- * incremental+  | Glucose41+  -- ^ Glucose41+  --+  -- * incremental+  | Lingeling+  -- ^ Lingeling+  --+  -- * not incremental+  | MiniSat+  -- ^ MiniSat+  --+  -- * incremental+  | MiniSatProver+  -- ^ MiniSatProver+  --+  -- * incremental+  | PLingeling+  -- ^ PLingeling+  --+  -- * not incremental+  | SAT4J+  -- ^ SAT4J+  --+  -- * incremental+  | Spear+  -- ^ Spear+  --+  -- * not tested+  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"++{-| Configuration for calling alloy. These are:   * maximal number of instances to retrieve ('Nothing' for all)@@ -96,6 +156,9 @@   maxInstances :: !(Maybe Integer),   -- | whether to not overflow when calculating numbers within Alloy   noOverflow   :: !Bool,+  -- | the 'SatSolver' to choose. Note that some are not incremental,+  --   i.e. will return only one solution, even if 'maxInstances' is set higher.+  satSolver    :: !SatSolver,   -- | the time in microseconds after which to forcibly kill Alloy   --   ('Nothing' for never)   timeout      :: !(Maybe Int)@@ -106,11 +169,13 @@   * retrieve all instances  * do not overflow+ * 'SAT4J' -} defaultCallAlloyConfig :: CallAlloyConfig defaultCallAlloyConfig = CallAlloyConfig {   maxInstances = Nothing,   noOverflow   = True,+  satSolver    = SAT4J,   timeout      = Nothing   } @@ -151,6 +216,7 @@         $ ["-cp", classPath, classPackage ++ '.' : className,            "-i", show $ fromMaybe (-1) $ maxInstances config]         ++ ["-o" | not $ noOverflow config]+        ++ ["-s", toParameter (satSolver config)]   createProcess callAlloy {     std_out = CreatePipe,     std_in  = CreatePipe,@@ -191,7 +257,7 @@     (out, err) <- fst <$> concurrently       (concurrently (getOutput hout) (getOutput herr))       evaluateAlloy-    printContentOnError abort ph+    printContentOnError out abort ph     let err' = removeInfoLines err     unless (null err') $ fail $ unpack $ BS.unlines err'     return $ fmap (BS.intercalate "\n")@@ -211,11 +277,13 @@     getOutput h = catch       (getOutput' h)       (\(_ :: IOException) -> return [partialInstance])-    printContentOnError abort ph = do+    printContentOnError out abort ph = do       code <- waitForProcess ph       aborted <- maybe (return False) readIORef abort       when (code == ExitFailure 1 && not aborted)-        $ putOutLn $ "Failed parsing the Alloy code:\n" <> content+        $ putOutLn $ "Failed parsing the Alloy code?:\n" <> content+      when (code == ExitFailure 2 && not aborted)+        $ withLock outLock $ BS.putStrLn $ BS.unlines out  partialInstance :: ByteString partialInstance = "---PARTIAL_INSTANCE---"

@@ -5,6 +5,8 @@ module Language.Alloy.CallSpec (spec) where  import Control.Concurrent.Async         (forConcurrently)+import Data.Foldable                    (for_)+import Data.List                        ((\\)) import Data.Map                         (Map) import Data.Set                         (Set) import Data.String.Interpolate          (i)@@ -12,6 +14,7 @@  import Language.Alloy.Call (   CallAlloyConfig (..),+  SatSolver (..),   defaultCallAlloyConfig,   existsInstance,   getInstances,@@ -39,6 +42,16 @@       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` []+    for_ solvers $ \solver ->+      it ("using solver " ++ show solver ++ " generates an instance") $ do+        xs <- length <$> getInstancesWith+          cfg {+            maxInstances = Just 1,+            satSolver = solver,+            timeout = Nothing+            }+          (graph 2)+        xs `shouldBe` 1     it "called in parallel does not create issues" $ do       ys <- forConcurrently [1 .. 6] $ \x ->         length <$> getInstances (Just $ x ^ (3 :: Integer)) (graph x)@@ -53,6 +66,8 @@       maxInstances = Nothing,       timeout      = Just 0       }+    untested = [BerkMin, Spear]+    solvers = [minBound ..] \\ untested  graph :: Integer -> String graph x = [i|