====== Lab 4 ======
Implement a listener, named StateFrequency, that prints the IDs of the states and the number of times the state has been visited. A sample run can be found below. It shows what type of output your listener should produce. Here are some hints that may be useful for implementing your listener.
* Consider the interface SearchListener, which are part of the package gov.nasa.jpf.search.
* Consider which methods of the interface SearchListener are relevant.
* Exclude the state with ID -1.
To compile your listener, use
javac -cp /cs/fac/packages/jpf/jpf-core/build/jpf.jar:. StateFrequency.java
or add /cs/fac/packages/jpf/jpf-core/build/jpf.jar as an external library to Eclipse.
To test your listener, you may want to use the following app.
import java.util.Random;
public class Traversal {
public static void main(String[] args) {
Random random = new Random();
System.out.println("0");
if (random.nextBoolean()) {
System.out.println("2");
} else {
System.out.println("1");
if (random.nextBoolean()) {
System.out.println("4");
} else {
System.out.println("3");
if (random.nextBoolean()) {
System.out.println("6");
} else {
System.out.println("5");
}
}
}
}
}
To run JPF on the above app, use the following configuration file.
target=Template
classpath=
native_classpath=
cg.enumerate_random=true
listener=StateFrequency
If the above configuration file is used with the above app, JPF should produce output similar to the following.
JavaPathfinder core system v8.0 (rev d772dfa80ea692f916aa6718d04c4f7bfb2a746b) - (C) 2005-2014 United States Government. All rights reserved.
====================================================== system under test
Traversal.main()
====================================================== search started: 1/28/19 8:09 PM
0
1
3
5
6
4
2
====================================================== frequencies
state frequency
0 3
1 3
2 3
3 4
====================================================== results
no errors detected
====================================================== statistics
elapsed time: 00:00:00
states: new=4,visited=3,backtracked=7,end=4
search: maxDepth=4,constraints=0
choice generators: thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=3
heap: new=368,released=42,maxLive=358,gcCycles=7
instructions: 3247
max memory: 240MB
loaded code: classes=62,methods=1341
====================================================== search finished: 1/28/19 8:09 PM
To receive feedback, submit your listener using the submit command before Tuesday February 5:
submit 4315 lab4 StateFrequency.java