diff --git a/prism/src/prism/Model.java b/prism/src/prism/Model.java index 6757c5a7..c6f82801 100644 --- a/prism/src/prism/Model.java +++ b/prism/src/prism/Model.java @@ -35,7 +35,12 @@ import parser.*; public interface Model { - String getType(); + public static final int DTMC = 1; + public static final int CTMC = 2; + public static final int MDP = 3; + + int getType(); + String getTypeString(); int getNumModules(); String[] getModuleNames(); diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 6921f114..e63dff16 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -3,6 +3,7 @@ // Copyright (c) 2002- // Authors: // * Dave Parker (University of Oxford, formerly University of Birmingham) +// * Carlos S. Bederián (Universidad Nacional de Córdoba) // //------------------------------------------------------------------------------ // @@ -26,12 +27,19 @@ package prism; +import java.util.*; + import jdd.*; import dv.*; import mtbdd.*; +import simulator.SimulatorException; import sparse.*; import hybrid.*; import parser.ast.*; +import parser.visitor.ASTTraverse; +import parser.visitor.ASTTraverseModify; +import jltl2ba.APElement; +import jltl2dstar.*; /* * Model checker for MDPs @@ -173,7 +181,7 @@ public class NondetModelChecker extends StateModelChecker // Compute probabilities boolean qual = pb != null && ((p == 0) || (p == 1)) && precomp; - probs = checkProbPathExpression(expr.getExpression(), qual, min); + probs = checkProbPathFormula(expr.getExpression(), qual, min); // Print out probabilities if (verbose) { @@ -302,20 +310,22 @@ public class NondetModelChecker extends StateModelChecker } } - // Contents of a P operator + // Contents of a P operator, i.e. a path formula - protected StateProbs checkProbPathExpression(Expression expr, boolean qual, boolean min) throws PrismException + protected StateProbs checkProbPathFormula(Expression expr, boolean qual, boolean min) throws PrismException { // Test whether this is a simple path formula (i.e. PCTL) // and then pass control to appropriate method. if (expr.isSimplePathFormula()) { - return checkProbPathExpressionSimple(expr, qual, min); + return checkProbPathFormulaSimple(expr, qual, min); } else { - throw new PrismException("LTL-style path formulas are not supported"); + return checkProbPathFormulaLTL(expr, qual, min); } } - protected StateProbs checkProbPathExpressionSimple(Expression expr, boolean qual, boolean min) + // Simple path formula for P operator (one temporal op, possibly negated) + + protected StateProbs checkProbPathFormulaSimple(Expression expr, boolean qual, boolean min) throws PrismException { StateProbs probs = null; @@ -326,12 +336,12 @@ public class NondetModelChecker extends StateModelChecker // Parentheses if (exprUnary.getOperator() == ExpressionUnaryOp.PARENTH) { // Recurse - probs = checkProbPathExpressionSimple(exprUnary.getOperand(), qual, min); + probs = checkProbPathFormulaSimple(exprUnary.getOperand(), qual, min); } // Negation else if (exprUnary.getOperator() == ExpressionUnaryOp.NOT) { // Flip min/max, then subtract from 1 - probs = checkProbPathExpressionSimple(exprUnary.getOperand(), qual, !min); + probs = checkProbPathFormulaSimple(exprUnary.getOperand(), qual, !min); probs.subtractFromOne(); } } @@ -352,7 +362,7 @@ public class NondetModelChecker extends StateModelChecker } // Anything else - convert to until and recurse else { - probs = checkProbPathExpressionSimple(exprTemp.convertToUntilForm(), qual, min); + probs = checkProbPathFormulaSimple(exprTemp.convertToUntilForm(), qual, min); } } @@ -362,6 +372,143 @@ public class NondetModelChecker extends StateModelChecker return probs; } + // LTL-like path formula for P operator + + protected StateProbs checkProbPathFormulaLTL(Expression expr, boolean qual, boolean min) throws PrismException + { + StateProbs probs = null; + Expression ltl; + Vector labelDDs; + DRA dra; + JDDNode draDD, product; + JDDVars draDDRowVars, draDDColVars; + long l; + int i, j, n; + + // Model check maximal state formulas + labelDDs = new Vector(); + ltl = checkMaximalStateFormulas(expr.deepCopy(), labelDDs); + System.out.println(ltl); + + // Convert LTL formula to deterministic Rabin automaton (DRA) + mainLog.println("\nBuilding deterministic Rabin automaton..."); + l = System.currentTimeMillis(); + dra = LTL2Rabin.ltl2rabin(ltl.convertForJltl2ba()); + mainLog.println("\nDRA has "+dra.size()+" states."); + //dra.print(System.out); + l = System.currentTimeMillis() - l; + mainLog.println("\nTime for Rabin translation: " + l/1000.0 + " seconds."); + + draDDRowVars = new JDDVars(); + draDDColVars = new JDDVars(); + n = (int)Math.ceil(PrismUtils.log2(dra.size())); + j = 1000; + for (i = 0; i < n; i++) { + draDDRowVars.addVar(JDD.Var(j++)); + draDDColVars.addVar(JDD.Var(j++)); + } + draDD = convertDRAToBDD(dra, labelDDs, draDDRowVars, draDDColVars); + JDD.Ref(trans); + product = JDD.Apply(JDD.TIMES, trans, draDD); + + mainLog.println("Model-DRA product: " + JDD.GetInfoString(product, model.getNumDDVarsInTrans()+n)); + + if (probs == null) + throw new PrismException("Yikes"); // TODO + + return probs; + } + + /* Extract maximal state formula from an LTL path formula, model check them + * and replace them with ExpressionLabel objects L0, L1, etc. + * As an optimisation, model checking that results in true/false for + * all states is converted to an actual true/false. + */ + private Expression checkMaximalStateFormulas(Expression expr, Vector labelDDs) throws PrismException + { + // A state formula + if (expr.getType() == Expression.BOOLEAN) { + // Model check + JDDNode dd = checkExpressionDD(expr); + // Detect special cases (true, false) for optimisation + if (dd.equals(JDD.ZERO)) { + return Expression.False(); + } + if (dd.equals(reach)) { + return Expression.True(); + } + // See if we already have an identical result + // (in which case, reuse it) + int i = labelDDs.indexOf(dd); + if (i != -1) return new ExpressionLabel("L"+i); + // Otherwise, add result to list, return new label + labelDDs.add(dd); + return new ExpressionLabel("L"+(labelDDs.size()-1)); + } + // A path formula (recurse, modify, return) + else if (expr.getType() == Expression.PATH_BOOLEAN) { + if (expr instanceof ExpressionBinaryOp) { + ExpressionBinaryOp exprBinOp = (ExpressionBinaryOp)expr; + exprBinOp.setOperand1(checkMaximalStateFormulas(exprBinOp.getOperand1(), labelDDs)); + exprBinOp.setOperand2(checkMaximalStateFormulas(exprBinOp.getOperand2(), labelDDs)); + } + else if (expr instanceof ExpressionUnaryOp) { + ExpressionUnaryOp exprUnOp = (ExpressionUnaryOp)expr; + exprUnOp.setOperand(checkMaximalStateFormulas(exprUnOp.getOperand(), labelDDs)); + } + else if (expr instanceof ExpressionTemporal) { + ExpressionTemporal exprTemp = (ExpressionTemporal)expr; + if (exprTemp.getOperand1() != null) { + exprTemp.setOperand1(checkMaximalStateFormulas(exprTemp.getOperand1(), labelDDs)); + } + if (exprTemp.getOperand2() != null) { + exprTemp.setOperand2(checkMaximalStateFormulas(exprTemp.getOperand2(), labelDDs)); + } + } + } + return expr; + } + + private JDDNode convertDRAToBDD(DRA dra, Vector labelDDs, JDDVars draDDRowVars, JDDVars draDDColVars) + { + JDDNode draMask; + Iterator it; + DA_State state; + JDDNode label, exprBDD, transition; + int i, n; + + draMask = JDD.Constant(0); + // Iterate through all (states and) transitions of DRA + for (it = dra.iterator(); it.hasNext(); ) { + state = it.next(); + for (Map.Entry edge : state.edges().entrySet()) { + // Build a transition label BDD for each edge + mainLog.println(state.getName() + " to " + edge.getValue().getName() + " through " + edge.getKey().toString(dra.getAPSet(), false)); + label = JDD.Constant(1); + n = dra.getAPSize(); + for (i = 0; i < n; i++) { + // Get the expression BDD for label i + exprBDD = labelDDs.get(Integer.parseInt(dra.getAPSet().getAP(i).substring(1))); + JDD.Ref(exprBDD); + if (!edge.getKey().get(i)) { + exprBDD = JDD.Not(exprBDD); + } + label = JDD.And(label, exprBDD); + } + // Switch label BDD to col vars + label = JDD.PermuteVariables(label, allDDRowVars, allDDColVars); + // Build a BDD for the edge + transition = JDD.SetMatrixElement(JDD.Constant(0), draDDRowVars, draDDColVars, state.getName(), edge.getValue().getName(), 1); + // Now get the conjunction of the two + transition = JDD.And(transition, label); + // Add edge BDD to the DRA transition mask + draMask = JDD.Or(draMask, transition); + } + } + + return draMask; + } + // next protected StateProbs checkProbNext(ExpressionTemporal expr, boolean min) throws PrismException @@ -369,10 +516,6 @@ public class NondetModelChecker extends StateModelChecker JDDNode b; StateProbs probs = null; - // check not LTL - if (expr.getOperand2().getType() != Expression.BOOLEAN) - throw new PrismException("Invalid path formula"); - // model check operand first b = checkExpressionDD(expr.getOperand2()); @@ -397,12 +540,6 @@ public class NondetModelChecker extends StateModelChecker JDDNode b1, b2; StateProbs probs = null; - // check not LTL - if (expr.getOperand1().getType() != Expression.BOOLEAN) - throw new PrismException("Invalid path formula"); - if (expr.getOperand2().getType() != Expression.BOOLEAN) - throw new PrismException("Invalid path formula"); - // get info from bounded until time = expr.getUpperBound().evaluateInt(constantValues, null); if (time < 0) { @@ -456,12 +593,6 @@ public class NondetModelChecker extends StateModelChecker StateProbs probs = null; long l; - // check not LTL - if (expr.getOperand1().getType() != Expression.BOOLEAN) - throw new PrismException("Invalid path formula"); - if (expr.getOperand2().getType() != Expression.BOOLEAN) - throw new PrismException("Invalid path formula"); - // model check operands first b1 = checkExpressionDD(expr.getOperand1()); try { diff --git a/prism/src/prism/ProbModel.java b/prism/src/prism/ProbModel.java index c4049bae..928fd163 100644 --- a/prism/src/prism/ProbModel.java +++ b/prism/src/prism/ProbModel.java @@ -35,136 +35,354 @@ import mtbdd.*; import parser.*; import sparse.*; -// class to store an instance of a fully probabilistic model (mtbdds) - +/* + * Class to store a PRISM model which is a DTMC + */ public class ProbModel implements Model { // model info - - // type - private static final String type = "Probabilistic (DTMC)"; + // modules - private int numModules; // number of modules - private String[] moduleNames; // module names + protected int numModules; // number of modules + protected String[] moduleNames; // module names // vars/consts - private int numVars; // total number of module variables - private VarList varList; // list of module variables - private long[] gtol; // numbers for use by globalToLocal - private Values constantValues; // values of constants + protected int numVars; // total number of module variables + protected VarList varList; // list of module variables + protected long[] gtol; // numbers for use by globalToLocal + protected Values constantValues; // values of constants // rewards - private int numRewardStructs; // number of reward structs - private String[] rewardStructNames; // reward struct names + protected int numRewardStructs; // number of reward structs + protected String[] rewardStructNames; // reward struct names // stats - private double numStates; // number of states - private double numTransitions; // number of transitions - private double numStartStates; // number of initial states + protected double numStates; // number of states + protected double numTransitions; // number of transitions + protected double numStartStates; // number of initial states // reachable state list - private StateListMTBDD reachStateList = null; + protected StateListMTBDD reachStateList = null; // deadlock state list - private StateListMTBDD deadlockStateList = null; + protected StateListMTBDD deadlockStateList = null; // initial state list - private StateListMTBDD startStateList = null; - + protected StateListMTBDD startStateList = null; + // mtbdd stuff - + // dds - private JDDNode trans; // transition matrix dd - private JDDNode trans01; // 0-1 transition matrix dd - private JDDNode start; // start state dd - private JDDNode reach; // reachable states dd - private JDDNode deadlocks; // deadlock states dd - private JDDNode fixdl; // fixed deadlock states dd - private JDDNode stateRewards[]; // state rewards dds - private JDDNode transRewards[]; // transition rewards dds + protected JDDNode trans; // transition matrix dd + protected JDDNode trans01; // 0-1 transition matrix dd + protected JDDNode start; // start state dd + protected JDDNode reach; // reachable states dd + protected JDDNode deadlocks; // deadlock states dd + protected JDDNode fixdl; // fixed deadlock states dd + protected JDDNode stateRewards[]; // state rewards dds + protected JDDNode transRewards[]; // transition rewards dds // dd vars - private JDDVars[] varDDRowVars; // dd vars for each module variable (rows) - private JDDVars[] varDDColVars; // dd vars for each module variable (cols) - private JDDVars[] moduleDDRowVars; // dd vars for each module (rows) - private JDDVars[] moduleDDColVars; // dd vars for each module (cols) - private JDDVars allDDRowVars; // all dd vars (rows) - private JDDVars allDDColVars; // all dd vars (cols) + protected JDDVars[] varDDRowVars; // dd vars for each module variable (rows) + protected JDDVars[] varDDColVars; // dd vars for each module variable (cols) + protected JDDVars[] moduleDDRowVars; // dd vars for each module (rows) + protected JDDVars[] moduleDDColVars; // dd vars for each module (cols) + protected JDDVars allDDRowVars; // all dd vars (rows) + protected JDDVars allDDColVars; // all dd vars (cols) // names for all dd vars used - private Vector ddVarNames; + protected Vector ddVarNames; - private ODDNode odd; // odd + protected ODDNode odd; // odd // accessor methods - + // model info - + // type - public String getType() { return type; } + public int getType() + { + return Model.DTMC; + } + + public String getTypeString() + { + return "Probabilistic (DTMC)"; // TODO: Change this after regression testing + //return "DTMC"; + } + // modules - public int getNumModules() { return numModules; } - public String[] getModuleNames() { return moduleNames; } - public String getModuleName(int i) { return moduleNames[i]; } + public int getNumModules() + { + return numModules; + } + + public String[] getModuleNames() + { + return moduleNames; + } + + public String getModuleName(int i) + { + return moduleNames[i]; + } + // vars - public int getNumVars() { return numVars; } - public VarList getVarList() { return varList; } - public String getVarName(int i) { return varList.getName(i); } - public int getVarIndex(String n) { return varList.getIndex(n); } - public int getVarModule(int i) { return varList.getModule(i); } - public int getVarLow(int i) { return varList.getLow(i); } - public int getVarHigh(int i) { return varList.getHigh(i); } - public int getVarRange(int i) { return varList.getRange(i); } - public Values getConstantValues() { return constantValues; } + public int getNumVars() + { + return numVars; + } + + public VarList getVarList() + { + return varList; + } + + public String getVarName(int i) + { + return varList.getName(i); + } + + public int getVarIndex(String n) + { + return varList.getIndex(n); + } + + public int getVarModule(int i) + { + return varList.getModule(i); + } + + public int getVarLow(int i) + { + return varList.getLow(i); + } + + public int getVarHigh(int i) + { + return varList.getHigh(i); + } + + public int getVarRange(int i) + { + return varList.getRange(i); + } + + public Values getConstantValues() + { + return constantValues; + } + // rewards - public int getNumRewardStructs() { return numRewardStructs; } + public int getNumRewardStructs() + { + return numRewardStructs; + } + // stats - public long getNumStates() { return (numStates>Long.MAX_VALUE) ? -1 : Math.round(numStates); } - public long getNumTransitions() { return (numTransitions>Long.MAX_VALUE) ? -1 : Math.round(numTransitions); } - public long getNumStartStates() { return (numStartStates>Long.MAX_VALUE) ? -1 : Math.round(numStartStates); } + public long getNumStates() + { + return (numStates > Long.MAX_VALUE) ? -1 : Math.round(numStates); + } + + public long getNumTransitions() + { + return (numTransitions > Long.MAX_VALUE) ? -1 : Math.round(numTransitions); + } + + public long getNumStartStates() + { + return (numStartStates > Long.MAX_VALUE) ? -1 : Math.round(numStartStates); + } + // additional methods to get stats as strings - public String getNumStatesString() { return PrismUtils.bigIntToString(numStates); } - public String getNumTransitionsString() { return PrismUtils.bigIntToString(numTransitions); } - public String getNumStartStatesString() { return PrismUtils.bigIntToString(numStartStates); } + public String getNumStatesString() + { + return PrismUtils.bigIntToString(numStates); + } + + public String getNumTransitionsString() + { + return PrismUtils.bigIntToString(numTransitions); + } + + public String getNumStartStatesString() + { + return PrismUtils.bigIntToString(numStartStates); + } + // lists of states - public StateList getReachableStates() { return reachStateList; } - public StateList getDeadlockStates() { return deadlockStateList; } - public StateList getStartStates() { return startStateList; } - + public StateList getReachableStates() + { + return reachStateList; + } + + public StateList getDeadlockStates() + { + return deadlockStateList; + } + + public StateList getStartStates() + { + return startStateList; + } + // mtbdd stuff - - public JDDNode getTrans() { return trans; } - public JDDNode getTrans01() { return trans01; } - public JDDNode getStart() { return start; } - public JDDNode getReach() { return reach; } - public JDDNode getDeadlocks() { return deadlocks; } - public JDDNode getFixedDeadlocks() { return fixdl; } - public JDDNode getStateRewards() { return getStateRewards(0); } - public JDDNode getStateRewards(int i) { return (i>=0&&i=0&&i= 0 && i < numRewardStructs) ? stateRewards[i] : null; + } + + public JDDNode getStateRewards(String s) + { + for (int i = 0; i < numRewardStructs; i++) + if (rewardStructNames[i].equals(s)) + return stateRewards[i]; + return null; + } + + public JDDNode getTransRewards() + { + return getTransRewards(0); + } + + public JDDNode getTransRewards(int i) + { + return (i >= 0 && i < numRewardStructs) ? transRewards[i] : null; + } + + public JDDNode getTransRewards(String s) + { + for (int i = 0; i < numRewardStructs; i++) + if (rewardStructNames[i].equals(s)) + return transRewards[i]; + return null; + } + // dd vars - public JDDVars[] getVarDDRowVars() { return varDDRowVars; } - public JDDVars[] getVarDDColVars() { return varDDColVars; } - public JDDVars getVarDDRowVars(int i) { return varDDRowVars[i]; } - public JDDVars getVarDDColVars(int i) { return varDDColVars[i]; } - public JDDVars[] getModuleDDRowVars() { return moduleDDRowVars; } - public JDDVars[] getModuleDDColVars() { return moduleDDColVars; } - public JDDVars getModuleDDRowVars(int i) { return moduleDDRowVars[i]; } - public JDDVars getModuleDDColVars(int i) { return moduleDDColVars[i]; } - public JDDVars getAllDDRowVars() { return allDDRowVars; } - public JDDVars getAllDDColVars() { return allDDColVars; } + public JDDVars[] getVarDDRowVars() + { + return varDDRowVars; + } + + public JDDVars[] getVarDDColVars() + { + return varDDColVars; + } + + public JDDVars getVarDDRowVars(int i) + { + return varDDRowVars[i]; + } + + public JDDVars getVarDDColVars(int i) + { + return varDDColVars[i]; + } + + public JDDVars[] getModuleDDRowVars() + { + return moduleDDRowVars; + } + + public JDDVars[] getModuleDDColVars() + { + return moduleDDColVars; + } + + public JDDVars getModuleDDRowVars(int i) + { + return moduleDDRowVars[i]; + } + + public JDDVars getModuleDDColVars(int i) + { + return moduleDDColVars[i]; + } + + public JDDVars getAllDDRowVars() + { + return allDDRowVars; + } + + public JDDVars getAllDDColVars() + { + return allDDColVars; + } + // additional useful methods to do with dd vars - public int getNumDDRowVars() { return allDDRowVars.n(); } - public int getNumDDColVars() { return allDDColVars.n(); } - public int getNumDDVarsInTrans() { return allDDRowVars.n()*2; } - public Vector getDDVarNames() { return ddVarNames; } + public int getNumDDRowVars() + { + return allDDRowVars.n(); + } + + public int getNumDDColVars() + { + return allDDColVars.n(); + } + + public int getNumDDVarsInTrans() + { + return allDDRowVars.n() * 2; + } + + public Vector getDDVarNames() + { + return ddVarNames; + } + + public ODDNode getODD() + { + return odd; + } - public ODDNode getODD() { return odd; } + public String getTransName() + { + return "Transition matrix"; + } - // constructor + public String getTransSymbol() + { + return "P"; + } - public ProbModel(JDDNode tr, JDDNode tr01, JDDNode s, JDDNode r, JDDNode dl, JDDNode sr[], JDDNode trr[], String rsn[], JDDVars arv, JDDVars acv, Vector ddvn, - int nm, String[] mn, JDDVars[] mrv, JDDVars[] mcv, - int nv, VarList vl, JDDVars[] vrv, JDDVars[] vcv, Values cv) + // constructor + + public ProbModel(JDDNode tr, JDDNode tr01, JDDNode s, JDDNode r, JDDNode dl, JDDNode sr[], JDDNode trr[], + String rsn[], JDDVars arv, JDDVars acv, Vector ddvn, int nm, String[] mn, JDDVars[] mrv, JDDVars[] mcv, + int nv, VarList vl, JDDVars[] vrv, JDDVars[] vcv, Values cv) { int i; - + trans = tr; trans01 = tr01; start = s; @@ -187,40 +405,40 @@ public class ProbModel implements Model varDDRowVars = vrv; varDDColVars = vcv; constantValues = cv; - + // compute numbers for globalToLocal converter gtol = new long[numVars]; for (i = 0; i < numVars; i++) { gtol[i] = 1l << (varDDRowVars[i].getNumVars()); } - for (i = numVars-2; i >= 0; i--) { - gtol[i] = gtol[i] * gtol[i+1]; + for (i = numVars - 2; i >= 0; i--) { + gtol[i] = gtol[i] * gtol[i + 1]; } - + // work out number of states numStates = JDD.GetNumMinterms(reach, allDDRowVars.n()); numStartStates = JDD.GetNumMinterms(start, allDDRowVars.n()); - + // work out number of transitions - numTransitions = JDD.GetNumMinterms(trans01, allDDRowVars.n()*2); - + numTransitions = JDD.GetNumMinterms(trans01, getNumDDVarsInTrans()); + // build odd odd = ODDUtils.BuildODD(reach, allDDRowVars); - + // store reachable states in a StateList reachStateList = new StateListMTBDD(reach, this); - + // store deadlock states in a StateList deadlockStateList = new StateListMTBDD(deadlocks, this); - + // store initial states in a StateList startStateList = new StateListMTBDD(start, this); } - + public void fixDeadlocks() { JDDNode tmp; - + if (!deadlocks.equals(JDD.ZERO)) { // remove deadlocks by adding self-loops JDD.Ref(deadlocks); @@ -234,165 +452,175 @@ public class ProbModel implements Model deadlocks = JDD.Constant(0); deadlockStateList = new StateListMTBDD(deadlocks, this); // update model stats - numTransitions = JDD.GetNumMinterms(trans01, getNumDDVarsInTrans()); + numTransitions = JDD.GetNumMinterms(trans01, getNumDDVarsInTrans()); } } public void printTrans() { -// JDD.PrintMatrix(trans, allDDRowVars, allDDColVars); + // JDD.PrintMatrix(trans, allDDRowVars, allDDColVars); } - + public void printTrans01() { -// JDD.PrintMatrix(trans01, allDDRowVars, allDDColVars, JDD.ZERO_ONE); + // JDD.PrintMatrix(trans01, allDDRowVars, allDDColVars, JDD.ZERO_ONE); } - - public void printTransInfo(PrismLog log) { printTransInfo(log, false); } + + public void printTransInfo(PrismLog log) + { + printTransInfo(log, false); + } + public void printTransInfo(PrismLog log, boolean extra) { int i, j, n; - + log.print("States: " + getNumStatesString() + " (" + getNumStartStatesString() + " initial)" + "\n"); log.print("Transitions: " + getNumTransitionsString() + "\n"); - + log.println(); - - log.print("Transition matrix: "); - log.print(JDD.GetNumNodes(trans) + " nodes ("); - log.print(JDD.GetNumTerminals(trans) + " terminal), "); - log.print(JDD.GetNumMintermsString(trans, getNumDDVarsInTrans()) + " minterms, "); - log.print("vars: " + getNumDDRowVars() + "r/" + getNumDDColVars() + "c\n"); + + log.print(getTransName() + ": " + JDD.GetInfoString(trans, getNumDDVarsInTrans())); + log.print(", vars: " + getNumDDRowVars() + "r/" + getNumDDColVars() + "c\n"); if (extra) { log.print("DD vars (r/c):"); n = allDDRowVars.getNumVars(); for (i = 0; i < n; i++) { j = allDDRowVars.getVarIndex(i); - log.print(" "+j+":"+ddVarNames.get(j)); + log.print(" " + j + ":" + ddVarNames.get(j)); j = allDDColVars.getVarIndex(i); - log.print(" "+j+":"+ddVarNames.get(j)); + log.print(" " + j + ":" + ddVarNames.get(j)); } log.println(); - log.print("Transition matrix terminals: " + JDD.GetTerminalsAndNumbersString(trans, getNumDDVarsInTrans())+"\n"); + log.print(getTransName() + " terminals: " + JDD.GetTerminalsAndNumbersString(trans, getNumDDVarsInTrans()) + + "\n"); log.print("Reach: " + JDD.GetNumNodes(reach) + " nodes\n"); log.print("ODD: " + ODDUtils.GetNumODDNodes() + " nodes\n"); } for (i = 0; i < numRewardStructs; i++) { if (stateRewards[i] != null && !stateRewards[i].equals(JDD.ZERO)) { - log.print("State rewards ("+(i+1)+(("".equals(rewardStructNames[i]))?"":(":\""+rewardStructNames[i]+"\""))+"): "); + log.print("State rewards (" + (i + 1) + + (("".equals(rewardStructNames[i])) ? "" : (":\"" + rewardStructNames[i] + "\"")) + "): "); log.print(JDD.GetNumNodes(stateRewards[i]) + " nodes ("); log.print(JDD.GetNumTerminals(stateRewards[i]) + " terminal), "); log.print(JDD.GetNumMintermsString(stateRewards[i], getNumDDRowVars()) + " minterms\n"); if (extra) { - log.print("State rewards terminals ("+(i+1)+(("".equals(rewardStructNames[i]))?"":(":\""+rewardStructNames[i]+"\""))+"): "); - log.print(JDD.GetTerminalsAndNumbersString(stateRewards[i], getNumDDRowVars())+"\n"); + log.print("State rewards terminals (" + (i + 1) + + (("".equals(rewardStructNames[i])) ? "" : (":\"" + rewardStructNames[i] + "\"")) + "): "); + log.print(JDD.GetTerminalsAndNumbersString(stateRewards[i], getNumDDRowVars()) + "\n"); } } if (transRewards[i] != null && !transRewards[i].equals(JDD.ZERO)) { - log.print("Transition rewards ("+(i+1)+(("".equals(rewardStructNames[i]))?"":(":\""+rewardStructNames[i]+"\""))+"): "); + log.print("Transition rewards (" + (i + 1) + + (("".equals(rewardStructNames[i])) ? "" : (":\"" + rewardStructNames[i] + "\"")) + "): "); log.print(JDD.GetNumNodes(transRewards[i]) + " nodes ("); log.print(JDD.GetNumTerminals(transRewards[i]) + " terminal), "); log.print(JDD.GetNumMintermsString(transRewards[i], getNumDDVarsInTrans()) + " minterms\n"); if (extra) { - log.print("Transition rewards terminals ("+(i+1)+(("".equals(rewardStructNames[i]))?"":(":\""+rewardStructNames[i]+"\""))+"): "); - log.print(JDD.GetTerminalsAndNumbersString(transRewards[i], getNumDDVarsInTrans())+"\n"); + log.print("Transition rewards terminals (" + (i + 1) + + (("".equals(rewardStructNames[i])) ? "" : (":\"" + rewardStructNames[i] + "\"")) + "): "); + log.print(JDD.GetTerminalsAndNumbersString(transRewards[i], getNumDDVarsInTrans()) + "\n"); } } } } // export transition matrix to a file - + public void exportToFile(int exportType, boolean explicit, File file) throws FileNotFoundException { if (!explicit) { - PrismMTBDD.ExportMatrix(trans, "P", allDDRowVars, allDDColVars, odd, exportType, (file != null)?file.getPath():null); - } - else { - PrismSparse.ExportMatrix(trans, "P", allDDRowVars, allDDColVars, odd, exportType, (file != null)?file.getPath():null); + PrismMTBDD.ExportMatrix(trans, getTransSymbol(), allDDRowVars, allDDColVars, odd, exportType, (file != null) ? file + .getPath() : null); + } else { + PrismSparse.ExportMatrix(trans, getTransSymbol(), allDDRowVars, allDDColVars, odd, exportType, (file != null) ? file + .getPath() : null); } } // export state rewards vector to a file - + // returns string containing files used if there were more than 1, null otherwise - + public String exportStateRewardsToFile(int exportType, File file) throws FileNotFoundException, PrismException { - if (numRewardStructs == 0) throw new PrismException("There are no state rewards to export"); + if (numRewardStructs == 0) + throw new PrismException("There are no state rewards to export"); int i; String filename, allFilenames = ""; for (i = 0; i < numRewardStructs; i++) { filename = (file != null) ? file.getPath() : null; if (filename != null && numRewardStructs > 1) { filename = PrismUtils.addCounterSuffixToFilename(filename, i); - allFilenames += ((i>0)?", ":"") + filename; + allFilenames += ((i > 0) ? ", " : "") + filename; } - PrismMTBDD.ExportVector(stateRewards[i], "c"+i, allDDRowVars, odd, exportType, filename); + PrismMTBDD.ExportVector(stateRewards[i], "c" + i, allDDRowVars, odd, exportType, filename); } - return (allFilenames.length()>0) ? allFilenames : null; + return (allFilenames.length() > 0) ? allFilenames : null; } // export transition rewards matrix to a file - + // returns string containing files used if there were more than 1, null otherwise - - public String exportTransRewardsToFile(int exportType, boolean explicit, File file) throws FileNotFoundException, PrismException + + public String exportTransRewardsToFile(int exportType, boolean explicit, File file) throws FileNotFoundException, + PrismException { - if (numRewardStructs == 0) throw new PrismException("There are no transition rewards to export"); + if (numRewardStructs == 0) + throw new PrismException("There are no transition rewards to export"); int i; String filename, allFilenames = ""; for (i = 0; i < numRewardStructs; i++) { filename = (file != null) ? file.getPath() : null; if (filename != null && numRewardStructs > 1) { filename = PrismUtils.addCounterSuffixToFilename(filename, i); - allFilenames += ((i>0)?", ":"") + filename; + allFilenames += ((i > 0) ? ", " : "") + filename; } if (!explicit) { - PrismMTBDD.ExportMatrix(transRewards[i], "C"+i, allDDRowVars, allDDColVars, odd, exportType, filename); - } - else { - PrismSparse.ExportMatrix(transRewards[i], "C"+i, allDDRowVars, allDDColVars, odd, exportType, filename); + PrismMTBDD + .ExportMatrix(transRewards[i], "C" + i, allDDRowVars, allDDColVars, odd, exportType, filename); + } else { + PrismSparse.ExportMatrix(transRewards[i], "C" + i, allDDRowVars, allDDColVars, odd, exportType, + filename); } } - return (allFilenames.length()>0) ? allFilenames : null; + return (allFilenames.length() > 0) ? allFilenames : null; } // convert global state index to local indices - + public String globalToLocal(long x) { int i; String s = ""; - + s += "("; - for (i = 0; i < numVars-1; i++) { - s += ((x/gtol[i+1]) + varList.getLow(i)) + ","; - x = x % gtol[i+1]; + for (i = 0; i < numVars - 1; i++) { + s += ((x / gtol[i + 1]) + varList.getLow(i)) + ","; + x = x % gtol[i + 1]; } - s += (x + varList.getLow(numVars-1)) + ")"; - + s += (x + varList.getLow(numVars - 1)) + ")"; + return s; } - + // convert global state index to local index - + public int globalToLocal(long x, int l) { int i; - - for (i = 0; i < numVars-1; i++) { + + for (i = 0; i < numVars - 1; i++) { if (i == l) { - return (int)((x/gtol[i+1]) + varList.getLow(i)); - } - else { - x = x % gtol[i+1]; + return (int) ((x / gtol[i + 1]) + varList.getLow(i)); + } else { + x = x % gtol[i + 1]; } } - - return (int)(x + varList.getLow(numVars-1)); + + return (int) (x + varList.getLow(numVars - 1)); } - + // clear up (deref all dds, dd vars) public void clear() diff --git a/prism/src/prism/StochModel.java b/prism/src/prism/StochModel.java index 4c70716e..3899c7c9 100644 --- a/prism/src/prism/StochModel.java +++ b/prism/src/prism/StochModel.java @@ -26,396 +26,45 @@ package prism; -import java.io.*; import java.util.Vector; import jdd.*; -import odd.*; -import mtbdd.*; import parser.*; -import sparse.*; -// class to store an instance of a stochastic model (ctmc) - -public class StochModel implements Model +/* + * Class to store a PRISM model which is a CTMC + */ +public class StochModel extends ProbModel { - // model info - - // type - private static final String type = "Stochastic (CTMC)"; - // modules - private int numModules; // number of modules - private String[] moduleNames; // module names - // vars/consts - private int numVars; // total number of module variables - private VarList varList; // list of module variables - private long[] gtol; // numbers for use by globalToLocal - private Values constantValues; // values of constants - // rewards - private int numRewardStructs; // number of reward structs - private String[] rewardStructNames; // reward struct names - // stats - private double numStates; // number of states - private double numTransitions; // number of transitions - private double numStartStates; // number of initial states - // reachable state list - private StateListMTBDD reachStateList = null; - // deadlock state list - private StateListMTBDD deadlockStateList = null; - // initial state list - private StateListMTBDD startStateList = null; - - // mtbdd stuff - - // dds - private JDDNode trans; // transition rate matrix dd - private JDDNode trans01; // 0-1 transition matrix dd - private JDDNode start; // start state dd - private JDDNode reach; // reachable states dd - private JDDNode deadlocks; // deadlock states dd - private JDDNode fixdl; // fixed deadlock states dd - private JDDNode stateRewards[]; // state rewards dds - private JDDNode transRewards[]; // transition rewards dds - // dd vars - private JDDVars[] varDDRowVars; // dd vars for each module variable (rows) - private JDDVars[] varDDColVars; // dd vars for each module variable (cols) - private JDDVars[] moduleDDRowVars; // dd vars for each module (rows) - private JDDVars[] moduleDDColVars; // dd vars for each module (cols) - private JDDVars allDDRowVars; // all dd vars (rows) - private JDDVars allDDColVars; // all dd vars (cols) - // names for all dd vars used - private Vector ddVarNames; - - private ODDNode odd; // odd - // accessor methods - - // model info - - // type - public String getType() { return type; } - // modules - public int getNumModules() { return numModules; } - public String[] getModuleNames() { return moduleNames; } - public String getModuleName(int i) { return moduleNames[i]; } - // vars - public int getNumVars() { return numVars; } - public VarList getVarList() { return varList; } - public String getVarName(int i) { return varList.getName(i); } - public int getVarIndex(String n) { return varList.getIndex(n); } - public int getVarModule(int i) { return varList.getModule(i); } - public int getVarLow(int i) { return varList.getLow(i); } - public int getVarHigh(int i) { return varList.getHigh(i); } - public int getVarRange(int i) { return varList.getRange(i); } - public Values getConstantValues() { return constantValues; } - // rewards - public int getNumRewardStructs() { return numRewardStructs; } - // stats - public long getNumStates() { return (numStates>Long.MAX_VALUE) ? -1 : Math.round(numStates); } - public long getNumTransitions() { return (numTransitions>Long.MAX_VALUE) ? -1 : Math.round(numTransitions); } - public long getNumStartStates() { return (numStartStates>Long.MAX_VALUE) ? -1 : Math.round(numStartStates); } - // additional methods to get stats as strings - public String getNumStatesString() { return PrismUtils.bigIntToString(numStates); } - public String getNumTransitionsString() { return PrismUtils.bigIntToString(numTransitions); } - public String getNumStartStatesString() { return PrismUtils.bigIntToString(numStartStates); } - // lists of states - public StateList getReachableStates() { return reachStateList; } - public StateList getDeadlockStates() { return deadlockStateList; } - public StateList getStartStates() { return startStateList; } - - // mtbdd stuff - - public JDDNode getTrans() { return trans; } - public JDDNode getTrans01() { return trans01; } - public JDDNode getStart() { return start; } - public JDDNode getReach() { return reach; } - public JDDNode getDeadlocks() { return deadlocks; } - public JDDNode getFixedDeadlocks() { return fixdl; } - public JDDNode getStateRewards() { return getStateRewards(0); } - public JDDNode getStateRewards(int i) { return (i>=0&&i=0&&i= 0; i--) { - gtol[i] = gtol[i] * gtol[i+1]; - } - - // work out number of states - numStates = JDD.GetNumMinterms(reach, allDDRowVars.n()); - numStartStates = JDD.GetNumMinterms(start, allDDRowVars.n()); - - // work out number of transitions - numTransitions = JDD.GetNumMinterms(trans01, allDDRowVars.n()*2); - - // build odd - odd = ODDUtils.BuildODD(reach, allDDRowVars); - - // store reachable states in a StateList - reachStateList = new StateListMTBDD(reach, this); - - // store deadlock states in a StateList - deadlockStateList = new StateListMTBDD(deadlocks, this); - - // store initial states in a StateList - startStateList = new StateListMTBDD(start, this); - } - - public void fixDeadlocks() - { - JDDNode tmp; - - if (!deadlocks.equals(JDD.ZERO)) { - // remove deadlocks by adding self-loops - JDD.Ref(deadlocks); - tmp = JDD.And(deadlocks, JDD.Identity(allDDRowVars, allDDColVars)); - JDD.Ref(tmp); - trans = JDD.Apply(JDD.PLUS, trans, tmp); - trans01 = JDD.Apply(JDD.PLUS, trans01, tmp); - // update lists of deadlocks - JDD.Deref(fixdl); - fixdl = deadlocks; - deadlocks = JDD.Constant(0); - deadlockStateList = new StateListMTBDD(deadlocks, this); - // update model stats - numTransitions = JDD.GetNumMinterms(trans01, getNumDDVarsInTrans()); - } - } - public void printTrans() + public int getType() { -// JDD.PrintMatrix(trans, allDDRowVars, allDDColVars); - } - - public void printTrans01() - { -// JDD.PrintMatrix(trans01, allDDRowVars, allDDColVars, JDD.ZERO_ONE); - } - - public void printTransInfo(PrismLog log) { printTransInfo(log, false); } - public void printTransInfo(PrismLog log, boolean extra) - { - int i, j, n; - - log.print("States: " + getNumStatesString() + " (" + getNumStartStatesString() + " initial)" + "\n"); - log.print("Transitions: " + getNumTransitionsString() + "\n"); - - log.println(); - - log.print("Rate matrix: "); - log.print(JDD.GetNumNodes(trans) + " nodes ("); - log.print(JDD.GetNumTerminals(trans) + " terminal), "); - log.print(JDD.GetNumMintermsString(trans, getNumDDVarsInTrans()) + " minterms, "); - log.print("vars: " + getNumDDRowVars() + "r/" + getNumDDColVars() + "c\n"); - if (extra) { - log.print("DD vars (r/c):"); - n = allDDRowVars.getNumVars(); - for (i = 0; i < n; i++) { - j = allDDRowVars.getVarIndex(i); - log.print(" "+j+":"+ddVarNames.get(j)); - j = allDDColVars.getVarIndex(i); - log.print(" "+j+":"+ddVarNames.get(j)); - } - log.println(); - log.print("Rate matrix terminals: " + JDD.GetTerminalsAndNumbersString(trans, getNumDDVarsInTrans())+"\n"); - log.print("Reach: " + JDD.GetNumNodes(reach) + " nodes\n"); - log.print("ODD: " + ODDUtils.GetNumODDNodes() + " nodes\n"); - } - - for (i = 0; i < numRewardStructs; i++) { - if (stateRewards[i] != null && !stateRewards[i].equals(JDD.ZERO)) { - log.print("State rewards ("+(i+1)+(("".equals(rewardStructNames[i]))?"":(":\""+rewardStructNames[i]+"\""))+"): "); - log.print(JDD.GetNumNodes(stateRewards[i]) + " nodes ("); - log.print(JDD.GetNumTerminals(stateRewards[i]) + " terminal), "); - log.print(JDD.GetNumMintermsString(stateRewards[i], getNumDDRowVars()) + " minterms\n"); - if (extra) { - log.print("State rewards terminals ("+(i+1)+(("".equals(rewardStructNames[i]))?"":(":\""+rewardStructNames[i]+"\""))+"): "); - log.print(JDD.GetTerminalsAndNumbersString(stateRewards[i], getNumDDRowVars())+"\n"); - } - } - if (transRewards[i] != null && !transRewards[i].equals(JDD.ZERO)) { - log.print("Transition rewards ("+(i+1)+(("".equals(rewardStructNames[i]))?"":(":\""+rewardStructNames[i]+"\""))+"): "); - log.print(JDD.GetNumNodes(transRewards[i]) + " nodes ("); - log.print(JDD.GetNumTerminals(transRewards[i]) + " terminal), "); - log.print(JDD.GetNumMintermsString(transRewards[i], getNumDDVarsInTrans()) + " minterms\n"); - if (extra) { - log.print("Transition rewards terminals ("+(i+1)+(("".equals(rewardStructNames[i]))?"":(":\""+rewardStructNames[i]+"\""))+"): "); - log.print(JDD.GetTerminalsAndNumbersString(transRewards[i], getNumDDVarsInTrans())+"\n"); - } - } - } - } - - // export transition matrix to a file - - public void exportToFile(int exportType, boolean explicit, File file) throws FileNotFoundException - { - if (!explicit) { - PrismMTBDD.ExportMatrix(trans, "R", allDDRowVars, allDDColVars, odd, exportType, (file != null)?file.getPath():null); - } - else { - PrismSparse.ExportMatrix(trans, "R", allDDRowVars, allDDColVars, odd, exportType, (file != null)?file.getPath():null); - } + return Model.CTMC; } - // export state rewards vector to a file - - // returns string containing files used if there were more than 1, null otherwise - - public String exportStateRewardsToFile(int exportType, File file) throws FileNotFoundException, PrismException - { - if (numRewardStructs == 0) throw new PrismException("There are no state rewards to export"); - int i; - String filename, allFilenames = ""; - for (i = 0; i < numRewardStructs; i++) { - filename = (file != null) ? file.getPath() : null; - if (filename != null && numRewardStructs > 1) { - filename = PrismUtils.addCounterSuffixToFilename(filename, i); - allFilenames += ((i>0)?", ":"") + filename; - } - PrismMTBDD.ExportVector(stateRewards[i], "c"+i, allDDRowVars, odd, exportType, filename); - } - return (allFilenames.length()>0) ? allFilenames : null; - } - - // export transition rewards matrix to a file - - // returns string containing files used if there were more than 1, null otherwise - - public String exportTransRewardsToFile(int exportType, boolean explicit, File file) throws FileNotFoundException, PrismException + public String getTypeString() { - if (numRewardStructs == 0) throw new PrismException("There are no transition rewards to export"); - int i; - String filename, allFilenames = ""; - for (i = 0; i < numRewardStructs; i++) { - filename = (file != null) ? file.getPath() : null; - if (filename != null && numRewardStructs > 1) { - filename = PrismUtils.addCounterSuffixToFilename(filename, i); - allFilenames += ((i>0)?", ":"") + filename; - } - if (!explicit) { - PrismMTBDD.ExportMatrix(transRewards[i], "C"+i, allDDRowVars, allDDColVars, odd, exportType, filename); - } - else { - PrismSparse.ExportMatrix(transRewards[i], "C"+i, allDDRowVars, allDDColVars, odd, exportType, filename); - } - } - return (allFilenames.length()>0) ? allFilenames : null; + return "Stochastic (CTMC)"; // TODO: Change this after regression testing + //return "CTMC"; } - // convert global state index to local indices - - public String globalToLocal(long x) + public String getTransName() { - int i; - String s = ""; - - s += "("; - for (i = 0; i < numVars-1; i++) { - s += ((x/gtol[i+1]) + varList.getLow(i)) + ","; - x = x % gtol[i+1]; - } - s += (x + varList.getLow(numVars-1)) + ")"; - - return s; + return "Rate matrix"; } - // convert global state index to local index - - public int globalToLocal(long x, int l) + public String getTransSymbol() { - int i; - - for (i = 0; i < numVars-1; i++) { - if (i == l) { - return (int)((x/gtol[i+1]) + varList.getLow(i)); - } - else { - x = x % gtol[i+1]; - } - } - - return (int)(x + varList.getLow(numVars-1)); + return "R"; } - // clear up (deref all dds, dd vars) + // constructor - public void clear() + public StochModel(JDDNode tr, JDDNode tr01, JDDNode s, JDDNode r, JDDNode dl, JDDNode sr[], JDDNode trr[], + String rsn[], JDDVars arv, JDDVars acv, Vector ddvn, int nm, String[] mn, JDDVars[] mrv, JDDVars[] mcv, + int nv, VarList vl, JDDVars[] vrv, JDDVars[] vcv, Values cv) { - for (int i = 0; i < numVars; i++) { - varDDRowVars[i].derefAll(); - varDDColVars[i].derefAll(); - } - for (int i = 0; i < numModules; i++) { - moduleDDRowVars[i].derefAll(); - moduleDDColVars[i].derefAll(); - } - allDDRowVars.derefAll(); - allDDColVars.derefAll(); - JDD.Deref(trans); - JDD.Deref(trans01); - JDD.Deref(start); - JDD.Deref(reach); - JDD.Deref(deadlocks); - JDD.Deref(fixdl); - for (int i = 0; i < numRewardStructs; i++) { - JDD.Deref(stateRewards[i]); - JDD.Deref(transRewards[i]); - } + super(tr, tr01, s, r, dl, sr, trr, rsn, arv, acv, ddvn, nm, mn, mrv, mcv, nv, vl, vrv, vcv, cv); } }