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
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
|
# Copilot: Stream DSL for hard real-time runtime verification
[](https://app.travis-ci.com/github/Copilot-Language/copilot)
[](https://hackage.haskell.org/package/copilot)
Copilot is a runtime verification framework written in Haskell. It allows the
user to write programs in a simple but powerful way using a stream-based
approach.
Programs can be interpreted for testing, or translated into C99 code to be
incorporated in a project or as a standalone application. The C99 backend
output is constant in memory and time, making it suitable for systems with hard
realtime requirements.
## Using Copilot
Assuming you have GHC and cabal already installed (see [Haskell
Platform](http://hackage.haskell.org/platform/) or
[ghcup](https://www.haskell.org/ghcup/)), there are several ways to use
Copilot:
* Adding Copilot to your project
Copilot is available from
[Hackage](https://hackage.haskell.org/package/copilot). Adding `copilot`
to your project's cabal file should be enough to get going.
* Adding Copilot to the default GHC environment
```bash
cabal v2-install --lib copilot
```
After which Copilot will be available from ghci.
* Launching a repl with Copilot
Another quick solution is to cabal to launch a repl with Copilot
available.
```bash
cabal v2-repl --build-depends copilot
```
Cabal will download and build Copilot only to make it available in the
launched repl. The global GHC environment will not be affected.
* Building from source (typically done for development):
```bash
git clone https://github.com/Copilot-Language/copilot.git
cd copilot
```
Compiling can either be done in a Nix-style build, or a traditional one:
_Nix-Style build (Cabal >= 2.x)_
```bash
cabal build copilot-*/ # For Cabal 3.x
cabal v2-build copilot-*/ # For Cabal 2.x
```
_Traditional build (Cabal 1.x)_
```bash
cd copilot
cabal install --dependencies-only . ../copilot-*/
cabal install ../copilot-*/
cabal build
```
Note there is a TravisCI build (linked to at the top of this README) if you
have trouble building/installing.
## Example
Here follows a simple example of a heating system. Other examples can be found
in the [examples
directory](https://github.com/Copilot-Language/copilot/tree/master/copilot/examples)
of the main repository.
```haskell
-- This is a simple example with basic usage. It implements a simple home
-- heating system: It heats when temp gets too low, and stops when it is high
-- enough. It read temperature as a byte (range -50C to 100C) and translates
-- this to Celsius.
module Heater where
import Language.Copilot
import Copilot.Compile.C99
import Prelude hiding ((>), (<), div)
-- External temperature as a byte, range of -50C to 100C
temp :: Stream Word8
temp = extern "temperature" Nothing
-- Calculate temperature in Celsius.
-- We need to cast the Word8 to a Float. Note that it is an unsafeCast, as there
-- is no direct relation between Word8 and Float.
ctemp :: Stream Float
ctemp = (unsafeCast temp) * (150.0 / 255.0) - 50.0
spec = do
-- Triggers that fire when the ctemp is too low or too high,
-- pass the current ctemp as an argument.
trigger "heaton" (ctemp < 18.0) [arg ctemp]
trigger "heatoff" (ctemp > 21.0) [arg ctemp]
-- Compile the spec
main = reify spec >>= compile "heater"
```
The examples located in the `examples/` directory can be run from the root of
the project. Each example has a name. As a rule of thumb, the examples are
named after the filename (without extension) in lowercase letters, and
directory seperators replaced with a '-'. For example:
```sh
cabal run addmult -f examples
cabal run counter -f examples
cabal run what4-arithmetic -f examples
```
## Contributions
Feel free to open new issues and send pull requests.
In order to contribute to Copilot, please use the following steps which will
make the process of evaluating and including your changes much easier:
* Create an issue for every individual change or problem with Copilot. Document
the issue well.
* Always comment on the issues you are addressing in every commit. Be
descriptive, and use the syntax `#<issue_number>` so that we can track
changes and issues easily.
* Every commit should mention one issue and, ideally, only one.
* Do not send a PR or commit that addresses multiple problems, unless they are
related and cannot be separated.
* Do not commit to master directly, except for branch merges. Make sure you
always merge onto master using `--no-ff` so that we can tell that features
were addressed separately, completed, tested, and then merged. If you are a
Copilot developer, create a branch for every issue you are addressing, complete
it, and then merge onto master. Document every commit in every branch,
including the last merge commit, stating the issues it addresses or closes.
This process is similar to [Git
Flow](http://nvie.com/posts/a-successful-git-branching-model/). The equivalent
of Git Flow's master branch is our latest tag, and the equivalent of Git Flow's
develop branch is our master.
## Further information
For further information, including documentation and a tutorial, please visit
the Copilot website:
[https://copilot-language.github.io](https://copilot-language.github.io).
## Acknowledgements
We are grateful for NASA Contract NNL08AD13T to Galois, Inc. and the National
Institute of Aerospace, which partially supported this work.
Additionally NASA Langley contracts 80LARC17C0004 and NNL09AA00A supported
further development of Copilot.
## License
Copilot is distributed under the BSD-3-Clause license, which can be found
[here](https://raw.githubusercontent.com/Copilot-Language/copilot/master/copilot/LICENSE).
## The Copilot Team
The development of Copilot spans across several years. During these years
the following people have helped develop Copilot (in no particular order):
* Lee Pike
* Alwyn Goodloe (maintainer)
* Robin Morisset
* Sebastian Niller
* Nis Wegmann
* Chris Hathhorn
* Eli Mendelson
* Jonathan Laurent
* Laura Titolo
* Georges-Axel Jolayan
* Macallan Cruff
* Ryan Spring
* Lauren Pick
* Frank Dedden (maintainer: contact at dev@dedden.net)
* Ivan Perez (maintainer)
|
