Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Exemplification and Satisfiability

Exemplification is the process of generating example traces that satisfy a specification.

Satisfiability is a closely related concept: a spec is satisfiable if there exists at least one trace that makes it true. SpecForge’s static analysis automatically checks whether your specs are satisfiable and warns you if they are not.

Both exemplification and satisfiability checking are influenced by assumptions, which are additional constraints that the solver takes into account.

Assumptions

An assumption is a property that is taken for granted when analysing a specification. Instead of being something you want to verify, it represents background knowledge about the system: physical laws, environmental constraints, or operating conditions that are expected to hold.

The assumption Keyword

In Lilo, you can declare an assumption using the assumption keyword:

signal temperature: Float
signal heater_on: Bool

assumption physics = always (heater_on => next temperature >= temperature)

spec eventually_warm = eventually (temperature > 30.0)

An assumption is syntactically like a spec (it has no parameters and its return type is always Bool) but it is treated differently by the tooling:

  • Exemplification: When generating example traces for any spec in the same system, all assumptions are automatically included as constraints. The solver must produce traces that satisfy both the spec and every assumption.
  • Satisfiability: When checking whether a spec is satisfiable, assumptions are included in the constraint set. A spec that would be satisfiable on its own may become unsatisfiable under assumptions.
  • Redundancy: Assumptions are included alongside other specs when checking for redundancy. A spec that follows from the assumptions (and other specs) will be flagged as redundant.

You can add the #[rigidity = "soft"] attribute to an assumption to make it a soft constraint for the exemplifier. See the section on Rigidity Levels below for details. By default, assumptions are considered hard.

This means you do not need to manually pass assumptions when running analyses. Declaring them in your Lilo source is enough.

Ad-hoc Assumptions

In addition to the assumption keyword, you can pass ad-hoc assumptions when running exemplification through the Python SDK or the VSCode extension. These are one-off constraints that apply only to a specific analysis run, rather than being part of the system definition.

Ad-hoc assumptions are useful when you want to explore “what if” scenarios without modifying your Lilo source, for example “generate a trace where the temperature starts above 20”.

Rigidity Levels

Each assumption (whether declared with the assumption keyword in the source or passed ad-hoc to an exemplification query) has a rigidity level that controls how the solver treats it:

  • Hard: The assumption is treated as an inviolable constraint. The generated trace must satisfy the assumption. If the solver cannot find a trace that satisfies both the spec and all hard assumptions, exemplification fails.
  • Soft: The assumption is treated as a preference. The solver first attempts to find a trace satisfying the spec and all hard assumptions, then tries to additionally satisfy soft assumptions. If a soft assumption cannot be satisfied together with the hard constraints, it is relaxed and the solver still produces a result.

In practice, use Hard for constraints that are essential (e.g., physical laws, safety bounds) and Soft for constraints that are desirable but not strictly required (e.g., “the temperature should increase at some point”).

Note: Assumptions declared with the assumption keyword default to hard rigidity. To make a keyword-declared assumption soft, annotate it with #[rigidity = "soft"].

Fixing Params to Default Values

When running an exemplification task, Lilo will automatically fix any parameters to their default values, if the Lilo source file supplies them. This means that the exemplifier will be forced to find a model in which the parameters take on those specific values.

In some cases, this can lead to unsatisfiability if the default values are incompatible with the spec or assumptions. In the easy analysis mode on the VSCode extension, you can disable this behavior by unchecking the “Fix Params to Defaults” option. In this case, the exemplifier will behave as if the parameters had no default values. In the Python SDK, you can achieve the same effect by passing fix_defaults = False to the exemplify method.

If you want to fix most params to their default values but allow some specific ones to vary, this can be done by passing the null JSON value for those params when running exemplification.

To consider a concrete example, consider the following system:

system VendingMachine

#[default = 1]
param cansMax : Int

signal cans : Int

assumption cansPositive = cans >= 0

spec reasonableCans = 0 < cans < cansMax

This spec is not satisfiable when cansMax is 1, which is its default value, since there is no integer cans satisfying 0 < cans < 1. Thus, this will be found unsatisfiable if the “Fix Params to Defaults” option is checked. If the option is unchecked, however, the exemplifier is free to choose a different value for cansMax (e.g., 5) so that the spec becomes satisfiable. Another way to achieve the same effect is to pass { cansMax: null }, which signals to the exemplifier that cansMax should be treated as a free variable.

Example

Consider a temperature sensor system with a spec always_in_bounds. You might run exemplification with a mix of rigidity levels:

  • A hard assumption "always_in_bounds" ensures the generated trace respects the bounds. The solver will fail if this is impossible.
  • A soft assumption "eventually (temperature > 30)" expresses a preference that the trace includes a high temperature reading, but the solver will still produce a result if this conflicts with the hard constraints.