Writing Queries for VyPR

• Introduction
• Defining Constraints
• Selecting Points of Interest
• Reference

States

Comparison

For the value to which a state q maps x, you can construct the predicates:

q('x').equals(v)
q('x')._in([n, m])
q('x')._in((n, m))
q('x') < v
q('x') <= v

Here, v is either a constant or another measurable quantity (see above).

Operators

You can find the next call in time to the function f with:

q.next_call('f')

and treat the result as a call.

You can find the length of the value held in the variable x with:

q('x').length()

Calls

For a call t, you can measure the duration with:

t.duration()

and write predicates on this duration:

t.duration()._in([n, m])
t.duration()._in((n, m))
t.duration() < v
t.duration() <= v

Here, v is either a constant or another measurable quantity (see above).

Currently arithmetic with measurable quantities with respect to constants is supported in a limited form:

t.duration() < v * n

where n is some constant of the same type of the measured quantity v. NB: here, multiplication must be on the right-hand side.

The states at either side of a call can be obtained with:

t.input(), t.result()

which gives a state object like any other. Hence, you could write something like:

t.input()('x') < t.result()('y')

The time between two states can be measured with:

timeBetween(q1, q2)

which can then be subject to a constraint by writing:

timeBetween(q1, q2)._in([n, m])
timeBetween(q1, q2) < n
timeBetween(q1, q2) <= n

Here, n and m must be constants; VyPR does not yet support comparison of the result of timeBetween with other measurable quantities.

Multiple Constraints

You can use boolean operators to combine predicates:

land(a1, a2, ..., a_n)
lor(a_1, ..., a_n)
lnot(a)

There is syntactic sugar for things like implication, which you can write as:

If(a).then(b)

You must wrap your final property in a lambda; VyPR will use this at runtime:

lambda q1, ..., qn : (...)

Point of Interest Selection

You can select points of interest based on states or calls with:

q = changes('x')
t = calls('f')

If a selection predicate is given after the first one in the list, it must depend on the previous one:

Forall(q = changes('x')).Forall(t = calls('f', after='q'))...

The property to check at each point of interest is given by supplying the lambda to the Check method defined on the result of a chain of calls to Forall:

Forall(q1 = ...). ... .Forall(qn = ...).\
Check(
  lambda q1, ..., qn : (...)
)