claferIG-0.4.4: claferIG is an interactive tool that generates instances of Clafer models.

Safe HaskellNone
LanguageHaskell2010

Language.Clafer.IG.AlloyIGInterface

Synopsis

Documentation

newtype AlloyIGT m a Source #

An interface to the Alloy Analyzer

Constructors

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

Instances

MonadTrans AlloyIGT Source # 

Methods

lift :: Monad m => m a -> AlloyIGT m a #

Monad m => Monad (AlloyIGT m) Source # 

Methods

(>>=) :: AlloyIGT m a -> (a -> AlloyIGT m b) -> AlloyIGT m b #

(>>) :: AlloyIGT m a -> AlloyIGT m b -> AlloyIGT m b #

return :: a -> AlloyIGT m a #

fail :: String -> AlloyIGT m a #

Functor m => Functor (AlloyIGT m) Source # 

Methods

fmap :: (a -> b) -> AlloyIGT m a -> AlloyIGT m b #

(<$) :: a -> AlloyIGT m b -> AlloyIGT m a #

Monad m => Applicative (AlloyIGT m) Source # 

Methods

pure :: a -> AlloyIGT m a #

(<*>) :: AlloyIGT m (a -> b) -> AlloyIGT m a -> AlloyIGT m b #

(*>) :: AlloyIGT m a -> AlloyIGT m b -> AlloyIGT m b #

(<*) :: AlloyIGT m a -> AlloyIGT m b -> AlloyIGT m a #

MonadIO m => MonadIO (AlloyIGT m) Source # 

Methods

liftIO :: IO a -> AlloyIGT m a #

MonadException m => MonadException (AlloyIGT m) Source # 

Methods

controlIO :: (RunIO (AlloyIGT m) -> IO (AlloyIGT m a)) -> AlloyIGT m a #

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

data AlloyIGEnv Source #

Instance generator's environment

data UnsatCore Source #

Constructors

UnsatCore 

Fields

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

load :: Process -> String -> IO AlloyIGEnv Source #

Call load before any other commands.

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

Get the next solution from alloyIG

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

Tell alloyIG to change the scope of a sig

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

Tell alloyIG to change the global scope

sendResolveCommand :: MonadIO m => AlloyIGT m () Source #

Tell alloyIG to recalculate the solution

sendSaveStateCommand :: MonadIO m => AlloyIGT m () Source #

Tell alloyIG to save the current state

sendRestoreStateCommand :: MonadIO m => AlloyIGT m () Source #

Tell alloyIG to restore the state

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

Tell alloyIG to remove the constraint

sendUnsatCoreCommand :: MonadIO m => AlloyIGT m UnsatCore Source #

Tell alloyIG to return the unsat core of the previous operation

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

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

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

Tell alloyIG to change the bitwidth

sendQuitCommand :: MonadIO m => AlloyIGT m () Source #

Tell alloyIG to quit

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