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.

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.

param temperature: Float = 25.0

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
param bound: Int = 1

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