The Reactive structure

The Reactive structure provides types and operations to build and run reactive systems. The inputs and outputs of a reactive system are sets of signals, which can either be present (i.e., true) or absent (i.e., false). A reactive system runs in discrete timesteps.

Synopsis

signature REACTIVE
structure Reactive : REACTIVE

Interface

type machine
type instruction
type signal = Atom.atom
type config
type in_signal
type out_signal

val machine : {
	inputs : signal list,
	outputs : signal list,
	body : instruction
      } -> machine

val run : machine -> bool
val reset : machine -> unit

val inputsOf : machine -> in_signal list
val outputsOf : machine -> out_signal list

val inputSignal : in_signal -> signal
val outputSignal : out_signal -> signal

val setInSignal  : (in_signal * bool) -> unit
val getInSignal  : in_signal -> bool
val getOutSignal : out_signal -> bool

val || : (instruction * instruction) -> instruction
val &  : (instruction * instruction) -> instruction

val nothing : instruction
val stop : instruction
val suspend : instruction

val action : (machine -> unit) -> instruction
val exec   : (machine -> {stop : unit -> unit, done : unit -> bool})
	      -> instruction

val ifThenElse : ((machine -> bool) * instruction * instruction) -> instruction
val repeat     : (int * instruction) -> instruction
val loop       : instruction -> instruction
val close      : instruction -> instruction

val signal   : (signal * instruction) -> instruction
val rebind   : (signal * signal * instruction) -> instruction
val when     : (config * instruction * instruction) -> instruction
val trap     : (config * instruction) -> instruction
val trapWith : (config * instruction * instruction) -> instruction
val emit     : signal -> instruction
val await    : config -> instruction

val posConfig : signal -> config
val negConfig : signal -> config
val orConfig  : (config * config) -> config
val andConfig : (config * config) -> config

Description

The description of the interface is organized into sections.

Types

type machine

The type of a reactive system.

type instruction

The abstract representation of a reactive program.

type signal = Atom.atom

The name of a signal.

type config

A signal configuration is a logical combination of signals.

type in_signal

An input signal for a reactive system.

type out_signal

An output signal for a reactive system.

Machines

val machine : { …​ } -> machine

machine {inputs, outputs, body} creates a new reactive system (or machine) from a list of input signal names, a list of output signal names, and a reactive program.

val run : machine -> bool

run m will run the reactive system m one instant (or activation). It returns true if, and only if, the machine ends in a terminal state (_i.e., by executing the stop instruction).

val reset : machine -> unit

reset m resets the state of m to its initial state.

val inputsOf : machine -> in_signal list

inputsOf m returns a list of the input signals in the machine.

val outputsOf : machine -> out_signal list

outputsOf m returns a list of the output signals in the machine.

val nameOfInput : in_signal -> signal

inputSignal inSig returns the name of the input signal.

val nameOfOutput : out_signal -> signal

inputSignal outSig returns the name of the output signal.

val setInSignal : (in_signal * bool) -> unit

setInSignal (inSig, b) sets the value of the input signal to b.

val getInSignal : in_signal -> bool

getInSignal inSig gets the current value of the input signal.

val getOutSignal : out_signal -> bool

getOutSignal inSig gets the current value of the output signal.

Instructions

val || : (instruction * instruction) -> instruction

|| (i1, i2) forms the parallel composition of the two programs. Activation of the resulting program will interleave the two programs until either one of them suspends (see the suspend instruction) or both programs terminate.

val & : (instruction * instruction) -> instruction

& (i1, i2) forms the sequential composition of the two programs.

val nothing : instruction

The program that does nothing.

val stop : instruction

The program that stops; i.e., reaches the terminal state for the current and all future activations.

val suspend : instruction

The program that suspends the current activation.

val action : (machine -> unit) -> instruction

something

val exec : (machine -> {stop : unit -> unit, done : unit -> bool}) -> instruction

exec f returns a program that encapsulates the SML computation defined by the function f.

val ifThenElse : ((machine -> bool) * instruction * instruction) -> instruction

something

val repeat : (int * instruction) -> instruction

something

val loop : instruction -> instruction

something

val close : instruction -> instruction

something

val signal : (signal * instruction) -> instruction

something

val rebind : (signal * signal * instruction) -> instruction

something

val when : (config * instruction * instruction) -> instruction

something

val trapWith : (config * instruction * instruction) -> instruction

trapWith (cfg, i1, i2) returns the program that …​

val trap : (config * instruction) -> instruction

trap (cfg, i) This expression is equivalent to

trapWith (cfg, i, nothing)
val emit : signal -> instruction

emit sigId returns the program that emits the signal with the given name (i.e., the signal is present).

val await : config -> instruction

await cfg returns the program that waits for the configuration to hold.

Signal configurations

val posConfig : signal -> config

posConfig sigId defines a configuration that holds if, and only if, the signal named sigId is present.

val negConfig : signal -> config

negConfig sigId defines a configuration that holds if, and only if, the signal named sigId is not present.

val orConfig : (config * config) -> config

orConfig (cfg1, cfg2) defines a configuration that holds if either cfg1 or cfg2 (inclusive) holds.

val andConfig : (config * config) -> config

andConfig (cfg1, cfg2) defines a configuration that holds if both cfg1 and cfg2 hold.

Deprecated functions

The following functions are part of the interface, but have been deprecated.

val inputSignal : in_signal → signal

use nameOfInput instead.

val outputSignal : out_signal → signal

use nameOfOutput instead.