[Javapathfinder-devel] /javapathfinder/src/gov/nasa/jpf/jvm/choice TwoIntChoice.java,NONE,1.1 Double

SourceForge Headquarters 225 Broadway Suite 1600 San Diego, CA 92101 +1 (858) 422-6466

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

Added Files:
	TwoIntChoice.java DoubleThresholdGenerator.java 
	IntIntervalGenerator.java IntChoiceFromSet.java 
Log Message:
* new package for choice generators
* moved in 2 classes from jvm
* 2 new choice generators hot off the press

--- NEW FILE: DoubleThresholdGenerator.java ---
//
//Copyright (C) 2005 United States Government as represented by the
//Administrator of the National Aeronautics and Space Administration
//(NASA).  All Rights Reserved.
//
//This software is distributed under the NASA Open Source Agreement
//(NOSA), version 1.3.  The NOSA has been approved by the Open Source
//Initiative.  See the file NOSA-1.3-JPF at the top of the distribution
//directory tree for the complete NOSA document.
//
//THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
//KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
//LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
//SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
//A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
//THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
//DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
//

package gov.nasa.jpf.jvm.choice;

import gov.nasa.jpf.Config;
import gov.nasa.jpf.jvm.DoubleChoiceGenerator;
import gov.nasa.jpf.jvm.JVM;

/**
* ChoiceGenerator instance that produces a simple 3 value enumeration
* 
*/
public class DoubleThresholdGenerator extends DoubleChoiceGenerator {

double low, threshold, high;
int state;

public DoubleThresholdGenerator (Config conf, String id) {
  super(id);
  
  low = conf.getDouble (id + ".low");
  threshold = conf.getDouble(id + ".threshold");
  high = conf.getDouble(id + ".high");
  state = -1;
}

public boolean hasMoreChoices () {
  return (state < 2);
}

public double getNextChoice () {
  switch (state) {
  case -1:
  case 0: return low;
  case 1: return threshold;
  default: return high;
  }
}

public void advance (JVM vm) {
  state++;
}
}

--- NEW FILE: IntChoiceFromSet.java ---
/*
 * Created on Sep 8, 2005
 *
 * TODO To change the template for this generated file go to
 * Window - Preferences - Java - Code Style - Code Templates
 */
package gov.nasa.jpf.jvm.choice;

import gov.nasa.jpf.Config;
import gov.nasa.jpf.jvm.IntChoiceGenerator;
import gov.nasa.jpf.jvm.JVM;

/**
 * @author jpenix
 *
 * choose from a set of values provided in configuration as
 * xxx.class = IntChoiceFromSet
 * xxx.values = {1, 2, 3, 400}
 * where "xxx" is the choice id.
 * 
 * choices can then made using: getInt("xxx");
 */
public class IntChoiceFromSet extends IntChoiceGenerator {

	String[] values;
	int count = 0;
	
	/**
	 * @param id
	 */
	public IntChoiceFromSet(Config conf, String id) {
		super(id);
		values = conf.getStringArray("values");
	}

	/* (non-Javadoc)
	 * @see gov.nasa.jpf.jvm.IntChoiceGenerator#getNextChoice()
	 */
	public int getNextChoice() {
//		try {
			int ret = Integer.parseInt(values[count]);
			System.out.println(id + ": " + ret);
	        return ret;
//	      } catch (NumberFormatException nfx) {
//	        return 0;
	}

	/* (non-Javadoc)
	 * @see gov.nasa.jpf.jvm.ChoiceGenerator#hasMoreChoices()
	 */
	public boolean hasMoreChoices() {
		if (count < values.length)
			return true;
		else
			return false;
	}

	/* (non-Javadoc)
	 * @see gov.nasa.jpf.jvm.ChoiceGenerator#advance(gov.nasa.jpf.jvm.JVM)
	 */
	public void advance(JVM vm) {
		count++;
	}

}

--- NEW FILE: IntIntervalGenerator.java ---
//
//Copyright (C) 2005 United States Government as represented by the
//Administrator of the National Aeronautics and Space Administration
//(NASA).  All Rights Reserved.
//
//This software is distributed under the NASA Open Source Agreement
//(NOSA), version 1.3.  The NOSA has been approved by the Open Source
//Initiative.  See the file NOSA-1.3-JPF at the top of the distribution
//directory tree for the complete NOSA document.
//
//THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
//KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
//LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
//SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
//A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
//THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
//DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
//package gov.nasa.jpf.jvm;
//
package gov.nasa.jpf.jvm.choice;

import gov.nasa.jpf.Config;
import gov.nasa.jpf.JPFException;
import gov.nasa.jpf.jvm.IntChoiceGenerator;
import gov.nasa.jpf.jvm.JVM;


/**
* Choice Generator that enumerates an interval of int values
* Pretty simplistic implementation for now, but at least it can count up and down
*/
public class IntIntervalGenerator extends IntChoiceGenerator {

int min, max;
int next;
int delta;

private void init () {
  if (delta == 0) {
    throw new JPFException ("IntIntervalGenerator delta value is 0");
  }
  
  if (delta > 0) {
    next = min - delta;
  } else {
    next = max + delta;
  }
}

public IntIntervalGenerator (int min, int max, int delta) {
  super("int");
  
  this.min = min;
  this.max = max;
  this.delta = delta;
  
  init();    
}

public IntIntervalGenerator (int min, int max) {
  this(min, max, 1);
}
  
public IntIntervalGenerator (Config conf, String id) {
  super(id);
  min = conf.getInt( id + ".min");
  max = conf.getInt( id + ".max");
  delta = conf.getInt( id + ".delta", 1);

  init();
}

public int getNextChoice () {
  return next;
}

public boolean hasMoreChoices () {
  if (delta > 0) {
    return (next <= max);
  } else {
    return (next >= min);
  }
}

public void advance (JVM vm) {
  next += delta;
}
}

--- NEW FILE: TwoIntChoice.java ---
/*
 * Created on Sep 7, 2005
 *
 * TODO To change the template for this generated file go to
 * Window - Preferences - Java - Code Style - Code Templates
 */
package gov.nasa.jpf.jvm.choice;

import gov.nasa.jpf.Config;
import gov.nasa.jpf.jvm.IntChoiceGenerator;
import gov.nasa.jpf.jvm.JVM;

/**
 * @author jpenix
 *
 * designed to choose return values from a function calls
 */
public class TwoIntChoice extends IntChoiceGenerator {

	int firstValue = 1;
	int secondValue = 0;

	String firstMsg = "pass";
	String secondMsg = "fail";
	
	int state = -1;
	
	public TwoIntChoice(Config conf, String id) {
		  super(id);
		  firstValue = conf.getInt( id + ".firstValue");
		  firstMsg = conf.getString( id + ".firstMessage");
		  secondValue = conf.getInt( id + ".secondValue");
		  secondMsg = conf.getString( id + ".secondMessage");
	}
	
	/* (non-Javadoc)
	 * @see gov.nasa.jpf.jvm.IntChoiceGenerator#getNextChoice()
	 */
	public int getNextChoice() {
		int ret;
		switch (state){
			case 0: {
				ret = firstValue;
				System.out.println(firstMsg);
				break;
			}
			case 1: {
				ret = secondValue;
				System.out.println(secondMsg);
			}
			default: { 
				ret = 99;
			}		
		}
		return ret;
	}

	/* (non-Javadoc)
	 * @see gov.nasa.jpf.jvm.ChoiceGenerator#hasMoreChoices()
	 */
	public boolean hasMoreChoices() {
		return state < 1;
	}

	/* (non-Javadoc)
	 * @see gov.nasa.jpf.jvm.ChoiceGenerator#advance(gov.nasa.jpf.jvm.JVM)
	 */
	public void advance(JVM vm) {
		state++;
	}

}

[Javapathfinder-devel] /javapathfinder/src/gov/nasa/jpf/jvm/choice TwoIntChoice.java,NONE,1.1 Double

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