Today I'm going to show a quick example of the kinds of output you might see when running jpf-prism. To do this, I'll talk about the Biased Die example that is provided by jpf-probabilistic (and has been copied into our repository), since this one is already publicly available. Over simplifying, the example is of a system that generates the roll of a die with some bias during computation. The computation of the roll result is done by an algorithm from Knuth and Yao in '76; the jpf-probabilistic repository describes it in greater detail, so check it out there if you're unfamiliar with it. jpf-probabilistic would display the something similar to following (taken from the jpf-probabilistic repository, note that in this case there's no bias, since the probabilities are all 0.5):
0 ------> 1 1 ------> 2 2 -0.50-> 3 3 -0.50-> 4 4 -0.50-> 3 4 -0.50-> 5 * 3 -0.50-> 6 6 -0.50-> 5 * 6 -0.50-> 5 * 2 -0.50-> 7 7 -0.50-> 8 8 -0.50-> 5 * 8 -0.50-> 5 * 7 -0.50-> 9 9 -0.50-> 7 9 -0.50-> 5 *
For this example, the property we'll check is whether or not the roll is less than 2 (i.e., a 1 is rolled).
While in jpf-prism we can do something similar, we only get an output like that if we're in debugging mode, and then we get a whole more (probably uninteresting) information, so don't expect quite that. We do display the Markov chain for our SUT, but only after we've built it, passed it to PRISM, and then queried for it. In short, this means a less pretty output for the chain itself. So what we actually get is the following:
Executing command: java -jar C:\Users\Jan\Documents\Google Summer of Code 2013\GSoC2013 Workspace\jpf-core\build\RunJPF.jar +shell.port=4242 C:\Users\Jan\Documents\Google Summer of Code 2013\GSoC2013 Workspace\jpf-prism\src\examples\prism\probabilistic\BiasedDieTest.jpf
JavaPathfinder v7.0 (rev 1067+) - (C) RIACS/NASA Ames Research Center
====================================================== system under test
prism.probabilistic.BiasedDieTest.main()
====================================================== search started: 15/09/13 5:19 PM
a: 1
a: 5
a: 4
a: 6
a: 2
a: 3
====================================================== Exporting to PRISM
Search finished, printing PRISM's interpretation of the Markov Chain
trans: [ 0: {1=1.0}, 1: {2=0.5, 3=0.5}, 2: {4=0.5, 5=0.5}, 3: {6=0.5, 7=0.5}, 4: {2=0.5, 8=0.5}, 5: {8=1.0}, 6: {8=0.5, 9=0.5}, 7: {3=0.5, 8=0.5}, 8: {}, 9: {8=1.0} ]
Printing to dot file "C:\Users\Jan\Documents\Google Summer of Code 2013\GSoC2013 Workspace\jpf-prism\dotfile.txt"
In order to make this easier to read, I suggest exporting the chain to a dotfile, and viewing the result with Graphviz. The result is an image like the following:
Which is much easier to read than a text representation anyways. Note that there may also be more or fewer states, depending on if we can condense a chain of probability 1 transition/state pairs, or if we need to add states because a property's evaluation in the SUT becomes different and we need to track that to determine which state to pass to PRISM.
After jpf-prism outputs this information, PRISM will then compute the reachability probabilities for each of the probabilities, and that will look something like this.
Starting probabilistic reachability...
Starting Prob0...
Prob0 took 4 iterations and 0.001 seconds.
Starting Prob1...
Prob1 took 8 iterations and 0.0 seconds.
target=1, yes=1, no=5, maybe=4
Starting Gauss-Seidel...
Gauss-Seidel took 17 iterations and 0.001 seconds.
Probabilistic reachability took 0.002 seconds.
0.16666666651144624
And then JPF will finish its output:
====================================================== results
no errors detected
====================================================== statistics
elapsed time: 00:00:00
states: new=10, visited=7, backtracked=17, end=6
search: maxDepth=0, constraints hit=0
choice generators: thread=3 (signal=0, lock=1, shared ref=0), data=7
heap: new=690, released=95, max live=0, gc-cycles=17
instructions: 10829
max memory: 120MB
loaded code: classes=65, methods=1334
====================================================== search finished: 15/09/13 5:19 PM
And that's it! To verify the accuracy, you might simulate the SUT a few times to see if this value matches in practice. If you did that, the output would look something like this:
Executing command: java -jar C:\Users\Jan\Documents\Google Summer of Code 2013\GSoC2013 Workspace\jpf-core\build\RunJPF.jar +shell.port=4242 C:\Users\Jan\Documents\Google Summer of Code 2013\GSoC2013 Workspace\jpf-prism\src\examples\prism\probabilistic\BiasedDieTest.jpf
JavaPathfinder v7.0 (rev 1067+) - (C) RIACS/NASA Ames Research Center
====================================================== system under test
prism.probabilistic.BiasedDieTest.main()
====================================================== search started: 15/09/13 5:14 PM
====================================================== Simulation #0
a: 3
...(omitted)
====================================================== Simulation #9999
a: 1
p1 was true in this simulation.
====================================================== Simulations over: results
p1 was true at the end of the simulation 1694/10000 = 0.1694% of the time.
====================================================== results
no errors detected
====================================================== statistics
elapsed time: 00:01:46
states: new=0, visited=0, backtracked=0, end=0
search: maxDepth=0, constraints hit=0
choice generators: thread=22793 (signal=0, lock=10000, shared ref=0), data=36708
heap: new=4210184, released=200000, max live=0, gc-cycles=59501
instructions: 104953788
max memory: 0MB
loaded code: classes=65, methods=1334
====================================================== search finished: 15/09/13 5:15 PM
Note that this value is pretty close to the one above, so things went as expected. And for a fair die, the probability of rolling a 1 should be 1/6 = ~0.166666..., so we have even more confidence in the answer.
No comments:
Post a Comment