User Tools

Site Tools


lab5

Lab 2

Write a listener, named LongestPath, that keeps track of the length of a longest path in the state space. The method getDepth of the class Search might be helpful (see JPF's API). To make it a little easier, you do not have to consider state spaces with cycles. A sample run can be found below. It shows what type of output your listener should produce.

To compile your listener, use

javac -cp /cs/fac/packages/jpf/jpf-core/build/jpf.jar:. LongestPath.java

or add /cs/fac/packages/jpf/jpf-core/build/jpf.jar as an external library to Eclipse.

Also write an app, named Path, to test your listener. Finally, write an application properties file to run JPF with your listener on the app.

To receive feedback, submit your listener, your app, and your application properties file using the submit command before Tuesday January 28:

submit 4315 lab2 LongestPath.java Path.java Path.jpf

Sample output:

JavaPathfinder core system v8.0 (rev d772dfa80ea692f916aa6718d04c4f7bfb2a746b) -
 (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
Path.main()

====================================================== search started: 1/19/20 4:08 PM
0
1
3
5
6
4
2
Longest path has length 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:         57MB
loaded code:        classes=62,methods=1341

====================================================== search finished: 1/19/20 4:08 PM
lab5.txt · Last modified: 2020/01/19 20:51 by franck