Copyright	(c) Marcellus Siegburg 2019 - 2025
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

alloyVersion :: String
data CallAlloyConfig = CallAlloyConfig {
- maxInstances :: !(Maybe Integer)
- noOverflow :: !Bool
- satSolver :: !SatSolver
- timeout :: !(Maybe Int)
}
data SatSolver
- = BerkMin
- | Glucose
- | Glucose41
- | Lingeling
- | MiniSat
- | MiniSatProver
- | PLingeling
- | SAT4J
- | SAT4JLight
- | SAT4JPMax
- | Spear
defaultCallAlloyConfig :: CallAlloyConfig
existsInstance :: (MonadIO m, MonadThrow m) => String -> m Bool
getInstances :: (MonadIO m, MonadThrow m) => Maybe Integer -> String -> m [AlloyInstance]
getInstancesWith :: (MonadIO m, MonadThrow m) => CallAlloyConfig -> String -> m [AlloyInstance]
object :: MonadThrow m => String -> (Int -> a) -> String -> Int -> m a
scoped :: String -> String -> Signature
int :: MonadThrow m => String -> Int -> m Int
getIdentityAs :: forall m b (a :: Type -> Type). MonadThrow m => String -> (String -> Int -> m b) -> Entry Map a -> m b
getSingleAs :: (MonadThrow m, Ord a) => String -> (String -> Int -> m a) -> AlloySig -> m (Set a)
getDoubleAs :: (MonadThrow m, Ord a, Ord b) => String -> (String -> Int -> m a) -> (String -> Int -> m b) -> AlloySig -> m (Set (a, b))
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))
lookupSig :: MonadThrow m => Signature -> AlloyInstance -> m AlloySig
unscoped :: String -> Signature
type AlloyInstance = Entries Map
type AlloySig = Entry Map Set
type Entries (a :: Type -> Type -> Type) = a Signature (Entry a Set)
data Object
data Signature

Documentation

alloyVersion :: String Source #

The currently used Alloy version.

>>> alloyVersion
"6.2.0"

Since: 0.6

data CallAlloyConfig Source #

Configuration for calling alloy.

Constructors

CallAlloyConfig

you should use defaultCallAlloyConfig instead of this constructor as additional configuration parameters might be introduced in later releases.

Fields

maxInstances :: !(Maybe Integer)
maximal number of instances to retrieve (Nothing for all)
noOverflow :: !Bool
whether to not overflow when calculating numbers within Alloy
satSolver :: !SatSolver
the SatSolver to choose. Note that some are not incremental, i.e. will return only one solution, even if maxInstances is set higher.
timeout :: !(Maybe Int)
the time in microseconds after which to forcibly kill Alloy (Nothing for never)

data SatSolver Source #

Available SAT solvers.

Note: solvers marked as not supported by default were supported in earlier versions of Alloy, but got removed. There might be a way of integrating those manually, but this has net been tried.

Constructors

BerkMin	BerkMin not supported by default
Glucose	Glucose incremental
Glucose41	Glucose41 not supported by default
Lingeling	Lingeling not incremental
MiniSat	MiniSat incremental
MiniSatProver	MiniSatProver incremental
PLingeling	PLingeling not supported by default
SAT4J	SAT4J incremental
SAT4JLight	SAT4J Light incremental
SAT4JPMax	SAT4Ji PMax incremental
Spear	Spear not supported by default

Instances

Instances details

Bounded SatSolver Source #
Instance details Defined in Language.Alloy.Internal.Call Methods minBound :: SatSolver # maxBound :: SatSolver #
Enum SatSolver Source #
Instance details 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 Source #
Instance details Defined in Language.Alloy.Internal.Call Methods readsPrec :: Int -> ReadS SatSolver # readList :: ReadS [SatSolver] # readPrec :: ReadPrec SatSolver # readListPrec :: ReadPrec [SatSolver] #
Show SatSolver Source #
Instance details Defined in Language.Alloy.Internal.Call Methods showsPrec :: Int -> SatSolver -> ShowS # show :: SatSolver -> String # showList :: [SatSolver] -> ShowS #
Eq SatSolver Source #
Instance details Defined in Language.Alloy.Internal.Call Methods (==) :: SatSolver -> SatSolver -> Bool # (/=) :: SatSolver -> SatSolver -> Bool #

defaultCallAlloyConfig :: CallAlloyConfig Source #

Default configuration for calling Alloy. Defaults to:

retrieve all instances
do not overflow
SAT4J

existsInstance Source #

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 Source #

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 Source #

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 Source #

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 Source #

Create a Signature given its scope and name.

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

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 Source #

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) Source #

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)) Source #

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)) Source #

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 Source #

Lookup a signature within a given Alloy instance.

unscoped :: String -> Signature Source #

Create an unscoped Signature given its name.

type AlloyInstance = Entries Map Source #

A complete Alloy instance.

type AlloySig = Entry Map Set Source #

A signature with all its objects and relations.

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

A collection of signatures with associated entries.

data Object Source #

A concrete instance of an Alloy signature.

Instances

Instances details

Show Object Source #
Instance details Defined in Language.Alloy.Types Methods showsPrec :: Int -> Object -> ShowS # show :: Object -> String # showList :: [Object] -> ShowS #
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 #

data Signature Source #

An Alloy signature.

Instances

Instances details

Show Signature Source #
Instance details Defined in Language.Alloy.Types Methods showsPrec :: Int -> Signature -> ShowS # show :: Signature -> String # showList :: [Signature] -> ShowS #
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 #