| Maintainer | Guilherme G. Azzi <ggazzi@inf.ufrgs.br> |
|---|---|
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Abstract.DPO.StateSpace
Contents
Description
A High-Level Replacement (HLR) system, along with a starting state, induces a state space that may be seen as a transition system or Kripke structure. This module provides a data structure for representing the explored portion of such a state space, as well as a monad for doing said exploration.
- data StateSpace m
- empty :: MorphismsConfig -> [Production m] -> [(String, Production m)] -> StateSpace m
- states :: StateSpace m -> IntMap (State m)
- transitions :: StateSpace m -> Set (Int, Int)
- searchForState :: forall m. DPO m => Obj m -> StateSpace m -> Maybe (Int, State m)
- toKripkeStructure :: StateSpace m -> KripkeStructure String
- data StateSpaceBuilder m a
- runStateSpaceBuilder :: StateSpaceBuilder m a -> StateSpace m -> (a, StateSpace m)
- evalStateSpaceBuilder :: StateSpaceBuilder m a -> StateSpace m -> a
- execStateSpaceBuilder :: StateSpaceBuilder m a -> StateSpace m -> StateSpace m
- getDpoConfig :: StateSpaceBuilder m MorphismsConfig
- getProductions :: StateSpaceBuilder m [Production m]
- putState :: DPO m => Obj m -> StateSpaceBuilder m (Int, Bool)
- putTransition :: (Int, Int) -> StateSpaceBuilder m ()
- findIsomorphicState :: DPO m => Obj m -> StateSpaceBuilder m (Maybe (Int, State m))
- expandSuccessors :: forall m. DPO m => (Int, Obj m) -> StateSpaceBuilder m [(Int, Obj m, Bool)]
- depthSearch :: forall m. DPO m => Int -> Obj m -> StateSpaceBuilder m ()
State spaces
data StateSpace m Source #
A data structure storing the explored portion of the state space induced by a High-Level Replacement (HLR) system.
The states are objects in the category, up to isomorphism. Such states are identified by numeric indices. The transitions are specified as pairs of indices, so multiple transitions between the same two states are seen as a single one.
The states are annotated with the set of predicates that hold in them. Predicates are expressed as rules, and a predicate holds in a state if the rule is applicable.
Instances
| MonadState (StateSpace m) (StateSpaceBuilder m) Source # | |
empty :: MorphismsConfig -> [Production m] -> [(String, Production m)] -> StateSpace m Source #
An empty state space for the HLR system defined by the given productions, with the given configuration of the DPO semantics.
states :: StateSpace m -> IntMap (State m) Source #
Obtain the set of (explored) indexed states in a state space.
transitions :: StateSpace m -> Set (Int, Int) Source #
Obtain the set of (explored) transitions in a state space.
searchForState :: forall m. DPO m => Obj m -> StateSpace m -> Maybe (Int, State m) Source #
Tries to find an isomorphic object in the state space, returning it along with its index.
toKripkeStructure :: StateSpace m -> KripkeStructure String Source #
Converts the state space to a transition system that may be used for model checking
State space builder
data StateSpaceBuilder m a Source #
A monad for exploring the state space of a High-Level Replacement System.
Provides a static configuration of the DPO semantics and a static set of
Instances
| Monad (StateSpaceBuilder m) Source # | |
| Functor (StateSpaceBuilder m) Source # | |
| Applicative (StateSpaceBuilder m) Source # | |
| MonadState (StateSpace m) (StateSpaceBuilder m) Source # | |
runStateSpaceBuilder :: StateSpaceBuilder m a -> StateSpace m -> (a, StateSpace m) Source #
Runs the builder with the given configuration and initial state space.
evalStateSpaceBuilder :: StateSpaceBuilder m a -> StateSpace m -> a Source #
Runs the builder with the given configuration and state space, providing only the computed value and ignoring the resulting state space.
execStateSpaceBuilder :: StateSpaceBuilder m a -> StateSpace m -> StateSpace m Source #
Runs the builder with the given configuration and state space, ignoring the computed value and providing only the resulting state space.
Getting the configuration
getDpoConfig :: StateSpaceBuilder m MorphismsConfig Source #
Gets the configuration of DPO semantics for this builder.
getProductions :: StateSpaceBuilder m [Production m] Source #
Gets the productions of the HLR system being explored in this builder.
Accessing the state space
putState :: DPO m => Obj m -> StateSpaceBuilder m (Int, Bool) Source #
Adds the given state if an isomorphic one doesn't exist. Returns a tuple (index, isNew),
where index is the index of the state and isNew is true if no isomorphic state existed.
putTransition :: (Int, Int) -> StateSpaceBuilder m () Source #
Adds a transition between the states with the given indices. Does not check if such states exist.
findIsomorphicState :: DPO m => Obj m -> StateSpaceBuilder m (Maybe (Int, State m)) Source #
Tries to find an isomorphic object in the current state space, returning its index.
Exploring the state space
expandSuccessors :: forall m. DPO m => (Int, Obj m) -> StateSpaceBuilder m [(Int, Obj m, Bool)] Source #
Finds all transformations of the given state with the productions of the HLR system being explored, adding them to the state space. Returns a list of the successor states as (index, object, isNew), where isNew indicates that the state was not present in the state space before.
depthSearch :: forall m. DPO m => Int -> Obj m -> StateSpaceBuilder m () Source #
Runs a depth-first search on the state space, starting on the given object and limiting the depth to the given number.