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=<path to the directory containing Traversal.class>
native_classpath=<path to the directory containing StateFrequency.class>
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