Language.Alloy.Call

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

Documentation

data CallAlloyConfig

Configuration for calling alloy. These are:

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

data SatSolver

Available SAT solvers.

Constructors

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

Instances

Bounded SatSolver

Defined in Language.Alloy.Internal.Call

Methods

minBound :: SatSolver

maxBound :: SatSolver

Enum SatSolver

Defined in Language.Alloy.Internal.Call

Methods

succ :: SatSolver -> SatSolver

pred :: SatSolver -> SatSolver

toEnum :: Int -> SatSolver

fromEnum :: SatSolver -> Int

enumFrom :: SatSolver -> [SatSolver]

enumFromThen :: SatSolver -> SatSolver -> [SatSolver]

enumFromTo :: SatSolver -> SatSolver -> [SatSolver]

enumFromThenTo :: SatSolver -> SatSolver -> SatSolver -> [SatSolver]

Read SatSolver

Defined in Language.Alloy.Internal.Call

Methods

readsPrec :: Int -> ReadS SatSolver

readList :: ReadS [SatSolver]

readPrec :: ReadPrec SatSolver

readListPrec :: ReadPrec [SatSolver]

Show SatSolver

Defined in Language.Alloy.Internal.Call

Methods

showsPrec :: Int -> SatSolver -> ShowS

show :: SatSolver -> String

showList :: [SatSolver] -> ShowS

Eq SatSolver

Defined in Language.Alloy.Internal.Call

Methods

(==) :: SatSolver -> SatSolver -> Bool

(/=) :: SatSolver -> SatSolver -> Bool

defaultCallAlloyConfig :: CallAlloyConfig

Default configuration for calling Alloy. Defaults to:

• retrieve all instances
• do not overflow
• SAT4J

existsInstance

Arguments

:: (MonadIO m, MonadThrow m)

=> String

The Alloy specification which should be loaded.

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

Arguments

:: (MonadIO m, MonadThrow m)

=> Maybe Integer

How many instances to return; Nothing for all.

-> String

The Alloy specification which should be loaded.

-> m [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

Arguments

:: (MonadIO m, MonadThrow m)

=> CallAlloyConfig

The configuration to be used.

-> String

The Alloy specification which should be loaded.

-> m [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.

object :: MonadThrow m => String -> (Int -> a) -> String -> Int -> m a

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, but failing in case anything different appears (unexpectedly).

scoped :: String -> String -> Signature

Create a Signature given its scope and name.

int :: MonadThrow m => String -> Int -> m Int

For retrieval of Int values using a get... function.

e.g. returning all (within Alloy) available Int values could look like this

do n <- lookupSig (unscoped "Int")
   getSingleAs "" int n

getIdentityAs :: forall m b (a :: Type -> Type). MonadThrow m => String -> (String -> Int -> m b) -> Entry Map a -> m b

Retrieve a single value of a given AlloySig. The Value will be created by applying the given mapping function from object name and Int to value. The mapping has to be injective (for all expected cases). Successful if the signature's relation is a single value.

getSingleAs :: (MonadThrow m, Ord a) => String -> (String -> Int -> m a) -> AlloySig -> m (Set a)

Retrieve a set of values of a given AlloySig. Values will be created by applying the given mapping function from object Name and Int to value. The mapping has to be injective (for all expected cases). Successful if the signature's relation is a set (or empty).

getDoubleAs :: (MonadThrow m, Ord a, Ord b) => String -> (String -> Int -> m a) -> (String -> Int -> m b) -> AlloySig -> m (Set (a, b))

Retrieve a binary relation of values of given AlloySig. Values will be created by applying the given mapping functions from object Name and Int to the value. The mapping has to be injective (for all expected cases). Successful if the signature's relation is binary (or empty).

getTripleAs :: (MonadThrow m, Ord a, Ord b, Ord c) => String -> (String -> Int -> m a) -> (String -> Int -> m b) -> (String -> Int -> m c) -> AlloySig -> m (Set (a, b, c))

Retrieve a ternary relation of values of a given AlloySig. Values will be created by applying the given mapping functions from object Name and Int to the value. The mapping has to be injective (for all expected cases). Successful if the signature's relation is ternary (or empty).

lookupSig :: MonadThrow m => Signature -> AlloyInstance -> m AlloySig

Lookup a signature within a given Alloy instance.

unscoped :: String -> Signature

Create an unscoped Signature given its name.

type AlloyInstance = Entries Map

A complete Alloy instance.

type AlloySig = Entry Map Set

A signature with all its objects and relations.

type Entries (a :: Type -> Type -> Type) = a Signature (Entry a Set)

A collection of signatures with associated entries.

data Object

A concrete instance of an Alloy signature.

Instances

Show Object

Defined in Language.Alloy.Types

Methods

showsPrec :: Int -> Object -> ShowS

show :: Object -> String

showList :: [Object] -> ShowS

Eq Object

Defined in Language.Alloy.Types

Methods

(==) :: Object -> Object -> Bool

(/=) :: Object -> Object -> Bool

Ord Object

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

data Signature

An Alloy signature.

Instances

Show Signature

Defined in Language.Alloy.Types

Methods

showsPrec :: Int -> Signature -> ShowS

show :: Signature -> String

showList :: [Signature] -> ShowS

Eq Signature

Defined in Language.Alloy.Types

Methods

(==) :: Signature -> Signature -> Bool

(/=) :: Signature -> Signature -> Bool

Ord Signature

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