EECS4315

User Tools

Site Tools

You are here: Mission Critical Systems » Lab 5
Trace:
lab8

Differences

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

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision		Previous revision
lab8 [2018/02/25 14:57] – francklab8 [2020/02/29 21:15] (current) – franck
Line 1: Line 1:
-====== Lab 6 ======+~~NOTOC~~ 
 + 
 +====== Lab 5 ======
  
 Consider the following app. Consider the following app.
Line 5: Line 7:
 public class Main { public class Main {
     public static void main(String[] args) {     public static void main(String[] args) {
-        System.out.println(StrictMath.cbrt(4.4));+         System.out.println(StrictMath.exp(23.7));
     }     }
 } }
Line 13: Line 15:
 <code> <code>
 target=Main target=Main
-classpath=.+classpath=(directory that contains Main.class)
 </code> </code>
 then we obtain output similar to the following. then we obtain output similar to the following.
 <code> <code>
-JavaPathfinder core system v8.0 (rev 29+) - (C) 2005-2014 United States Government. All rights reserved.+JavaPathfinder core system v8.0 (rev 26e11d1de726c19ba8ae10551e048ec0823aabc6) - (C) 2005-2014 United States Government. All rights reserved.
  
  
Line 23: Line 25:
 Main.main() Main.main()
  
-====================================================== search started: 3/12/17 9:55 PM+====================================================== search started: 2/29/20 4:01 PM
  
 ====================================================== error 1 ====================================================== error 1
 gov.nasa.jpf.vm.NoUncaughtExceptionsProperty gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
-java.lang.UnsatisfiedLinkError: cannot find native java.lang.StrictMath.cbrt +java.lang.UnsatisfiedLinkError: cannot find native java.lang.StrictMath.exp 
-        at java.lang.StrictMath.cbrt(no peer) +        at java.lang.StrictMath.exp(gov.nasa.jpf.vm.JPF_java_lang_StrictMath) 
-        at Main.main(Main.java:6) +        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> </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> +===== Approach 1: native peer ===== 
-JavaPathfinder core system v8.0 (rev 29+) - (C) 2005-2014 United States Government. All rights reserved.+ 
 +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.
  
  
Line 40: Line 68:
 Main.main() Main.main()
  
-====================================================== search started: 3/12/17 9:59 PM +====================================================== search started: 2/29/20 4:02 PM 
-native peer class +native peer 
-1.6386425412012917+1.9623624323651344E10
  
 ====================================================== results ====================================================== results
 no errors detected no errors detected
-... + 
-</code>Submit your native peer class <b>and</b> your configuration file (name it Main-native-peer.jpf). +====================================================== statistics 
-  * 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 {{|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> +elapsed time:       00:00:00 
-JavaPathfinder core system v8.0 (rev 29+) - (C) 2005-2014 United States Government. All rights reserved.+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=11,maxLive=0,gcCycles=1 
 +instructions:       3189 
 +max memory:         240MB 
 +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.
  
  
Line 55: Line 107:
 Main.main() Main.main()
  
-====================================================== search started: 3/12/17 10:06 PM +====================================================== search started: 2/29/20 4:05 PM 
-peer class +[WARNING] orphan NativePeer method: java.lang.StrictMath.log(D)D 
-1.6386425412012982+peer 
 +1.9623624323651325E10
  
 ====================================================== results ====================================================== results
 no errors detected 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+====================================================== 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> <code>
-javac -cp /cs/fac/packages/jpf/jpf-core/build/jpf.jar:. (class name).java+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 
 +1.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> </code>
-or add /cs/fac/packages/jpf/jpf-core/build/jpf.jar as an external library to Eclipse. 
  
-To receive feedback, submit both classes and configuration files using+Submit your configuration file (name it Main-nhandler.jpf). 
 + 
 +To receive feedback, submit your classes and configuration files using
 <code> <code>
-submit 4315 lab6 (name of file)+submit 4315 lab5 (name of file)
 </code> </code>
-before Tuesday March 6.+before Thursday March 12.
  
  
lab8.1519570668.txt.gz · Last modified: by franck