.. include:: _substitutions.rst

=======================
Welcome to |psy-taliro|
=======================

|psy-taliro| is a python toolbox for search-based test generation, typically at the system
level. The objective of this library is to make writing and testing requirements for systems fast
and easy in order to help facilitate the adoption of formal and semi-formal methods for verifying
systems of all kinds. To this end, |psy-taliro| defines several testing interfaces and
multiple ready-to-use implementations so that users can quickly set up tests to ensure no bugs or
behavioral violations hide in their systems.

Motivation
----------

Consider that we are designing a simple switching thermostat system described by the following state
machine:

.. _thermostat:

.. figure:: _images/thermostat.svg
    :width: 600
    :align: center

    *Source: An Algebra of Hybrid Systems by Bernhard Moller and Peter Hofner (2009).*

When designing a system such as this one, we may be curious if there are any system inputs that
cause the system to violate its operating bounds. A naive approach would be to test all possible
inputs, but in a continuous input space like ours this approach is infeasible. Furthermore, for more
complex systems the input space may be very large, making a brute force approach even more
intractable. Therefore, we will instead leverage search techniques to test a subset of inputs, using
the results from each test to try and select inputs that will put the system closer to violating its
operating bounds. In order to do this, we must first create a representation of our system that we
can use to simulate its behavior. One possible representation of this system is the following Python
class:

.. code-block:: Python

    import enum

    class Thermostat:
        class Mode(enum.IntEnum):
            HEATING = 1
            COOLING = 2

        def __init__(self, initial_temp: float):
            self.temp = initial_temp
            self.mode = Thermostat.Mode.COOLING

        def step(self, step_size: float):
            if self.mode is Thermostat.Mode.COOLING and self.temp < 19:
                self.mode = Thermostat.Mode.HEATING

            if self.mode is Thermostat.Mode.COOLING and self.temp > 21:
                self.mode = Thermostat.Mode.COOLING

            temp_dot = -0.1 * self.temp

            if self.mode is Thermostat.Mode.HEATING:
                temp_dot = 5 + temp_dot

            self.temp = self.temp + temp_dot * step_size

Using this definition, we can define a :doc:`model <models>` component that is responsible for
encapsulating the execution logic of the model given a set of inputs.

.. code-block:: Python

    from staliro import models

    STEP_SIZE = 0.1

    @models.model()
    def thermostat(inputs: models.Sample) -> models.Trace[list[float]]:
        system = Thermostat(inputs.static["temp"])
        states = {}

        for step in range(100):
            time = step * STEP_SIZE
            states[time] = [system.temp]
            system.step(STEP_SIZE)

        return models.Trace(states)

Then we can represent a requirement of our system (in this case that the temperature of the system
stays within the interval :math:`[18.0, 22.0]`) using
:ref:`Signal Temporal Logic <signal-temporal-logic>`.

.. code-block:: Python

    from staliro import specifications

    req = specifications.RTAMTDense("(always (temp >= 18.0 and temp <= 22.0)", {"temp": 0})

Finally, we can instantiate an optimizer and define the test parameters in order to begin executing tests

.. code-block:: Python
    
    from staliro import TestOptions, optimizers, staliro

    optimizer = optimizers.UniformRandom()
    options = TestOptions(
        runs=1,
        iterations=100,
        static_inputs={
            "temp": (18.0, 22.0),
        }
    )

    runs = staliro(thermostat, req, optimizer, options)

The optimizer we have chosen to use is the :ref:`Uniform Random <uniform-random>` optimizer which
will generate samples uniformly across the input space. For our test parameters, we run a single
optimization attempt, with a sample budget of 100 samples, and we generate a single system input
called :math:`temp` which will be within the interval :math:`[18.0, 22.0]`. We execute the test by
calling the :py:func:`~staliro.staliro` function, which returns a set of :py:class:`~staliro.Run`
values containing all the samples generated by the optimizer, as well as their associated cost
values.

To quickly begin setting up your own tests, please refer to the :any:`quickstart` and
:any:`examples` pages. For more in-depth descriptions of the interfaces and components provided
by |psy-taliro| please refer to the :any:`API documentation <api/index>`.

Citing this project
-------------------

To cite our work, please include a reference to the following paper or include our :math:`Bib\TeX`
entry in your bibliography file.

`PSY-TaLiRo: A Python Toolbox for Search-Based Test Generation for Cyber-Physical Systems <https://arxiv.org/abs/2106.02200>`_

..
    cSpell: disable

.. code-block:: BibTeX

   @InProceedings{10.1007/978-3-030-85248-1_15,
       author="Thibeault, Quinn and Anderson, Jacob and Chandratre, Aniruddh and Pedrielli, Giulia and Fainekos, Georgios",
       editor="Lluch Lafuente, Alberto and Mavridou, Anastasia",
       title="PSY-TaLiRo: A Python Toolbox for Search-Based Test Generation for Cyber-Physical Systems",
       booktitle="Formal Methods for Industrial Critical Systems",
       year="2021",
       publisher="Springer International Publishing",
       address="Cham",
       pages="223--231",
       isbn="978-3-030-85248-1"
   }

..
    cSpell: enable

.. toctree::
    :hidden:

    quickstart
    installation
    examples

.. toctree::
    :hidden:
    :caption: Components

    signals
    cost_func
    models
    specifications
    optimizers

.. toctree::
    :hidden:
    :caption: Library

    options
    architecture
    API <api/index>
    caveats