01: //
02: //Copyright (C) 2005 United States Government as represented by the
03: //Administrator of the National Aeronautics and Space Administration
04: //(NASA). All Rights Reserved.
05: //
06: //This software is distributed under the NASA Open Source Agreement
07: //(NOSA), version 1.3. The NOSA has been approved by the Open Source
08: //Initiative. See the file NOSA-1.3-JPF at the top of the distribution
09: //directory tree for the complete NOSA document.
10: //
11: //THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
12: //KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
13: //LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
14: //SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
15: //A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
16: //THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
17: //DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
18: //package gov.nasa.jpf.jvm;
19: //
20: package gov.nasa.jpf.jvm.choice;
21:
22: import gov.nasa.jpf.Config;
23: import gov.nasa.jpf.JPFException;
24: import gov.nasa.jpf.jvm.IntChoiceGenerator;
25: import gov.nasa.jpf.jvm.JVM;
26:
27: /**
28: * Choice Generator that enumerates an interval of int values
29: * Pretty simplistic implementation for now, but at least it can count up and down
30: */
31: public class IntIntervalGenerator extends IntChoiceGenerator {
32:
33: int min, max;
34: int next;
35: int delta;
36:
37: private void init() {
38: if (delta == 0) {
39: throw new JPFException(
40: "IntIntervalGenerator delta value is 0");
41: }
42:
43: if (min > max) {
44: int t = max;
45: max = min;
46: min = t;
47: }
48:
49: if (delta > 0) {
50: next = min - delta;
51: } else {
52: next = max + delta;
53: }
54: }
55:
56: public IntIntervalGenerator(int min, int max, int delta) {
57: super ("int");
58:
59: this .min = min;
60: this .max = max;
61: this .delta = delta;
62:
63: init();
64: }
65:
66: public IntIntervalGenerator(int min, int max) {
67: this (min, max, 1);
68: }
69:
70: public IntIntervalGenerator(Config conf, String id) {
71: super (id);
72: min = conf.getInt(id + ".min");
73: max = conf.getInt(id + ".max");
74: delta = conf.getInt(id + ".delta", 1);
75:
76: init();
77: }
78:
79: public int getNextChoice(JVM vm) {
80: return next;
81: }
82:
83: public boolean hasMoreChoices(JVM vm) {
84: if (delta > 0) {
85: return (next < max);
86: } else {
87: return (next > min);
88: }
89: }
90:
91: public void advance(JVM vm) {
92: next += delta;
93: }
94: }
|