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

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

lab3 [2016/01/18 15:20]
lab3 [2017/01/22 20:19] (current)
Line 1: Line 1:
-In 1994, John Trono introduced the Santa Claus problemIts 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 executionsFor 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.  + 
-[[|A new exercise in concurrency]]. +{{:public:statespace.png|}} 
-//ACM SIGCSE Bulletin//, 26(3):8-10, September 1994.\\ + 
-The paper also contains a solutionImplement this solution in Java.  In particular, create the classes Santa, Reindeer, and ElfUse the Semaphore class whose API can be found [[|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 outputWhen 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 or  
 +**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 Secondly, set the search.RandomSearch.path_limit property to be any integer larger than 0.  Compare the resulting state space diagrams.
Last modified:
2017/01/22 20:19