.. _writing-requirements:

Writing Requirements
====================

OPPAS supports writing requirements in Linear Temporal Logic (LTL) :cite:p:`BaierK08`
and Precedence Oriented Temporal Logic (POTL) :cite:p:`ChiariMP21`.

POTL formulas can be written by using the operators in the “POMC
Operator” column of the table below, following the same
syntax rules as in :cite:p:`ChiariMP21`.

For technical reasons explained in
:cite:p:`abs-2404-03515`, POPACheck does not support the whole POTL logic.
Rather, it supports a fragment thereof called POTL :math:`\chi`, plus full future LTL.
The last column of the table shows whether an operator is supported by POPACheck.

.. table:: This table contains all currently supported (temporal) logic
  operators, in descending order of precedence. Operators listed on the
  same line are synonyms. Operators in the same group have the same
  precedence. Note that operators are case sensitive.

  +----------------------------+----------------+----------+----------------+-------------------+
  | Operator                   | POMC Operator  | Notation | Associativity  | POTL :math:`\chi` |
  +============================+================+==========+================+===================+
  | :math:`\neg`               | ``~``, ``Not`` | Prefix   | –              | ✓                 |
  +----------------------------+----------------+----------+----------------+-------------------+
  | :math:`\bigcirc^d`         | ``PNd``        | Prefix   | –              | ✓                 |
  +----------------------------+----------------+----------+----------------+-------------------+
  | :math:`\bigcirc^u`         | ``PNu``        | Prefix   | –              | ✓                 |
  +----------------------------+----------------+----------+----------------+-------------------+
  | :math:`\circleddash^d`     | ``PBd``        | Prefix   | –              | ✗                 |
  +----------------------------+----------------+----------+----------------+-------------------+
  | :math:`\circleddash^u`     | ``PBu``        | Prefix   | –              | ✗                 |
  +----------------------------+----------------+----------+----------------+-------------------+
  | :math:`\chi_F^{d}`         | ``XNd``        | Prefix   | –              | ✓                 |
  +----------------------------+----------------+----------+----------------+-------------------+
  | :math:`\chi_F^{u}`         | ``XNu``        | Prefix   | –              | ✓                 |
  +----------------------------+----------------+----------+----------------+-------------------+
  | :math:`\chi_P^{d}`         | ``XBd``        | Prefix   | –              | ✗                 |
  +----------------------------+----------------+----------+----------------+-------------------+
  | :math:`\chi_P^{u}`         | ``XBu``        | Prefix   | –              | ✗                 |
  +----------------------------+----------------+----------+----------------+-------------------+
  | :math:`\bigcirc_H^{d}`     | ``HNd``        | Prefix   | –              | ✗                 |
  +----------------------------+----------------+----------+----------------+-------------------+
  | :math:`\bigcirc_H^{u}`     | ``HNu``        | Prefix   | –              | ✗                 |
  +----------------------------+----------------+----------+----------------+-------------------+
  | :math:`\circleddash_H^{d}` | ``HBd``        | Prefix   | –              | ✗                 |
  +----------------------------+----------------+----------+----------------+-------------------+
  | :math:`\circleddash_H^{u}` | ``HBu``        | Prefix   | –              | ✗                 |
  +----------------------------+----------------+----------+----------------+-------------------+
  | :math:`\bigcirc` (LTL)     | ``N``          | Prefix   | –              | ✓                 |
  +----------------------------+----------------+----------+----------------+-------------------+
  | :math:`\Diamond` (LTL)     | ``F``,         | Prefix   | –              | ✓                 |
  |                            | ``Eventually`` |          |                |                   |
  +----------------------------+----------------+----------+----------------+-------------------+
  | :math:`\square` (LTL)      | ``G``,         | Prefix   | –              | ✓                 |
  |                            | ``Always``     |          |                |                   |
  +----------------------------+----------------+----------+----------------+-------------------+
  | :math:`\mathcal{U}` (LTL)  | ``U``          | Infix    | Right          | ✓                 |
  +----------------------------+----------------+----------+----------------+-------------------+
  | :math:`\mathcal{U}_\chi^d` | ``Ud``         | Infix    | Right          | ✓                 |
  +----------------------------+----------------+----------+----------------+-------------------+
  | :math:`\mathcal{U}_\chi^u` | ``Uu``         | Infix    | Right          | ✓                 |
  +----------------------------+----------------+----------+----------------+-------------------+
  | :math:`\mathcal{S}_\chi^d` | ``Sd``         | Infix    | Right          | ✗                 |
  +----------------------------+----------------+----------+----------------+-------------------+
  | :math:`\mathcal{S}_\chi^u` | ``Su``         | Infix    | Right          | ✗                 |
  +----------------------------+----------------+----------+----------------+-------------------+
  | :math:`\mathcal{U}_H^d`    | ``HUd``        | Infix    | Right          | ✗                 |
  +----------------------------+----------------+----------+----------------+-------------------+
  | :math:`\mathcal{U}_H^u`    | ``HUu``        | Infix    | Right          | ✗                 |
  +----------------------------+----------------+----------+----------------+-------------------+
  | :math:`\mathcal{S}_H^d`    | ``HSd``        | Infix    | Right          | ✗                 |
  +----------------------------+----------------+----------+----------------+-------------------+
  | :math:`\mathcal{S}_H^u`    | ``HSu``        | Infix    | Right          | ✗                 |
  +----------------------------+----------------+----------+----------------+-------------------+
  | :math:`\land`              | ``And``,       | Infix    | Left           | ✓                 |
  |                            | ``&&``         |          |                |                   |
  +----------------------------+----------------+----------+----------------+-------------------+
  | :math:`\lor`               | ``Or``, ``||`` | Infix    | Left           | ✓                 |
  +----------------------------+----------------+----------+----------------+-------------------+
  | :math:`\oplus`             | ``Xor``        | Infix    | Left           | ✓                 |
  +----------------------------+----------------+----------+----------------+-------------------+
  | :math:`\implies`           | ``Implies``,   | Infix    | Right          | ✓                 |
  |                            | ``-->``        |          |                |                   |
  +----------------------------+----------------+----------+----------------+-------------------+
  | :math:`\iff`               | ``Iff``,       | Infix    | Right          | ✓                 |
  |                            | ``<-->``       |          |                |                   |
  +----------------------------+----------------+----------+----------------+-------------------+