Repository navigation
Expand file tree
/
Copy pathLanguage-Copilot-Libs-LTL.html
More file actions
48 lines (48 loc) · 9.78 KB
/
Copy pathLanguage-Copilot-Libs-LTL.html
File metadata and controls
48 lines (48 loc) · 9.78 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
<!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>Language.Copilot.Libs.LTL</title><link href="ocean.css" rel="stylesheet" type="text/css" title="Ocean" /><script src="haddock-util.js" type="text/javascript"></script><script type="text/javascript">//<![CDATA[
window.onload = function () {pageLoad();setSynopsis("mini_Language-Copilot-Libs-LTL.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="http://github.com/leepike/Copilot/Language.Copilot.Libs.LTL.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">copilot-0.28: A stream DSL for writing embedded C monitors.</p></div><div id="content"><div id="module-header"><p class="caption">Language.Copilot.Libs.LTL</p></div><div id="description"><p class="caption">Description</p><div class="doc"><p>Bounded Linear Temporal Logic (LTL) operators. For a bound <code>n</code>, a property
<code>p</code> holds if it holds on the next <code>n</code> transitions (between periods). If <code>n
== 0</code>, then the trace includes only the current period. For example,
<code>
always 3 p
</code>
holds if <code>p</code> holds at least once every four periods (3 transitions).
</p><p>Interface: see Examples/LTLExamples.hs You can embed a LTL specification
within a Copilot specification using the form:
<code>
var <code><a href="Language-Copilot-Libs-LTL.html#v:ltl">ltl</a></code> (operator spec)
</code>
where <code><a href="Language-Copilot-Language.html#v:var">var</a></code> is the variable you want to assign to the LTL specification
you're writing.
</p><p>For some properties, stream dependencies may not allow their specification.
In particular, you cannot determine the <a href="future.html">future</a> value of an external
variable. In general, the ptLTL library is probaby more useful.
</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"><a href="#v:ltl">ltl</a> :: <a href="Language-Copilot-Core.html#t:Spec">Spec</a> <a href="Language-Copilot-Language.html#t:Bool">Bool</a> -> (<a href="Language-Copilot-Core.html#t:Spec">Spec</a> <a href="Language-Copilot-Language.html#t:Bool">Bool</a> -> <a href="Language-Copilot-Core.html#t:Streams">Streams</a>) -> <a href="Language-Copilot-Core.html#t:Streams">Streams</a></li><li class="src short"><a href="#v:eventually">eventually</a> :: <a href="/Library/Frameworks/GHC.framework/Versions/612/usr/share/doc/ghc/html/libraries/base-4.2.0.2/Data-Int.html#t:Int">Int</a> -> <a href="Language-Copilot-Core.html#t:Spec">Spec</a> <a href="Language-Copilot-Language.html#t:Bool">Bool</a> -> <a href="Language-Copilot-Core.html#t:Spec">Spec</a> <a href="Language-Copilot-Language.html#t:Bool">Bool</a> -> <a href="Language-Copilot-Core.html#t:Streams">Streams</a></li><li class="src short"><a href="#v:next">next</a> :: <a href="Language-Copilot-Core.html#t:Spec">Spec</a> <a href="Language-Copilot-Language.html#t:Bool">Bool</a> -> <a href="Language-Copilot-Core.html#t:Spec">Spec</a> <a href="Language-Copilot-Language.html#t:Bool">Bool</a> -> <a href="Language-Copilot-Core.html#t:Streams">Streams</a></li><li class="src short"><a href="#v:always">always</a> :: <a href="/Library/Frameworks/GHC.framework/Versions/612/usr/share/doc/ghc/html/libraries/base-4.2.0.2/Data-Int.html#t:Int">Int</a> -> <a href="Language-Copilot-Core.html#t:Spec">Spec</a> <a href="Language-Copilot-Language.html#t:Bool">Bool</a> -> <a href="Language-Copilot-Core.html#t:Spec">Spec</a> <a href="Language-Copilot-Language.html#t:Bool">Bool</a> -> <a href="Language-Copilot-Core.html#t:Streams">Streams</a></li><li class="src short"><a href="#v:until">until</a> :: <a href="/Library/Frameworks/GHC.framework/Versions/612/usr/share/doc/ghc/html/libraries/base-4.2.0.2/Data-Int.html#t:Int">Int</a> -> <a href="Language-Copilot-Core.html#t:Spec">Spec</a> <a href="Language-Copilot-Language.html#t:Bool">Bool</a> -> <a href="Language-Copilot-Core.html#t:Spec">Spec</a> <a href="Language-Copilot-Language.html#t:Bool">Bool</a> -> <a href="Language-Copilot-Core.html#t:Spec">Spec</a> <a href="Language-Copilot-Language.html#t:Bool">Bool</a> -> <a href="Language-Copilot-Core.html#t:Streams">Streams</a></li><li class="src short"><a href="#v:release">release</a> :: <a href="/Library/Frameworks/GHC.framework/Versions/612/usr/share/doc/ghc/html/libraries/base-4.2.0.2/Data-Int.html#t:Int">Int</a> -> <a href="Language-Copilot-Core.html#t:Spec">Spec</a> <a href="Language-Copilot-Language.html#t:Bool">Bool</a> -> <a href="Language-Copilot-Core.html#t:Spec">Spec</a> <a href="Language-Copilot-Language.html#t:Bool">Bool</a> -> <a href="Language-Copilot-Core.html#t:Spec">Spec</a> <a href="Language-Copilot-Language.html#t:Bool">Bool</a> -> <a href="Language-Copilot-Core.html#t:Streams">Streams</a></li></ul></div><div id="interface"><h1>Documentation</h1><div class="top"><p class="src"><a name="v:ltl" class="def">ltl</a> :: <a href="Language-Copilot-Core.html#t:Spec">Spec</a> <a href="Language-Copilot-Language.html#t:Bool">Bool</a> -> (<a href="Language-Copilot-Core.html#t:Spec">Spec</a> <a href="Language-Copilot-Language.html#t:Bool">Bool</a> -> <a href="Language-Copilot-Core.html#t:Streams">Streams</a>) -> <a href="Language-Copilot-Core.html#t:Streams">Streams</a></p></div><div class="top"><p class="src"><a name="v:eventually" class="def">eventually</a> :: <a href="/Library/Frameworks/GHC.framework/Versions/612/usr/share/doc/ghc/html/libraries/base-4.2.0.2/Data-Int.html#t:Int">Int</a> -> <a href="Language-Copilot-Core.html#t:Spec">Spec</a> <a href="Language-Copilot-Language.html#t:Bool">Bool</a> -> <a href="Language-Copilot-Core.html#t:Spec">Spec</a> <a href="Language-Copilot-Language.html#t:Bool">Bool</a> -> <a href="Language-Copilot-Core.html#t:Streams">Streams</a></p><div class="doc"><p>Property <code>s</code> holds at some period in the next <code>n</code> periods. If <code>n == 0</code>,
then <code>s</code> holds in the current period. We require <code>n >= 0</code>. E.g., if <code>p =
eventually 2 s</code>, then we have the following relationship between the streams
generated:
<code>
s => F F F T F F F T ...
p => F T T T F T T T ...
</code>
</p></div></div><div class="top"><p class="src"><a name="v:next" class="def">next</a> :: <a href="Language-Copilot-Core.html#t:Spec">Spec</a> <a href="Language-Copilot-Language.html#t:Bool">Bool</a> -> <a href="Language-Copilot-Core.html#t:Spec">Spec</a> <a href="Language-Copilot-Language.html#t:Bool">Bool</a> -> <a href="Language-Copilot-Core.html#t:Streams">Streams</a></p><div class="doc"><p>Property <code>s</code> holds at the next period. For example:
<code>
0 1 2 3 4 5 6 7
s => F F F T F F T F ...
next s => F F T F F T F ...
</code>
Note: s must have sufficient history to drop a value from it.
</p></div></div><div class="top"><p class="src"><a name="v:always" class="def">always</a> :: <a href="/Library/Frameworks/GHC.framework/Versions/612/usr/share/doc/ghc/html/libraries/base-4.2.0.2/Data-Int.html#t:Int">Int</a> -> <a href="Language-Copilot-Core.html#t:Spec">Spec</a> <a href="Language-Copilot-Language.html#t:Bool">Bool</a> -> <a href="Language-Copilot-Core.html#t:Spec">Spec</a> <a href="Language-Copilot-Language.html#t:Bool">Bool</a> -> <a href="Language-Copilot-Core.html#t:Streams">Streams</a></p><div class="doc"><p>Property <code>s</code> holds for the next <code>n</code> periods. We require <code>n >= 0</code>. If <code>n ==
0</code>, then <code>s</code> holds in the current period. E.g., if <code>p = always 2 s</code>, then we
have the following relationship between the streams generated:
<code>
0 1 2 3 4 5 6 7
s => T T T F T T T T ...
p => T F F F T T ...
</code>
</p></div></div><div class="top"><p class="src"><a name="v:until" class="def">until</a> :: <a href="/Library/Frameworks/GHC.framework/Versions/612/usr/share/doc/ghc/html/libraries/base-4.2.0.2/Data-Int.html#t:Int">Int</a> -> <a href="Language-Copilot-Core.html#t:Spec">Spec</a> <a href="Language-Copilot-Language.html#t:Bool">Bool</a> -> <a href="Language-Copilot-Core.html#t:Spec">Spec</a> <a href="Language-Copilot-Language.html#t:Bool">Bool</a> -> <a href="Language-Copilot-Core.html#t:Spec">Spec</a> <a href="Language-Copilot-Language.html#t:Bool">Bool</a> -> <a href="Language-Copilot-Core.html#t:Streams">Streams</a></p><div class="doc"><p><code>until n s0 s1</code> means that <code>eventually n s1</code>, and up until at least the
period before <code>s1</code> holds, <code>s0</code> continuously holds.
</p></div></div><div class="top"><p class="src"><a name="v:release" class="def">release</a> :: <a href="/Library/Frameworks/GHC.framework/Versions/612/usr/share/doc/ghc/html/libraries/base-4.2.0.2/Data-Int.html#t:Int">Int</a> -> <a href="Language-Copilot-Core.html#t:Spec">Spec</a> <a href="Language-Copilot-Language.html#t:Bool">Bool</a> -> <a href="Language-Copilot-Core.html#t:Spec">Spec</a> <a href="Language-Copilot-Language.html#t:Bool">Bool</a> -> <a href="Language-Copilot-Core.html#t:Spec">Spec</a> <a href="Language-Copilot-Language.html#t:Bool">Bool</a> -> <a href="Language-Copilot-Core.html#t:Streams">Streams</a></p><div class="doc"><p><code>release n s0 s1</code> means that either <code>always n s1</code>, or <code>s1</code> holds up to and
including the period at which <code>s0</code> becomes true.
</p></div></div></div></div><div id="footer"><p>Produced by <a href="http://www.haskell.org/haddock/">Haddock</a> version 2.8.1</p></div></body></html>