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

Safe Haskell	None
Language	Haskell2010

Language.Clafer.IG.ClaferIG

Documentation

claferIGVersion :: String Source

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 String Source

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 String Source

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

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

getGlobalScope :: MonadIO m => ClaferIGT m Integer Source

getBitwidth :: MonadIO m => ClaferIGT m Integer Source

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 Integer Source

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 String Source

sigToClaferName :: String -> String Source