Here, we will introduce you via a simple script to VyPR's offline analysis library. This library provides a set of functions that make it easy for developers to query data obtained by VyPR and perform post-processing to gain more insight into why their programs gave certain results.
See Part 2 for an example of an analysis script that has been used in the software development process of a real system.
To gain access to the analysis library's functions, assuming that you're in a directory into which the analysis library has been pulled (from here), our first step is to import the library:
import VyPRAnalysis as va
Before we perform any analysis, we need to tell the analysis library from which server we would like to take data. Here, we assume that VyPR's server is running locally on port 8080.
In order to set the URL of the verdict server, pass it as an argument to the set_server function.
va.set_server("http://localhost:8080/")
Use the instruction below to get the list of all function/property pairs that are monitored.
functions = va.list_functions()
We can now iterate through the functions list to get the calls of each function. For every function call, we can find the verdicts that were reached during that call. This is shown in the code section below.
for function in functions:
print(function)
calls = function.get_calls()
# for each call, get the verdicts reached during it
for call in calls:
print("\t%s" % call)
verdicts = call.get_verdicts()
for verdict in verdicts:
print("\t\t%s" % verdict)
observations = verdict.get_observations()
for observation in observations:
print("\t\t\t%s" % observation)
Example output from this script could look something like
<Function id=1, fully_qualified_name=app.routes.paths_branching_test, property=bfedfae3adddc758fc06e1d09cc7697f179c3414>
<FunctionCall id=1, function=1, time_of_call=2020-05-08T11:43:59.379985, end_time_of_call=2020-05-08T11:43:59.380236, trans=1>
<Verdict id=1, binding=1, verdict=1, time_obtained=2020-05-08T13:43:59.382659, function_call=1, collapsing_atom=1, collapsing_atom_sub_index=0>
<Observation id=1, instrumentation_point=2, verdict=1, observed_value=2.3e-05, observation_time=2020-05-08T11:43:59.380177, observation_end_time=2020-05-08T11:43:59.380200, atom_index=1, sub_index=0, previous_condition_offset=2>
<Observation id=2, instrumentation_point=1, verdict=1, observed_value={u'n': 5}, observation_time=2020-05-08T11:43:59.380147, observation_end_time=2020-05-08T11:43:59.380147, atom_index=0, sub_index=0, previous_condition_offset=2>
<FunctionCall id=2, function=1, time_of_call=2020-05-08T11:44:14.222275, end_time_of_call=2020-05-08T11:44:15.338245, trans=2>
<Verdict id=2, binding=1, verdict=1, time_obtained=2020-05-08T13:44:15.353779, function_call=2, collapsing_atom=0, collapsing_atom_sub_index=0>
<Observation id=3, instrumentation_point=2, verdict=2, observed_value=1.115589, observation_time=2020-05-08T11:44:14.222529, observation_end_time=2020-05-08T11:44:15.338118, atom_index=1, sub_index=0, previous_condition_offset=14>
<Observation id=4, instrumentation_point=1, verdict=2, observed_value={u'n': 11}, observation_time=2020-05-08T11:44:14.222498, observation_end_time=2020-05-08T11:44:14.222498, atom_index=0, sub_index=0, previous_condition_offset=14>
Based on the specification file found at http://cern.ch/vypr/VyPR_queries.py :
verification_conf = {
"app.routes" : {
"paths_branching_test" : [
Forall(
t = calls('f')
).Check(
lambda t : (
If(t.input()('n')._in([0, 10])).then(
t.duration()._in([0, 1])
)
)
)
]
}
}
In particular, in the output shown above, we see that, for each FunctionCall, there is a single a Verdict object generated by VyPR during monitoring. For the query above, we expect one verdict per call of f observed (based on the name used in code; VyPR does not yet try to determine calls to f under different names).
For each verdict that we get, for our specification above, VyPR needed to observe the value of n and the duration of the call to f, so we have two observations. You can see that each verdict contains an observation with a value representing a number of second, and another observation with a value representing a value of n.