[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf/jvm/choice TwoIntChoice.java,1.1,1.2 DoubleThresholdGenerator.java,1.1,1.2 IntChoiceFromSet.java,1.1,1.2 IntIntervalGenerator.java,1.2,1.3

[pcm <pcm...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/choice
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv3727/src/gov/nasa/jpf/jvm/choice

Modified Files:
	TwoIntChoice.java DoubleThresholdGenerator.java 
	IntChoiceFromSet.java IntIntervalGenerator.java 
Log Message:
slightly changed the ChoiceGenerator API so that advance(), hasMoreChoices() and getNextChoice() all get the VM passed in as a parameter. So that ChoiceGenerators can do real fancy stuff at any time.

Still the preferred way should be to somehow compute the choice set the first time advance() is called - for performance, traceability and esp. coverage reasons. That way, we can JPF ask at any time "how many open upstream choices do you still have?"

Index: DoubleThresholdGenerator.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/choice/DoubleThresholdGenerator.java,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -d -r1.1 -r1.2
--- DoubleThresholdGenerator.java	8 Sep 2005 23:21:04 -0000	1.1
+++ DoubleThresholdGenerator.java	9 Sep 2005 23:31:42 -0000	1.2
@@ -41,11 +41,11 @@
   state = -1;
 }
 
-public boolean hasMoreChoices () {
+public boolean hasMoreChoices (JVM vm) {
   return (state < 2);
 }
 
-public double getNextChoice () {
+public double getNextChoice (JVM vm) {
   switch (state) {
   case -1:
   case 0: return low;

Index: IntChoiceFromSet.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/choice/IntChoiceFromSet.java,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -d -r1.1 -r1.2
--- IntChoiceFromSet.java	8 Sep 2005 23:21:04 -0000	1.1
+++ IntChoiceFromSet.java	9 Sep 2005 23:31:42 -0000	1.2
@@ -36,7 +36,7 @@
 	/* (non-Javadoc)
 	 * @see gov.nasa.jpf.jvm.IntChoiceGenerator#getNextChoice()
 	 */
-	public int getNextChoice() {
+	public int getNextChoice(JVM vm) {
 //		try {
 			int ret = Integer.parseInt(values[count]);
 			System.out.println(id + ": " + ret);
@@ -48,7 +48,7 @@
 	/* (non-Javadoc)
 	 * @see gov.nasa.jpf.jvm.ChoiceGenerator#hasMoreChoices()
 	 */
-	public boolean hasMoreChoices() {
+	public boolean hasMoreChoices(JVM vm) {
 		if (count < values.length)
 			return true;
 		else

Index: IntIntervalGenerator.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/choice/IntIntervalGenerator.java,v
retrieving revision 1.2
retrieving revision 1.3
diff -u -d -r1.2 -r1.3
--- IntIntervalGenerator.java	9 Sep 2005 04:55:39 -0000	1.2
+++ IntIntervalGenerator.java	9 Sep 2005 23:31:42 -0000	1.3
@@ -76,11 +76,11 @@
   init();
 }
 
-public int getNextChoice () {
+public int getNextChoice (JVM vm) {
   return next;
 }
 
-public boolean hasMoreChoices () {
+public boolean hasMoreChoices (JVM vm) {
   if (delta > 0) {
     return (next < max);
   } else {

Index: TwoIntChoice.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/choice/TwoIntChoice.java,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -d -r1.1 -r1.2
--- TwoIntChoice.java	8 Sep 2005 23:21:04 -0000	1.1
+++ TwoIntChoice.java	9 Sep 2005 23:31:42 -0000	1.2
@@ -36,7 +36,7 @@
 	/* (non-Javadoc)
 	 * @see gov.nasa.jpf.jvm.IntChoiceGenerator#getNextChoice()
 	 */
-	public int getNextChoice() {
+	public int getNextChoice(JVM vm) {
 		int ret;
 		switch (state){
 			case 0: {
@@ -58,7 +58,7 @@
 	/* (non-Javadoc)
 	 * @see gov.nasa.jpf.jvm.ChoiceGenerator#hasMoreChoices()
 	 */
-	public boolean hasMoreChoices() {
+	public boolean hasMoreChoices(JVM vm) {
 		return state < 1;
 	}