Writing Requirements

OPPAS supports writing requirements in Linear Temporal Logic (LTL) [12] and Precedence Oriented Temporal Logic (POTL) [1].

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 [1].

For technical reasons explained in [8], POPACheck does not support the whole POTL logic. Rather, it supports a fragment thereof called POTL \(\chi\), plus full future LTL. The last column of the table shows whether an operator is supported by POPACheck.

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