Differences

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

--- lab4 [2017/01/27 21:46] – franck
+++ lab4 [2018/11/06 15:55] (current) – franck
@@ Line 1: / Line 1: @@
-====== LAB 4 ======
+~~NOTOC~~
+====== LAB 3 ======
 ====== Listeners ======
@@ Line 67: / Line 69: @@
       * vt.methods
- To receive feedback, submit your work as a text file using the submit command before Tuesday January 31:
+To receive feedback, submit your work as a text file using the submit command before Tuesday January 29:\\
-submit 4315 lab4 <name of the listener>
+submit 4315 lab3 <name of the listener>
 ====== Sample ======
@@ Line 180: / Line 182: @@
 One can constrain JPF from checking more than 100 bytecode instructions as follows.
-We can assign any int value to the property budget.max_insn.
+We can assign any long value to the property budget.max_insn.
 <code>
@@ Line 205: / Line 207: @@
 ...
 </code>
+We can also limit the number of states that JPF explores by setting the property budget.max_state.  We can assign any int value to this property.
 <code>
@@ Line 214: / Line 218: @@
 </code>
+Since the statespace of this app consists of more than 100 states, JPF stops and produces the following output.
+<code>
-</code>
 JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved.
@@ Line 229: / Line 233: @@
 ...
 </code>
+We can also constrain the depth of the search.  The corresponding property, budget.max_depth, can take any int value.
 <code>
@@ Line 237: / Line 243: @@
 budget.max_depth=100
 </code>
+Since the depth of the search is greater than 100 for this app, JPF stops and produces the following output.
 <code>