lab8
Differences
This shows you the differences between two versions of the page.
Both sides previous revisionPrevious revisionNext revision | Previous revision | ||
lab8 [2016/03/02 21:09] – franck | lab8 [2020/02/29 21:15] (current) – franck | ||
---|---|---|---|
Line 1: | Line 1: | ||
- | Implement a listener and publisher that, given the following app, | + | ~~NOTOC~~ |
- | < | + | |
- | < | + | |
- | import java.util.Random; | + | |
- | public class Example | + | ====== Lab 5 ====== |
+ | |||
+ | Consider the following app. | ||
+ | <code java> | ||
+ | public class Main { | ||
public static void main(String[] args) { | public static void main(String[] args) { | ||
- | Random random = new Random(); | + | System.out.println(StrictMath.exp(23.7)); |
- | if (random.nextBoolean()) { | + | |
- | | + | |
- | } else { | + | |
- | System.out.println(" | + | |
- | } | + | |
} | } | ||
} | } | ||
- | </pre> | + | </code> |
- | </ | + | |
- | and the application | + | If we run JPF with the following |
- | <html> | + | <code> |
- | <pre> | + | target=Main |
- | target=Example | + | classpath=(directory that contains Main.class) |
- | classpath=. | + | </code> |
- | native_classpath=. | + | then we obtain |
- | listener=AmountOfNonDeterminism | + | <code> |
- | cg.enumerate_random=true | + | JavaPathfinder core system v8.0 (rev 26e11d1de726c19ba8ae10551e048ec0823aabc6) - (C) 2005-2014 United States Government. All rights reserved. |
- | </pre> | + | |
- | </ | + | |
- | produces | + | |
- | <html> | + | |
- | <pre> | + | |
- | JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved. | + | |
====================================================== system under test | ====================================================== system under test | ||
- | Example.main() | + | Main.main() |
- | ====================================================== search started: | + | ====================================================== search started: 2/29/20 4:01 PM |
- | false | + | |
- | true | + | |
- | ====================================================== | + | ====================================================== |
- | 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: | ||
+ | |||
+ | |||
+ | ====================================================== snapshot #1 | ||
+ | thread java.lang.Thread: | ||
+ | call stack: | ||
+ | at java.lang.StrictMath.exp(StrictMath.java) | ||
+ | at Main.main(Main.java: | ||
+ | |||
+ | |||
+ | ====================================================== results | ||
+ | error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty " | ||
+ | |||
+ | ====================================================== statistics | ||
+ | elapsed time: | ||
+ | states: | ||
+ | search: | ||
+ | choice | ||
+ | heap: | ||
+ | instructions: | ||
+ | max memory: | ||
+ | loaded code: classes=66, | ||
+ | |||
+ | ====================================================== search finished: 2/29/20 4:01 PM | ||
+ | </ | ||
+ | |||
+ | ===== Approach 1: native peer ===== | ||
+ | |||
+ | Implement a native peer class. | ||
+ | |||
+ | < | ||
+ | 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 | ||
+ | 1.9623624323651344E10 | ||
====================================================== results | ====================================================== results | ||
Line 50: | Line 80: | ||
search: | search: | ||
choice generators: | choice generators: | ||
- | heap: new=352,released=12, | + | heap: new=353,released=11, |
- | instructions: | + | instructions: |
- | max memory: | + | max memory: |
- | loaded code: classes=61,methods=1332 | + | loaded code: classes=62,methods=1399 |
+ | |||
+ | ====================================================== search finished: 2/29/20 4:02 PM | ||
+ | </ | ||
+ | |||
+ | To compile your class, you may want to use | ||
+ | < | ||
+ | javac -cp / | ||
+ | </ | ||
+ | or add / | ||
+ | |||
+ | Submit your native peer class **and** your configuration file (name it Main-native-peer.jpf). | ||
+ | |||
+ | ===== Approach 2: peer ===== | ||
+ | |||
+ | Implement a peer class. | ||
+ | |||
+ | < | ||
+ | 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 | ||
+ | 1.9623624323651325E10 | ||
+ | |||
+ | ====================================================== results | ||
+ | no errors detected | ||
+ | |||
+ | ====================================================== statistics | ||
+ | elapsed time: | ||
+ | states: | ||
+ | search: | ||
+ | choice generators: | ||
+ | heap: | ||
+ | instructions: | ||
+ | max memory: | ||
+ | loaded code: classes=62, | ||
+ | |||
+ | ====================================================== search finished: 2/29/20 4:05 PM | ||
+ | </ | ||
+ | |||
+ | 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. | ||
+ | |||
+ | < | ||
+ | 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: | ||
+ | states: | ||
+ | search: | ||
+ | choice generators: | ||
+ | heap: | ||
+ | instructions: | ||
+ | max memory: | ||
+ | loaded code: classes=62, | ||
+ | |||
+ | ====================================================== search finished: 2/29/20 4:10 PM | ||
+ | </ | ||
+ | |||
+ | Submit your configuration file (name it Main-nhandler.jpf). | ||
+ | |||
+ | To receive feedback, submit your classes and configuration files using | ||
+ | < | ||
+ | submit 4315 lab5 (name of file) | ||
+ | </ | ||
+ | before Thursday March 12. | ||
- | ====================================================== search finished: 3/2/16 2:27 PM | ||
- | </ | ||
- | </ | ||
- | 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, | ||
- | Try not to hard-code ====================================================== but | ||
- | use an appropriate methods provided by JPF. | ||
lab8.1456952940.txt.gz · Last modified: 2016/03/02 21:09 by franck