Implement a listener and publisher that, given the following app,
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");
}
}
}
and the application configuration file
target=Example
classpath=.
native_classpath=.
listener=AmountOfNonDeterminism
cg.enumerate_random=true
produces output similar to
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
That is, JPF reports the maximum amount of nondeterminism (maximum number of outgoing transitions from any state of the system under test).
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.