Mercurial > hg > Members > kono > jpf-core

annotate doc/intro/random_example.md @ 0:61d41facf527

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
initial v8 import (history reset)
author Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
date Fri, 23 Jan 2015 10:14:01 -0800
parents
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
0
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
1 # Example: `java.util.Random` #
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
2
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
3 We start with a simple example that uses java.util.Random. Consider the following program that obtains two random values in (2) and (3), and then performs some computation (4) with them.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
4
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
5 ~~~~~~~~ {.java}
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
6 import java.util.Random;
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
7
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
8 public class Rand {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
9 public static void main (String[] args) {
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
10 Random random = new Random(42); // (1)
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
11
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
12 int a = random.nextInt(2); // (2)
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
13 System.out.println("a=" + a);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
14
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
15 //... lots of code here
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
16
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
17 int b = random.nextInt(3); // (3)
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
18 System.out.println(" b=" + b);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
19
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
20 int c = a/(b+a -2); // (4)
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
21 System.out.println(" c=" + c);
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
22 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
23 }
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
24 ~~~~~~~~
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
25
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
26
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
27 ## Testing ##
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
28
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
29 Executing this program with a normal Java VM yields something like the following output. If we don't provide an explicit seed when creating the Random object in (1), the result is going to differ between runs, but every run will choose just a single `a` and `b` value (i.e. print just a single `"a=.."` and `"b=.."` line.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
30
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
31 ~~~~~~~~ {.java}
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
32 > java Rand
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
33 a=1
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
34 b=0
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
35 c=-1
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
36 >
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
37 ~~~~~~~~
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
38
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
39 Let's look at a graphical representation of all the ways our program could be executed, and how it actually was executed in our test run. The nodes of the graph represent *program states*, and the edges *transitions* the execution could take from a certain state.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
40
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
41 ![Figure 1: Random example](../graphics/sw-model-checking.svg){align=center width=700}
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
42
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
43 ## Model Checking ##
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
44
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
45 Enter JPF - not much different results if we start JPF as a plain 'java' replacement. The only difference is that it (a) takes longer to complete, and (b) tells us something about a "search", which hints on that something more than in our test run is going on
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
46
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
47 ~~~~~~~~ {.bash}
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
48 > bin/jpf Rand
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
49 JavaPathfinder v4.1 - (C) 1999-2007 RIACS/NASA Ames Research Center
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
50 ====================================================== system under test
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
51 application: /Users/pcmehlitz/tmp/Rand.java
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
52
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
53 ====================================================== search started: 5/23/07 11:48 PM
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
54 a=1
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
55 b=0
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
56 c=-1
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
57
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
58 ====================================================== results
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
59 no errors detected
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
60
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
61 ====================================================== search finished: 5/23/07 11:48 PM
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
62 >
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
63 ~~~~~~~~
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
64
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
65 What is this "search" supposed to mean? Looking at source line (4) we realize that there is a potential problem: for certain `a` and `b` values, this expression can cause a division by zero `ArithmeticException`. Depending on the random seed used in (1), it's quite possible we would never encounter this case if we run (i.e. test) the program with a normal JVM.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
66
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
67 Re-enter JPF - but this time we tell it to not only consider single values for `a` and `b`, but look at all possible choices:
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
68
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
69 ~~~~~~~~ {.bash}
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
70 > bin/jpf +cg.enumerate_random=true Rand
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
71 JavaPathfinder v4.1 - (C) 1999-2007 RIACS/NASA Ames Research Center
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
72 ====================================================== system under test
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
73 application: /Users/pcmehlitz/tmp/Rand.java
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
74
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
75 ====================================================== search started: 5/23/07 11:49 PM
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
76 a=0
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
77 b=0
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
78 c=0
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
79 b=1
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
80 c=0
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
81 b=2
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
82
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
83 ====================================================== error #1
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
84 gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
85 java.lang.ArithmeticException: division by zero
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
86 at Rand.main(Rand.java:15)
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
87 ....
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
88 >
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
89 ~~~~~~~~
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
90
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
91 What has happened? By specifying "+vm.enumerate_random=true" we told JPF to consider all possible values for expressions (2) and (3). JPF starts with `"a=0"`, then picks `"b=0"`, which yields a valid `"c=0"` value. But instead of terminating like a normal VM, JPF recognized that there are more choices left, so it backtracks to (3) and picks `"b=1"`. Again, no problem here with computing `"c=0"`. Back to (3), JPF now tries `"b=2"`, which of course spells disaster for our little program when executing (4), as can be seen by the following error report.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
92
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
93 Here is a graphical representation of this search process. It should be noted that JPF per default only runs up to the point where it finds an error or there are no more choices left to explore. But if we would somehow fix the `"a=0,b=2"` case, JPF would still find the `"a=1,b=1"` case in the next run, since it systematically tries all choices. No matter what error it finds, JPF also keeps the complete trace (execution path) how it got to this error (denoted by the red arrows), which means we don't have to debug the program to find out.
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
94
61d41facf527 initial v8 import (history reset)
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
95 ![Figure 2: Random example](../graphics/sw-model-checking-2.svg){align=center width=450}