Differences

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

--- lab8 [2016/03/02 21:15] – franck
+++ lab8 [2020/02/29 21:15] (current) – franck
@@ Line 1: / Line 1: @@
-Implement a listener and publisher that, given the following app,
+~~NOTOC~~
-<html>
-<pre>
-import java.util.Random;
-public class Example {
+====== Lab 5 ======
+Consider the following app.
+<code java>
+public class Main {
     public static void main(String[] args) {
-	Random random = new Random();
+         System.out.println(StrictMath.exp(23.7));
-	if (random.nextBoolean()) {
-	    System.out.println("true");
-	} else {
-	    System.out.println("false");
-	}
     }
 }
-</pre>
+</code>
-</html>
-and the application configuration file
+If we run JPF with the following configuration file
-<html>
+<code>
-<pre>
+target=Main
-target=Example
+classpath=(directory that contains Main.class)
-classpath=.
+</code>
-native_classpath=.
+then we obtain output similar to the following.
-listener=AmountOfNonDeterminism
+<code>
-cg.enumerate_random=true
+JavaPathfinder core system v8.0 (rev 26e11d1de726c19ba8ae10551e048ec0823aabc6) - (C) 2005-2014 United States Government. All rights reserved.
-</pre>
-</html>
-produces output similar to
-<html>
-<pre>
-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: 2/29/20 4:01 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.exp
+        at java.lang.StrictMath.exp(gov.nasa.jpf.vm.JPF_java_lang_StrictMath)
+        at Main.main(Main.java:3)
+====================================================== snapshot #1
+thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
+  call stack:
+        at java.lang.StrictMath.exp(StrictMath.java)
+        at Main.main(Main.java:3)
+====================================================== results
+error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.UnsatisfiedLinkError: cannot find native..."
+====================================================== statistics
+elapsed time:       00:00:00
+states:             new=1,visited=0,backtracked=0,end=0
+search:             maxDepth=1,constraints=0
+choice generators:  thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=0
+heap:               new=369,released=0,maxLive=0,gcCycles=0
+instructions:       3182
+max memory:         240MB
+loaded code:        classes=66,methods=1427
+====================================================== search finished: 2/29/20 4:01 PM
+</code>
+===== Approach 1: native peer =====
+Implement a native peer class.  Add to the native peer a call to println with "native peer" so that JPF produces the following output for the above app.
+<code>
+JavaPathfinder core system v8.0 (rev 26e11d1de726c19ba8ae10551e048ec0823aabc6) - (C) 2005-2014 United States Government. All rights reserved.
+====================================================== system under test
+Main.main()
+====================================================== search started: 2/29/20 4:02 PM
+native peer
+.9623624323651344E10
 ====================================================== results
@@ Line 50: / Line 80: @@
 search:             maxDepth=1,constraints=0
 choice generators:  thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=0
-heap:               new=352,released=12,maxLive=0,gcCycles=1
+heap:               new=353,released=11,maxLive=0,gcCycles=1
-instructions:       3176
+instructions:       3189
-max memory:         56MB
+max memory:         240MB
-loaded code:        classes=61,methods=1332
+loaded code:        classes=62,methods=1399
+====================================================== search finished: 2/29/20 4:02 PM
+</code>
+To compile your class, 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.
+Submit your native peer class **and** your configuration file (name it Main-native-peer.jpf).
+===== Approach 2: peer =====
+Implement a peer class.  Add to the peer class a call to println with "peer" so that JPF produces output for the above app similar to the following.  To model exp, you may want to use a [[https://en.wikipedia.org/wiki/Taylor_series|Taylor series]].  Ensure that the modelled exp 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 26e11d1de726c19ba8ae10551e048ec0823aabc6) - (C) 2005-2014 United States Government. All rights reserved.
+====================================================== system under test
+Main.main()
+====================================================== search started: 2/29/20 4:05 PM
+[WARNING] orphan NativePeer method: java.lang.StrictMath.log(D)D
+peer
+.9623624323651325E10
+====================================================== 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=355,released=11,maxLive=0,gcCycles=1
+instructions:       5184
+max memory:         240MB
+loaded code:        classes=62,methods=1331
+====================================================== search finished: 2/29/20 4:05 PM
+</code>
+Submit your peer class **and** your configuration file (name it Main-peer.jpf).
+===== Approach 3: jpf-nhandler =====
+Use jpf-nhandler so that JPF produces the following output.
+<code>
+JavaPathfinder core system v8.0 (rev 26e11d1de726c19ba8ae10551e048ec0823aabc6) - (C) 2005-2014 United States Government. All rights reserved.
+====================================================== system under test
+Main.main()
+====================================================== search started: 2/29/20 4:10 PM
+* DELEGATING Unhandled Native -> java.lang.StrictMath.exp
+.9623624323651344E10
+====================================================== 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=555,released=13,maxLive=0,gcCycles=1
+instructions:       9955
+max memory:         240MB
+loaded code:        classes=62,methods=1399
+====================================================== search finished: 2/29/20 4:10 PM
+</code>
+Submit your configuration file (name it Main-nhandler.jpf).
+To receive feedback, submit your classes and configuration files using
+<code>
+submit 4315 lab5 (name of file)
+</code>
+before Thursday March 12.
-====================================================== search finished: 3/2/16 2:27 PM
-</pre>
-</html>
-That is, JPF reports the maximum amount of nondeterminism (maximum number of outgoing transitions from any state of the system under test).
-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.
-Try not to hard-code
-<html>
-<pre>
-======================================================
-</pre>
-</html>
-but use an appropriate method provided by JPF.