Differences

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

--- lab3 [2016/01/18 20:20] – franck
+++ lab3 [2017/01/23 01:19] (current) – franck
@@ Line 1: / Line 1: @@
-In 1994, John Trono introduced the Santa Claus problem.  Its description can be found in\\
+JPF in its basic form is a state exploring Java virtual machine (JVM) which can systematically explore all potential executions of Java code. There are many different ways to explore the executions.  For example, JPF can use different search strategies such as breadth-first search (BFS) and depth-first search (DFS). Consider a Java code that gives rise to the following state space diagram.
-John Trono.
-[[http://dx.doi.org.ezproxy.library.yorku.ca/10.1145/187387.187391|A new exercise in concurrency]].
+{{:public:statespace.png|}}
-//ACM SIGCSE Bulletin//, 26(3):8-10, September 1994.\\
-The paper also contains a solution.  Implement this solution in Java.  In particular, create the classes Santa, Reindeer, and Elf.  Use the Semaphore class whose API can be found [[https://docs.oracle.com/javase/8/docs/api/java/util/concurrent/Semaphore.html|here]].
+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.