About

Copilot is a realtime programming language and Runtime Verification framework. It allows users to write concise programs in a simple but powerful way using a stream-based approach.

Programs can be interpreted for testing, or translated C99 code to be incorporated in a project, or as a standalone application. The C99 backend ensures us that the output is constant in memory and time, making it suitable for systems with hard realtime requirements. Copilot provides a strong type system that helps keeping programmers from making common mistakes, aiding in the quality of the code.

Copilot provides a library providing higher-level constructs, for example for defining clocks, a Boyer-Moore majority voting implementation and various temporal logics, including Linear Temporal logic (LTL) and Past Time LTL.

Code example

This is a simple example showing basic usage. It implements a home heating system: It heats when temp gets too low, and stops when it is high enough. It reads temperature as a byte (range -50C to 100C) and translates this to Celsius.

{-# LANGUAGE RebindableSyntax #-}

module Main where

import Language.Copilot
import Copilot.Compile.C99

-- 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"