claferIG-0.4.3: 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) 

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

data AlloyIGEnv Source

Instance generator's environment

data UnsatCore Source

Constructors

UnsatCore 

Fields

core :: [Span]
 

Instances

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