.. _property_statecharts:

Monitoring properties
=====================


About runtime verification
--------------------------

Another key feature of Sismic's interpreter is its support for monitoring properties at runtime, not only contracts.
To avoid a statechart designer needing to learn a different language for expressing such properties,
these properties are expressed using the statechart notation. These properties are then called *property statecharts*


Using statecharts to express properties
---------------------------------------

Property statecharts can be used to express functional properties of the intended behaviour in terms of the events
that are consumed or sent, or in terms of the states that are entered or exited by a statechart.
When a statechart is executed by Sismic, specific meta-events are created based on the events that are sent or
consumed, the states that are entered of exited, etc. When the statechart being monitored is executed, the meta-events
are propagated to all associated property statecharts.
The property statecharts will look for property violations based on those meta-events, following a *fail fast*
approach: they will report a failure as soon as the monitored behavior leads to a final state of the property
statechart.

Due to the meta-events being considered and the "fail-fast" approach adopted by Sismic for their
verification, property statecharts are mainly intended to check for the presence of undesirable behavior
(safety properties), i.e., properties that can be checked on a (finite) prefix of a (possibly infinite) execution trace.
While it is technically possible to use property statecharts to express liveliness properties
(something desirable *eventually* happens), this would require additional code for their verification since
liveliness properties are not supported "as is" by Sismic.

During the execution of a statechart, several meta-events are created depending on what happens in the statechart
being executed. Those meta-events are automatically send to any previously bound property statechart.

To bind a property statechart to an interpreter, it suffices to provide the property statechart as a
parameter of the :py:meth:`~sismic.interpreter.Interpreter.bind_property_statechart` method of an interpreter.
This method accepts a :py:class:`~sismic.model.Statechart` instance that is used to create an interpreter for 
the property statechart. This method also accepts an optional ``interpreter_klass`` parameter as a callable accepting
a :py:class:`~sismic.model.Statechart` and a named parameter ``clock`` (a :py:class:`~sismic.clock.Clock` instance)
and is used to build an interpreter for the property statechart. 

If a property statechart reaches a final state during its execution, then the property is considered as not
satisfied, and a :py:class:`~sismic.exceptions.PropertyStatechartError` is raised.
This exception provides access to the interpreter that executed the property, the active configuration of statechart
being executed, the latest executed :py:class:`~sismic.model.MacroStep` and the current context of the interpreter.


Meta-events generated by the interpreter
----------------------------------------

The complete list of :py:class:`~sismic.model.MetaEvent` that are created by the interpreter is described in the
documentation of the :py:meth:`~sismic.interpreter.Interpreter.attach` method:

.. automethod:: sismic.interpreter.Interpreter.attach
    :noindex:

.. note:: 

    Property statecharts are not the only way to listen to these meta-events. Any listener
    that is attached with :py:meth:`~sismic.interpreter.Interpreter.attach` will receive these 
    meta-events.
    
Property statecharts can listen to what happens in an interpreter when they are bound to 
this interpreter, using :py:meth:`~sismic.interpreter.Interpreter.bind_property_statechart` method:

.. automethod:: sismic.interpreter.Interpreter.bind_property_statechart
    :noindex:

Internally, this method wraps given property statechart to an appropriate listener, and 
calls :py:meth:`~sismic.interpreter.Interpreter.attach` so you don't have to.
Bound property statecharts can be unbound from the interpreter by calling the 
:py:meth:`~sismic.interpreter.Interpreter.detach` method. This method accepts a 
previously attached listener, so you'll need to keep track of the listener returned
by the initial call to :py:meth:`~sismic.interpreter.Interpreter.bind_property_statechart`.


Examples of property statecharts
--------------------------------

7th floor is never reached
^^^^^^^^^^^^^^^^^^^^^^^^^^

This property statechart ensures that the 7th floor is never reached.
It stores the current floor based on the number of times the elevator goes up
and goes down.

.. literalinclude:: /examples/elevator/tester_elevator_7th_floor_never_reached.yaml
   :language: yaml


Elevator moves after 10 seconds
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

This property statechart checks that the elevator automatically moves after some idle time if it is not on
the ground floor. The test sets a timeout of 12 seconds, but it should work for any number strictly greater than
10 seconds.

.. literalinclude:: /examples/elevator/tester_elevator_moves_after_10s.yaml
   :language: yaml


Heating does not start if door is opened
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

This property statechart checks that the heating of a microwave could not start if the door is currently opened.

.. literalinclude:: /examples/microwave/heating_on_property.yaml
   :language: yaml

Heating must stop when door is opened
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

This property statechart ensures that the heating should quickly stop when the door is open while cooking occurs.

.. literalinclude:: /examples/elevator/heating_off_property.yaml
   :language: yaml