code: //==============================================================================
  //	
  //	Copyright (c) 2013-
  //	Authors:
  //	* Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
  //	
  //------------------------------------------------------------------------------
  //	
  //	This file is part of PRISM.
  //	
  //	PRISM is free software; you can redistribute it and/or modify
  //	it under the terms of the GNU General Public License as published by
  //	the Free Software Foundation; either version 2 of the License, or
  //	(at your option) any later version.
  //	
  //	PRISM is distributed in the hope that it will be useful,
  //	but WITHOUT ANY WARRANTY; without even the implied warranty of
  //	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  //	GNU General Public License for more details.
  //	
  //	You should have received a copy of the GNU General Public License
  //	along with PRISM; if not, write to the Free Software Foundation,
  //	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
  //	
  //==============================================================================
  
  package param;
  
  import prism.PrismException;
  import prism.PrismNotSupportedException;
  
  /**
   * Reward structure for parametric model.
   * We only consider rewards assigned to a certain nondeterministic choice,
   * because for the properties we consider, state rewards can be stored
   * as equivalent choice rewards.
   * 
   * @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
   */
  final class ParamRewardStruct {
  	/** rewards for all choices */
  	Function[] rewards;
  	/** function factory the functions used for rewards belong to */
  	FunctionFactory factory;
  	
  	/**
  	 * Constructs a new reward structure for with given number of choices.
  	 * Initially, all rewards will be zero.
  	 * 
  	 * @param factory function factory to use
  	 * @param numChoices number of different rewards
  	 */
  	ParamRewardStruct(FunctionFactory factory, int numChoices)
  	{
  		this.rewards = new Function[numChoices];
  		this.factory = factory;
  		for (int choice = 0; choice < numChoices; choice++) {
  			rewards[choice] = factory.getZero();
  		}
  	}
  	
  	/**
  	 * Constructs a new reward structure which is the copy of another one.
  	 * 
  	 * @param other original to construct copy of
  	 */
  	ParamRewardStruct(ParamRewardStruct other)
  	{
  		this.rewards = new Function[other.rewards.length];
  		for (int choice = 0; choice < other.rewards.length; choice++) {
  			this.rewards[choice] = other.rewards[choice];
  		}
  		this.factory = other.factory;
  	}
  	
  	/**
  	 * Instantiate reward structure at a given point.
  	 * That is, a reward structure is computed in which the corresponding
  	 * values have been inserted for each parameter, and which is thus
  	 * nonparametric.
  	 * 
  	 * @param point instantiate for these parameter values
  	 * @return non-parametric reward structure instantiated at given point
  	 */
  	ParamRewardStruct instantiate(Point point)
  	{
  		ParamRewardStruct result = new ParamRewardStruct(factory, rewards.length);
  		for (int choice = 0; choice < rewards.length; choice++) {
  			result.rewards[choice] = factory.fromBigRational(this.rewards[choice].evaluate(point));
  		}
  		result.factory = this.factory;
  		
  		return result;
  	}
  	
  	/**
  	 * Set reward for given choice.
  	 * 
  	 * @param choice choice to set reward for
  	 * @param reward reward to set
  	 */
  	void setReward(int choice, Function reward)
  	{
  		rewards[choice] = reward;
  	}
  	
  	/**
  	 * Add reward to given choice.
  	 * 
  	 * @param choice choice to add reward to
  	 * @param reward reward to add to existing reward for choice
  	 */
  	void addReward(int choice, Function reward)
  	{
  		rewards[choice] = rewards[choice].add(reward);
  	}
  	
  	/**
  	 * Get reward for given choice.
  	 * 
  	 * @param choice choice to get reward of
  	 * @return reward for given choice
  	 */
  	Function getReward(int choice)
  	{
  		return rewards[choice];
  	}
  
  	/**
  	 * Returns true if there are negative rewards.
  	 * <br>
  	 * Can only be called on a reward structure that
  	 * has been instantiated, i.e., where all rewards
  	 * are constant rational numbers.
  	 * <br>
  	 * If either +/-Inf or NaN are encountered, an exception is thrown.
  	 */
  	public boolean hasNegativeRewards() throws PrismException
  	{
  		for (Function r : rewards) {
  			if (!r.isConstant()) {
  				throw new UnsupportedOperationException("Can not check for negative rewards against non-constant functions");
  			}
  			BigRational v = r.asBigRational();
  			if (v.isSpecial()) {
  				throw new PrismNotSupportedException("Reward value " + v + " not supported");
  			}
  			if (r.asBigRational().signum() < 0) {
  				return true;
  			}
  		}
  
  		return false;
  	}
  
  	/**
  	 * Check for non-normal reward values, i.e., +/-Inf and NaN,
  	 * throw exception if detected.
  	 */
  	public void checkForNonNormalRewards() throws PrismException
  	{
  		for (Function r : rewards) {
  			if (r.isInf() || r.isMInf() || r.isNaN()) {
  				throw new PrismNotSupportedException("Reward value " + r + " not supported");
  			}
  		}
  	}
  
  	@Override
  	public String toString() {
  		StringBuffer result = new StringBuffer();
  		for (int state = 0; state < rewards.length; state++) {
  			result.append(state);
  			result.append(": ");
  			result.append(rewards[state]);
  			result.append("\n");
  		}
  		return result.toString();
  	}
  	
  	@Override
  	public boolean equals(Object obj) {
  		if (!(obj instanceof ParamRewardStruct)) {
  			return false;
  		}
  		ParamRewardStruct other = (ParamRewardStruct) obj;
  		if (!this.factory.equals(other.factory)) {
  			return false;
  		}
  		if (this.rewards.length != other.rewards.length) {
  			return false;
  		}
  		for (int choice = 0; choice < rewards.length; choice++) {
  			if (!this.rewards[choice].equals(other.rewards[choice])) {
  				return false;
  			}
  		}
  		return true;
  	}
  	
  	@Override
  	public int hashCode() {
  		int hash = 0;
  		
  		hash = factory.hashCode();
  		for (int choice = 0; choice < rewards.length; choice++) {
  			hash = rewards[choice].hashCode() + (hash << 6) + (hash << 16) - hash;
  		}
  
  		return hash;
  	}
  }
  