code: //==============================================================================
  //	
  //	Copyright (c) 2002-
  //	Authors:
  //	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/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 explicit;
  
  import java.util.ArrayList;
  import java.util.BitSet;
  import java.util.Iterator;
  import java.util.List;
  import java.util.Map;
  
  import parser.State;
  import prism.PrismComponent;
  import prism.PrismException;
  import prism.PrismNotSupportedException;
  
  /**
   * Class to perform bisimulation minimisation for explicit-state models.
   */
  public class Bisimulation extends PrismComponent
  {
  	// Local storage of partition info
  	protected int numStates;
  	protected int[] partition;
  	protected int numBlocks;
  	protected MDPSimple mdp;
  
  	/**
  	 * Construct a new Bisimulation object.
  	 */
  	public Bisimulation(PrismComponent parent) throws PrismException
  	{
  		super(parent);
  	}
  
  	/**
  	 * Perform bisimulation minimisation on a model.
  	 * @param model The model
  	 * @param propNames Names of the propositions in {@code propBSs}
  	 * @param propBSs Propositions (satisfying sets of states) to be preserved by bisimulation.
  	 */
  	public Model minimise(Model model, List<String> propNames, List<BitSet> propBSs) throws PrismException
  	{
  		switch (model.getModelType()) {
  		case DTMC:
  			return minimiseDTMC((DTMC) model, propNames, propBSs);
  		case CTMC:
  			return minimiseCTMC((CTMC) model, propNames, propBSs);
  		default:
  			throw new PrismNotSupportedException("Bisimulation minimisation not yet supported for " + model.getModelType() + "s");
  		}
  	}
  
  	/**
  	 * Perform bisimulation minimisation on a DTMC.
  	 * @param dtmc The DTMC
  	 * @param propNames Names of the propositions in {@code propBSs}
  	 * @param propBSs Propositions (satisfying sets of states) to be preserved by bisimulation.
  	 */
  	private DTMC minimiseDTMC(DTMC dtmc, List<String> propNames, List<BitSet> propBSs)
  	{
  		// Create initial partition based on propositions
  		initialisePartitionInfo(dtmc, propBSs);
  		//printPartition(dtmc);
  
  		// Iterative splitting
  		boolean changed = true;
  		while (changed)
  			changed = splitDTMC(dtmc);
  		mainLog.println("Minimisation: " + numStates + " to " + numBlocks + " States");
  		//printPartition(dtmc);
  
  		// Build reduced model
  		DTMCSimple dtmcNew = new DTMCSimple(numBlocks);
  		for (int i = 0; i < numBlocks; i++) {
  			for (Map.Entry<Integer, Double> e : mdp.getChoice(i, 0)) {
  				dtmcNew.setProbability((Integer) mdp.getAction(i, 0), e.getKey(), e.getValue());
  			}
  		}
  		attachStatesAndLabels(dtmc, dtmcNew, propNames, propBSs);
  
  		return dtmcNew;
  	}
  
  	/**
  	 * Perform bisimulation minimisation on a CTMC.
  	 * @param ctmc The CTMC
  	 * @param propNames Names of the propositions in {@code propBSs}
  	 * @param propBSs Propositions (satisfying sets of states) to be preserved by bisimulation.
  	 */
  	private CTMC minimiseCTMC(CTMC ctmc, List<String> propNames, List<BitSet> propBSs)
  	{
  		// Create initial partition based on propositions
  		initialisePartitionInfo(ctmc, propBSs);
  		//printPartition(ctmc);
  
  		// Iterative splitting
  		boolean changed = true;
  		while (changed)
  			changed = splitDTMC(ctmc);
  		mainLog.println("Minimisation: " + numStates + " to " + numBlocks + " States");
  		//printPartition(ctmc);
  
  		// Build reduced model
  		CTMCSimple ctmcNew = new CTMCSimple(numBlocks);
  		for (int i = 0; i < numBlocks; i++) {
  			for (Map.Entry<Integer, Double> e : mdp.getChoice(i, 0)) {
  				ctmcNew.setProbability((Integer) mdp.getAction(i, 0), e.getKey(), e.getValue());
  			}
  		}
  		attachStatesAndLabels(ctmc, ctmcNew, propNames, propBSs);
  
  		return ctmcNew;
  	}
  
  	/**
  	 * Construct the initial partition based on a set of proposition bitsets.
  	 * Store info in {@code numStates}, {@code numBlocks} and {@code partition}.
  	 */
  	private void initialisePartitionInfo(Model model, List<BitSet> propBSs)
  	{
  		BitSet bs1, bs0;
  		numStates = model.getNumStates();
  		partition = new int[numStates];
  
  		// Compute all non-empty combinations of propositions
  		List<BitSet> all = new ArrayList<BitSet>();
  		bs1 = (BitSet) propBSs.get(0).clone();
  		bs0 = (BitSet) bs1.clone();
  		bs0.flip(0, numStates);
  		all.add(bs1);
  		all.add(bs0);
  		int n = propBSs.size();
  		for (int i = 1; i < n; i++) {
  			BitSet bs = propBSs.get(i);
  			int m = all.size();
  			for (int j = 0; j < m; j++) {
  				bs1 = all.get(j);
  				bs0 = (BitSet) bs1.clone();
   				bs0.andNot(bs);
  				bs1.and(bs);
  				if (bs1.isEmpty()) {
  					all.set(j, bs0);
  				} else {
  					if (!bs0.isEmpty())
  						all.add(bs0);
  				}
  			}
  		}
  
  		// Construct initial partition
  		numBlocks = all.size();
  		for (int j = 0; j < numBlocks; j++) {
  			BitSet bs = all.get(j);
  			for (int i = bs.nextSetBit(0); i >= 0; i = bs.nextSetBit(i + 1)) {
  				partition[i] = j;
  			}
  		}
  	}
  
  	/**
  	 * Perform a split of the current partition, if possible, updating {@code numBlocks} and {@code partition}.
  	 * @return whether or not the partition was split 
  	 */
  	private boolean splitDTMC(DTMC dtmc)
  	{
  		int s, a, i, numBlocksNew, numChoicesOld;
  		Distribution distrNew;
  		int partitionNew[];
  
  		partitionNew = new int[numStates];
  		numBlocksNew = 0;
  		// Compute the signature for each state (i.e. the distribution for outgoing
  		// transitions, lifted to the current partition)
  		// For convenience, we just store them as an MDP, with action label equal to the index of the block
  		mdp = new MDPSimple(numBlocks);
  		for (s = 0; s < numStates; s++) {
  			// Build lifted distribution
  			Iterator<Map.Entry<Integer, Double>> iter = dtmc.getTransitionsIterator(s);
  			distrNew = new Distribution();
  			while (iter.hasNext()) {
  				Map.Entry<Integer, Double> e = iter.next();
  				distrNew.add(partition[e.getKey()], e.getValue());
  			}
  			// Store in MDP, update new partition
  			a = partition[s];
  			numChoicesOld = mdp.getNumChoices(a);
  			i = mdp.addChoice(a, distrNew);
  			if (i == numChoicesOld)
  				mdp.setAction(a, i, numBlocksNew++);
  			partitionNew[s] = (Integer) mdp.getAction(a, i);
  		}
  		// Debug info
  		//mainLog.println("New partition: " + java.util.Arrays.toString(partitionNew));
  		//mainLog.println("Signatures MDP: " + mdp.infoString());
  		//mainLog.println("Signatures MDP: " + mdp);
  		//try { mdp.exportToDotFile("mdp.dot"); } catch (PrismException e) {}
  		// Update info
  		boolean changed = numBlocks != numBlocksNew;
  		partition = partitionNew;
  		numBlocks = numBlocksNew;
  
  		return changed;
  	}
  
  	/**
  	 * Display the current partition, showing the states in each block.
  	 */
  	@SuppressWarnings("unused")
  	private void printPartition(Model model)
  	{
  		for (int i = 0; i < numBlocks; i++) {
  			mainLog.print(i + ":");
  			for (int j = 0; j < numStates; j++)
  				if (partition[j] == i)
  					if (model.getStatesList() != null)
  						mainLog.print(" " + model.getStatesList().get(j));
  					else
  						mainLog.print(" " + j);
  			mainLog.println();
  		}
  	}
  
  	/**
  	 * Attach a list of states to the minimised model by adding a representative state
  	 * from the original model.
  	 * Also attach information about the propositions (used for bisimulation minimisation)
  	 * to the minimised model, in the form of labels (stored as BitSets).
  	 * @param model The original model
  	 * @param modelNew The minimised model
  	 * @param propNames The names of the propositions
  	 * @param propBSs Satisfying states (of the minimised model) for the propositions
  	 */
  	private void attachStatesAndLabels(Model model, ModelExplicit modelNew, List<String> propNames, List<BitSet> propBSs)
  	{
  		// Attach states
  		if (model.getStatesList() != null) {
  			List<State> statesList = model.getStatesList();
  			List<State> statesListNew = new ArrayList<State>(numBlocks);
  			for (int i = 0; i < numBlocks; i++) {
  				statesListNew.add(null);
  			}
  			for (int i = 0; i < numStates; i++) {
  				if (statesListNew.get(partition[i]) == null)
  					statesListNew.set(partition[i], statesList.get(i));
  			}
  			modelNew.setStatesList(statesListNew);
  		}
  
  		// Build/attach new labels
  		int numProps = propBSs.size();
  		for (int i = 0; i < numProps; i++) {
  			String propName = propNames.get(i);
  			BitSet propBS = propBSs.get(i);
  			BitSet propBSnew = new BitSet();
  			for (int j = propBS.nextSetBit(0); j >= 0; j = propBS.nextSetBit(j + 1))
  				propBSnew.set(partition[j]);
  			modelNew.addLabel(propName, propBSnew);
  		}
  	}
  }
  