call-alloy (empty) → 0.1.0.0

raw patch · 12 files changed

+331/−0 lines, 12 filesdep +basedep +bytestringdep +call-alloysetup-changedbinary-added

Dependencies added: base, bytestring, call-alloy, directory, file-embed, filepath, hashable, hspec, process, split

Files

• ChangeLog.md +3/−0
• LICENSE +18/−0
• README.md +19/−0
• Setup.hs +2/−0
• bin/alloy/RunAlloy.class binary
• bin/org.alloytools.alloy.dist.jar too large to diff
• call-alloy.cabal +73/−0
• src/Language/Alloy/Call.hs +166/−0
• src/Language/Alloy/RessourceNames.hs +14/−0
• src/Language/Alloy/Ressources.hs +17/−0
• test/Language/Alloy/CallSpec.hs +18/−0
• test/Spec.hs +1/−0

@@ -0,0 +1,3 @@+# Changelog for call-alloy++## Unreleased changes

@@ -0,0 +1,18 @@+Copyright Marcellus Siegburg (c) 2019++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.

@@ -0,0 +1,19 @@+# `call-alloy` [![Build Status](https://travis-ci.org/marcellussiegburg/call-alloy.svg?branch=master)](https://travis-ci.org/marcellussiegburg/call-alloy)++This is a simple library to call [Alloy](http://alloytools.org) given a specification.+This package includes a simple Java Library to make an API call to the Alloy Library.+Alloy is included (as JAR file) within this library as well.++## Requriements++- 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 availible when a call to Alloy happens.+  If you want to force a check, perform the test cases.++## Please note++The Java interface to get Alloy instances as well as the Alloy Jar file are backed into this library.++On every call the application checks the [`XdgDirectory`](https://hackage.haskell.org/package/directory/docs/System-Directory.html#t:XdgDirectory) if the libraries exist in a current version.+If not they are placed there together with a version identifier.

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

binary file changed (absent → 2734 bytes)

file too large to diff

@@ -0,0 +1,73 @@+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.31.2.+--+-- see: https://github.com/sol/hpack+--+-- hash: cb90623890ff4edd9f37856fc196d7ff619272da4c3519f2c2d1c082670a936a++name:           call-alloy+version:        0.1.0.0+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+homepage:       https://github.com/marcellussiegburg/call-alloy#readme+bug-reports:    https://github.com/marcellussiegburg/call-alloy/issues+author:         Marcellus Siegburg+maintainer:     marcellus.siegburg@uni-due.de+copyright:      2019 Marcellus Siegburg+license:        MIT+license-file:   LICENSE+build-type:     Simple+extra-source-files:+    README.md+    LICENSE+    ChangeLog.md+    bin/alloy/RunAlloy.class+    bin/org.alloytools.alloy.dist.jar++source-repository head+  type: git+  location: https://github.com/marcellussiegburg/call-alloy++library+  exposed-modules:+      Language.Alloy.Call+  other-modules:+      Language.Alloy.RessourceNames+      Language.Alloy.Ressources+      Paths_call_alloy+  hs-source-dirs:+      src+  build-depends:+      base >=4.7 && <5+    , bytestring+    , directory+    , file-embed+    , filepath+    , hashable+    , process+    , split+  default-language: Haskell2010++test-suite call-alloy-test+  type: exitcode-stdio-1.0+  main-is: Spec.hs+  other-modules:+      Language.Alloy.CallSpec+      Paths_call_alloy+  hs-source-dirs:+      test+  ghc-options: -threaded -rtsopts -with-rtsopts=-N+  build-depends:+      base >=4.7 && <5+    , bytestring+    , call-alloy+    , directory+    , file-embed+    , filepath+    , hashable+    , hspec+    , process+    , split+  default-language: Haskell2010

@@ -0,0 +1,166 @@+{-|+Module      : Language.Alloy.Call+Description : A simple library to call Alloy given a specification+Copyright   : (c) Marcellus Siegburg, 2019+License     : MIT+Maintainer  : marcellus.siegburg@uni-due.de++This module provides basic functionality to interact with Alloy.+This library contains Alloy and an (internal) interface to interact with it.+These libraries will be placed into the users directory during execution.+A requirement for this library to work is a Java Runtime Environment+(as it is required by Alloy).+-}+module Language.Alloy.Call (+  existsInstance,+  getInstances,+  ) where++import qualified Data.ByteString                  as BS (writeFile)++import Control.Monad                    (unless)+import Data.Hashable                    (hash)+import Data.IORef                       (IORef, newIORef, readIORef)+import Data.List                        (intercalate)+import Data.List.Split                  (splitOn)+import Data.Maybe                       (fromMaybe)+import System.Directory+  (XdgDirectory (..), createDirectoryIfMissing, doesFileExist, getXdgDirectory)+import System.Exit                      (ExitCode (..))+import System.FilePath                  ((</>), (<.>), searchPathSeparator)+import System.IO                        (hClose, hGetLine, hIsEOF, hPutStr)+import System.IO.Unsafe                 (unsafePerformIO)+import System.Process++import Language.Alloy.RessourceNames    (alloyJarName, className, classPackage)+import Language.Alloy.Ressources        (alloyJar, classFile)++{-# NOINLINE mclassPath #-}+{-|+'IORef' for storing the class path.+-}+mclassPath :: IORef (Maybe FilePath)+mclassPath = unsafePerformIO (newIORef Nothing)++{-|+This function may be used to get all model instances for a given Alloy+specification. It calls Alloy via a Java interface and returns the raw instance+answers as list of 'String's.+-}+getInstances+  :: Maybe Integer+  -- ^ How many instances to return 'Nothing' for all.+  -> String+  -- ^ The Alloy specification which should be loaded.+  -> IO [String]+getInstances maxInstances content = do+  classPath <- getClassPath+  let callAlloy = proc "java"+        ["-cp", classPath, classPackage ++ '.' : className,+         show $ fromMaybe (-1) maxInstances]+  (Just hin, Just hout, Just herr, ph) <-+    createProcess callAlloy {+        std_out = CreatePipe,+        std_in  = CreatePipe,+        std_err = CreatePipe+      }+  hPutStr hin content+  hClose hin+  printCallErrors herr+  printContentOnError ph `seq`+    fmap (intercalate "\n") . drop 1 . splitOn [begin] <$> getWholeOutput hout+  where+    begin = "---INSTANCE---"+    getWholeOutput h = do+      eof <- hIsEOF h+      if eof+        then return []+        else (:) <$> hGetLine h <*> getWholeOutput h+    printContentOnError ph = do+      code <- waitForProcess ph+      unless (code == ExitSuccess)+        $ fail $ "Failed parsing your file:\n" <> content+    printCallErrors err = do+      errors <- getWholeOutput err+      unless (null errors) $ fail $ intercalate "\n" errors++{-|+Check if the class path was determined already, if so use it, otherwise call+'readClassPath'.++Returns the class path.+-}+getClassPath :: IO FilePath+getClassPath = do+  mclassPath' <- readIORef mclassPath+  maybe readClassPath return mclassPath'++{-|+Read the class path version specified in the user directory, if it is not+current or if it does not exist, call 'createVersionFile'.++Returns the class path.+-}+readClassPath :: IO FilePath+readClassPath = do+  configDir <- getXdgDirectory XdgConfig appName+  let versionFile = configDir </> "version"+  exists <- doesFileExist versionFile+  if exists+    then do+    version <- read <$> readFile versionFile+    unless (version == versionHash) $ createVersionFile configDir versionFile+    else createVersionFile configDir versionFile+  dataDir <- getXdgDirectory XdgData $ appName </> "dataDir"+  return $ dataDir ++ searchPathSeparator : dataDir </> alloyJarName++{-|+Create all library files within the users 'XdgDirectory' by calling+'createDataDir' then place the current version number into a configuration File.+-}+createVersionFile :: FilePath -> FilePath -> IO ()+createVersionFile configDir versionFile = do+  createDataDir+  createDirectoryIfMissing True configDir+  writeFile versionFile $ show versionHash++{-|+Create all library files within the users 'XdgDirectory' based on the source+files enclosed into this library (see also 'Language.Alloy.RessourceNames' and+'Language.Alloy.Ressources').+-}+createDataDir :: IO ()+createDataDir = do+  dataDir <- getXdgDirectory XdgData $ appName </> "dataDir"+  createDirectoryIfMissing True $ dataDir </> classPackage+  BS.writeFile (dataDir </> classPackage </> className <.> "class") classFile+  BS.writeFile (dataDir </> alloyJarName) alloyJar++{-|+Check if there exists a model for the given specification. This function calls+Alloy retrieving one instance. If there is no such instance, it returns false.+This function calls 'getInstances'.+-}+existsInstance+  :: String+  -- ^ The Alloy specification which should be loaded.+  -> IO Bool+  -- ^ Whether there exists a instance (within the given scope)+existsInstance = fmap (not . null) . getInstances (Just 1)++{-|+The application name (used to store data in a specific directory.+-}+appName :: String+appName = "call-alloy"++{-# INLINE versionHash #-}+{-|+Used to determine possible source code and Alloy version changes across multiple+versions of this library.+-}+versionHash :: Int+versionHash = hash $ alloyHash + classFileHash+  where+    alloyHash = hash alloyJar+    classFileHash = hash classFile

@@ -0,0 +1,14 @@+module Language.Alloy.RessourceNames (+  alloyJarName,+  className,+  classPackage,+  ) where++alloyJarName :: String+alloyJarName = "org.alloytools.alloy.dist.jar"++className :: String+className = "RunAlloy"++classPackage :: String+classPackage = "alloy"

@@ -0,0 +1,17 @@+{-# LANGUAGE TemplateHaskell #-}+module Language.Alloy.Ressources (+  alloyJar,+  classFile,+  ) where++import Data.ByteString                  (ByteString)+import Data.FileEmbed                   (embedFile)+import System.FilePath                  ((</>), (<.>))++import Language.Alloy.RessourceNames    (alloyJarName, className, classPackage)++alloyJar :: ByteString+alloyJar = $(embedFile $ "bin" </> alloyJarName)++classFile :: ByteString+classFile = $(embedFile $ "bin" </> classPackage </> className <.> "class")

@@ -0,0 +1,18 @@+module Language.Alloy.CallSpec (spec) where++import Test.Hspec++import Language.Alloy.Call              (existsInstance, getInstances)++spec :: Spec+spec = do+  describe "existsInstance" $ do+    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+  describe "getInstances" $ do+    it "an empty spec returns a single trivial instance" $+      getInstances (Just 2) "" `shouldReturn` ["integers={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}\nuniv={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}\nInt={-8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7}\nseq/Int={0, 1, 2, 3}\nString={}\nnone={}"]+    it "a conflicting spec returns no instance" $+      getInstances (Just 1) "pred a (a: Int) { a > a }\nrun a" `shouldReturn` []

@@ -0,0 +1,1 @@+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}