Once a property is defined, VyPR must be told where in the program to check. Without this, the variables you use in your property have no meaning. Suppose that you want to take
If(q('x') <= 10).then(
q.next_call('f') <= 0.5
)
and check it whenever x changes (so q holds the state in which x has changed). You can do this with:
Forall(q = changes('x')).\
Check(
lambda q : (
If(q('x') <= 10).then(
q.next_call('f') <= 0.5
)
)
)
The Forall tells VyPR that the property given to Check should be checked whenever x changes at runtime. Further, each time x changes, the state induced will be bound to the variable q.
Suppose you want to check that, whenever file changes, if file is equal to some string, every future call to write should satisfy some constraint. Then you can write the query:
Forall(q = changes('file')).\
Forall(t = calls('write', after='q')).\
Check(
lambda q, t : (
If(q('file').equals('some file name')).then(
t.duration() <= 1
)
)
)