Safe Haskell	None

Language.Clafer.IG.ClaferIG

Documentation

claferIGVersion :: StringSource

data IGArgs Source

Constructors

IGArgs
Fields all :: Maybe Integer saveDir :: Maybe FilePath claferModelFile :: FilePath alloySolution :: Bool bitwidth :: Integer maxInt :: Integer useUids :: Bool addTypes :: Bool json :: Bool flatten_inheritance_comp :: Bool no_layout_comp :: Bool check_duplicates_comp :: Bool skip_resolver_comp :: Bool scope_strategy_comp :: ScopeStrategy

Instances

Data IGArgs
Show IGArgs
Typeable IGArgs

data ClaferIGEnv Source

Constructors

ClaferIGEnv
Fields claferEnv' :: ClaferEnv claferIGArgs :: IGArgs constraints :: [Constraint] claferModel :: String qNameMaps :: QNameMaps info :: Info strMap :: Map Int String lineNumMap :: Map Integer String

getClaferEnv :: Monad m => ClaferIGT m ClaferEnv Source

getClaferIGArgs :: Monad m => ClaferIGT m IGArgs Source

getConstraints :: Monad m => ClaferIGT m [Constraint]Source

getClaferModel :: Monad m => ClaferIGT m StringSource

getInfo :: Monad m => ClaferIGT m Info Source

getStrMap :: Monad m => ClaferIGT m (Map Int String)Source

newtype ClaferIGT m a Source

Constructors

ClaferIGT (StateT ClaferIGEnv (AlloyIGT m) a)

Instances

MonadTrans ClaferIGT
Monad m => Monad (ClaferIGT m)
Functor m => Functor (ClaferIGT m)
(Monad m, Functor m) => Applicative (ClaferIGT m)
MonadIO m => MonadIO (ClaferIGT m)
MonadException m => MonadException (ClaferIGT m)

data Instance Source

Constructors

Instance
Fields modelInstance :: ClaferModel alloyModelInstance :: String
UnsatCore
Fields unsatConstraints :: [Constraint] counterexample :: Maybe Counterexample
NoInstance

data Counterexample Source

Constructors

Counterexample
Fields removedConstraints :: [Constraint] counterexampleInstance :: ClaferModel counterexampleAlloyInstance :: String

runClaferIGT :: MonadIO m => IGArgs -> ClaferIGT m a -> m (Either ClaferErrs a)Source

getAlloyModel :: MonadIO m => ClaferIGT m StringSource

solve :: MonadIO m => ClaferIGT m ()Source

getClafers :: MonadIO m => ClaferIGT m [String]Source

getGlobalScope :: MonadIO m => ClaferIGT m IntegerSource

getBitwidth :: MonadIO m => ClaferIGT m IntegerSource

setGlobalScope :: MonadIO m => Integer -> ClaferIGT m ()Source

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

getScope :: MonadIO m => QName -> ClaferIGT m [String]Source

getQNameMaps :: MonadIO m => ClaferIGT m QNameMaps Source

valueOfScope :: MonadIO m => String -> ClaferIGT m IntegerSource

increaseScope :: MonadIO m => Integer -> (String, Integer) -> ClaferIGT m (Either String ())Source

setScope :: MonadIO m => Integer -> (String, Integer) -> ClaferIGT m (Either String ())Source

setAlloyScope :: MonadIO m => Integer -> String -> ClaferIGT m (Either String ())Source

next :: MonadIO m => ClaferIGT m Instance Source

setUnsatCoreMinimization :: MonadIO m => Integer -> ClaferIGT m ()Source

setBitwidth :: MonadIO m => Integer -> ClaferIGT m ()Source

quit :: MonadIO m => ClaferIGT m ()Source

reload :: MonadIO m => ClaferIGT m (Either ClaferErrs ())Source

findRemovable :: ClaferEnv -> [Span] -> [Constraint] -> [Maybe Constraint]Source

fst3 :: (IModule, GEnv, Bool) -> IModule Source

getlineNumMap :: Monad m => ClaferIGT m (Map Integer String)Source

strictReadFile :: FilePath -> IO StringSource

sigToClaferName :: String -> StringSource