-
Notifications
You must be signed in to change notification settings - Fork 1
/
Logic-Ctl.html
7 lines (7 loc) · 24.4 KB
/
Logic-Ctl.html
1
2
3
4
5
6
7
<!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.Ctl</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-Ctl.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Logic.Ctl.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 <ggazzi@inf.ufrgs.br></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.Ctl</p></div><div id="table-of-contents"><p class="caption">Contents</p><ul><li><a href="#g:1">CTL Expressions</a></li><li><a href="#g:2">Model checking</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:Expr">Expr</a><ul class="subs"><li>= <a href="#v:Literal">Literal</a> <a href="../base-4.9.1.0/Data-Bool.html#t:Bool">Bool</a></li><li>| <a href="#v:Atom">Atom</a> <a href="../base-4.9.1.0/Data-String.html#t:String">String</a></li><li>| <a href="#v:Not">Not</a> <a href="Logic-Ctl.html#t:Expr">Expr</a></li><li>| <a href="#v:And">And</a> <a href="Logic-Ctl.html#t:Expr">Expr</a> <a href="Logic-Ctl.html#t:Expr">Expr</a></li><li>| <a href="#v:Or">Or</a> <a href="Logic-Ctl.html#t:Expr">Expr</a> <a href="Logic-Ctl.html#t:Expr">Expr</a></li><li>| <a href="#v:Implies">Implies</a> <a href="Logic-Ctl.html#t:Expr">Expr</a> <a href="Logic-Ctl.html#t:Expr">Expr</a></li><li>| <a href="#v:Equiv">Equiv</a> <a href="Logic-Ctl.html#t:Expr">Expr</a> <a href="Logic-Ctl.html#t:Expr">Expr</a></li><li>| <a href="#v:Temporal">Temporal</a> (<a href="Logic-Ctl.html#t:PathQuantified">PathQuantified</a> <a href="Logic-Ctl.html#t:Expr">Expr</a>)</li></ul></li><li class="src short"><span class="keyword">data</span> <a href="#t:PathQuantified">PathQuantified</a> e<ul class="subs"><li>= <a href="#v:A">A</a> (<a href="Logic-Ctl.html#t:StateQuantified">StateQuantified</a> e)</li><li>| <a href="#v:E">E</a> (<a href="Logic-Ctl.html#t:StateQuantified">StateQuantified</a> e)</li></ul></li><li class="src short"><span class="keyword">data</span> <a href="#t:StateQuantified">StateQuantified</a> e<ul class="subs"><li>= <a href="#v:X">X</a> e</li><li>| <a href="#v:G">G</a> e</li><li>| <a href="#v:F">F</a> e</li><li>| <a href="#v:U">U</a> e e</li></ul></li><li class="src short"><a href="#v:parseExpr">parseExpr</a> :: SourceName -> <a href="../base-4.9.1.0/Data-String.html#t:String">String</a> -> <a href="../base-4.9.1.0/Data-Either.html#t:Either">Either</a> ParseError <a href="Logic-Ctl.html#t:Expr">Expr</a></li><li class="src short"><a href="#v:check">check</a> :: <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="Logic-Ctl.html#t:Expr">Expr</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:satisfyExpr">satisfyExpr</a> :: <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="Logic-Ctl.html#t:Expr">Expr</a> -> [<a href="Logic-Model.html#t:State">State</a> <a href="../base-4.9.1.0/Data-String.html#t:String">String</a>]</li><li class="src short"><a href="#v:satisfyExpr-39-">satisfyExpr'</a> :: <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="Logic-Ctl.html#t:Expr">Expr</a> -> [<a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a>]</li></ul></div><div id="interface"><h1 id="g:1">CTL Expressions</h1><div class="top"><p class="src"><span class="keyword">data</span> <a id="t:Expr" class="def">Expr</a> <a href="src/Logic.Ctl.Base.html#Expr" class="link">Source</a> <a href="#t:Expr" class="selflink">#</a></p><div class="doc"><p>CTL expressions</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a id="v:Literal" class="def">Literal</a> <a href="../base-4.9.1.0/Data-Bool.html#t:Bool">Bool</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a id="v:Atom" class="def">Atom</a> <a href="../base-4.9.1.0/Data-String.html#t:String">String</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a id="v:Not" class="def">Not</a> <a href="Logic-Ctl.html#t:Expr">Expr</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a id="v:And" class="def">And</a> <a href="Logic-Ctl.html#t:Expr">Expr</a> <a href="Logic-Ctl.html#t:Expr">Expr</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a id="v:Or" class="def">Or</a> <a href="Logic-Ctl.html#t:Expr">Expr</a> <a href="Logic-Ctl.html#t:Expr">Expr</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a id="v:Implies" class="def">Implies</a> <a href="Logic-Ctl.html#t:Expr">Expr</a> <a href="Logic-Ctl.html#t:Expr">Expr</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a id="v:Equiv" class="def">Equiv</a> <a href="Logic-Ctl.html#t:Expr">Expr</a> <a href="Logic-Ctl.html#t:Expr">Expr</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a id="v:Temporal" class="def">Temporal</a> (<a href="Logic-Ctl.html#t:PathQuantified">PathQuantified</a> <a href="Logic-Ctl.html#t:Expr">Expr</a>)</td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:Expr" class="caption collapser" onclick="toggleSection('i:Expr')">Instances</p><div id="section.i:Expr" class="show"><table><tr><td class="src clearfix"><span class="inst-left"><span id="control.i:id:Expr:Eq:1" class="instance expander" onclick="toggleSection('i:id:Expr:Eq:1')"></span> <a href="../base-4.9.1.0/Data-Eq.html#t:Eq">Eq</a> <a href="Logic-Ctl.html#t:Expr">Expr</a></span> <a href="src/Logic.Ctl.Base.html#line-20" class="link">Source</a> <a href="#t:Expr" class="selflink">#</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div id="section.i:id:Expr: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-Ctl.html#t:Expr">Expr</a> -> <a href="Logic-Ctl.html#t:Expr">Expr</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-Ctl.html#t:Expr">Expr</a> -> <a href="Logic-Ctl.html#t:Expr">Expr</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:Expr:Read:2" class="instance expander" onclick="toggleSection('i:id:Expr:Read:2')"></span> <a href="../base-4.9.1.0/Text-Read.html#t:Read">Read</a> <a href="Logic-Ctl.html#t:Expr">Expr</a></span> <a href="src/Logic.Ctl.Base.html#line-20" class="link">Source</a> <a href="#t:Expr" class="selflink">#</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div id="section.i:id:Expr: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-Ctl.html#t:Expr">Expr</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-Ctl.html#t:Expr">Expr</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-Ctl.html#t:Expr">Expr</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-Ctl.html#t:Expr">Expr</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:Expr:Show:3" class="instance expander" onclick="toggleSection('i:id:Expr:Show:3')"></span> <a href="../base-4.9.1.0/Text-Show.html#t:Show">Show</a> <a href="Logic-Ctl.html#t:Expr">Expr</a></span> <a href="src/Logic.Ctl.Base.html#line-20" class="link">Source</a> <a href="#t:Expr" class="selflink">#</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div id="section.i:id:Expr: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-Ctl.html#t:Expr">Expr</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-Ctl.html#t:Expr">Expr</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-Ctl.html#t:Expr">Expr</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:Expr:Pretty:4" class="instance expander" onclick="toggleSection('i:id:Expr:Pretty:4')"></span> Pretty <a href="Logic-Ctl.html#t:Expr">Expr</a></span> <a href="src/Logic.Ctl.Base.html#line-39" class="link">Source</a> <a href="#t:Expr" class="selflink">#</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div id="section.i:id:Expr:Pretty:4" class="inst-details hide"><div class="subs methods"><p class="caption">Methods</p><p class="src"><a href="#v:pretty">pretty</a> :: <a href="Logic-Ctl.html#t:Expr">Expr</a> -> Doc</p><p class="src"><a href="#v:prettyList">prettyList</a> :: [<a href="Logic-Ctl.html#t:Expr">Expr</a>] -> Doc</p></div></div></td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a id="t:PathQuantified" class="def">PathQuantified</a> e <a href="src/Logic.Ctl.Base.html#PathQuantified" class="link">Source</a> <a href="#t:PathQuantified" class="selflink">#</a></p><div class="doc"><p>Path-quantified CTL expressions</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a id="v:A" class="def">A</a> (<a href="Logic-Ctl.html#t:StateQuantified">StateQuantified</a> e)</td><td class="doc empty"> </td></tr><tr><td class="src"><a id="v:E" class="def">E</a> (<a href="Logic-Ctl.html#t:StateQuantified">StateQuantified</a> e)</td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:PathQuantified" class="caption collapser" onclick="toggleSection('i:PathQuantified')">Instances</p><div id="section.i:PathQuantified" class="show"><table><tr><td class="src clearfix"><span class="inst-left"><span id="control.i:id:PathQuantified:Eq:1" class="instance expander" onclick="toggleSection('i:id:PathQuantified:Eq:1')"></span> <a href="../base-4.9.1.0/Data-Eq.html#t:Eq">Eq</a> e => <a href="../base-4.9.1.0/Data-Eq.html#t:Eq">Eq</a> (<a href="Logic-Ctl.html#t:PathQuantified">PathQuantified</a> e)</span> <a href="src/Logic.Ctl.Base.html#line-27" class="link">Source</a> <a href="#t:PathQuantified" class="selflink">#</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div id="section.i:id:PathQuantified: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-Ctl.html#t:PathQuantified">PathQuantified</a> e -> <a href="Logic-Ctl.html#t:PathQuantified">PathQuantified</a> e -> <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-Ctl.html#t:PathQuantified">PathQuantified</a> e -> <a href="Logic-Ctl.html#t:PathQuantified">PathQuantified</a> e -> <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:PathQuantified:Read:2" class="instance expander" onclick="toggleSection('i:id:PathQuantified:Read:2')"></span> <a href="../base-4.9.1.0/Text-Read.html#t:Read">Read</a> e => <a href="../base-4.9.1.0/Text-Read.html#t:Read">Read</a> (<a href="Logic-Ctl.html#t:PathQuantified">PathQuantified</a> e)</span> <a href="src/Logic.Ctl.Base.html#line-27" class="link">Source</a> <a href="#t:PathQuantified" class="selflink">#</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div id="section.i:id:PathQuantified: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-Ctl.html#t:PathQuantified">PathQuantified</a> e) <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-Ctl.html#t:PathQuantified">PathQuantified</a> e] <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-Ctl.html#t:PathQuantified">PathQuantified</a> e) <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-Ctl.html#t:PathQuantified">PathQuantified</a> e] <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:PathQuantified:Show:3" class="instance expander" onclick="toggleSection('i:id:PathQuantified:Show:3')"></span> <a href="../base-4.9.1.0/Text-Show.html#t:Show">Show</a> e => <a href="../base-4.9.1.0/Text-Show.html#t:Show">Show</a> (<a href="Logic-Ctl.html#t:PathQuantified">PathQuantified</a> e)</span> <a href="src/Logic.Ctl.Base.html#line-27" class="link">Source</a> <a href="#t:PathQuantified" class="selflink">#</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div id="section.i:id:PathQuantified: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-Ctl.html#t:PathQuantified">PathQuantified</a> e -> <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-Ctl.html#t:PathQuantified">PathQuantified</a> e -> <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-Ctl.html#t:PathQuantified">PathQuantified</a> e] -> <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:StateQuantified" class="def">StateQuantified</a> e <a href="src/Logic.Ctl.Base.html#StateQuantified" class="link">Source</a> <a href="#t:StateQuantified" class="selflink">#</a></p><div class="doc"><p>State-quantified CTL expressions</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a id="v:X" class="def">X</a> e</td><td class="doc empty"> </td></tr><tr><td class="src"><a id="v:G" class="def">G</a> e</td><td class="doc empty"> </td></tr><tr><td class="src"><a id="v:F" class="def">F</a> e</td><td class="doc empty"> </td></tr><tr><td class="src"><a id="v:U" class="def">U</a> e e</td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:StateQuantified" class="caption collapser" onclick="toggleSection('i:StateQuantified')">Instances</p><div id="section.i:StateQuantified" class="show"><table><tr><td class="src clearfix"><span class="inst-left"><span id="control.i:id:StateQuantified:Eq:1" class="instance expander" onclick="toggleSection('i:id:StateQuantified:Eq:1')"></span> <a href="../base-4.9.1.0/Data-Eq.html#t:Eq">Eq</a> e => <a href="../base-4.9.1.0/Data-Eq.html#t:Eq">Eq</a> (<a href="Logic-Ctl.html#t:StateQuantified">StateQuantified</a> e)</span> <a href="src/Logic.Ctl.Base.html#line-36" class="link">Source</a> <a href="#t:StateQuantified" class="selflink">#</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div id="section.i:id:StateQuantified: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-Ctl.html#t:StateQuantified">StateQuantified</a> e -> <a href="Logic-Ctl.html#t:StateQuantified">StateQuantified</a> e -> <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-Ctl.html#t:StateQuantified">StateQuantified</a> e -> <a href="Logic-Ctl.html#t:StateQuantified">StateQuantified</a> e -> <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:StateQuantified:Read:2" class="instance expander" onclick="toggleSection('i:id:StateQuantified:Read:2')"></span> <a href="../base-4.9.1.0/Text-Read.html#t:Read">Read</a> e => <a href="../base-4.9.1.0/Text-Read.html#t:Read">Read</a> (<a href="Logic-Ctl.html#t:StateQuantified">StateQuantified</a> e)</span> <a href="src/Logic.Ctl.Base.html#line-36" class="link">Source</a> <a href="#t:StateQuantified" class="selflink">#</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div id="section.i:id:StateQuantified: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-Ctl.html#t:StateQuantified">StateQuantified</a> e) <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-Ctl.html#t:StateQuantified">StateQuantified</a> e] <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-Ctl.html#t:StateQuantified">StateQuantified</a> e) <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-Ctl.html#t:StateQuantified">StateQuantified</a> e] <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:StateQuantified:Show:3" class="instance expander" onclick="toggleSection('i:id:StateQuantified:Show:3')"></span> <a href="../base-4.9.1.0/Text-Show.html#t:Show">Show</a> e => <a href="../base-4.9.1.0/Text-Show.html#t:Show">Show</a> (<a href="Logic-Ctl.html#t:StateQuantified">StateQuantified</a> e)</span> <a href="src/Logic.Ctl.Base.html#line-36" class="link">Source</a> <a href="#t:StateQuantified" class="selflink">#</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div id="section.i:id:StateQuantified: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-Ctl.html#t:StateQuantified">StateQuantified</a> e -> <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-Ctl.html#t:StateQuantified">StateQuantified</a> e -> <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-Ctl.html#t:StateQuantified">StateQuantified</a> e] -> <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"><a id="v:parseExpr" class="def">parseExpr</a> :: SourceName -> <a href="../base-4.9.1.0/Data-String.html#t:String">String</a> -> <a href="../base-4.9.1.0/Data-Either.html#t:Either">Either</a> ParseError <a href="Logic-Ctl.html#t:Expr">Expr</a> <a href="src/Logic.Ctl.Parser.html#parseExpr" class="link">Source</a> <a href="#v:parseExpr" class="selflink">#</a></p><div class="doc"><p>Parse a CTL expressions from the given string.</p><p>The first parameter will be used to identify the source of the
text in error messages.</p><p>This parser is compatible with the pretty printer of expressions,
that is, pretty printed expressions will be parseable by this
(unless they contain illegal identifiers for atomic propositions).</p></div></div><h1 id="g:2">Model checking</h1><div class="top"><p class="src"><a id="v:check" class="def">check</a> :: <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="Logic-Ctl.html#t:Expr">Expr</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.Ctl.html#check" class="link">Source</a> <a href="#v:check" class="selflink">#</a></p><div class="doc"><p>Check if the given expression holds in the given state of the Kripke structure.</p></div></div><div class="top"><p class="src"><a id="v:satisfyExpr" class="def">satisfyExpr</a> :: <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="Logic-Ctl.html#t:Expr">Expr</a> -> [<a href="Logic-Model.html#t:State">State</a> <a href="../base-4.9.1.0/Data-String.html#t:String">String</a>] <a href="src/Logic.Ctl.Semantics.html#satisfyExpr" class="link">Source</a> <a href="#v:satisfyExpr" class="selflink">#</a></p><div class="doc"><p>Obtain all states that satisfy the given CTL expression.</p></div></div><div class="top"><p class="src"><a id="v:satisfyExpr-39-" class="def">satisfyExpr'</a> :: <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="Logic-Ctl.html#t:Expr">Expr</a> -> [<a href="../base-4.9.1.0/Data-Int.html#t:Int">Int</a>] <a href="src/Logic.Ctl.Semantics.html#satisfyExpr%27" class="link">Source</a> <a href="#v:satisfyExpr-39-" class="selflink">#</a></p><div class="doc"><p>Obtain the identifiers of all states that satisfy the given CTL expression.</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>