We break down function runs into sequences of states (variables and their values) and operations that take place to transform those values.
VyPR currently supports writing constraints over variables' values and function calls. These are treated as objects on which you can call methods to build up constraints.
Suppose that q holds a state. Then we can check that the value given to x by q is no more than 1:
q('x') <= 1
Currently the only transitions that are supported are function calls. We can take a call t that corresponds to a function call and check that it lasts for no more than 2 seconds:
t.duration() <= 2
Given a variable, say q, you can obtain the earliest state or call in the future based on some criteria, and then use the result like a normal variable:
q.next_call('f').duration() <= 1
Given any variable t that represents a call, we can ask for the states at either side with
t.input()
and
t.result()
We can then treat these like any other states, for example by measuring the value to which they map a program variable:
t.result()('x')
Measured quantities can also be compared to each other. We can compare state, for example to check that a function is not modifying a variable:
t.input()('x').equals(t.result()('x'))
or to check that the duration of a function call has a certain relation to some state:
q.next_call('f').duration() < q('val')
There are standard propositional operators for you to link predicates on variables. For example, you can place a constraint on the next call along from the state q, but guarded by a constraint on q:
If(q('x') <= 10).then(
q.next_call('f').duration() <= 0.5
)
We could combine the if-then construct to write something like
If(q.next_call('f').input()('x') <= 10).then(
q.next_call('f').duration() <= 0.5)
)
which asserts that, for some state held by the variable q, if the value of x immediately before the next call to f is no more than 10, then the next call to f should take no more than 0.5 seconds.