Components

Components are a way of organizing Lilo Systems in hierarchical building blocks.

Consider the following Vehicle system, which is organized in the following way:

• A Vehicle has a PowerUnit and a Battery.
• The battery consists of two BatteryCells.
• Each of the systems PowerUnit, Battery, BatteryCell and Vehicle have their own signals, parameters and specifications.

The systems BatteryCell and PowerUnit do not have any components, so they can be declared in a straightforward way:

// BatteryCell.lilo
system BatteryCell

pub signal voltage: Float
pub signal temperature: Float
pub param nominal_voltage: Float

pub def over_voltage: Bool = voltage > nominal_voltage * 1.15

spec voltage_range = voltage >= 2.5 && voltage <= 4.5

// PowerUnit.lilo
system PowerUnit

pub signal temperature: Float
pub signal output: Float
pub param max_output: Float

pub def is_overheating: Bool = temperature > 85.0

spec output_bounded = output <= max_output

Here, the use of the pub keyword indicates that these signals, params and definitions will be accessible to other systems which instantiate these systems as components. Specifications declared with spec are always public.

Instantiating Components

The Battery system uses BatteryCell components, which can be declared using the component keyword:

// Battery.lilo

system Battery

pub signal level: Float
pub signal voltage: Float
pub param capacity: Float

component cell1: BatteryCell

// ...

Lifted vs Mapped Signals and Params

When a system is instantiated as a component in another system, its params and signals are lifted to the parent system. Thus, in addition to level, voltage and capacity, the schema for Battery involves cell1::voltage, cell1::temperature and cell1::nominal_voltage.

Some signals or params of a component may be mapped, meaning that they are not a part of the input schema, but their values are determined by other signals or params (of the parent system). For example, consider the following example where the schema of Battery still exposes cell1::voltage, cell1::temperature and cell1::nominal_voltage, as well as cell2::temperature, but not cell2::nominal_voltage or cell2::voltage. The value of cell2::nominal_voltage is fixed to 3.7, and the value of cell2::voltage is derived from the Battery’s voltage signal.

// Unmapped component - all signals and params will be lifted
component cell1: BatteryCell

// Partially mapped component - voltage is mapped, temperature is lifted
component cell2: BatteryCell {
  param nominal_voltage = 3.7
  signal voltage = voltage / 2.0  // Derived from battery voltage
}

Accessing Component Signals and Params

Lilo expressions in a system can refer to signals and params of their components using the :: operator to access the component’s signals and params.

// Use cell component signals
pub def any_cell_over_voltage: Bool = cell1::over_voltage || cell2::over_voltage

spec level_valid = level >= 0.0 && level <= 100.0

// Reference cell component specs
spec cells_safe = cell1::voltage_range && cell2::voltage_range

A system can refer to signals and params of components of its components. For example, consider the Vehicle system which has both a Battery and a PowerUnit component. One can write specifications in the Vehicle system in the following manner.

// Vehicle.lilo

// ...

// Two-level signal references

def low_battery: Bool = battery::level < 20.0
def power_hot: Bool = power::temperature > 80.0

def bat_cell1_voltage: Float = battery::cell1::voltage

def at_meihan: Bool = 34.63 < gps.lat < 34.65 && 135.99 < gps.lon < 136.01

// Three-level signal references (Vehicle -> Battery -> BatteryCell)

def cell1_overheated: Bool = battery::cell1::temperature > 65.0
def cell2_voltage_ok: Bool = battery::cell2::voltage > 3.0

// Two-level def references

def battery_or_power_issue: Bool = battery::is_low || power::is_overheating

// Three-level def references (Vehicle -> Battery -> BatteryCell)

def any_cell_overvoltage: Bool = battery::cell1::over_voltage || battery::cell2::over_voltage

// Combined two-level and three-level
def critical_state: Bool = battery::is_low && battery::any_cell_over_voltage

// ...

System Schema

The schema of a system refers to the set of signals and params that constitutes it input. When monitoring, the user provides values for elements of the schema. The schema corresponding to the Vehicle system is shown in the diagram below.

The SpecForge CLI schema command can be used to view the schema of a system. Notice that the mapped signals and params do not appear in the schema, since their values are derived from different signals or params.

$ schema --project /Users/agnishom/code/reqeng/api/examples/projects/vehicle -s Vehicle flat
Signals:
  ambient_temp  Float
  battery::cell1::temperature  Float
  battery::cell1::voltage  Float
  battery::cell2::temperature  Float
  battery::level  Float
  battery::voltage  Float
  gps_lat  Float
  gps_lon  Float
  power::output  Float
  speed  Float


Params:
  battery::capacity  Float
  battery::cell1::nominal_voltage  Float
  temp_threshold  Float   (default: 75.0)

Refer to the documentation on Data Files for details on the format for providing values for the schema when monitoring.