ControlThermostat

Toy discrete-time thermal plant, one minute per step. T' = T + 0.05*(outside-T) + 1.2*heater. Target: 22 Celsius.
Imports
import Control; open Control; import Math;
Table of Contents

Types

ControlThermostat

(inductive)
inductive ControlThermostat

Constructors

For each type in this module: inductive types list their declared constructors; opaque types list any local function whose name starts with mk and which returns a value of that type.

ControlThermostat (inductive)

mk

constructor
ControlThermostat

Functions

temperature

def temperature (s : ControlThermostat) : Float

heater

def heater (s : ControlThermostat) : Bool

step

def step (s : ControlThermostat) (action : Bool) : ControlThermostat

invalid

def invalid (s : ControlThermostat) : Bool

hysteresis

A policy observes temperature and the previous heater setting, allowing hysteresis rather than forced on/off chattering at one threshold.
def hysteresis (low : Float) (high : Float) (t : Float) (was_on : Bool) : Bool

reference

def reference (t : Float) (was_on : Bool) : Bool

off

def off (t : Float) (was_on : Bool) : Bool

advance

def advance (policy : (t : Float) → (on : Bool) → Bool) (s : ControlThermostat) : ControlThermostat

cost

def cost (policy : (t : Float) → (on : Bool) → Bool) (s : ControlThermostat) : Float

episode

def episode (horizon : Int | horizon ≥ 0 && horizon ≤ 500) (policy : (t : Float) → (on : Bool) → Bool) (initial : ControlThermostat) : Control

training

def training (policy : (t : Float) → (on : Bool) → Bool) : Float

held_out

def held_out (policy : (t : Float) → (on : Bool) → Bool) : Float