EECS4315

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.
====== 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
<code>
javac -cp /cs/fac/packages/jpf/jpf-core/build/jpf.jar:. StateFrequency.java
</code>
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.
<code java>
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");
                }
            }
        }
    }
}
</code> 

To run JPF on the above app, use the following configuration file.
<code>
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
</code>

If the above configuration file is used with the above app, JPF should produce output similar to the following.
<code>
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
</code>

To receive feedback, submit your listener using the submit command before Tuesday February 5:
submit 4315 lab4 StateFrequency.java