Systems

Ultimately Lilo is used to specify systems. A system groups together declarations for the temporal input signals, the (non-temporal) parameters and the specifications. A system also includes auxiliary definitions.

A system file should start with a system declaration, e.g.:

system Engine

The name of the system should match the file name.

Type declarations

A new type is declared with the type keyword. To define a new record type Point:

type Point = { x: Float, y: Float }

We can then use Point as a type anywhere else in the file.

Signals

The time varying values of the system are called signals. They are declared with the signal keyword. E.g.:

signal x: Float
signal y: Float
signal speed: Float
signal rain_sensor: Bool
signal wipers_on: Bool

The definitions and specifications of a system can freely refer to the system's signals.

A signal can be of any type that does not contain function types, i.e. a combination of primitive types and records.

System Parameters

Variables of a system which are constant over time are called system parameters. They are declared with the param keyword. E.g.:

param temp_threshold: Float
param max_errors: Int

The definitions and specifications of a system can freely refer to the system's parameters. Note that system parameters must be provided upfront before monitoring can begin. For exemplification, system parameters are optional. That is, they can be provided, in which case the example must conform to them, or otherwise the exemplification process will try to find values that work.

Definitions

A definition is declared with the def keyword:

def foo: Int = 42

A definition can depend on parameters:

def foo(x: Float) = x + 42

One can also specify the return type of a definition:

def foo(x: Float): Float = x + 42

The type annotations on parameters and the return type are both optional, if they are not provided they are inferred. It is recommended to always specify these types as a form of documentation.

The parameters of a definition can also be be record types, for instance:

type S = { x: Float, y: Float }

def foo(s: S) = eventually [0,1] s.x > s.y

Definitions can be used in other definitions, e.g.:

type S = { x: Float, y: Float }

def more_x_than_y(s: S) = s.x > s.y

def foo(s: S) = eventually [0,1] more_x_than_y(s)

Definitions can be specified in any order, as long as this doesn't create any circular dependencies.

Definitions can freely use any of the signals of the system, without having to declare them as parameters.

Specifications

A spec says something that should be true of the system. They can use all the signals and defs of the system. They are declared using the spec keyword. They are much like defs except:

The return type is always Bool (and doesn't need to be specified)
They cannot have parameters.

Example:

signal speed: Float

def above_min = 0 <= speed

def below_max = speed <= 100

spec valid_speed =
  always (above_min && below_max)