Differences

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

--- lab4 [2016/01/27 21:46] – created franck
+++ lab4 [2016/01/27 22:02] (current) – franck
@@ Line 2: / Line 2: @@
 {{: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.