Add experimental bisimulation option (explicit engine, hidden option).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7630 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/explicit/Bisimulation.java

@@ -0,0 +1,282 @@
+//==============================================================================
+//	
+//	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;
+
+/**
+ * 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 PrismException("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.
+	 */
+	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.labels.put(propName, propBSnew);
+		}
+	}
+}

prism/src/explicit/ModelExplicit.java

@@ -30,6 +30,8 @@ import java.io.File;
 import java.util.ArrayList;
 import java.util.BitSet;
 import java.util.List;
+import java.util.Map;
+import java.util.TreeMap;
 import java.util.TreeSet;
 
 import parser.State;
@@ -60,6 +62,8 @@ public abstract class ModelExplicit implements Model
 	// Constant info (read only, just a pointer)
 	protected Values constantValues;
 
+	public Map<String,BitSet> labels = new TreeMap<String, BitSet>();
+	
 	// Mutators
 
 	/**

prism/src/explicit/StateModelChecker.java

@@ -35,6 +35,7 @@ import java.util.BitSet;
 import java.util.HashMap;
 import java.util.List;
 import java.util.Map;
+import java.util.Vector;
 
 import parser.State;
 import parser.Values;
@@ -50,6 +51,7 @@ import parser.ast.ExpressionIdent;
 import parser.ast.ExpressionLabel;
 import parser.ast.ExpressionLiteral;
 import parser.ast.ExpressionProp;
+import parser.ast.ExpressionTemporal;
 import parser.ast.ExpressionUnaryOp;
 import parser.ast.ExpressionVar;
 import parser.ast.LabelList;
@@ -59,6 +61,8 @@ import parser.ast.Property;
 import parser.type.TypeBool;
 import parser.type.TypeDouble;
 import parser.type.TypeInt;
+import parser.type.TypePathBool;
+import parser.visitor.ASTTraverseModify;
 import prism.Filter;
 import prism.ModelType;
 import prism.PrismComponent;
@@ -87,6 +91,9 @@ public class StateModelChecker extends PrismComponent
 	// Generate/store a strategy during model checking?
 	protected boolean genStrat = false;
 
+	// Do bisimulation minimisation before model checking?
+	protected boolean doBisim = false;
+
 	// Model file (for reward structures, etc.)
 	protected ModulesFile modulesFile = null;
 
@@ -196,6 +203,14 @@ public class StateModelChecker extends PrismComponent
 		this.genStrat = genStrat;
 	}
 
+	/**
+	 * Specify whether or not to do bisimulation minimisation before model checking.
+	 */
+	public void setDoBisim(boolean doBisim)
+	{
+		this.doBisim = doBisim;
+	}
+
 	// Get methods for flags/settings
 
 	public int getVerbosity()
@@ -211,6 +226,14 @@ public class StateModelChecker extends PrismComponent
 		return genStrat;
 	}
 
+	/**
+	 * Whether or not to do bisimulation minimisation before model checking.
+	 */
+	public boolean getDoBisim()
+	{
+		return doBisim;
+	}
+
 	// Other setters/getters
 
 	/**
@@ -293,6 +316,18 @@ public class StateModelChecker extends PrismComponent
 			expr = exprFilter;
 		}
 
+		// If required, do bisimulation minimisation
+		if (doBisim) {
+			mainLog.println("\nPerforming bisimulation minimisation...");
+			ArrayList<String> propNames = new ArrayList<String>();
+			ArrayList<BitSet> propBSs = new ArrayList<BitSet>();
+			Expression exprNew = checkMaximalPropositionalFormulas(model, expr.deepCopy(), propNames, propBSs);
+			Bisimulation bisim = new Bisimulation(this);
+			model = bisim.minimise(model, propNames, propBSs);
+			mainLog.println("Modified property: " + exprNew);
+			expr = exprNew;
+		}
+		
 		// Do model checking and store result vector
 		timer = System.currentTimeMillis();
 		vals = checkExpression(model, expr);
@@ -634,6 +669,10 @@ public class StateModelChecker extends PrismComponent
 			}
 			return StateValues.createFromBitSet(bs, model);
 		} else {
+			BitSet bs = ((ModelExplicit) model).labels.get(expr.getName());
+			if (bs != null) {
+				return StateValues.createFromBitSet((BitSet) bs.clone(), model);
+			}
 			ll = propertiesFile.getCombinedLabelList();
 			i = ll.getLabelIndex(expr.getName());
 			if (i == -1)
@@ -951,6 +990,143 @@ public class StateModelChecker extends PrismComponent
 		return resVals;
 	}
 
+	/**
+	 * Extract maximal propositional subformulas of an expression, model check them and
+	 * replace them with ExpressionLabel objects (L0, L1, etc.) Expression passed in is modified directly, but the result
+	 * is also returned. As an optimisation, model checking that results in true/false for all states is converted to an
+	 * actual true/false, and duplicate results are given the same proposition. BitSets giving the states which satisfy each proposition
+	 * are put into the list {@code propBSs}, which should be empty when this function is called.
+	 * The names of the labels (L0, L1, etc. by default) are put into {@code propNames}, which should also be empty. 
+	 */
+	public Expression checkMaximalPropositionalFormulas(Model model, Expression expr, List<String> propNames, List<BitSet> propBSs) throws PrismException
+	{
+		Expression exprNew = (Expression) expr.accept(new CheckMaximalPropositionalFormulas(this, model, propNames, propBSs));
+		return exprNew;
+	}
+
+	/**
+	 * Class to replace maximal propositional subformulas of an expression
+	 * with labels corresponding to BitSets for the states that satisfy them.
+	 */
+	class CheckMaximalPropositionalFormulas extends ASTTraverseModify
+	{
+		private StateModelChecker mc;
+		private Model model;
+		private List<String> propNames;
+		private List<BitSet> propBSs;
+		
+		public CheckMaximalPropositionalFormulas(StateModelChecker mc, Model model, List<String> propNames, List<BitSet> propBSs)
+		{
+			this.mc = mc;
+			this.model = model;
+			this.propNames = propNames;
+			this.propBSs = propBSs;
+		}
+		
+		public Object visit(ExpressionITE e) throws PrismLangException
+		{
+			return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visit(e);
+		}
+		
+		public Object visit(ExpressionBinaryOp e) throws PrismLangException
+		{
+			return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visit(e);
+		}
+		
+		public Object visit(ExpressionUnaryOp e) throws PrismLangException
+		{
+			return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visit(e);
+		}
+		
+		public Object visit(ExpressionFunc e) throws PrismLangException
+		{
+			return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visit(e);
+		}
+		
+		public Object visit(ExpressionIdent e) throws PrismLangException
+		{
+			return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visit(e);
+		}
+		
+		public Object visit(ExpressionLiteral e) throws PrismLangException
+		{
+			return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visit(e);
+		}
+		
+		public Object visit(ExpressionConstant e) throws PrismLangException
+		{
+			return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visit(e);
+		}
+		
+		public Object visit(ExpressionFormula e) throws PrismLangException
+		{
+			return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visit(e);
+		}
+		
+		public Object visit(ExpressionVar e) throws PrismLangException
+		{
+			return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visit(e);
+		}
+		
+		public Object visit(ExpressionLabel e) throws PrismLangException
+		{
+			return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visit(e);
+		}
+		
+		public Object visit(ExpressionProp e) throws PrismLangException
+		{
+			// Look up property and recurse
+			Property prop = propertiesFile.lookUpPropertyObjectByName(e.getName());
+			if (prop != null) {
+				return e.accept(this);
+			} else {
+				throw new PrismLangException("Unknown property reference " + e, e);
+			}
+		}
+		
+		public Object visit(ExpressionFilter e) throws PrismLangException
+		{
+			return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visit(e);
+		}
+		
+		/**
+		 * Evaluate this expression in all states (i.e. model check it),
+		 * store the resulting BitSet in the list {@code propBSs},
+		 * and return an ExpressionLabel with name Li to replace it
+		 * (where i denotes the 0-indexed index into the list propBSs).
+		 */
+		private Object replaceWithLabel(Expression e) throws PrismLangException
+		{
+			// Model check
+			StateValues sv;
+			try {
+				sv = mc.checkExpression(model, e);
+			} catch (PrismException ex) {
+				throw new PrismLangException(ex.getMessage());
+			}
+			BitSet bs = sv.getBitSet();
+			// Detect special cases (true, false) for optimisation
+			if (bs.isEmpty()) {
+				return Expression.False();
+			}
+			if (bs.cardinality() == model.getNumStates()) {
+				return Expression.True();
+			}
+			// See if we already have an identical result
+			// (in which case, reuse it)
+			int i = propBSs.indexOf(bs);
+			if (i != -1) {
+				sv.clear();
+				return new ExpressionLabel("L" + i);
+			}
+			// Otherwise, add result to list, return new label
+			String newLabelName = "L" + propBSs.size();
+			propNames.add(newLabelName);
+			propBSs.add(bs);
+			return new ExpressionLabel(newLabelName);
+		}
+	}
+	
 	/**
 	 * Loads labels from a PRISM labels file and stores them in BitSet objects.
 	 * (Actually, it returns a map from label name Strings to BitSets.)

prism/src/prism/Prism.java

@@ -193,6 +193,8 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 	protected String exportProductStatesFilename = null;
 	// Generate/store a strategy during model checking?
 	protected boolean genStrat = false; 
+	// Do bisimulation minimisation before model checking?
+	protected boolean doBisim = false;
 
 	// A few miscellaneous options (i.e. defunct/hidden/undocumented/etc.)
 	// See constructor below for default values
@@ -583,6 +585,14 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 		this.genStrat = genStrat;
 	}
 
+	/**
+	 * Specify whether or not to do bisimulation minimisation before model checking.
+	 */
+	public void setDoBisim(boolean doBisim)
+	{
+		this.doBisim = doBisim;
+	}
+
 	public void setDoReach(boolean b) throws PrismException
 	{
 		doReach = b;
@@ -873,6 +883,14 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 		return genStrat;
 	}
 
+	/**
+	 * Whether or not to do bisimulation minimisation before model checking.
+	 */
+	public boolean getDoBisim()
+	{
+		return doBisim;
+	}
+
 	public boolean getDoReach()
 	{
 		return doReach;
@@ -3415,6 +3433,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 		mc.setModulesFileAndPropertiesFile(currentModulesFile, propertiesFile);
 		// Pass any additional local settings
 		mc.setGenStrat(genStrat);
+		mc.setDoBisim(doBisim);
 		
 		return mc;
 	}

prism/src/prism/PrismCL.java

@@ -1601,6 +1601,10 @@ public class PrismCL implements PrismModelListener
 				} else if (sw.equals("bfs")) {
 					prism.setReachMethod(Prism.REACH_BFS);
 				}
+				// enable bisimulation minimisation before model checking (hidden option)
+				else if (sw.equals("bisim")) {
+					prism.setDoBisim(true);
+				}
 
 				// Other switches - pass to PrismSettings