-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathAbstract-DPO-StateSpace.html
18 lines (18 loc) · 26.3 KB
/
Abstract-DPO-StateSpace.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Abstract.DPO.StateSpace</title><link href="ocean.css" rel="stylesheet" type="text/css" title="Ocean" /><script src="haddock-util.js" type="text/javascript"></script><script src="https://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS-MML_HTMLorMML" type="text/javascript"></script><script type="text/javascript">//<![CDATA[
window.onload = function () {pageLoad();setSynopsis("mini_Abstract-DPO-StateSpace.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Abstract.DPO.StateSpace.html">Source</a></li><li><a href="index.html">Contents</a></li><li><a href="doc-index.html">Index</a></li></ul><p class="caption">verigraph-1.1.1: Software specification and verification tool based on graph rewriting.</p></div><div id="content"><div id="module-header"><table class="info"><tr><th>Maintainer</th><td>Guilherme G. Azzi <[email protected]></td></tr><tr><th>Stability</th><td>experimental</td></tr><tr><th>Safe Haskell</th><td>None</td></tr><tr><th>Language</th><td>Haskell2010</td></tr></table><p class="caption">Abstract.DPO.StateSpace</p></div><div id="table-of-contents"><p class="caption">Contents</p><ul><li><a href="#g:1">State spaces</a></li><li><a href="#g:2">State space builder</a><ul><li><a href="#g:3">Getting the configuration</a></li><li><a href="#g:4">Accessing the state space</a></li><li><a href="#g:5">Exploring the state space</a></li></ul></li></ul></div><div id="description"><p class="caption">Description</p><div class="doc"><p>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.</p></div></div><div id="synopsis"><p id="control.syn" class="caption expander" onclick="toggleSection('syn')">Synopsis</p><ul id="section.syn" class="hide" onclick="toggleSection('syn')"><li class="src short"><span class="keyword">data</span> <a href="#t:StateSpace">StateSpace</a> m</li><li class="src short"><a href="#v:empty">empty</a> :: <a href="Abstract-AdhesiveHLR.html#t:MorphismsConfig">MorphismsConfig</a> -> [<a href="Abstract-DPO.html#t:Production">Production</a> m] -> [(<a href="../base-4.9.1.0/Data-String.html#t:String">String</a>, <a href="Abstract-DPO.html#t:Production">Production</a> m)] -> <a href="Abstract-DPO-StateSpace.html#t:StateSpace">StateSpace</a> m</li><li class="src short"><a href="#v:states">states</a> :: <a href="Abstract-DPO-StateSpace.html#t:StateSpace">StateSpace</a> m -> <a href="../containers-0.5.7.1/Data-IntMap-Lazy.html#t:IntMap">IntMap</a> (State m)</li><li class="src short"><a href="#v:transitions">transitions</a> :: <a href="Abstract-DPO-StateSpace.html#t:StateSpace">StateSpace</a> m -> <a href="../containers-0.5.7.1/Data-Set.html#t:Set">Set</a> (<a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a>, <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a>)</li><li class="src short"><a href="#v:searchForState">searchForState</a> :: <span class="keyword">forall</span> m. <a href="Abstract-DPO.html#t:DPO">DPO</a> m => <a href="Abstract-Morphism.html#t:Obj">Obj</a> m -> <a href="Abstract-DPO-StateSpace.html#t:StateSpace">StateSpace</a> m -> <a href="../base-4.9.1.0/Data-Maybe.html#t:Maybe">Maybe</a> (<a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a>, State m)</li><li class="src short"><a href="#v:toKripkeStructure">toKripkeStructure</a> :: <a href="Abstract-DPO-StateSpace.html#t:StateSpace">StateSpace</a> m -> <a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> <a href="../base-4.9.1.0/Data-String.html#t:String">String</a></li><li class="src short"><span class="keyword">data</span> <a href="#t:StateSpaceBuilder">StateSpaceBuilder</a> m a</li><li class="src short"><a href="#v:runStateSpaceBuilder">runStateSpaceBuilder</a> :: <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m a -> <a href="Abstract-DPO-StateSpace.html#t:StateSpace">StateSpace</a> m -> (a, <a href="Abstract-DPO-StateSpace.html#t:StateSpace">StateSpace</a> m)</li><li class="src short"><a href="#v:evalStateSpaceBuilder">evalStateSpaceBuilder</a> :: <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m a -> <a href="Abstract-DPO-StateSpace.html#t:StateSpace">StateSpace</a> m -> a</li><li class="src short"><a href="#v:execStateSpaceBuilder">execStateSpaceBuilder</a> :: <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m a -> <a href="Abstract-DPO-StateSpace.html#t:StateSpace">StateSpace</a> m -> <a href="Abstract-DPO-StateSpace.html#t:StateSpace">StateSpace</a> m</li><li class="src short"><a href="#v:getDpoConfig">getDpoConfig</a> :: <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m <a href="Abstract-AdhesiveHLR.html#t:MorphismsConfig">MorphismsConfig</a></li><li class="src short"><a href="#v:getProductions">getProductions</a> :: <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m [<a href="Abstract-DPO.html#t:Production">Production</a> m]</li><li class="src short"><a href="#v:putState">putState</a> :: <a href="Abstract-DPO.html#t:DPO">DPO</a> m => <a href="Abstract-Morphism.html#t:Obj">Obj</a> m -> <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m (<a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a>, <a href="../base-4.9.1.0/Data-Bool.html#t:Bool">Bool</a>)</li><li class="src short"><a href="#v:putTransition">putTransition</a> :: (<a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a>, <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a>) -> <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m ()</li><li class="src short"><a href="#v:findIsomorphicState">findIsomorphicState</a> :: <a href="Abstract-DPO.html#t:DPO">DPO</a> m => <a href="Abstract-Morphism.html#t:Obj">Obj</a> m -> <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m (<a href="../base-4.9.1.0/Data-Maybe.html#t:Maybe">Maybe</a> (<a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a>, State m))</li><li class="src short"><a href="#v:expandSuccessors">expandSuccessors</a> :: <span class="keyword">forall</span> m. <a href="Abstract-DPO.html#t:DPO">DPO</a> m => (<a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a>, <a href="Abstract-Morphism.html#t:Obj">Obj</a> m) -> <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m [(<a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a>, <a href="Abstract-Morphism.html#t:Obj">Obj</a> m, <a href="../base-4.9.1.0/Data-Bool.html#t:Bool">Bool</a>)]</li><li class="src short"><a href="#v:depthSearch">depthSearch</a> :: <span class="keyword">forall</span> m. <a href="Abstract-DPO.html#t:DPO">DPO</a> m => <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a> -> <a href="Abstract-Morphism.html#t:Obj">Obj</a> m -> <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m ()</li></ul></div><div id="interface"><h1 id="g:1">State spaces</h1><div class="top"><p class="src"><span class="keyword">data</span> <a id="t:StateSpace" class="def">StateSpace</a> m <a href="src/Abstract.DPO.StateSpace.html#StateSpace" class="link">Source</a> <a href="#t:StateSpace" class="selflink">#</a></p><div class="doc"><p>A data structure storing the explored portion of the state space induced by a
High-Level Replacement (HLR) system.</p><p>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.</p><p>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.</p></div><div class="subs instances"><p id="control.i:StateSpace" class="caption collapser" onclick="toggleSection('i:StateSpace')">Instances</p><div id="section.i:StateSpace" class="show"><table><tr><td class="src clearfix"><span class="inst-left"><span id="control.i:id:StateSpace:MonadState:1" class="instance expander" onclick="toggleSection('i:id:StateSpace:MonadState:1')"></span> MonadState (<a href="Abstract-DPO-StateSpace.html#t:StateSpace">StateSpace</a> m) (<a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m)</span> <a href="src/Abstract.DPO.StateSpace.html#line-133" class="link">Source</a> <a href="#t:StateSpace" class="selflink">#</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div id="section.i:id:StateSpace:MonadState:1" class="inst-details hide"><div class="subs methods"><p class="caption">Methods</p><p class="src"><a href="#v:get">get</a> :: <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m (<a href="Abstract-DPO-StateSpace.html#t:StateSpace">StateSpace</a> m)</p><p class="src"><a href="#v:put">put</a> :: <a href="Abstract-DPO-StateSpace.html#t:StateSpace">StateSpace</a> m -> <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m ()</p><p class="src"><a href="#v:state">state</a> :: (<a href="Abstract-DPO-StateSpace.html#t:StateSpace">StateSpace</a> m -> (a, <a href="Abstract-DPO-StateSpace.html#t:StateSpace">StateSpace</a> m)) -> <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m a</p></div></div></td></tr></table></div></div></div><div class="top"><p class="src"><a id="v:empty" class="def">empty</a> :: <a href="Abstract-AdhesiveHLR.html#t:MorphismsConfig">MorphismsConfig</a> -> [<a href="Abstract-DPO.html#t:Production">Production</a> m] -> [(<a href="../base-4.9.1.0/Data-String.html#t:String">String</a>, <a href="Abstract-DPO.html#t:Production">Production</a> m)] -> <a href="Abstract-DPO-StateSpace.html#t:StateSpace">StateSpace</a> m <a href="src/Abstract.DPO.StateSpace.html#empty" class="link">Source</a> <a href="#v:empty" class="selflink">#</a></p><div class="doc"><p>An empty state space for the HLR system defined by the given productions, with the given
configuration of the DPO semantics.</p></div></div><div class="top"><p class="src"><a id="v:states" class="def">states</a> :: <a href="Abstract-DPO-StateSpace.html#t:StateSpace">StateSpace</a> m -> <a href="../containers-0.5.7.1/Data-IntMap-Lazy.html#t:IntMap">IntMap</a> (State m) <a href="src/Abstract.DPO.StateSpace.html#states" class="link">Source</a> <a href="#v:states" class="selflink">#</a></p><div class="doc"><p>Obtain the set of (explored) indexed states in a state space.</p></div></div><div class="top"><p class="src"><a id="v:transitions" class="def">transitions</a> :: <a href="Abstract-DPO-StateSpace.html#t:StateSpace">StateSpace</a> m -> <a href="../containers-0.5.7.1/Data-Set.html#t:Set">Set</a> (<a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a>, <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a>) <a href="src/Abstract.DPO.StateSpace.html#transitions" class="link">Source</a> <a href="#v:transitions" class="selflink">#</a></p><div class="doc"><p>Obtain the set of (explored) transitions in a state space.</p></div></div><div class="top"><p class="src"><a id="v:searchForState" class="def">searchForState</a> :: <span class="keyword">forall</span> m. <a href="Abstract-DPO.html#t:DPO">DPO</a> m => <a href="Abstract-Morphism.html#t:Obj">Obj</a> m -> <a href="Abstract-DPO-StateSpace.html#t:StateSpace">StateSpace</a> m -> <a href="../base-4.9.1.0/Data-Maybe.html#t:Maybe">Maybe</a> (<a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a>, State m) <a href="src/Abstract.DPO.StateSpace.html#searchForState" class="link">Source</a> <a href="#v:searchForState" class="selflink">#</a></p><div class="doc"><p>Tries to find an isomorphic object in the state space, returning it along with its index.</p></div></div><div class="top"><p class="src"><a id="v:toKripkeStructure" class="def">toKripkeStructure</a> :: <a href="Abstract-DPO-StateSpace.html#t:StateSpace">StateSpace</a> m -> <a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> <a href="../base-4.9.1.0/Data-String.html#t:String">String</a> <a href="src/Abstract.DPO.StateSpace.html#toKripkeStructure" class="link">Source</a> <a href="#v:toKripkeStructure" class="selflink">#</a></p><div class="doc"><p>Converts the state space to a transition system that may be used for model checking</p></div></div><h1 id="g:2">State space builder</h1><div class="top"><p class="src"><span class="keyword">data</span> <a id="t:StateSpaceBuilder" class="def">StateSpaceBuilder</a> m a <a href="src/Abstract.DPO.StateSpace.html#StateSpaceBuilder" class="link">Source</a> <a href="#t:StateSpaceBuilder" class="selflink">#</a></p><div class="doc"><p>A monad for exploring the state space of a High-Level Replacement System.</p><p>Provides a static configuration of the DPO semantics and a static set of</p></div><div class="subs instances"><p id="control.i:StateSpaceBuilder" class="caption collapser" onclick="toggleSection('i:StateSpaceBuilder')">Instances</p><div id="section.i:StateSpaceBuilder" class="show"><table><tr><td class="src clearfix"><span class="inst-left"><span id="control.i:id:StateSpaceBuilder:Monad:1" class="instance expander" onclick="toggleSection('i:id:StateSpaceBuilder:Monad:1')"></span> <a href="../base-4.9.1.0/Control-Monad.html#t:Monad">Monad</a> (<a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m)</span> <a href="src/Abstract.DPO.StateSpace.html#line-132" class="link">Source</a> <a href="#t:StateSpaceBuilder" class="selflink">#</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div id="section.i:id:StateSpaceBuilder:Monad:1" class="inst-details hide"><div class="subs methods"><p class="caption">Methods</p><p class="src"><a href="#v:-62--62--61-">(>>=)</a> :: <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m a -> (a -> <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m b) -> <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m b <a href="#v:-62--62--61-" class="selflink">#</a></p><p class="src"><a href="#v:-62--62-">(>>)</a> :: <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m a -> <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m b -> <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m b <a href="#v:-62--62-" class="selflink">#</a></p><p class="src"><a href="#v:return">return</a> :: a -> <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m a <a href="#v:return" class="selflink">#</a></p><p class="src"><a href="#v:fail">fail</a> :: <a href="../base-4.9.1.0/Data-String.html#t:String">String</a> -> <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m a <a href="#v:fail" class="selflink">#</a></p></div></div></td></tr><tr><td class="src clearfix"><span class="inst-left"><span id="control.i:id:StateSpaceBuilder:Functor:2" class="instance expander" onclick="toggleSection('i:id:StateSpaceBuilder:Functor:2')"></span> <a href="../base-4.9.1.0/Data-Functor.html#t:Functor">Functor</a> (<a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m)</span> <a href="src/Abstract.DPO.StateSpace.html#line-132" class="link">Source</a> <a href="#t:StateSpaceBuilder" class="selflink">#</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div id="section.i:id:StateSpaceBuilder:Functor:2" class="inst-details hide"><div class="subs methods"><p class="caption">Methods</p><p class="src"><a href="#v:fmap">fmap</a> :: (a -> b) -> <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m a -> <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m b <a href="#v:fmap" class="selflink">#</a></p><p class="src"><a href="#v:-60--36-">(<$)</a> :: a -> <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m b -> <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m a <a href="#v:-60--36-" class="selflink">#</a></p></div></div></td></tr><tr><td class="src clearfix"><span class="inst-left"><span id="control.i:id:StateSpaceBuilder:Applicative:3" class="instance expander" onclick="toggleSection('i:id:StateSpaceBuilder:Applicative:3')"></span> <a href="../base-4.9.1.0/Control-Applicative.html#t:Applicative">Applicative</a> (<a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m)</span> <a href="src/Abstract.DPO.StateSpace.html#line-132" class="link">Source</a> <a href="#t:StateSpaceBuilder" class="selflink">#</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div id="section.i:id:StateSpaceBuilder:Applicative:3" class="inst-details hide"><div class="subs methods"><p class="caption">Methods</p><p class="src"><a href="#v:pure">pure</a> :: a -> <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m a <a href="#v:pure" class="selflink">#</a></p><p class="src"><a href="#v:-60--42--62-">(<*>)</a> :: <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m (a -> b) -> <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m a -> <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m b <a href="#v:-60--42--62-" class="selflink">#</a></p><p class="src"><a href="#v:-42--62-">(*>)</a> :: <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m a -> <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m b -> <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m b <a href="#v:-42--62-" class="selflink">#</a></p><p class="src"><a href="#v:-60--42-">(<*)</a> :: <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m a -> <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m b -> <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m a <a href="#v:-60--42-" class="selflink">#</a></p></div></div></td></tr><tr><td class="src clearfix"><span class="inst-left"><span id="control.i:id:StateSpaceBuilder:MonadState:4" class="instance expander" onclick="toggleSection('i:id:StateSpaceBuilder:MonadState:4')"></span> MonadState (<a href="Abstract-DPO-StateSpace.html#t:StateSpace">StateSpace</a> m) (<a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m)</span> <a href="src/Abstract.DPO.StateSpace.html#line-133" class="link">Source</a> <a href="#t:StateSpaceBuilder" class="selflink">#</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div id="section.i:id:StateSpaceBuilder:MonadState:4" class="inst-details hide"><div class="subs methods"><p class="caption">Methods</p><p class="src"><a href="#v:get">get</a> :: <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m (<a href="Abstract-DPO-StateSpace.html#t:StateSpace">StateSpace</a> m)</p><p class="src"><a href="#v:put">put</a> :: <a href="Abstract-DPO-StateSpace.html#t:StateSpace">StateSpace</a> m -> <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m ()</p><p class="src"><a href="#v:state">state</a> :: (<a href="Abstract-DPO-StateSpace.html#t:StateSpace">StateSpace</a> m -> (a, <a href="Abstract-DPO-StateSpace.html#t:StateSpace">StateSpace</a> m)) -> <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m a</p></div></div></td></tr></table></div></div></div><div class="top"><p class="src"><a id="v:runStateSpaceBuilder" class="def">runStateSpaceBuilder</a> :: <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m a -> <a href="Abstract-DPO-StateSpace.html#t:StateSpace">StateSpace</a> m -> (a, <a href="Abstract-DPO-StateSpace.html#t:StateSpace">StateSpace</a> m) <a href="src/Abstract.DPO.StateSpace.html#runStateSpaceBuilder" class="link">Source</a> <a href="#v:runStateSpaceBuilder" class="selflink">#</a></p><div class="doc"><p>Runs the builder with the given configuration and initial state space.</p></div></div><div class="top"><p class="src"><a id="v:evalStateSpaceBuilder" class="def">evalStateSpaceBuilder</a> :: <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m a -> <a href="Abstract-DPO-StateSpace.html#t:StateSpace">StateSpace</a> m -> a <a href="src/Abstract.DPO.StateSpace.html#evalStateSpaceBuilder" class="link">Source</a> <a href="#v:evalStateSpaceBuilder" class="selflink">#</a></p><div class="doc"><p>Runs the builder with the given configuration and state space, providing only
the computed value and ignoring the resulting state space.</p></div></div><div class="top"><p class="src"><a id="v:execStateSpaceBuilder" class="def">execStateSpaceBuilder</a> :: <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m a -> <a href="Abstract-DPO-StateSpace.html#t:StateSpace">StateSpace</a> m -> <a href="Abstract-DPO-StateSpace.html#t:StateSpace">StateSpace</a> m <a href="src/Abstract.DPO.StateSpace.html#execStateSpaceBuilder" class="link">Source</a> <a href="#v:execStateSpaceBuilder" class="selflink">#</a></p><div class="doc"><p>Runs the builder with the given configuration and state space, ignoring
the computed value and providing only the resulting state space.</p></div></div><h2 id="g:3">Getting the configuration</h2><div class="top"><p class="src"><a id="v:getDpoConfig" class="def">getDpoConfig</a> :: <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m <a href="Abstract-AdhesiveHLR.html#t:MorphismsConfig">MorphismsConfig</a> <a href="src/Abstract.DPO.StateSpace.html#getDpoConfig" class="link">Source</a> <a href="#v:getDpoConfig" class="selflink">#</a></p><div class="doc"><p>Gets the configuration of DPO semantics for this builder.</p></div></div><div class="top"><p class="src"><a id="v:getProductions" class="def">getProductions</a> :: <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m [<a href="Abstract-DPO.html#t:Production">Production</a> m] <a href="src/Abstract.DPO.StateSpace.html#getProductions" class="link">Source</a> <a href="#v:getProductions" class="selflink">#</a></p><div class="doc"><p>Gets the productions of the HLR system being explored in this builder.</p></div></div><h2 id="g:4">Accessing the state space</h2><div class="top"><p class="src"><a id="v:putState" class="def">putState</a> :: <a href="Abstract-DPO.html#t:DPO">DPO</a> m => <a href="Abstract-Morphism.html#t:Obj">Obj</a> m -> <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m (<a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a>, <a href="../base-4.9.1.0/Data-Bool.html#t:Bool">Bool</a>) <a href="src/Abstract.DPO.StateSpace.html#putState" class="link">Source</a> <a href="#v:putState" class="selflink">#</a></p><div class="doc"><p>Adds the given state if an isomorphic one doesn't exist. Returns a tuple <code>(index, isNew)</code>,
where <code>index</code> is the index of the state and <code>isNew</code> is true if no isomorphic state existed.</p></div></div><div class="top"><p class="src"><a id="v:putTransition" class="def">putTransition</a> :: (<a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a>, <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a>) -> <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m () <a href="src/Abstract.DPO.StateSpace.html#putTransition" class="link">Source</a> <a href="#v:putTransition" class="selflink">#</a></p><div class="doc"><p>Adds a transition between the states with the given indices. Does <strong>not</strong> check if
such states exist.</p></div></div><div class="top"><p class="src"><a id="v:findIsomorphicState" class="def">findIsomorphicState</a> :: <a href="Abstract-DPO.html#t:DPO">DPO</a> m => <a href="Abstract-Morphism.html#t:Obj">Obj</a> m -> <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m (<a href="../base-4.9.1.0/Data-Maybe.html#t:Maybe">Maybe</a> (<a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a>, State m)) <a href="src/Abstract.DPO.StateSpace.html#findIsomorphicState" class="link">Source</a> <a href="#v:findIsomorphicState" class="selflink">#</a></p><div class="doc"><p>Tries to find an isomorphic object in the current state space, returning its index.</p></div></div><h2 id="g:5">Exploring the state space</h2><div class="top"><p class="src"><a id="v:expandSuccessors" class="def">expandSuccessors</a> :: <span class="keyword">forall</span> m. <a href="Abstract-DPO.html#t:DPO">DPO</a> m => (<a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a>, <a href="Abstract-Morphism.html#t:Obj">Obj</a> m) -> <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m [(<a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a>, <a href="Abstract-Morphism.html#t:Obj">Obj</a> m, <a href="../base-4.9.1.0/Data-Bool.html#t:Bool">Bool</a>)] <a href="src/Abstract.DPO.StateSpace.html#expandSuccessors" class="link">Source</a> <a href="#v:expandSuccessors" class="selflink">#</a></p><div class="doc"><p>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 <code>(index, object, isNew)</code>, where <code>isNew</code> indicates that the state was not present in the state space before.</p></div></div><div class="top"><p class="src"><a id="v:depthSearch" class="def">depthSearch</a> :: <span class="keyword">forall</span> m. <a href="Abstract-DPO.html#t:DPO">DPO</a> m => <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a> -> <a href="Abstract-Morphism.html#t:Obj">Obj</a> m -> <a href="Abstract-DPO-StateSpace.html#t:StateSpaceBuilder">StateSpaceBuilder</a> m () <a href="src/Abstract.DPO.StateSpace.html#depthSearch" class="link">Source</a> <a href="#v:depthSearch" class="selflink">#</a></p><div class="doc"><p>Runs a depth-first search on the state space, starting on the given object and limiting
the depth to the given number.</p></div></div></div></div><div id="footer"><p>Produced by <a href="http://www.haskell.org/haddock/">Haddock</a> version 2.17.3</p></div></body></html>