Quickstart#

\(\Psi\)-TaLiRo is available on PyPI. You can follow our installation guide to set up your environment for running \(\Psi\)-TaLiRo tests.

Basic Structure#

A test in \(\Psi\)-TaLiRo is composed of three components, which are:

  • a Cost Function

  • an Optimizer

  • the test options

Very simply, the cost function is responsible for evaluating a Sample - a vector of floating point values - into a cost value, while the optimizer is responsible for generating the samples. Using the sample space defined in the test options , the optimizer selects samples and passes them to the cost function, and receives back the cost value to inform subsequent sample selection. The sample provided to the cost function is decomposed into the static system inputs and the signal inputs. The static inputs are time-invariant and can be viewed as the initial conditions to the system, while the signal inputs are time-varying and can be queried over the time interval defined in the options. Samples are generated until the sample budget defined in the options is exhausted or the optimizer terminates.

Evaluating Samples#

\(\Psi\)-TaLiRo provides supports two ways of evaluating the Sample values generated by the optimizer. The first is called a Cost Function, which evaluates a sample directly into a cost value. The other is a composition of two components called a Model, which uses the sample to simulate the system and produce a timed set of system states, and a Specification, which evaluates the timed system states into a cost value. You can find more information about these two approaches in the following sections or in the API documentation for each component.

Each Sample value provides both the static and the signals attributes which contain the static and signal inputs to the system respectively.

Cost Functions#

A Cost Function represents the transformation from a sample generated by the optimizer to a cost value that can be minimized. A cost function can be created by applying the costfunc() decorator to a function that accepts a sample and returns a cost value.

import staliro

@staliro.costfunc()
def cost(sample: staliro.Sample) -> float:
    return 0.0

You can also optionally provide additional metadata from the cost function by returning a Result value containing both the cost and extra values.

import staliro

@staliro.costfunc
def result(sample: staliro.Sample) -> staliro.Result[float, str]:
    return staliro.Result(0.0, "foo")

Models & Specifications#

One special case of a cost function is the composition of a Model and a Specification, and \(\Psi\)-TaLiRo provides dedicated functionality for users who wish to express their tests in terms of this composition.

Models represents the simulation of the system under test (SUT) and is responsible for using the input sample to produce a set of timed system states known as a Trace. You can create a model by using the model() decorator with a function that returns a Trace or a Result containing a Trace. For convenience, you can construct an instance of models.Result, which combines the construction a Trace and a Result object.

from staliro import models

@models.model()
def trace(sample: models.Sample) -> models.Trace[list[float]]:
    return models.Trace({1.0: [0.1, 4.8, 2.9], 2.0: [-0.5, 3.2, 2.1]})


@models.model
def result(sample: models.Sample) -> models.Result[float, str]:
    return models.Result(times=[1.0, 2.0, 3.0], states=[-4.1, 3.2, 100.7], extra="foo")

\(\Psi\)-TaLiRo also provides alternative model implementations for representing different systems. The first is the Blackbox model, which provides a discrete set of uniformly spaced signal values rather than a continuous signal function. Blackbox models can be constructed using the blackbox() decorator function on a function that accepts a Blackbox.Inputs value and returns either a Trace or Result. The blackbox decorator optionally accepts a step_size parameter indicating the length of time between each signal value (default: 0.1).

from staliro import models

@models.blackbox(step_size=0.5)
def trace(inputs: models.Blackbox.Inputs) -> models.Trace[dict[str, float]]:
    ...

@models.blackbox()
def result(inputs: models.Blackbox.Inputs) -> models.Result[list[float], str]:
    ...

For systems that can be represented using ordinary differential equations, \(\Psi\)-TaLiRo provides the Ode model. To create this type of model, users can use the ode() decorator to annotate a function that accepts an Ode.Inputs value and returns a vector of values representing the derivative of the state at the given time. The ode decorator optionally accepts a method argument specifying the integration method to use during simulation.

from staliro import models

@models.ode(method="RK45")
def system(inputs: models.Ode.Inputs) -> list[float]:
    ...

After defining a Model, users must also define a Specification> to evaluate the Trace produced by the simulation. A specification represents a requirement of the system being tested, and evaluating a specification should produce a metric value that represents how well the system satisfies the requirement. Users can create their own specifications using the specification() decorator on a function that returns either a cost value or a Result value containing extra metadata as well as the cost value.

import staliro

@staliro.specification()
def cost(trace: staliro.Trace[list[float]]) -> float:
    ...

@staliro.specification
def result(trace: staliro.Trace[list[float]]) -> staliro.Result[float, str]:
    ...

For users interested in expressing their requirements using Signal Temporal Logic (STL), \(\Psi\)-TaLiRo provides two different specification implementations. The first is the RTAMTDiscrete specification, which requires input Trace values to have a constant time-step. The other is the RTAMTDense specification which does not require a constant time -step. Both implementations expect to evaluate traces with states of type Sequence[float] and are constructed with an STL formula written as a string and a Mapping of variable names in the formula to columns in the state vector.

from staliro import specifications

dense = RTAMTDense("always (alt >= 0)", {"alt": 0})
discrete = RTAMTDiscrete("eventually (rpm >= 3000 and speed >= 40)", {"rpm": 0, "speed": 1})

Generating Samples#

Optimizers#

The Optimizer is responsible for selecting samples that the model will use to execute a simulation. At its core, an optimizer provides samples to the cost function which returns a single scalar value that the optimizer uses to select the next sample. Different optimizers can have different strategies for selecting samples, for example some optimizers will use the result of the last simulation to help guide the selection of the next sample, while some optimizers may not. The objective function provided to the optimizer is capable of evaluating a single sample, or multiple samples. If test parallelization is configured, then multiple sample evaluations will happen in parallel.

Creating an optimizer can be accomplished using the optimizer() decorator on a function that accepts an ObjFunc and a set of optimization parameters Optimizer.Params. The function can optionally return a result value at the end of an optimization attempt that is returned to the user.

from staliro import optimizers

class OptResult:
    ...

@optimizers.optimizer()
def result(func: optimizers.ObjFunc[float], params: optimizers.Optimizer.Params) -> OptResult:
    ...

@optimizers.optimizer()
def no_result(func: optimizers.ObjFunc[float], params: optimizers.Optimizer.Params) -> None:
    ...

\(\Psi\)-TaLiRo provides two optimizers: UniformRandom and DualAnnealing. Both optimizers accept an optional behavior parameter which sets the mode to either minimization or falsification (default minimization). In minimization mode the optimizer will exhaust the budget to find the most falsifying sample, while in falsification mode the optimizer will terminate when the first falsifying example is found.

from staliro.optimizers import Behavior, DualAnnealing, UniformRandom

ur_optimizer = UniformRandom()
da_optimizer = DualAnnealing(behavior=Behavior.FALSIFICATION)

Samplers#

Warning

This feature is not currently available, but is planned for one of our upcoming releases. As such, the API documented here may not be the final version once this feature is released.

The Optimizer interface provides a push-style API, where samples are “pushed” to the objective function. However, in some instances it may be easier or more straight-forward to implement sample generation in a pull-style interface, where samples are requested for analysis from outside the data structure. To facilitate this representation, \(\Psi\)-TaLiRo provides a type called Sampler, which is created using the sampler() decorator on a generator function. An example of a Sampler implementation would look like the following:

from staliro import optimizers

@optimizers.sampler()
def sampler(params: optimizers.Optimizer.Params) -> optimizers.Sampler[float, OptResult]:
    for _ in range(params.budget):
        sample = [0.1, 1.3, 4.5]
        cost = yield sample

Options#

Note

All parameters when constructing a TestOptions or SignalInput value must be provided as keywords.

The test options are used to configure the behavior of a \(\Psi\)-TaLiRo test. When defining the test options, you must ensure that there is at least one input declared in either the static_inputs or signals arguments. All other properties are optional with default values. Some of the most important options are:

Option

Description

static_inputs

Time-invariant model inputs. Often used to represent initial conditions of the system.

signals

Time-varying model inputs

runs

Number of times to execute the optimizer

iterations

Number of samples to evaluate per run

seed

Initial seed of the random number generator. Necessary for repeatability

The options for a signal input are passed as instances of the SignalInput class. SignalInput values must have at least one control point defined. The signal control points can be defined as either a list, in which case they will be associated with an evenly spaced set of times, or a dictionary, which will use the dictionary keys as the times. You can also specify the type of interpolation to use for the signal using the factory argument. If any signal inputs are defined, then you must ensure that the tspan parameters is also defined. The following is an example of constructing a TestOptions value with both static and signal inputs.

from staliro import TestOptions, signals

options = TestOptions(
    runs=10,
    iterations=100,
    tspan=(0, 10),
    static_inputs={"speed": (0, 100), "rpm": (3000, 8000)},
    signals={
        "throttle": signals.SignalInput(
            control_points=[(0, 100), (0, 100)],
            factory=signals.piecewise_linear,
        ),
        "brake": signals.SignalInput(
            control_points={0: (0, 255), 4: (128, 255), 8: (0, 255)},
            factory=signals.pchip,
        )
    }

Writing tests#

A typical PSY-TaLiRo script is composed of component definitions and then a call to the staliro() function. staliro takes as input either 3 parameters (a Cost Function, an Optimizer, and a TestOptions value) or 4 parameters (a Model, a Specification, an Optimizer, and a TestOptions value). As output, the staliro function returns a list of Run objects which contains the result data from each run of the optimizer, as well as an evaluation history from the cost function. You can also use the staliro.test() function if you choose.

Test using a Cost Function#
import staliro
import staliro.optimizers as optimizers
import staliro.specifications as specifications

@staliro.costfunc()
def costfunc(sample: staliro.Sample) -> float:
    ...

optimizer = optimizers.DualAnnealing()
opts = staliro.TestOptions(static_inputs={"y": (10, 20)})
runs = staliro.test(costfunc, optimizer, options)
Test using a Model and Specification#
from staliro import TestOptions, models, optimizers, specifications, staliro

@models.model()
def model(sample: staliro.Sample) -> float:
    ...

optimizer = optimizers.DualAnnealing()
spec = specifications.RTAMTDense("always (x >= 3.0)", {"x": 0})
opts = TestOptions(static_inputs={"y": (10, 20)})
runs = staliro(model, spec, optimizer, options)

Executable scripts#

Keeping tests in executable scripts can be convenient if you plan on executing a test many times. Python has a few idioms for creating executable scripts which can make them much easier to work with. The first is a comment line called a shebang.

#!/usr/bin/env python3

This instructs the system on how to select the python interpreter to use when executing the script. The second important idiom is the main guard.

if __name__ == "__main__":
    ...

The purpose of the main guard is to avoid executing code unless the module is itself being executed as the top-level script. For more information about the main guard, you can consult the Python documentation.

Putting these together, we get a module that looks like the following:

#!/usr/bin/env python3

# Define test components
model = ...
specification = ...
optimizer = ...
options = ...

if __name__ == "__main__":
    runs = staliro(model, specification, optimizers, options)
    # Process result

Analyzing test results#

The output of the staliro function is a list of Run objects, with a length equal to the runs attribute of the TestOptions used for the test. Each Run object has the following attributes: - evaluations - result

The result attribute contains the return value from the optimizer while the evaluations attribute contains each sample generated by the optimizer, and its associated cost. Each evaluation also contains the extra data from the Result value returned from the cost function if a Result value was returned. If a Model and Specification were used, then the extra attribute for each evaluation will contain a value containing the Trace produced by the model, and the extra data returned from the both the Model and Specification if either returned a Result value.