Language.Clafer.IG.AlloyIGInterface

Documentation

newtype AlloyIGT m a

An interface to the Alloy Analyzer

Constructors

AlloyIGT (StateT (Maybe AlloyIGEnv) (ReaderT Process m) a)

Instances

MonadTrans AlloyIGT

Monad m => Monad (AlloyIGT m)

Functor m => Functor (AlloyIGT m)

(Monad m, Functor m) => Applicative (AlloyIGT m)

MonadIO m => MonadIO (AlloyIGT m)

MonadException m => MonadException (AlloyIGT m)

fetch :: Monad m => AlloyIGT m AlloyIGEnv

fetches :: Monad m => (AlloyIGEnv -> a) -> AlloyIGT m a

set :: Monad m => AlloyIGEnv -> AlloyIGT m ()

proc :: Monad m => AlloyIGT m Process

data AlloyIGEnv

Instance generator's environment

Constructors

AlloyIGEnv

Fields

alloyModel :: String

sigMap :: Map String Sig

scopes :: Map String Integer

globalScope :: Integer

data Sig

Constructors

Sig

Fields

s_name :: String

s_multiplicity :: Multiplicity

s_subset :: Maybe String

s_startingScope :: Maybe Integer

data Multiplicity

Constructors

One

Lone

Some

Any

Instances

Eq Multiplicity

Read Multiplicity

Show Multiplicity

data UnsatCore

Constructors

UnsatCore

Fields

core :: [Span]

Instances

Show UnsatCore

withinRange :: Integer -> Multiplicity -> Bool

runAlloyIGT :: MonadIO m => AlloyIGT m a -> m a

getAlloyModel :: MonadIO m => AlloyIGT m String

getSigs :: MonadIO m => AlloyIGT m [String]

load :: Process -> String -> IO AlloyIGEnv

Call load before any other commands.

sendLoadCommand :: MonadIO m => String -> AlloyIGT m ()

sendNextCommand :: MonadIO m => AlloyIGT m (Maybe String)

Get the next solution from alloyIG

getScope :: MonadIO m => String -> AlloyIGT m Integer

getScopes :: MonadIO m => AlloyIGT m [(String, Integer)]

sendSetScopeCommand :: MonadIO m => String -> Integer -> AlloyIGT m (Maybe String)

Tell alloyIG to change the scope of a sig

getGlobalScope :: MonadIO m => AlloyIGT m Integer

sendSetGlobalScopeCommand :: MonadIO m => Integer -> AlloyIGT m ()

Tell alloyIG to change the global scope

sendResolveCommand :: MonadIO m => AlloyIGT m ()

Tell alloyIG to recalculate the solution

sendSaveStateCommand :: MonadIO m => AlloyIGT m ()

Tell alloyIG to save the current state

sendRestoreStateCommand :: MonadIO m => AlloyIGT m ()

Tell alloyIG to restore the state

sendRemoveConstraintCommand :: MonadIO m => Span -> AlloyIGT m ()

Tell alloyIG to remove the constraint

sendUnsatCoreCommand :: MonadIO m => AlloyIGT m UnsatCore

Tell alloyIG to return the unsat core of the previous operation

sendSetUnsatCoreMinimizationCommand :: MonadIO m => Integer -> AlloyIGT m ()

Tell alloyIG to change the unsat core minimization level. 0 -> Fastest, 1 -> Medium, 2 -> Best

sendSetBitwidthCommand :: MonadIO m => Integer -> AlloyIGT m ()

Tell alloyIG to change the bitwidth

sendQuitCommand :: MonadIO m => AlloyIGT m ()

Tell alloyIG to quit

getMsg :: MonadIO m => AlloyIGT m String

readMsg :: (MonadIO m, Read r) => AlloyIGT m r

putMsg :: MonadIO m => String -> AlloyIGT m ()