Reelay reads executable specifications written in plain text and verifies that the system does what those specifications say at runtime. To construct runtime monitors automatically, those specifications must follow some basic syntax rules, called Rye format for short.
Rye format uses a set of special constructs (that is, keywords and punctuation) to describe desired system behavior over temporal data streams expressed in structured data formats like multiline JSON or CSV.
These syntactic constructs are divided into four categories:
- Atomic expressions
- Boolean logic expressions
- Temporal logic expressions
- Regular expressions (in future releases)
Let's start with atomic expressions.
Atomic expressions are the basic building blocks of Reelay expressions. Basic atoms use the curly-bracket syntax {...} and describes a set of constraints over data objects. For example, an atomic expression such as
{lights_on: true, speed > 20.0, mode: "Sport XL"}
will be evaluated to true for time points 101 and 102 below over a temporal behavior given as a sequence of JSON objects such that
...
{"time": 101, "lights_on": true, "speed": 21.23, "mode": "Sport XL"}
{"time": 102, "lights_on": true, "speed": 20.01, "mode": "Sport XL"}
{"time": 103, "lights_on": true, "speed": 19.12, "mode": "Sport XL"}
...Currently Reelay supports Booleans (true, false), numerical comparisons (<, <=, >, >=, ==, !=), string equivalences inside curly atoms over data objects.
Non-existent or unspecified field names in data objects and their values do not change the value of the atomic expression. For example, an atomic expression such as
{speed > 21.0}
will be evaluated to true for the time point 101 and false for time points 102 and 103 regardless of the value of other fields in the objects. For the case where you require that a field exists in the object but don't care about its value, Reelay uses the asterisk (*) symbol to denote that any value is acceptable. For example,
{lights_on: true, speed > 19.0, mode: *}
will be evaluated to true for time points 101, 102, and 103 but to false for a data object
{"time": 104, "lights_on": true, "speed": 21.23}since it does not contain any field named as mode.
Finally Reelay allows to declare categorical variable references inside atoms using the *ref_name syntax such that
{lights_on: true, speed > 20, mode: *myref}
Then this reference called myref can be used elsewhere in the expression and quantified by exists and forall operators. More details regarding these operators are given in the following section of logical constructs.
This section describe Boolean logic operations over atomic Reelay expressions. we mainly use curly atoms in the examples but these constructs are equally applicable unless anything noted.
The negation of Reelay expressions is defined by using keywords not and !.
not {key1: value1, key2: value2}
The conjuction of Reelay expressions is defined by using keywords and and &&.
One can see that atomic expression syntax is a shortcut for conjunction between atomic constraints. Two Reelay expressions below are functionally equivalent:
{key1: value1, key2: value2}
and
{key1: value1} and {key2: value2}
The disjunction of constraints has to defined explicitly using keywords or and ||.
{key1: value1} or {key2: value2}
Logical implication is a popular Boolean operation when writing conditional specifications. The logical implication of constraints has to defined explicitly using keywords implies and ->.
{key1: value1} -> {key2: value2}
The ability to refer to data values (unknown at compile time) is one of the advanced features of Reelay. Roughly speaking, a reference variable acts a memory location where many data values (from a key) can be stored and can be checked later (or with another key) for the equality. Then these data values can quantified for existence (exists) and universality (forall). Note that this feature is currently supported for categorical variables (e.g. strings) only.
The syntax for references and quantifiers is as follows:
exists[ref1, ref2, ...]. RYE(ref1, ref2, ...)
forall[ref1, ref2, ...]. RYE(ref1, ref2, ...)
where RYE(ref1, ref2, ...) is an arbitrary Reelay expression that contains reference declarations ref1, ref2, ... inside its atoms.
For example, we may want to check the equality of data values for two fields but don't know or cannot write all possible cases at compile time.
exists[refname]. {key1: *refname, key2: *refname}
This expression above will be evaluated to true for the data object
{"key1": "hello", "key2": "hello"}but false for the data object
{"key1": "hello", "key2": "world"}as two string values are not equal in the latter. More advanced use of references involve temporal expressions explained in the following sections, which allow us checking data values from different time points.
The unary operation of previously is defined using keywords pre and Y. For example, consider the Reelay expression
pre{lights_on: true}
which is true at the current time point if lights were on in the previous time point.
Note that previously operation is only meaningful for untimed and discrete timed settings but dense timed settings.
The unary operation of once is defined using keywords once and P. For example, consider the Reelay expression
once{lights_on: true}
which is true at the current time point if lights were on in sometime in the past. It is possible to add timing constraints to the specification such that
once[a:b]{lights_on: true}
which is true at the current time point if lights were always on in sometime between b and a time units before now. We use the syntax [a:] and [:b] if there is no constraints on upper and lower bounds, respectively.
The unary operation of historically is defined using keywords historically and H. For example, consider the Reelay expression
historically{lights_on: true}
which is true at the current time point if lights were on in some time in the past. It is possible to add timing constraints to the specification such that
historically[a:b]{lights_on: true}
which is true at the current time point if lights were always on between b and a time units before now. We use the syntax [a:] and [:b] if there is no constraints on upper and lower bounds, respectively.
The binary operation of since is defined using keywords since and S. For example, consider the Reelay expression
{speed < 30} since {lights_on: true}
which is true at the current time point if the variable speed is always less than 30 units since lights_on is true last time. It is possible to add timing constraints to the specification such that
{speed < 30} since[a:b] {lights_on: true}
which is true at the current time point if the variable speed is always less than 30 since lights_on is true sometime between b and a time units before now. We use the syntax [a:] and [:b] if there is no constraints on upper and lower bounds, respectively.
As a rule of thumb, unary operators bind stronger than binary operators (except quantifiers, better use parantheses) and unary operators are eagerly matching therefore an expression such as
not {...} since {...}
would be parsed as
(not {...}) since {...}
and not as
not ({...} since {...})