.. include:: _substitutions.rst ========== Quickstart ========== |psy-taliro| is available on `PyPI `_. You can follow our :doc:`installation guide ` to set up your environment for running |psy-taliro| tests. Basic Structure --------------- A test in |psy-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 :ref:`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 :doc:`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 ------------------ |psy-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 :py:attr:`~staliro.Sample.static` and the :py:attr:`~staliro.Sample.signals` attributes which contain the static and signal inputs to the system respectively. .. _cost-function: Cost Functions ^^^^^^^^^^^^^^ A :any:`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 :py:func:`~staliro.costfunc` decorator to a function that accepts a sample and returns a cost value. .. code-block:: python 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. .. code-block:: python 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 |psy-taliro| provides dedicated functionality for users who wish to express their tests in terms of this composition. .. _model: :doc:`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 :ref:`Trace `. You can create a model by using the :py:func:`~staliro.model` :ref:`decorator ` with a function that returns a :py:class:`~staliro.models.Trace` or a |result| containing a ``Trace``. For convenience, you can construct an instance of :py:class:`models.Result `, which combines the construction a ``Trace`` and a ``Result`` object. .. code-block:: python 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") |psy-taliro| also provides alternative model implementations for representing different systems. The first is the :py:class:`~staliro.models.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 :py:func:`~staliro.blackbox` decorator function on a function that accepts a :py:class:`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). .. code-block:: python 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, |psy-taliro| provides the :py:class:`~staliro.models.Ode` model. To create this type of model, users can use the :py:func:`~staliro.ode` decorator to annotate a function that accepts an :py:class:`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. .. code-block:: python from staliro import models @models.ode(method="RK45") def system(inputs: models.Ode.Inputs) -> list[float]: ... .. _specification: After defining a ``Model``, users must also define a :py:class:`~staliro.specifications.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 :py:func:`~staliro.specification` decorator on a function that returns either a cost value or a |result| value containing extra metadata as well as the cost value. .. code-block:: python 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 :any:`Signal Temporal Logic ` (STL), |psy-taliro| provides two different specification implementations. The first is the :py:class:`~staliro.specifications.RTAMTDiscrete` specification, which requires input ``Trace`` values to have a constant time-step. The other is the :py:class:`~staliro.specifications.RTAMTDense` specification which does not require a constant time -step. Both implementations expect to evaluate traces with states of type :py:class:`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. .. code-block:: python 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: Optimizers ^^^^^^^^^^ The :py:class:`~staliro.optimizers.Optimizer` is responsible for selecting samples that the model will use to execute a simulation. At its core, an optimizer provides samples to the :ref:`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 :ref:`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 :py:func:`~staliro.optimizers.optimizer` decorator on a function that accepts an :py:class:`~staliro.optimizers.ObjFunc` and a set of optimization parameters :py:class:`Optimizer.Params `. The function can *optionally* return a result value at the end of an optimization attempt that is returned to the user. .. code-block:: python 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: ... |psy-taliro| provides two optimizers: :py:class:`~staliro.optimizers.UniformRandom` and :py:class:`~staliro.optimizers.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. .. code-block:: python 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 :py:class:`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, |psy-taliro| provides a type called :py:class:`Sampler`, which is created using the :py:func:`sampler` decorator on a generator function. An example of a :py:class:`Sampler` implementation would look like the following: .. code-block:: python 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: Options ------- .. note:: All parameters when constructing a ``TestOptions`` or ``SignalInput`` value must be provided as keywords. The :doc:`test options ` are used to configure the behavior of a |psy-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 :py:class:`~staliro.signals.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. .. code-block:: python 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 :py:func:`~staliro.staliro` function. ``staliro`` takes as input either 3 parameters (a :ref:`Cost Function `, an :ref:`Optimizer `, and a :ref:`TestOptions ` value) or 4 parameters (a :ref:`Model `, a :ref:`Specification `, an ``Optimizer``, and a ``TestOptions`` value). As output, the ``staliro`` function returns a list of :py:class:`~staliro.tests.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 :py:func:`staliro.test` function if you choose. .. code-block:: python :caption: 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) .. code-block:: python :caption: 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 `_. .. code-block:: python #!/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. .. code-block:: python 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: .. code-block:: python #!/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 :py:class:`Run` objects, with a length equal to the ``runs`` attribute of the :py:class:`TestOptions` used for the test. Each :py:class:`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 :py:class:`Result` value returned from the cost function if a ``Result`` value was returned. If a |model| and :py:class:`Specification` were used, then the ``extra`` attribute for each evaluation will contain a value containing the :py:class:`Trace` produced by the model, and the extra data returned from the both the ``Model`` and ``Specification`` if either returned a ``Result`` value.