Safe Haskell | None |
---|
- newtype AlloyIGT m a = AlloyIGT (StateT (Maybe AlloyIGEnv) (ReaderT Process m) a)
- 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 = AlloyIGEnv {
- alloyModel :: String
- sigMap :: Map String Sig
- scopes :: Map String Integer
- globalScope :: Integer
- data Sig = Sig {
- s_name :: String
- s_multiplicity :: Multiplicity
- s_subset :: Maybe String
- s_startingScope :: Maybe Integer
- data Multiplicity
- data UnsatCore = 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
- sendLoadCommand :: MonadIO m => String -> AlloyIGT m ()
- sendNextCommand :: MonadIO m => AlloyIGT m (Maybe String)
- getScope :: MonadIO m => String -> AlloyIGT m Integer
- getScopes :: MonadIO m => AlloyIGT m [(String, Integer)]
- sendSetScopeCommand :: MonadIO m => String -> Integer -> AlloyIGT m (Maybe String)
- getGlobalScope :: MonadIO m => AlloyIGT m Integer
- sendSetGlobalScopeCommand :: MonadIO m => Integer -> AlloyIGT m ()
- sendResolveCommand :: MonadIO m => AlloyIGT m ()
- sendSaveStateCommand :: MonadIO m => AlloyIGT m ()
- sendRestoreStateCommand :: MonadIO m => AlloyIGT m ()
- sendRemoveConstraintCommand :: MonadIO m => Span -> AlloyIGT m ()
- sendUnsatCoreCommand :: MonadIO m => AlloyIGT m UnsatCore
- sendSetUnsatCoreMinimizationCommand :: MonadIO m => Integer -> AlloyIGT m ()
- sendSetBitwidthCommand :: MonadIO m => Integer -> AlloyIGT m ()
- sendQuitCommand :: MonadIO m => AlloyIGT m ()
- getMsg :: MonadIO m => AlloyIGT m String
- readMsg :: (MonadIO m, Read r) => AlloyIGT m r
- putMsg :: MonadIO m => String -> AlloyIGT m ()
Documentation
An interface to the Alloy Analyzer
AlloyIGT (StateT (Maybe AlloyIGEnv) (ReaderT Process m) a) |
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 AlloyIGEnvSource
fetches :: Monad m => (AlloyIGEnv -> a) -> AlloyIGT m aSource
set :: Monad m => AlloyIGEnv -> AlloyIGT m ()Source
data AlloyIGEnv Source
Instance generator's environment
AlloyIGEnv | |
|
Sig | |
|
withinRange :: Integer -> Multiplicity -> BoolSource
runAlloyIGT :: MonadIO m => AlloyIGT m a -> m aSource
getAlloyModel :: MonadIO m => AlloyIGT m StringSource
load :: Process -> String -> IO AlloyIGEnvSource
Call load before any other commands.
sendLoadCommand :: MonadIO m => String -> AlloyIGT m ()Source
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
getGlobalScope :: MonadIO m => AlloyIGT m IntegerSource
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 UnsatCoreSource
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