Skip Navigation
York U: Redefine the PossibleHOME | Current Students | Faculty & Staff | Research | International
Search »FacultiesLibrariesCampus MapsYork U OrganizationDirectorySite Index
Future Students, Alumni & Visitors
lab4

This shows you the differences between two versions of the page.

lab4 [2016/01/27 16:46]
franck created
lab4 [2016/01/27 17:02] (current)
franck
Line 2: Line 2:
{{:public:statespace.png|}} {{:public:statespace.png|}}
 +
 +If we run JPF with the search strategy BFS, the states are explored in the following order: s0, s1, s2, s3, s4; with DFS, the order is : s0, s1, s3, s4, s2.
 +
 +JPF also contains a search strategy which is called random search (RS).  The strategy will start with the initial state (s0 in our example) and follow one path of the execution until there is no next state and then it continues its search from the initial state. Two possible paths explored by RS are: s0, s2 and s0, s1, s_3.
 +
 +**Task 1.** Develop a Java app that prints output.  When checking the Java app by JPF with DFS the output should be different from the output for BFS.
 +
 +**Task 2.** Verify your program using JPF with BFS, DFS. To do that, you need to create an application properties file (.jpf file) for your Java app developed in Task 1. Configure the search property to be gov.nasa.jpf.search.heuristic.BFSHeuristic or gov.nasa.jpf.search.heuristic.DFSHeuristic.
 +
 +**Task 3.** Generate the state space diagram for BFS and DFS. To do this you need to set  the listener to StateSpaceDot.
 +
 +**Task 4.** Verify your program using RS. RS can explore several random executions and in JPF you have the freedom to set the maximum number of executions you would like RS to explore. Firstly, set your search strategy to gov.nasa.jpf.search.RandomSearch. Secondly, set the search.RandomSearch.path_limit property to be any integer larger than 0.  Compare the resulting state space diagrams.
Last modified:
2016/01/27 17:02