Differences

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

--- lab8 [2016/03/02 19:30] – created franck
+++ lab8 [2018/02/25 15:00] (current) – franck
@@ Line 1: / Line 1: @@
-Implement a listener and publisher that, given the following app,
+====== Lab 6 ======
-<html>
-<pre>
-import java.util.Random;
-public class Example {
+Consider the following app.
+<code java>
+public class Main {
     public static void main(String[] args) {
-	Random random = new Random();
+        System.out.println(StrictMath.cbrt(4.4));
-	if (random.nextBoolean()) {
-	    System.out.println("true");
-	} else {
-	    System.out.println("false");
-	}
     }
 }
-</pre>
+</code>
-</html>
-and the application configuration file
-<html>
-<pre>
-target=Example
-classpath=.
-native_classpath=.
-listener=AmountOfNonDeterminism
-</pre>
+If we run JPF with the following configuration file
-</html>
+<code>
-produces output similar to
+target=Main
-<html>
+classpath=(directory that contains Main.class)
-<pre>
+</code>
-JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved.
+then we obtain 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
-Example.main()
+Main.main()
-====================================================== search started: 3/2/16 2:27 PM
+====================================================== search started: 3/12/17 9:55 PM
-false
-true
-======================================================
+====================================================== error 1
-maximum amount of nondeterminism: 2 choice(s)
+gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
+java.lang.UnsatisfiedLinkError: cannot find native java.lang.StrictMath.cbrt
+        at java.lang.StrictMath.cbrt(no peer)
+        at Main.main(Main.java:6)
+...
+</code>
+  * Implement a native peer class.  Add to the native peer a call to println with "native peer class" so that JPF produces the following output for the above app.<code>
+JavaPathfinder core system v8.0 (rev 29+) - (C) 2005-2014 United States Government. All rights reserved.
+====================================================== system under test
+Main.main()
+====================================================== search started: 3/12/17 9:59 PM
+native peer class
+.6386425412012917
 ====================================================== results
 no errors detected
+...
+</code>Submit your native peer class **and** your configuration file (name it Main-native-peer.jpf).
+  * Implement a peer class.  Add to the peer class a call to println with "peer class" so that JPF produces output for the above app similar to the following.  Information about the cubic root can be found {{https://en.wikipedia.org/wiki/Cube_root|here}}.  Ensure that the modelled cbrt method satisfies the specification given in the API of the StrictMath class.  Some methods in the Double class might be useful.<code>
+JavaPathfinder core system v8.0 (rev 29+) - (C) 2005-2014 United States Government. All rights reserved.
+====================================================== system under test
+Main.main()
+====================================================== search started: 3/12/17 10:06 PM
+peer class
+.6386425412012982
+====================================================== results
+no errors detected
+...
+</code>Submit your peer class <b>and</b> your configuration file (name it Main-model-class.jpf).
+To compile your classes, you may want to use
+<code>
+javac -cp /cs/fac/packages/jpf/jpf-core/build/jpf.jar:. (class name).java
+</code>
+or add /cs/fac/packages/jpf/jpf-core/build/jpf.jar as an external library to Eclipse.
-====================================================== statistics
+To receive feedback, submit both classes and configuration files using
-elapsed time:       00:00:00
+<code>
-states:             new=1,visited=0,backtracked=1,end=1
+submit 4315 lab6 (name of file)
-search:             maxDepth=1,constraints=0
+</code>
-choice generators:  thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=0
+before Tuesday March 6.
-heap:               new=352,released=12,maxLive=0,gcCycles=1
-instructions:       3176
-max memory:         56MB
-loaded code:        classes=61,methods=1332
-====================================================== search finished: 3/2/16 2:27 PM
-</pre>
-</html>
-Apart from the classes that have been discussed in the lectures, also the class ChoiceGenerator, which is part of the package gov.nasa.jpf.vm, may be useful.