This is an old revision of the document!
Implement a listener and publisher that, given the following app,
<pre>
import java.util.Random;
public class Example {
public static void main(String[] args) {
Random random = new Random();
if (random.nextBoolean()) {
System.out.println("true");
} else {
System.out.println("false");
}
}
}
</pre>
and the application configuration file
<pre>
target=Example
classpath=.
native_classpath=.
listener=AmountOfNonDeterminism
cg.enumerate_random=true
</pre>
produces output similar to
<pre>
JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved.
====================================================== system under test
Example.main()
====================================================== search started: 3/2/16 2:27 PM
false
true
======================================================
maximum amount of nondeterminism: 2 choice(s)
====================================================== results
no errors detected
====================================================== statistics
elapsed time: 00:00:00
states: new=1,visited=0,backtracked=1,end=1
search: maxDepth=1,constraints=0
choice generators: thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=0
heap: new=352,released=12,maxLive=0,gcCycles=1
instructions: 3176
max memory: 56MB
loaded code: classes=61,methods=1332
====================================================== search finished: 3/2/16 2:27 PM
</pre>
Apart from the classes that have been discussed in the lectures, also the class ChoiceGenerator, which is part of the package gov.nasa.jpf.vm, may be useful.