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

Documentation

existsInstance

Arguments

:: String

The Alloy specification which should be loaded.

-> IO Bool

Whether there exists an instance (within the given 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

:: 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 returns the raw instance answers as list of Strings.

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

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

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

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

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

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

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

Lookup a signature within a given Alloy Instance.

objectName :: Object -> String

Retrieve an objects name.

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

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

Create a Signature given its scope and name.

unscoped :: String -> Signature

Create an unscoped Signature given its name.

data Signature

An Alloy signature.

Instances

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

Show Signature

Defined in Language.Alloy.Types

Methods

showsPrec :: Int -> Signature -> ShowS

show :: Signature -> String

showList :: [Signature] -> ShowS

type Entries a = a Signature (Entry a Set)

A collection of Signatures with associated entries.

type AlloySig = Entry Map Set

A signature with all its objects and relations.

type AlloyInstance = Entries Map

A complete Alloy instance.