diff --git a/prism/src/explicit/Bisimulation.java b/prism/src/explicit/Bisimulation.java new file mode 100644 index 00000000..64588a9a --- /dev/null +++ b/prism/src/explicit/Bisimulation.java @@ -0,0 +1,282 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (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 propNames, List 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 propNames, List 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 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 propNames, List 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 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 propBSs) + { + BitSet bs1, bs0; + numStates = model.getNumStates(); + partition = new int[numStates]; + + // Compute all non-empty combinations of propositions + List all = new ArrayList(); + 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> iter = dtmc.getTransitionsIterator(s); + distrNew = new Distribution(); + while (iter.hasNext()) { + Map.Entry 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 propNames, List propBSs) + { + // Attach states + if (model.getStatesList() != null) { + List statesList = model.getStatesList(); + List statesListNew = new ArrayList(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); + } + } +} diff --git a/prism/src/explicit/ModelExplicit.java b/prism/src/explicit/ModelExplicit.java index 2500d049..fc05946c 100644 --- a/prism/src/explicit/ModelExplicit.java +++ b/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 labels = new TreeMap(); + // Mutators /** diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index bd147074..f0b017f6 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/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 propNames = new ArrayList(); + ArrayList propBSs = new ArrayList(); + 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 propNames, List 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 propNames; + private List propBSs; + + public CheckMaximalPropositionalFormulas(StateModelChecker mc, Model model, List propNames, List 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.) diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 2b9f66e4..96d4d030 100644 --- a/prism/src/prism/Prism.java +++ b/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; } diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 9aec2f8f..f525ebd1 100644 --- a/prism/src/prism/PrismCL.java +++ b/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