Property File - xsafran1/pepmc2 GitHub Wiki

It is specification of property of the model which satisfaction will be verified. There are two types of line. #define line and #property line. Both mandatory.

#define line is used for definition of so-called atomic proposition (AP) which is composed of model's variable, relational operator (<, >, <=, >=) and threshold value of this variable. Every AP is named, for example:
#define a Var1 > 2.524
#define b gene_a <= 0.08

#property line is used for definition of property using the names of APs, temporal operators (X, F, G, U, R) and logical operators (||, &&, ->, <->, !). For example:
#property F (G a)
#property ((a && !b) U (!a && b)) || ((!a && b) U (a && !b))

For more informations about atomic propositions, temporal operators or just about linear temporal logic see wiki or in slovak my master thesis.