Copyright	(c) Marcellus Siegburg 2019
License	MIT
Maintainer	marcellus.siegburg@uni-due.de
Safe Haskell	None
Language	Haskell2010

Language.Alloy.Call

Description

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 user's directory during execution. A requirement for this library to work is a Java Runtime Environment (as it is required by Alloy).

Synopsis

data CallAlloyConfig
defaultCallAlloyConfig :: CallAlloyConfig
existsInstance :: String -> IO Bool
getInstances :: Maybe Integer -> String -> IO [AlloyInstance]
getInstancesWith :: CallAlloyConfig -> String -> IO [AlloyInstance]
getSingle :: (IsString s, MonadError s m) => String -> AlloySig -> m (Set Object)
getDouble :: (IsString s, MonadError s m) => String -> AlloySig -> m (Set (Object, Object))
getTriple :: (IsString s, MonadError s m) => String -> AlloySig -> m (Set (Object, Object, Object))
lookupSig :: (IsString s, MonadError s m) => Signature -> AlloyInstance -> m AlloySig
objectName :: Object -> String
relToMap :: (IsString s, MonadError s m, Ord k, Ord v) => (a -> (k, v)) -> Set a -> m (Map k (Set v))
scoped :: String -> String -> Signature
unscoped :: String -> Signature
data Object
data Signature
type Entries a = a Signature (Entry a Set)
type AlloySig = Entry Map Set
type AlloyInstance = Entries Map

Documentation

data CallAlloyConfig Source #

Configuration for calling alloy. These are:

maximal number of instances to retrieve (Nothing for all)
wheather 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)

defaultCallAlloyConfig :: CallAlloyConfig Source #

Default configuration for calling Alloy. Defaults to:

retrieve all instances
do not overflow

existsInstance Source #

Arguments

:: String	The Alloy specification which should be loaded.
-> IO Bool	Whether there exists an instance (within the relevant scope).

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.

getInstances Source #

Arguments

:: Maybe Integer	How many instances to return; `Nothing` for all.
-> String	The Alloy specification which should be loaded.
-> IO [AlloyInstance]

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

getInstancesWith Source #

Arguments

:: CallAlloyConfig	The configuration to be used.
-> String	The Alloy specification which should be loaded.
-> IO [AlloyInstance]

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 AlloyInstances. Parameters are set using a CallAlloyConfig.

getSingle :: (IsString s, MonadError s m) => String -> AlloySig -> m (Set Object) Source #

Retrieve a set of objects of a given AlloySig. Successful if the signature's relation is a set (or empty).

getDouble :: (IsString s, MonadError s m) => String -> AlloySig -> m (Set (Object, Object)) Source #

Retrieve a binary relation of objects of a given AlloySig. Successful if the signature's relation is binary (or empty).

getTriple :: (IsString s, MonadError s m) => String -> AlloySig -> m (Set (Object, Object, Object)) Source #

Retrieve a ternary relation of objects of a given AlloySig. Successful if the signature's relation is ternary (or empty).

lookupSig :: (IsString s, MonadError s m) => Signature -> AlloyInstance -> m AlloySig Source #

Lookup a signature within a given Alloy instance.

objectName :: Object -> String Source #

Retrieve an object's name.

relToMap :: (IsString s, MonadError s m, Ord k, Ord v) => (a -> (k, v)) -> Set a -> m (Map k (Set v)) Source #

Transforms a relation into a Mapping. Is only successful (i.e. returns return) if the given transformation function is able to map the given values injectively.

scoped :: String -> String -> Signature Source #

Create a Signature given its scope and name.

unscoped :: String -> Signature Source #

Create an unscoped Signature given its name.

data Object Source #

A concrete instance of an Alloy signature.

Instances

Eq Object Source #
Instance details Defined in Language.Alloy.Types Methods (==) :: Object -> Object -> Bool # (/=) :: Object -> Object -> Bool #
Ord Object Source #
Instance details Defined in Language.Alloy.Types Methods compare :: Object -> Object -> Ordering # (<) :: Object -> Object -> Bool # (<=) :: Object -> Object -> Bool # (>) :: Object -> Object -> Bool # (>=) :: Object -> Object -> Bool # max :: Object -> Object -> Object # min :: Object -> Object -> Object #
Show Object Source #
Instance details Defined in Language.Alloy.Types Methods showsPrec :: Int -> Object -> ShowS # show :: Object -> String # showList :: [Object] -> ShowS #

data Signature Source #

An Alloy signature.

Instances

Eq Signature Source #
Instance details Defined in Language.Alloy.Types Methods (==) :: Signature -> Signature -> Bool # (/=) :: Signature -> Signature -> Bool #
Ord Signature Source #
Instance details Defined in Language.Alloy.Types Methods compare :: Signature -> Signature -> Ordering # (<) :: Signature -> Signature -> Bool # (<=) :: Signature -> Signature -> Bool # (>) :: Signature -> Signature -> Bool # (>=) :: Signature -> Signature -> Bool # max :: Signature -> Signature -> Signature # min :: Signature -> Signature -> Signature #
Show Signature Source #
Instance details Defined in Language.Alloy.Types Methods showsPrec :: Int -> Signature -> ShowS # show :: Signature -> String # showList :: [Signature] -> ShowS #

type Entries a = a Signature (Entry a Set) Source #

A collection of signatures with associated entries.

type AlloySig = Entry Map Set Source #

A signature with all its objects and relations.

type AlloyInstance = Entries Map Source #

A complete Alloy instance.