prism-accumulation/prism/src/param/Lumper.java

//==============================================================================
//	
//	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 java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;

/**
 * Base class for signature-based bisimulation lumping.
 * Derived classes could implement specific types of bisimulation,
 * e.g. weak, strong, etc.
 * 
 * @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
 * @see NullLumper
 * @see StrongLumper
 * @see WeakLumper
 */
abstract class Lumper {
	/**
	 * Kind of lumping to be used.
	 */
	enum BisimType {
		NULL,
		STRONG,
		WEAK
	}
	
	/** stores the original model to be lumped */
	protected MutablePMC origPmc;
	/** stores the lumped model */
	protected MutablePMC optPmc;
	/** stores the state partitioning */
	protected Partition partition;
	/** maintains a mapping from blocks to block numbers */
	protected HashMap<HashSet<Integer>, Integer> blockToNumber;
	/** list of all blocks */
	protected ArrayList<HashSet<Integer>> blocks;
	/** maps states from original to containing states in lumped model */
	protected int[] originalToOptimised;

	/**
	 * Creates new lumper for given parametric Markov chain.
	 * 
	 * @param origPmc Markov chain to build lumper for
	 */
	Lumper(MutablePMC origPmc)
	{
		this.origPmc = origPmc;
		partition = new Partition(origPmc);
		createInitialPartition();
		lump();
		mapBlocksToNumber();
		buildQuotient();
	}

	/**
	 * Creates a new lumper.
	 * This constructor needs to be present for technical reasons.
	 */
	protected Lumper()
	{
		
	}

	/**
	 * Stores combination of state reward and state time.
	 * This class is used subsume states with the same reward and time.
	 * If the time entry is irrelevant, it can be set to null.
	 *  
	 * @author Ernst Moritz Hahn <emhahn@cs.ox.ac.uk> (University of Oxford)
	 */
	class RewardEntry
	{
		/** reward for this entry */
		final Function reward;
		/** time for this entry */
		final Function time;
		
		/**
		 * Creates a new reward entry.
		 * 
		 * @param reward reward for this entry
		 * @param time time for this entry.
		 */
		RewardEntry(Function reward, Function time) {
			this.reward = reward;
			this.time = time;
		}
		
		@Override
		public int hashCode()
		{
			int hash = reward.hashCode() << 13;
			if (time != null) {
				hash |= time.hashCode();
			}
			return hash;
		}
		
		@Override
		public boolean equals(Object obj)
		{
			if (!(obj instanceof RewardEntry)) {
				return false;
			}
			
			RewardEntry other = (RewardEntry) obj;
			if (!this.reward.equals(other.reward)) {
				return false;
			}
			if ((this.time == null) != (other.time == null)) {
				return false;
			}
			if (this.time != null && !this.time.equals(other.time)) {
				return false;
			}
			return true;
		}
	}
	
	/**
	 * Creates an initial partitioning appropriate for analysis to perform.
	 * For reachability, takes care that only target-states / non-target
	 * are stored in one initial block, for reward analyses takes care
	 * that only states with same reward are subsumed, etc. For certain types
	 * of bisimulations, this is not enough, and the initial partition must be
	 * refined further before starting the main refinement process. This is
	 * the case for instance for weak bisimulation.
	 */
	protected void createInitialPartition()
	{
		HashSet<Integer> oldBlock = partition.nextChangeableBlock();
		if (!origPmc.isUseRewards()) {
			HashSet<Integer> safeStates = new HashSet<Integer>();
			HashSet<Integer> unsafeStates = new HashSet<Integer>();
			for (int state : oldBlock) {
				if (origPmc.isTargetState(state)) {
					unsafeStates.add(state);
				} else {
					safeStates.add(state);
				}
			}
			ArrayList<HashSet<Integer>> newBlocks = new ArrayList<HashSet<Integer>>(); 
			if (safeStates.size() != 0) {
				newBlocks.add(safeStates);
			}
			if (unsafeStates.size() != 0) {
				newBlocks.add(unsafeStates);
			}
			partition.addBlocks(newBlocks);
		} else {
			HashMap<RewardEntry, HashSet<Integer>> rewardToStateMap = new HashMap<RewardEntry, HashSet<Integer>>();
			for (int state : oldBlock) {
				Function reward = origPmc.getReward(state);
				Function time = null;
				if (origPmc.isUseTime()) {
					time = origPmc.getTime(state);
				}
				RewardEntry entry = new RewardEntry(reward, time);
				HashSet<Integer> block = rewardToStateMap.get(entry);
				if (block == null) {
					block = new HashSet<Integer>();
					rewardToStateMap.put(entry, block);
				}
				block.add(state);
			}
			ArrayList<HashSet<Integer>> newBlocks = new ArrayList<HashSet<Integer>>(); 
			for (HashSet<Integer> block : rewardToStateMap.values()) {
				if (block.size() != 0) {
					newBlocks.add(block);
				}
			}
			partition.addBlocks(newBlocks);
		}
		partition.markAllBlocksAsNew();
	}
	
	/**
	 * Return the quotient of the original model.
	 * Before calling this method, {@code lump()} must have been called.
	 * 
	 * @return quotient of original model
	 */
	MutablePMC getQuotient()
	{
		return optPmc;
	}
	
	/**
	 * Enumerates the blocks after refinement is finished.
	 * This is done as a preparation to create the quotient and the
	 * mapping from original to quotient states.
	 */
	protected void mapBlocksToNumber()
	{
		blocks = partition.getAllBlocks();
		blockToNumber = new HashMap<HashSet<Integer>, Integer>();
		originalToOptimised = new int[origPmc.getNumStates()];
		int nextBlockNumber = 0;
		for (HashSet<Integer> block : blocks) {
			blockToNumber.put(block, nextBlockNumber);
			for (int state : block) {
				originalToOptimised[state] = nextBlockNumber;
			}
			nextBlockNumber++;
		}
	}
	
	/**
	 * Returns a mapping from original model states to quotient states.
	 * Thus, {@result[state]} is the state of the quotient to which
	 * {@code state} belongs.
	 * 
	 * @return mapping from original model states to quotient states
	 */
	int[] getOriginalToOptimised()
	{
		return originalToOptimised;
	}
	
	/**
	 * Perform the lumping process.
	 * Refines blocks from the list of blocks to refine, it is clear that
	 * further tries to refine blocks will not lead to the creation of any
	 * new blocks.
	 */
	protected void lump()
	{
		ArrayList<HashSet<Integer>> newBlocks = new ArrayList<HashSet<Integer>>();
		while (partition.mayChange()) {
			newBlocks.clear();
			HashSet<Integer> oldBlock = partition.nextChangeableBlock();
			refineBlock(oldBlock, newBlocks);
			partition.addBlocks(newBlocks);
		}
	}
	
	/**
	 * Refine a given block.
	 * The exact way of how this is done depends on the type of bisimulation used.
	 * 
	 * @param oldBlock block to refine
	 * @param newBlocks list of new blocks generated
	 */
	abstract protected void refineBlock(HashSet<Integer> oldBlock, ArrayList<HashSet<Integer>> newBlocks);
	
	/**
	 * Build the quotients after refinement has finished.
	 * Each state of the quotient will be a block of states from the original
	 * model. The exact way of how transitions between states are computed
	 * depends on the type of bisimulation used.
	 */
	abstract protected void buildQuotient();
}