-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathLogic-Model.html
9 lines (9 loc) · 38.1 KB
/
Logic-Model.html
1
2
3
4
5
6
7
8
9
<!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>Logic.Model</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_Logic-Model.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Logic.Model.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>provisional</td></tr><tr><th>Safe Haskell</th><td>Safe</td></tr><tr><th>Language</th><td>Haskell2010</td></tr></table><p class="caption">Logic.Model</p></div><div id="table-of-contents"><p class="caption">Contents</p><ul><li><a href="#g:1">Kripke structures</a><ul><li><a href="#g:2">Looking up states</a></li><li><a href="#g:3">Looking up transitions</a></li><li><a href="#g:4">Lookup by adjacency</a></li></ul></li><li><a href="#g:5">Utilities for labeled elements</a></li></ul></div><div id="description"><p class="caption">Description</p><div class="doc empty"> </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:KripkeStructure">KripkeStructure</a> a = <a href="#v:KripkeStructure">KripkeStructure</a> {<ul class="subs"><li><a href="#v:states">states</a> :: [<a href="Logic-Model.html#t:State">State</a> a]</li><li><a href="#v:transitions">transitions</a> :: [<a href="Logic-Model.html#t:Transition">Transition</a> a]</li></ul>}</li><li class="src short"><span class="keyword">data</span> <a href="#t:State">State</a> a = <a href="#v:State">State</a> <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a> [a]</li><li class="src short"><span class="keyword">data</span> <a href="#t:Transition">Transition</a> a = <a href="#v:Transition">Transition</a> {<ul class="subs"><li><a href="#v:transitionId">transitionId</a> :: <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a></li><li><a href="#v:source">source</a> :: <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a></li><li><a href="#v:target">target</a> :: <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a></li><li><a href="#v:transitionPayload">transitionPayload</a> :: [a]</li></ul>}</li><li class="src short"><a href="#v:stateIds">stateIds</a> :: <a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> a -> [<a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a>]</li><li class="src short"><a href="#v:lookupState">lookupState</a> :: <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a> -> <a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> a -> <a href="../base-4.9.1.0/Data-Maybe.html#t:Maybe">Maybe</a> (<a href="Logic-Model.html#t:State">State</a> a)</li><li class="src short"><a href="#v:getState">getState</a> :: <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a> -> <a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> a -> <a href="Logic-Model.html#t:State">State</a> a</li><li class="src short"><a href="#v:transitionIds">transitionIds</a> :: <a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> a -> [<a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a>]</li><li class="src short"><a href="#v:lookupTransition">lookupTransition</a> :: <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a> -> <a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> a -> <a href="../base-4.9.1.0/Data-Maybe.html#t:Maybe">Maybe</a> (<a href="Logic-Model.html#t:Transition">Transition</a> a)</li><li class="src short"><a href="#v:getTransition">getTransition</a> :: <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a> -> <a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> a -> <a href="Logic-Model.html#t:Transition">Transition</a> a</li><li class="src short"><a href="#v:nextStates">nextStates</a> :: <a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> 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:precedes">precedes</a> :: <a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> 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="../base-4.9.1.0/Data-Bool.html#t:Bool">Bool</a></li><li class="src short"><a href="#v:prevStates">prevStates</a> :: <a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> 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:follows">follows</a> :: <a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> 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="../base-4.9.1.0/Data-Bool.html#t:Bool">Bool</a></li><li class="src short"><span class="keyword">class</span> <a href="#t:Element">Element</a> e <span class="keyword">where</span><ul class="subs"><li><span class="keyword">type</span> <a href="#t:Payload">Payload</a> e :: <a href="../base-4.9.1.0/Data-Kind.html#t:-42-">*</a></li></ul></li><li class="src short"><a href="#v:findById">findById</a> :: <a href="Logic-Model.html#t:Element">Element</a> a => <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a> -> [a] -> <a href="../base-4.9.1.0/Data-Maybe.html#t:Maybe">Maybe</a> a</li></ul></div><div id="interface"><h1 id="g:1">Kripke structures</h1><div class="top"><p class="src"><span class="keyword">data</span> <a id="t:KripkeStructure" class="def">KripkeStructure</a> a <a href="src/Logic.Model.html#KripkeStructure" class="link">Source</a> <a href="#t:KripkeStructure" class="selflink">#</a></p><div class="doc"><p>A Kripke structure is composed of a list of states and a list of
transitions between such states. States are labeled with the atomic
propositions that hold in it.</p><p>This particular kind of labeled transition system may be used as a model
for temporal logics. In particular, it may be used for model checking.</p><p>This structure is polymorphic on the type of atomic propositions.</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a id="v:KripkeStructure" class="def">KripkeStructure</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div class="subs fields"><p class="caption">Fields</p><ul><li><dfn class="src"><a id="v:states" class="def">states</a> :: [<a href="Logic-Model.html#t:State">State</a> a]</dfn><div class="doc"><p>List of labeled states of the Kripke structure</p></div></li><li><dfn class="src"><a id="v:transitions" class="def">transitions</a> :: [<a href="Logic-Model.html#t:Transition">Transition</a> a]</dfn><div class="doc"><p>List of transitions of the Kripke structure</p></div></li></ul></div></td></tr></table></div><div class="subs instances"><p id="control.i:KripkeStructure" class="caption collapser" onclick="toggleSection('i:KripkeStructure')">Instances</p><div id="section.i:KripkeStructure" class="show"><table><tr><td class="src clearfix"><span class="inst-left"><span id="control.i:id:KripkeStructure:Eq:1" class="instance expander" onclick="toggleSection('i:id:KripkeStructure:Eq:1')"></span> <a href="../base-4.9.1.0/Data-Eq.html#t:Eq">Eq</a> a => <a href="../base-4.9.1.0/Data-Eq.html#t:Eq">Eq</a> (<a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> a)</span> <a href="src/Logic.Model.html#line-51" class="link">Source</a> <a href="#t:KripkeStructure" class="selflink">#</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div id="section.i:id:KripkeStructure:Eq:1" class="inst-details hide"><div class="subs methods"><p class="caption">Methods</p><p class="src"><a href="#v:-61--61-">(==)</a> :: <a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> a -> <a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> a -> <a href="../base-4.9.1.0/Data-Bool.html#t:Bool">Bool</a> <a href="#v:-61--61-" class="selflink">#</a></p><p class="src"><a href="#v:-47--61-">(/=)</a> :: <a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> a -> <a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> a -> <a href="../base-4.9.1.0/Data-Bool.html#t:Bool">Bool</a> <a href="#v:-47--61-" class="selflink">#</a></p></div></div></td></tr><tr><td class="src clearfix"><span class="inst-left"><span id="control.i:id:KripkeStructure:Read:2" class="instance expander" onclick="toggleSection('i:id:KripkeStructure:Read:2')"></span> <a href="../base-4.9.1.0/Text-Read.html#t:Read">Read</a> a => <a href="../base-4.9.1.0/Text-Read.html#t:Read">Read</a> (<a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> a)</span> <a href="src/Logic.Model.html#line-51" class="link">Source</a> <a href="#t:KripkeStructure" class="selflink">#</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div id="section.i:id:KripkeStructure:Read:2" class="inst-details hide"><div class="subs methods"><p class="caption">Methods</p><p class="src"><a href="#v:readsPrec">readsPrec</a> :: <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a> -> <a href="../base-4.9.1.0/Text-ParserCombinators-ReadP.html#t:ReadS">ReadS</a> (<a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> a) <a href="#v:readsPrec" class="selflink">#</a></p><p class="src"><a href="#v:readList">readList</a> :: <a href="../base-4.9.1.0/Text-ParserCombinators-ReadP.html#t:ReadS">ReadS</a> [<a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> a] <a href="#v:readList" class="selflink">#</a></p><p class="src"><a href="#v:readPrec">readPrec</a> :: <a href="../base-4.9.1.0/Text-ParserCombinators-ReadPrec.html#t:ReadPrec">ReadPrec</a> (<a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> a) <a href="#v:readPrec" class="selflink">#</a></p><p class="src"><a href="#v:readListPrec">readListPrec</a> :: <a href="../base-4.9.1.0/Text-ParserCombinators-ReadPrec.html#t:ReadPrec">ReadPrec</a> [<a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> a] <a href="#v:readListPrec" class="selflink">#</a></p></div></div></td></tr><tr><td class="src clearfix"><span class="inst-left"><span id="control.i:id:KripkeStructure:Show:3" class="instance expander" onclick="toggleSection('i:id:KripkeStructure:Show:3')"></span> <a href="../base-4.9.1.0/Text-Show.html#t:Show">Show</a> a => <a href="../base-4.9.1.0/Text-Show.html#t:Show">Show</a> (<a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> a)</span> <a href="src/Logic.Model.html#line-51" class="link">Source</a> <a href="#t:KripkeStructure" class="selflink">#</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div id="section.i:id:KripkeStructure:Show:3" class="inst-details hide"><div class="subs methods"><p class="caption">Methods</p><p class="src"><a href="#v:showsPrec">showsPrec</a> :: <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a> -> <a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> a -> <a href="../base-4.9.1.0/Text-Show.html#t:ShowS">ShowS</a> <a href="#v:showsPrec" class="selflink">#</a></p><p class="src"><a href="#v:show">show</a> :: <a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> a -> <a href="../base-4.9.1.0/Data-String.html#t:String">String</a> <a href="#v:show" class="selflink">#</a></p><p class="src"><a href="#v:showList">showList</a> :: [<a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> a] -> <a href="../base-4.9.1.0/Text-Show.html#t:ShowS">ShowS</a> <a href="#v:showList" class="selflink">#</a></p></div></div></td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a id="t:State" class="def">State</a> a <a href="src/Logic.Model.html#State" class="link">Source</a> <a href="#t:State" class="selflink">#</a></p><div class="doc"><p>A state contains its unique identifier and a list of atomic
propositions that hold in it.</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a id="v:State" class="def">State</a> <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a> [a]</td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:State" class="caption collapser" onclick="toggleSection('i:State')">Instances</p><div id="section.i:State" class="show"><table><tr><td class="src clearfix"><span class="inst-left"><span id="control.i:id:State:Eq:1" class="instance expander" onclick="toggleSection('i:id:State:Eq:1')"></span> <a href="../base-4.9.1.0/Data-Eq.html#t:Eq">Eq</a> a => <a href="../base-4.9.1.0/Data-Eq.html#t:Eq">Eq</a> (<a href="Logic-Model.html#t:State">State</a> a)</span> <a href="src/Logic.Model.html#line-58" class="link">Source</a> <a href="#t:State" class="selflink">#</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div id="section.i:id:State:Eq:1" class="inst-details hide"><div class="subs methods"><p class="caption">Methods</p><p class="src"><a href="#v:-61--61-">(==)</a> :: <a href="Logic-Model.html#t:State">State</a> a -> <a href="Logic-Model.html#t:State">State</a> a -> <a href="../base-4.9.1.0/Data-Bool.html#t:Bool">Bool</a> <a href="#v:-61--61-" class="selflink">#</a></p><p class="src"><a href="#v:-47--61-">(/=)</a> :: <a href="Logic-Model.html#t:State">State</a> a -> <a href="Logic-Model.html#t:State">State</a> a -> <a href="../base-4.9.1.0/Data-Bool.html#t:Bool">Bool</a> <a href="#v:-47--61-" class="selflink">#</a></p></div></div></td></tr><tr><td class="src clearfix"><span class="inst-left"><span id="control.i:id:State:Read:2" class="instance expander" onclick="toggleSection('i:id:State:Read:2')"></span> <a href="../base-4.9.1.0/Text-Read.html#t:Read">Read</a> a => <a href="../base-4.9.1.0/Text-Read.html#t:Read">Read</a> (<a href="Logic-Model.html#t:State">State</a> a)</span> <a href="src/Logic.Model.html#line-58" class="link">Source</a> <a href="#t:State" class="selflink">#</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div id="section.i:id:State:Read:2" class="inst-details hide"><div class="subs methods"><p class="caption">Methods</p><p class="src"><a href="#v:readsPrec">readsPrec</a> :: <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a> -> <a href="../base-4.9.1.0/Text-ParserCombinators-ReadP.html#t:ReadS">ReadS</a> (<a href="Logic-Model.html#t:State">State</a> a) <a href="#v:readsPrec" class="selflink">#</a></p><p class="src"><a href="#v:readList">readList</a> :: <a href="../base-4.9.1.0/Text-ParserCombinators-ReadP.html#t:ReadS">ReadS</a> [<a href="Logic-Model.html#t:State">State</a> a] <a href="#v:readList" class="selflink">#</a></p><p class="src"><a href="#v:readPrec">readPrec</a> :: <a href="../base-4.9.1.0/Text-ParserCombinators-ReadPrec.html#t:ReadPrec">ReadPrec</a> (<a href="Logic-Model.html#t:State">State</a> a) <a href="#v:readPrec" class="selflink">#</a></p><p class="src"><a href="#v:readListPrec">readListPrec</a> :: <a href="../base-4.9.1.0/Text-ParserCombinators-ReadPrec.html#t:ReadPrec">ReadPrec</a> [<a href="Logic-Model.html#t:State">State</a> a] <a href="#v:readListPrec" class="selflink">#</a></p></div></div></td></tr><tr><td class="src clearfix"><span class="inst-left"><span id="control.i:id:State:Show:3" class="instance expander" onclick="toggleSection('i:id:State:Show:3')"></span> <a href="../base-4.9.1.0/Text-Show.html#t:Show">Show</a> a => <a href="../base-4.9.1.0/Text-Show.html#t:Show">Show</a> (<a href="Logic-Model.html#t:State">State</a> a)</span> <a href="src/Logic.Model.html#line-58" class="link">Source</a> <a href="#t:State" class="selflink">#</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div id="section.i:id:State:Show:3" class="inst-details hide"><div class="subs methods"><p class="caption">Methods</p><p class="src"><a href="#v:showsPrec">showsPrec</a> :: <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a> -> <a href="Logic-Model.html#t:State">State</a> a -> <a href="../base-4.9.1.0/Text-Show.html#t:ShowS">ShowS</a> <a href="#v:showsPrec" class="selflink">#</a></p><p class="src"><a href="#v:show">show</a> :: <a href="Logic-Model.html#t:State">State</a> a -> <a href="../base-4.9.1.0/Data-String.html#t:String">String</a> <a href="#v:show" class="selflink">#</a></p><p class="src"><a href="#v:showList">showList</a> :: [<a href="Logic-Model.html#t:State">State</a> a] -> <a href="../base-4.9.1.0/Text-Show.html#t:ShowS">ShowS</a> <a href="#v:showList" class="selflink">#</a></p></div></div></td></tr><tr><td class="src clearfix"><span class="inst-left"><span id="control.i:id:State:Element:4" class="instance expander" onclick="toggleSection('i:id:State:Element:4')"></span> <a href="Logic-Model.html#t:Element">Element</a> (<a href="Logic-Model.html#t:State">State</a> a)</span> <a href="src/Logic.Model.html#line-144" class="link">Source</a> <a href="#t:State" class="selflink">#</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div id="section.i:id:State:Element:4" class="inst-details hide"><div class="subs associated-types"><p class="caption">Associated Types</p><p class="src"><span class="keyword">type</span> <a href="Logic-Model.html#t:Payload">Payload</a> (<a href="Logic-Model.html#t:State">State</a> a) :: <a href="../base-4.9.1.0/Data-Kind.html#t:-42-">*</a> <a href="src/Logic.Model.html#Payload" class="link">Source</a> <a href="#t:Payload" class="selflink">#</a></p></div> <div class="subs methods"><p class="caption">Methods</p><p class="src"><a href="#v:elementId">elementId</a> :: <a href="Logic-Model.html#t:State">State</a> a -> <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a> <a href="src/Logic.Model.html#elementId" class="link">Source</a> <a href="#v:elementId" class="selflink">#</a></p><p class="src"><a href="#v:values">values</a> :: <a href="Logic-Model.html#t:State">State</a> a -> [<a href="Logic-Model.html#t:Payload">Payload</a> (<a href="Logic-Model.html#t:State">State</a> a)] <a href="src/Logic.Model.html#values" class="link">Source</a> <a href="#v:values" class="selflink">#</a></p></div></div></td></tr><tr><td class="src clearfix"><span class="inst-left"><span id="control.i:id:State:Payload:5" class="instance expander" onclick="toggleSection('i:id:State:Payload:5')"></span> <span class="keyword">type</span> <a href="Logic-Model.html#t:Payload">Payload</a> (<a href="Logic-Model.html#t:State">State</a> a)</span> <a href="src/Logic.Model.html#line-145" class="link">Source</a> <a href="#t:State" class="selflink">#</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div id="section.i:id:State:Payload:5" class="inst-details hide"><div class="src"><span class="keyword">type</span> <a href="Logic-Model.html#t:Payload">Payload</a> (<a href="Logic-Model.html#t:State">State</a> a) = a</div></div></td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a id="t:Transition" class="def">Transition</a> a <a href="src/Logic.Model.html#Transition" class="link">Source</a> <a href="#t:Transition" class="selflink">#</a></p><div class="doc"><p>A transition contains the identifiers of the source and target states.</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a id="v:Transition" class="def">Transition</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div class="subs fields"><p class="caption">Fields</p><ul><li><dfn class="src"><a id="v:transitionId" class="def">transitionId</a> :: <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a></dfn><div class="doc empty"> </div></li><li><dfn class="src"><a id="v:source" class="def">source</a> :: <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a></dfn><div class="doc empty"> </div></li><li><dfn class="src"><a id="v:target" class="def">target</a> :: <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a></dfn><div class="doc empty"> </div></li><li><dfn class="src"><a id="v:transitionPayload" class="def">transitionPayload</a> :: [a]</dfn><div class="doc empty"> </div></li></ul></div></td></tr></table></div><div class="subs instances"><p id="control.i:Transition" class="caption collapser" onclick="toggleSection('i:Transition')">Instances</p><div id="section.i:Transition" class="show"><table><tr><td class="src clearfix"><span class="inst-left"><span id="control.i:id:Transition:Eq:1" class="instance expander" onclick="toggleSection('i:id:Transition:Eq:1')"></span> <a href="../base-4.9.1.0/Data-Eq.html#t:Eq">Eq</a> a => <a href="../base-4.9.1.0/Data-Eq.html#t:Eq">Eq</a> (<a href="Logic-Model.html#t:Transition">Transition</a> a)</span> <a href="src/Logic.Model.html#line-68" class="link">Source</a> <a href="#t:Transition" class="selflink">#</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div id="section.i:id:Transition:Eq:1" class="inst-details hide"><div class="subs methods"><p class="caption">Methods</p><p class="src"><a href="#v:-61--61-">(==)</a> :: <a href="Logic-Model.html#t:Transition">Transition</a> a -> <a href="Logic-Model.html#t:Transition">Transition</a> a -> <a href="../base-4.9.1.0/Data-Bool.html#t:Bool">Bool</a> <a href="#v:-61--61-" class="selflink">#</a></p><p class="src"><a href="#v:-47--61-">(/=)</a> :: <a href="Logic-Model.html#t:Transition">Transition</a> a -> <a href="Logic-Model.html#t:Transition">Transition</a> a -> <a href="../base-4.9.1.0/Data-Bool.html#t:Bool">Bool</a> <a href="#v:-47--61-" class="selflink">#</a></p></div></div></td></tr><tr><td class="src clearfix"><span class="inst-left"><span id="control.i:id:Transition:Read:2" class="instance expander" onclick="toggleSection('i:id:Transition:Read:2')"></span> <a href="../base-4.9.1.0/Text-Read.html#t:Read">Read</a> a => <a href="../base-4.9.1.0/Text-Read.html#t:Read">Read</a> (<a href="Logic-Model.html#t:Transition">Transition</a> a)</span> <a href="src/Logic.Model.html#line-68" class="link">Source</a> <a href="#t:Transition" class="selflink">#</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div id="section.i:id:Transition:Read:2" class="inst-details hide"><div class="subs methods"><p class="caption">Methods</p><p class="src"><a href="#v:readsPrec">readsPrec</a> :: <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a> -> <a href="../base-4.9.1.0/Text-ParserCombinators-ReadP.html#t:ReadS">ReadS</a> (<a href="Logic-Model.html#t:Transition">Transition</a> a) <a href="#v:readsPrec" class="selflink">#</a></p><p class="src"><a href="#v:readList">readList</a> :: <a href="../base-4.9.1.0/Text-ParserCombinators-ReadP.html#t:ReadS">ReadS</a> [<a href="Logic-Model.html#t:Transition">Transition</a> a] <a href="#v:readList" class="selflink">#</a></p><p class="src"><a href="#v:readPrec">readPrec</a> :: <a href="../base-4.9.1.0/Text-ParserCombinators-ReadPrec.html#t:ReadPrec">ReadPrec</a> (<a href="Logic-Model.html#t:Transition">Transition</a> a) <a href="#v:readPrec" class="selflink">#</a></p><p class="src"><a href="#v:readListPrec">readListPrec</a> :: <a href="../base-4.9.1.0/Text-ParserCombinators-ReadPrec.html#t:ReadPrec">ReadPrec</a> [<a href="Logic-Model.html#t:Transition">Transition</a> a] <a href="#v:readListPrec" class="selflink">#</a></p></div></div></td></tr><tr><td class="src clearfix"><span class="inst-left"><span id="control.i:id:Transition:Show:3" class="instance expander" onclick="toggleSection('i:id:Transition:Show:3')"></span> <a href="../base-4.9.1.0/Text-Show.html#t:Show">Show</a> a => <a href="../base-4.9.1.0/Text-Show.html#t:Show">Show</a> (<a href="Logic-Model.html#t:Transition">Transition</a> a)</span> <a href="src/Logic.Model.html#line-68" class="link">Source</a> <a href="#t:Transition" class="selflink">#</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div id="section.i:id:Transition:Show:3" class="inst-details hide"><div class="subs methods"><p class="caption">Methods</p><p class="src"><a href="#v:showsPrec">showsPrec</a> :: <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a> -> <a href="Logic-Model.html#t:Transition">Transition</a> a -> <a href="../base-4.9.1.0/Text-Show.html#t:ShowS">ShowS</a> <a href="#v:showsPrec" class="selflink">#</a></p><p class="src"><a href="#v:show">show</a> :: <a href="Logic-Model.html#t:Transition">Transition</a> a -> <a href="../base-4.9.1.0/Data-String.html#t:String">String</a> <a href="#v:show" class="selflink">#</a></p><p class="src"><a href="#v:showList">showList</a> :: [<a href="Logic-Model.html#t:Transition">Transition</a> a] -> <a href="../base-4.9.1.0/Text-Show.html#t:ShowS">ShowS</a> <a href="#v:showList" class="selflink">#</a></p></div></div></td></tr><tr><td class="src clearfix"><span class="inst-left"><span id="control.i:id:Transition:Element:4" class="instance expander" onclick="toggleSection('i:id:Transition:Element:4')"></span> <a href="Logic-Model.html#t:Element">Element</a> (<a href="Logic-Model.html#t:Transition">Transition</a> a)</span> <a href="src/Logic.Model.html#line-151" class="link">Source</a> <a href="#t:Transition" class="selflink">#</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div id="section.i:id:Transition:Element:4" class="inst-details hide"><div class="subs associated-types"><p class="caption">Associated Types</p><p class="src"><span class="keyword">type</span> <a href="Logic-Model.html#t:Payload">Payload</a> (<a href="Logic-Model.html#t:Transition">Transition</a> a) :: <a href="../base-4.9.1.0/Data-Kind.html#t:-42-">*</a> <a href="src/Logic.Model.html#Payload" class="link">Source</a> <a href="#t:Payload" class="selflink">#</a></p></div> <div class="subs methods"><p class="caption">Methods</p><p class="src"><a href="#v:elementId">elementId</a> :: <a href="Logic-Model.html#t:Transition">Transition</a> a -> <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a> <a href="src/Logic.Model.html#elementId" class="link">Source</a> <a href="#v:elementId" class="selflink">#</a></p><p class="src"><a href="#v:values">values</a> :: <a href="Logic-Model.html#t:Transition">Transition</a> a -> [<a href="Logic-Model.html#t:Payload">Payload</a> (<a href="Logic-Model.html#t:Transition">Transition</a> a)] <a href="src/Logic.Model.html#values" class="link">Source</a> <a href="#v:values" class="selflink">#</a></p></div></div></td></tr><tr><td class="src clearfix"><span class="inst-left"><span id="control.i:id:Transition:Payload:5" class="instance expander" onclick="toggleSection('i:id:Transition:Payload:5')"></span> <span class="keyword">type</span> <a href="Logic-Model.html#t:Payload">Payload</a> (<a href="Logic-Model.html#t:Transition">Transition</a> a)</span> <a href="src/Logic.Model.html#line-152" class="link">Source</a> <a href="#t:Transition" class="selflink">#</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div id="section.i:id:Transition:Payload:5" class="inst-details hide"><div class="src"><span class="keyword">type</span> <a href="Logic-Model.html#t:Payload">Payload</a> (<a href="Logic-Model.html#t:Transition">Transition</a> a) = a</div></div></td></tr></table></div></div></div><h2 id="g:2">Looking up states</h2><div class="top"><p class="src"><a id="v:stateIds" class="def">stateIds</a> :: <a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> a -> [<a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a>] <a href="src/Logic.Model.html#stateIds" class="link">Source</a> <a href="#v:stateIds" class="selflink">#</a></p><div class="doc"><p>List of all state IDs from a given Kripke structure</p></div></div><div class="top"><p class="src"><a id="v:lookupState" class="def">lookupState</a> :: <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a> -> <a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> a -> <a href="../base-4.9.1.0/Data-Maybe.html#t:Maybe">Maybe</a> (<a href="Logic-Model.html#t:State">State</a> a) <a href="src/Logic.Model.html#lookupState" class="link">Source</a> <a href="#v:lookupState" class="selflink">#</a></p><div class="doc"><p>Finds the state with given ID in the given Kripke structure</p></div></div><div class="top"><p class="src"><a id="v:getState" class="def">getState</a> :: <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a> -> <a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> a -> <a href="Logic-Model.html#t:State">State</a> a <a href="src/Logic.Model.html#getState" class="link">Source</a> <a href="#v:getState" class="selflink">#</a></p><div class="doc"><p>Gets the state with given ID in the given Kripke structure, <strong>fails if there is none</strong>.</p></div></div><h2 id="g:3">Looking up transitions</h2><div class="top"><p class="src"><a id="v:transitionIds" class="def">transitionIds</a> :: <a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> a -> [<a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a>] <a href="src/Logic.Model.html#transitionIds" class="link">Source</a> <a href="#v:transitionIds" class="selflink">#</a></p><div class="doc"><p>List of all transition IDs on a given Kripke structure</p></div></div><div class="top"><p class="src"><a id="v:lookupTransition" class="def">lookupTransition</a> :: <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a> -> <a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> a -> <a href="../base-4.9.1.0/Data-Maybe.html#t:Maybe">Maybe</a> (<a href="Logic-Model.html#t:Transition">Transition</a> a) <a href="src/Logic.Model.html#lookupTransition" class="link">Source</a> <a href="#v:lookupTransition" class="selflink">#</a></p><div class="doc"><p>Finds the transition with given ID in the given Kripke structure.</p></div></div><div class="top"><p class="src"><a id="v:getTransition" class="def">getTransition</a> :: <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a> -> <a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> a -> <a href="Logic-Model.html#t:Transition">Transition</a> a <a href="src/Logic.Model.html#getTransition" class="link">Source</a> <a href="#v:getTransition" class="selflink">#</a></p><div class="doc"><p>Gets the transition with given ID in the given Kripke structure, <strong>fails if there is none</strong>.</p></div></div><h2 id="g:4">Lookup by adjacency</h2><div class="top"><p class="src"><a id="v:nextStates" class="def">nextStates</a> :: <a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> 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/Logic.Model.html#nextStates" class="link">Source</a> <a href="#v:nextStates" class="selflink">#</a></p><div class="doc"><p>Obtains the IDs of the states that are reachable by a single transition
from the state with given ID.</p></div></div><div class="top"><p class="src"><a id="v:precedes" class="def">precedes</a> :: <a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> 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="../base-4.9.1.0/Data-Bool.html#t:Bool">Bool</a> <a href="src/Logic.Model.html#precedes" class="link">Source</a> <a href="#v:precedes" class="selflink">#</a></p><div class="doc"><p>Tests if the second given state is reachable from the first by a single transition</p></div></div><div class="top"><p class="src"><a id="v:prevStates" class="def">prevStates</a> :: <a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> 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/Logic.Model.html#prevStates" class="link">Source</a> <a href="#v:prevStates" class="selflink">#</a></p><div class="doc"><p>Obtains the IDs of the states from which the given state is reachable by a single transition.</p></div></div><div class="top"><p class="src"><a id="v:follows" class="def">follows</a> :: <a href="Logic-Model.html#t:KripkeStructure">KripkeStructure</a> 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="../base-4.9.1.0/Data-Bool.html#t:Bool">Bool</a> <a href="src/Logic.Model.html#follows" class="link">Source</a> <a href="#v:follows" class="selflink">#</a></p><div class="doc"><p>Tests if the first given state is reachable from the second by a single transition</p></div></div><h1 id="g:5">Utilities for labeled elements</h1><div class="top"><p class="src"><span class="keyword">class</span> <a id="t:Element" class="def">Element</a> e <span class="keyword">where</span> <a href="src/Logic.Model.html#Element" class="link">Source</a> <a href="#t:Element" class="selflink">#</a></p><div class="doc"><p>Type class for elements that have a numeric identifier and a list of associated values.</p></div><div class="subs minimal"><p class="caption">Minimal complete definition</p><p class="src"><a href="Logic-Model.html#v:elementId">elementId</a>, <a href="Logic-Model.html#v:values">values</a></p></div><div class="subs associated-types"><p class="caption">Associated Types</p><p class="src"><span class="keyword">type</span> <a id="t:Payload" class="def">Payload</a> e :: <a href="../base-4.9.1.0/Data-Kind.html#t:-42-">*</a> <a href="src/Logic.Model.html#Payload" class="link">Source</a> <a href="#t:Payload" class="selflink">#</a></p><div class="doc"><p>Type of associated values.</p></div></div><div class="subs methods"><p class="caption">Methods</p><p class="src"><a id="v:elementId" class="def">elementId</a> :: e -> <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a> <a href="src/Logic.Model.html#elementId" class="link">Source</a> <a href="#v:elementId" class="selflink">#</a></p><div class="doc"><p>Obtain the numeric identifier of an element.</p></div><p class="src"><a id="v:values" class="def">values</a> :: e -> [<a href="Logic-Model.html#t:Payload">Payload</a> e] <a href="src/Logic.Model.html#values" class="link">Source</a> <a href="#v:values" class="selflink">#</a></p><div class="doc"><p>Obtain the associated values of an element.</p></div></div><div class="subs instances"><p id="control.i:Element" class="caption collapser" onclick="toggleSection('i:Element')">Instances</p><div id="section.i:Element" class="show"><table><tr><td class="src clearfix"><span class="inst-left"><span id="control.i:ic:Element:Element:1" class="instance expander" onclick="toggleSection('i:ic:Element:Element:1')"></span> <a href="Logic-Model.html#t:Element">Element</a> (<a href="Logic-Model.html#t:Transition">Transition</a> a)</span> <a href="src/Logic.Model.html#line-151" class="link">Source</a> <a href="#t:Element" class="selflink">#</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div id="section.i:ic:Element:Element:1" class="inst-details hide"><div class="subs associated-types"><p class="caption">Associated Types</p><p class="src"><span class="keyword">type</span> <a href="Logic-Model.html#t:Payload">Payload</a> (<a href="Logic-Model.html#t:Transition">Transition</a> a) :: <a href="../base-4.9.1.0/Data-Kind.html#t:-42-">*</a> <a href="src/Logic.Model.html#Payload" class="link">Source</a> <a href="#t:Payload" class="selflink">#</a></p></div> <div class="subs methods"><p class="caption">Methods</p><p class="src"><a href="#v:elementId">elementId</a> :: <a href="Logic-Model.html#t:Transition">Transition</a> a -> <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a> <a href="src/Logic.Model.html#elementId" class="link">Source</a> <a href="#v:elementId" class="selflink">#</a></p><p class="src"><a href="#v:values">values</a> :: <a href="Logic-Model.html#t:Transition">Transition</a> a -> [<a href="Logic-Model.html#t:Payload">Payload</a> (<a href="Logic-Model.html#t:Transition">Transition</a> a)] <a href="src/Logic.Model.html#values" class="link">Source</a> <a href="#v:values" class="selflink">#</a></p></div></div></td></tr><tr><td class="src clearfix"><span class="inst-left"><span id="control.i:ic:Element:Element:2" class="instance expander" onclick="toggleSection('i:ic:Element:Element:2')"></span> <a href="Logic-Model.html#t:Element">Element</a> (<a href="Logic-Model.html#t:State">State</a> a)</span> <a href="src/Logic.Model.html#line-144" class="link">Source</a> <a href="#t:Element" class="selflink">#</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div id="section.i:ic:Element:Element:2" class="inst-details hide"><div class="subs associated-types"><p class="caption">Associated Types</p><p class="src"><span class="keyword">type</span> <a href="Logic-Model.html#t:Payload">Payload</a> (<a href="Logic-Model.html#t:State">State</a> a) :: <a href="../base-4.9.1.0/Data-Kind.html#t:-42-">*</a> <a href="src/Logic.Model.html#Payload" class="link">Source</a> <a href="#t:Payload" class="selflink">#</a></p></div> <div class="subs methods"><p class="caption">Methods</p><p class="src"><a href="#v:elementId">elementId</a> :: <a href="Logic-Model.html#t:State">State</a> a -> <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a> <a href="src/Logic.Model.html#elementId" class="link">Source</a> <a href="#v:elementId" class="selflink">#</a></p><p class="src"><a href="#v:values">values</a> :: <a href="Logic-Model.html#t:State">State</a> a -> [<a href="Logic-Model.html#t:Payload">Payload</a> (<a href="Logic-Model.html#t:State">State</a> a)] <a href="src/Logic.Model.html#values" class="link">Source</a> <a href="#v:values" class="selflink">#</a></p></div></div></td></tr></table></div></div></div><div class="top"><p class="src"><a id="v:findById" class="def">findById</a> :: <a href="Logic-Model.html#t:Element">Element</a> a => <a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a> -> [a] -> <a href="../base-4.9.1.0/Data-Maybe.html#t:Maybe">Maybe</a> a <a href="src/Logic.Model.html#findById" class="link">Source</a> <a href="#v:findById" class="selflink">#</a></p><div class="doc"><p>Given a list of elements, find the element with the given identifier.</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>