Additional Features

Attributes

In addition to docstrings (which begin with ///), Lilo definitions, specs, params and signals can be annotated with attributes. They must immediately precede the item they annotate.

The attributes are used to convey metadata about items they annotate which is used by the tooling (notably the VSCode extension).

#[key = "value", fn(arg), flag]
spec foo = true

• Suppressing unused variable warnings: #[disable(unused)]
  • Using this attribute on a definition, param or signal will suppress warnings about it being unused.
  • Specs or public definitions are always considered used.
• Timeout for Static Analyses
  • To override the default timeout for static analyses, a timeout can be specified in seconds.
  • They can be specified individually #[timeout(satisfiability = 20, redundancy = 30)]
  • Or together #[timeout(10)] which sets both to 10 seconds.
• Disabling static analyses
  • Use #[disable(satisfiability)] or #[disable(redundancy)] to disable specific static analyses on a definition.
• Soft assumptions: #[rigidity = "soft"]
  • Applied to an assumption, marks it as a soft constraint that the solver tries to satisfy but may relax if it conflicts with hard constraints. See Rigidity Levels for details.

Labels, Aliases, and Custom Fields

Specifications can be annotated with labels, aliases, and custom fields, using attributes.

A label is a string attached to a specification. The VSCode extension’s spec sidebar groups specifications by label. This is useful for focusing on a subset of specifications, such as the safety-related ones.

#[label("safety", "critical")]
spec brake_must_work = always (brake_pedal => eventually (deceleration > 0))

An alias is an alternative name in a particular language. The spec sidebar shows the alias alongside the name used in the source file.

#[alias(en = "Brake Must Work", ja = "ブレーキは動作しなければならない")]
spec brake_must_work = always (brake_pedal => eventually (deceleration > 0))

A specification can have multiple #[label] or #[alias] attributes. All of them are applied.

A label can be associated with a color (represented via a hex code or any standard HTML5 color name) in the lilo.toml config file. To do so, simply add a section [labels.colors] like the following:

[labels.colors]
production = "blue"
consumption = "magenta"
renewable = "0x00ff00"
'mitigation strategy' = "yellow"

Custom fields attach extra scalar metadata to a specification. They are useful for project-specific categorization such as review status, owner, priority, etc.

#[field(priority = 1, reviewed = true, owner = "ops")]
spec brake_must_work = always (brake_pedal => eventually (deceleration > 0))

Custom field values must be scalar values (strings, numbers, booleans). For a single specification, if the same custom field is provided more than once, the first value is used and a warning is emitted.

The VSCode extension can use custom fields in the Spec Status Pane filter. For example:

• reviewed:true
• owner:"ops"
• priority:>=2

See VSCode Extension for the full query syntax.

Default Values for Parameters

When specifying a system, parameters can optionally be given a default value. The intent of such a default value is to indicate that the parameter is expected to be instantiated with the default value in a typical use case.

#[default = 25.0]
param temperature: Float

Default values should not be used to declare constants. For them, use a def instead.

def pi: Float = 3.14159

• When monitoring, parameters with default values can be omitted from the input. If omitted, the default value is used. They can also be explicitly provided, in which case the provided value is used.
• When exporting a formula, parameters with a default value will be substituted with the default value before the export.
• When exemplifying, the exemplifier will require the solver to fix the parameter to the default value.

When running an analysis such as export or exemplification, one can provide the JSON null value for a field in the config. This has the effect of requesting SpecForge to ignore the default value for the parameter.

system main

signal p: Int
#[default = 1]
param bound: Int

spec foo = p > 1 && p < bound

• Exemplification
  • With params = {}: Unsatisfiable (the default value of bound is used)
  • With params = { "bound": null }: Satisfiable (the solver is free to choose a value of bound that satisfies the constraints)
• Export
  • With params = {}, result: p > 1 && p < 1
  • With params = { "bound": 100 }, result: p > 1 && p < 100
  • With params = { "bound": null }, result: p > 1 && p < bound

Note that the JSON null value cannot be used as a default value as a part of the Lilo program.

Spec Stubs

The user may create a spec stub, a spec without a body. Such a stub may still have a docstring and attributes. This can be used as a placeholder, and is interpreted as true by the Lilo tooling.

The VSCode extension will display a codelens to generate an implementation for the stub based on the docstring using an LLM (if configured).

/// The system should always eventually recover from errors.
spec error_recovery

Stubs can also be used for assumptions which have not yet been formalized.

/// height is always non-negative
assumption height_non_negative