====== Lab 2 ======


  * In your home directory create a directory named .jpf (note that the name of the directory starts with a dot).  
  * In the created directory, create a file named site.properties with the following contents.
<code>
# JPF site configuration
jpf-core=/eecs/fac/pkg/jpf/jpf-core
extensions=${jpf-core}
</code>
  * In your home directory create a directory name 4315.
  * In the created directory 4315, create a directory named lab2.
  * In the created directory lab2, create the class RandomFraction with the following content.
<code java>
import java.util.Random;

public class RandomFraction 
{
	public static void run() 
	{
		Random random = new Random(System.currentTimeMillis());
		System.out.println(1 / random.nextInt(1000000));
	}
}
</code>
  * Compile the RandomFraction  class.
  * In the created directory lab2, create the class RandomFractionTest with the following content.
<code java>
public class RandomFractionTest 
{
	public static void main(String[] args) 
	{
		RandomFraction.run();
	}
}
</code>
  * Compile the RandomFractionTest class.
  * Run the RandomFractionTest class.
  * Create the file RandomFractionTest.jpf with the following content.
<code>
target=RandomFractionTest
classpath=.
</code>
  * Run Java PathFinder (JPF) on RandomFractionTest by running
<code>
jpf RandomFractionTest.jpf
</code>
It should produce output similar to the following.
<code>
JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved.


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

====================================================== search started: 1/14/17 12:06 PM
0
====================================================== results
no errors detected

====================================================== statistics
elapsed time:       00:00:00
states:             new=1,visited=0,backtracked=1,end=1
search:             maxDepth=1,constraints=0
choice generators:  thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=0
heap:               new=353,released=12,maxLive=0,gcCycles=1
instructions:       3181
max memory:         299MB
loaded code:        classes=62,methods=1334

====================================================== search finished: 1/14/17 12:06 PM
</code>
  * To the file RandomFractionTest.jpf add the following.
<code>
cg.enumerate_random=true
</code>
  * Run JPF on RandomFractionTest again.  It should produce output similar to the following.
<code>
JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved.


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

====================================================== search started: 1/14/17 12:19 PM

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.ArithmeticException: division by zero
        at RandomFraction.run(RandomFraction.java:8)
        at RandomFractionTest.main(RandomFractionTest.java:5)


====================================================== snapshot #1
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  call stack:
        at RandomFraction.run(RandomFraction.java:8)
        at RandomFractionTest.main(RandomFractionTest.java:5)


====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.ArithmeticException: division by zero  a..."

====================================================== statistics
elapsed time:       00:00:00
states:             new=2,visited=0,backtracked=0,end=0
search:             maxDepth=2,constraints=0
choice generators:  thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=1
heap:               new=369,released=2,maxLive=0,gcCycles=1
instructions:       3175
max memory:         299MB
loaded code:        classes=66,methods=1364

====================================================== search finished: 1/14/17 12:19 PM
</code>