-- Copyright 2025 NASA
-- Copyright 2019 National Institute of Aerospace / Galois, Inc.
-- 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 Main where
import Language.Copilot
import Copilot.Visualize.Static
import Prelude hiding ((>), (<))
-- External temperature as a byte, range of -50C to 100C
temp :: Stream Word8
temp = extern "temperature" (Just [ 10, 15, 18, 19, 25, 5, 45 ])
-- 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 and produce a LaTeX file in the current directory with a
-- Tikz drawing of the spec.
main :: IO ()
main = do
spec' <- reify spec
visualize 3 spec' "tikz" "."