diff --git a/prism/src/prism/NondetModel.java b/prism/src/prism/NondetModel.java index c60687d5..36470411 100644 --- a/prism/src/prism/NondetModel.java +++ b/prism/src/prism/NondetModel.java @@ -35,222 +35,121 @@ import mtbdd.*; import parser.*; import sparse.*; -// class to store an instance of a concurrent probabilistic model (mtbdds) - -public class NondetModel implements Model +/* + * Class to store a PRISM model which is an MDP + */ +public class NondetModel extends ProbModel { - // model info - - // type - private static final String type = "Nondeterministic (MDP)"; - // 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 numChoices; // number of choices - 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 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 nondetMask; // mask for nondeterministic choices - 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) - private JDDVars allDDSynchVars; // synch actions dd vars - private JDDVars allDDSchedVars; // scheduler dd vars - private JDDVars allDDChoiceVars; // local nondet choice dd vars - private JDDVars allDDNondetVars; // all nondet dd vars (union of two above) - // names for all dd vars used - private Vector ddVarNames; - - private ODDNode odd; // odd + // Extra stats + protected double numChoices; // number of choices + + // Extra dd stuff + protected JDDNode nondetMask; // mask for nondeterministic choices + protected JDDVars allDDSynchVars; // synch actions dd vars + protected JDDVars allDDSchedVars; // scheduler dd vars + protected JDDVars allDDChoiceVars; // local nondet choice dd vars + protected JDDVars allDDNondetVars; // all nondet dd vars (union of two above) // 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 getNumChoices() { return (numChoices>Long.MAX_VALUE) ? -1 : Math.round(numChoices); } - 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 getNumChoicesString() { return PrismUtils.bigIntToString(numChoices); } - 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 - - // dds - 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 getNondetMask() { return nondetMask; } - public JDDNode getStateRewards() { return getStateRewards(0); } - public JDDNode getStateRewards(int i) { return (i>=0&&i=0&&i Long.MAX_VALUE) ? -1 : Math.round(numChoices); + } + + public String getNumChoicesString() + { + return PrismUtils.bigIntToString(numChoices); + } + + public JDDNode getNondetMask() + { + return nondetMask; + } + + public JDDVars getAllDDSynchVars() + { + return allDDSynchVars; + } + + public JDDVars getAllDDSchedVars() + { + return allDDSchedVars; + } + + public JDDVars getAllDDChoiceVars() + { + return allDDChoiceVars; + } + + public JDDVars getAllDDNondetVars() + { + return allDDNondetVars; + } + // additional useful methods to do with dd vars - public int getNumDDRowVars() { return allDDRowVars.n(); } - public int getNumDDColVars() { return allDDColVars.n(); } - public int getNumDDNondetVars() { return allDDNondetVars.n(); } - public int getNumDDVarsInTrans() { return allDDRowVars.n()*2+allDDNondetVars.n(); } - public Vector getDDVarNames() { return ddVarNames; } + public int getNumDDNondetVars() + { + return allDDNondetVars.n(); + } + + public int getNumDDVarsInTrans() + { + return allDDRowVars.n() * 2 + allDDNondetVars.n(); + } + + public String getTransName() + { + return "Transition matrix"; + } - public ODDNode getODD() { return odd; } + public String getTransSymbol() + { + return "S"; + } // constructor - - public NondetModel(JDDNode tr, JDDNode tr01, JDDNode s, JDDNode r, JDDNode dl, JDDNode sr[], JDDNode trr[], String rsn[], JDDVars arv, JDDVars acv, - JDDVars asyv, JDDVars asv, JDDVars achv, JDDVars andv, Vector ddvn, - int nm, String[] mn, JDDVars[] mrv, JDDVars[] mcv, - int nv, VarList vl, JDDVars[] vrv, JDDVars[] vcv, Values cv) + + public NondetModel(JDDNode tr, JDDNode tr01, JDDNode s, JDDNode r, JDDNode dl, JDDNode sr[], JDDNode trr[], + String rsn[], JDDVars arv, JDDVars acv, JDDVars asyv, JDDVars asv, JDDVars achv, JDDVars andv, Vector ddvn, + int nm, String[] mn, JDDVars[] mrv, JDDVars[] mcv, int nv, VarList vl, JDDVars[] vrv, JDDVars[] vcv, + Values cv) { - int i; - double d; + super(tr, tr01, s, r, dl, sr, trr, rsn, arv, acv, ddvn, nm, mn, mrv, mcv, nv, vl, vrv, vcv, cv); - trans = tr; - trans01 = tr01; - start = s; - reach = r; - deadlocks = dl; - fixdl = JDD.Constant(0); - stateRewards = sr; - transRewards = trr; - numRewardStructs = stateRewards.length; // which should == transRewards.length - rewardStructNames = rsn; - allDDRowVars = arv; - allDDColVars = acv; allDDSynchVars = asyv; allDDSchedVars = asv; allDDChoiceVars = achv; allDDNondetVars = andv; - ddVarNames = ddvn; - numModules = nm; - moduleNames = mn; - moduleDDRowVars = mrv; - moduleDDColVars = mcv; - numVars = nv; - varList = vl; - 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]; - } - + // build mask for nondeterminstic choices JDD.Ref(trans01); JDD.Ref(reach); // nb: this assumes that there are no deadlock states nondetMask = JDD.And(JDD.Not(JDD.ThereExists(trans01, allDDColVars)), reach); - - // 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+allDDNondetVars.n()); - + // work out number of choices - d = JDD.GetNumMinterms(nondetMask, getNumDDRowVars()+getNumDDNondetVars()); + double d = JDD.GetNumMinterms(nondetMask, getNumDDRowVars() + getNumDDNondetVars()); numChoices = ((Math.pow(2, getNumDDNondetVars())) * numStates) - d; - - // 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; double d; - + if (!deadlocks.equals(JDD.ZERO)) { // remove deadlocks by adding self-loops JDD.Ref(deadlocks); @@ -271,207 +170,147 @@ public class NondetModel implements Model JDD.Ref(reach); nondetMask = JDD.And(JDD.Not(JDD.ThereExists(trans01, allDDColVars)), reach); // update model stats - numTransitions = JDD.GetNumMinterms(trans01, getNumDDVarsInTrans()); - d = JDD.GetNumMinterms(nondetMask, getNumDDRowVars()+getNumDDNondetVars()); + numTransitions = JDD.GetNumMinterms(trans01, getNumDDVarsInTrans()); + d = JDD.GetNumMinterms(nondetMask, getNumDDRowVars() + getNumDDNondetVars()); numChoices = ((Math.pow(2, getNumDDNondetVars())) * numStates) - d; } } - public void printTrans() - { -// 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.print("Choices: " + getNumChoicesString() + "\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/" + getNumDDNondetVars() + "nd\n"); + + log.print(getTransName() + ": " + JDD.GetInfoString(trans, getNumDDVarsInTrans())); + log.print(", vars: " + getNumDDRowVars() + "r/" + getNumDDColVars() + "c/" + getNumDDNondetVars() + "nd\n"); if (extra) { log.print("DD vars (nd):"); n = allDDNondetVars.getNumVars(); for (i = 0; i < n; i++) { j = allDDNondetVars.getVarIndex(i); - log.print(" "+j+":"+ddVarNames.get(j)); + log.print(" " + j + ":" + ddVarNames.get(j)); } log.println(); 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"); log.print("Mask: " + JDD.GetNumNodes(nondetMask) + " nodes, "); - log.print(JDD.GetNumMintermsString(nondetMask, getNumDDRowVars()+getNumDDNondetVars()) + " minterms\n"); + log.print(JDD.GetNumMintermsString(nondetMask, getNumDDRowVars() + getNumDDNondetVars()) + " minterms\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) { // can only do explicit (sparse matrix based) export for mdps - } - else { - PrismSparse.ExportMDP(trans, "S", allDDRowVars, allDDColVars, allDDNondetVars, odd, exportType, (file != null)?file.getPath():null); + } else { + PrismSparse.ExportMDP(trans, getTransSymbol(), allDDRowVars, allDDColVars, allDDNondetVars, 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) { // can only do explicit (sparse matrix based) export for mdps + } else { + PrismSparse.ExportSubMDP(trans, transRewards[i], "C" + i, allDDRowVars, allDDColVars, allDDNondetVars, + odd, exportType, filename); } - else { - PrismSparse.ExportSubMDP(trans, transRewards[i], "C"+i, allDDRowVars, allDDColVars, allDDNondetVars, odd, exportType, filename); - } - } - 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]; } - s += (x + varList.getLow(numVars-1)) + ")"; - - return s; + return (allFilenames.length() > 0) ? allFilenames : null; } - // convert global state index to local index - - public int globalToLocal(long x, int l) - { - 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)); - } - // clear up (deref all dds, dd vars) public void clear() { - 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(); + super.clear(); allDDSynchVars.derefAll(); allDDSchedVars.derefAll(); allDDChoiceVars.derefAll(); allDDNondetVars.derefAll(); - JDD.Deref(trans); - JDD.Deref(trans01); - JDD.Deref(start); - JDD.Deref(reach); - JDD.Deref(deadlocks); - JDD.Deref(fixdl); JDD.Deref(nondetMask); - for (int i = 0; i < numRewardStructs; i++) { - JDD.Deref(stateRewards[i]); - JDD.Deref(transRewards[i]); - } } } diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index e63dff16..6921f114 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -3,7 +3,6 @@ // Copyright (c) 2002- // Authors: // * Dave Parker (University of Oxford, formerly University of Birmingham) -// * Carlos S. Bederián (Universidad Nacional de Córdoba) // //------------------------------------------------------------------------------ // @@ -27,19 +26,12 @@ 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 @@ -181,7 +173,7 @@ public class NondetModelChecker extends StateModelChecker // Compute probabilities boolean qual = pb != null && ((p == 0) || (p == 1)) && precomp; - probs = checkProbPathFormula(expr.getExpression(), qual, min); + probs = checkProbPathExpression(expr.getExpression(), qual, min); // Print out probabilities if (verbose) { @@ -310,22 +302,20 @@ public class NondetModelChecker extends StateModelChecker } } - // Contents of a P operator, i.e. a path formula + // Contents of a P operator - protected StateProbs checkProbPathFormula(Expression expr, boolean qual, boolean min) throws PrismException + protected StateProbs checkProbPathExpression(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 checkProbPathFormulaSimple(expr, qual, min); + return checkProbPathExpressionSimple(expr, qual, min); } else { - return checkProbPathFormulaLTL(expr, qual, min); + throw new PrismException("LTL-style path formulas are not supported"); } } - // Simple path formula for P operator (one temporal op, possibly negated) - - protected StateProbs checkProbPathFormulaSimple(Expression expr, boolean qual, boolean min) + protected StateProbs checkProbPathExpressionSimple(Expression expr, boolean qual, boolean min) throws PrismException { StateProbs probs = null; @@ -336,12 +326,12 @@ public class NondetModelChecker extends StateModelChecker // Parentheses if (exprUnary.getOperator() == ExpressionUnaryOp.PARENTH) { // Recurse - probs = checkProbPathFormulaSimple(exprUnary.getOperand(), qual, min); + probs = checkProbPathExpressionSimple(exprUnary.getOperand(), qual, min); } // Negation else if (exprUnary.getOperator() == ExpressionUnaryOp.NOT) { // Flip min/max, then subtract from 1 - probs = checkProbPathFormulaSimple(exprUnary.getOperand(), qual, !min); + probs = checkProbPathExpressionSimple(exprUnary.getOperand(), qual, !min); probs.subtractFromOne(); } } @@ -362,7 +352,7 @@ public class NondetModelChecker extends StateModelChecker } // Anything else - convert to until and recurse else { - probs = checkProbPathFormulaSimple(exprTemp.convertToUntilForm(), qual, min); + probs = checkProbPathExpressionSimple(exprTemp.convertToUntilForm(), qual, min); } } @@ -372,143 +362,6 @@ 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 @@ -516,6 +369,10 @@ 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()); @@ -540,6 +397,12 @@ 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) { @@ -593,6 +456,12 @@ 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 {