lab4
Differences
This shows you the differences between two versions of the page.
| Both sides previous revisionPrevious revisionNext revision | Previous revisionLast revisionBoth sides next revision | ||
| lab4 [2017/01/27 21:46] – franck | lab4 [2017/01/27 21:55] – franck | ||
|---|---|---|---|
| Line 180: | Line 180: | ||
| One can constrain JPF from checking more than 100 bytecode instructions as follows. | 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. |
| < | < | ||
| Line 205: | Line 205: | ||
| ... | ... | ||
| </ | </ | ||
| + | |||
| + | We can also limit the number of states that JPF explores by setting the property budget.max_state. | ||
| < | < | ||
| Line 214: | Line 216: | ||
| </ | </ | ||
| + | Since the statespace of this app consists of more than 100 states, JPF stops and produces the following output. | ||
| - | + | < | |
| - | </code> | + | |
| JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved. | JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved. | ||
| Line 229: | Line 231: | ||
| ... | ... | ||
| </ | </ | ||
| + | |||
| + | We can also constrain the depth of the search. | ||
| < | < | ||
| Line 237: | Line 241: | ||
| budget.max_depth=100 | budget.max_depth=100 | ||
| </ | </ | ||
| + | |||
| + | Since the depth of the search is greater than 100 for this app, JPF stops and produces the following output. | ||
| < | < | ||
lab4.txt · Last modified: 2017/01/30 13:56 by franck