From 701ad333505764a6b4401f1283ceaed3d5f6d5c2 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 11 Apr 2008 18:10:29 +0000 Subject: [PATCH] Moved reachability/deadlocks/etc. into Model classes. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@746 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/Explicit2MTBDD.java | 216 +++++----------------------- prism/src/prism/Model.java | 5 + prism/src/prism/Modules2MTBDD.java | 173 ++++------------------ prism/src/prism/NondetModel.java | 73 ++++++++-- prism/src/prism/Prism.java | 3 +- prism/src/prism/PrismCL.java | 2 +- prism/src/prism/ProbModel.java | 125 +++++++++++++--- prism/src/prism/StochModel.java | 14 +- 8 files changed, 245 insertions(+), 366 deletions(-) diff --git a/prism/src/prism/Explicit2MTBDD.java b/prism/src/prism/Explicit2MTBDD.java index e52fc066..d96b7aee 100644 --- a/prism/src/prism/Explicit2MTBDD.java +++ b/prism/src/prism/Explicit2MTBDD.java @@ -31,7 +31,6 @@ import java.util.Vector; import java.util.HashMap; import jdd.*; -import mtbdd.*; import parser.*; import parser.ast.*; @@ -39,13 +38,13 @@ import parser.ast.*; public class Explicit2MTBDD { + // prism + private Prism prism; + // logs private PrismLog mainLog; // main log private PrismLog techLog; // tech log - // flags/settings - private boolean doReach = true; // by default, do reachability (sometimes might want to skip it though) - // files to read in from private File statesFile; private File transFile; @@ -78,10 +77,7 @@ public class Explicit2MTBDD // dds/dd vars - whole system private JDDNode trans; // transition matrix dd private JDDNode range; // dd giving range for system - private JDDNode trans01; // 0-1 transition matrix dd private JDDNode start; // dd for start state - private JDDNode reach; // dd of reachable states - private JDDNode deadlocks; // dd of deadlock states private JDDNode stateRewards; // dd of state rewards private JDDNode transRewards; // dd of transition rewards private JDDVars allDDRowVars; // all dd vars (rows) @@ -112,10 +108,11 @@ public class Explicit2MTBDD // constructor - public Explicit2MTBDD(PrismLog log1, PrismLog log2, File sf, File tf, int t, String is) + public Explicit2MTBDD(Prism prism, File sf, File tf, int t, String is) { - mainLog = log1; - techLog = log2; + this.prism = prism; + mainLog = prism.getMainLog(); + techLog = prism.getTechLog(); statesFile = sf; transFile = tf; // set type at this point @@ -131,28 +128,6 @@ public class Explicit2MTBDD initString = is; } - // set options (generic) - - public void setOption(String option, boolean b) - { - if (option.equals("doreach")) { - doReach = b; - } - else { - mainLog.println("\nWarning: option \""+option+"\" not supported by Explicit2MTBDD translator."); - } - } - - public void setOption(String option, int i) - { - mainLog.println("\nWarning: option \""+option+"\" not supported by Explicit2MTBDD translator."); - } - - public void setOption(String option, String s) - { - mainLog.println("\nWarning: option \""+option+"\" not supported by Explicit2MTBDD translator."); - } - // build state space public ModulesFile buildStates() throws PrismException @@ -461,20 +436,16 @@ public class Explicit2MTBDD // mainLog.println(); // JDD.Deref(tmp); + // calculate dd for initial state + start = JDD.Constant(1); + for (i = 0; i < numVars; i++) { + tmp = JDD.SetVectorElement(JDD.Constant(0), varDDRowVars[i], varList.getStart(i)-varList.getLow(i), 1); + start = JDD.And(start, tmp); + } + // compute state rewards computeStateRewards(); - // do reachability (or not!) - if (doReach) { - doReachability(); - } - else { - skipReachability(); - } - - // find any deadlocks - findDeadlocks(); - int numModules = 1; // just one module String moduleNames[] = modulesFile.getModuleNames(); // whose name is stored here Values constantValues = new Values(); // no constants @@ -485,22 +456,42 @@ public class Explicit2MTBDD // create new Model object to be returned if (type == ModulesFile.PROBABILISTIC) { - model = new ProbModel(trans, trans01, start, reach, deadlocks, stateRewardsArray, transRewardsArray, rewardStructNames, allDDRowVars, allDDColVars, ddVarNames, + model = new ProbModel(trans, start, stateRewardsArray, transRewardsArray, rewardStructNames, allDDRowVars, allDDColVars, ddVarNames, numModules, moduleNames, moduleDDRowVars, moduleDDColVars, numVars, varList, varDDRowVars, varDDColVars, constantValues); } else if (type == ModulesFile.NONDETERMINISTIC) { - model = new NondetModel(trans, trans01, start, reach, deadlocks, stateRewardsArray, transRewardsArray, rewardStructNames, allDDRowVars, allDDColVars, + model = new NondetModel(trans, start, stateRewardsArray, transRewardsArray, rewardStructNames, allDDRowVars, allDDColVars, allDDSynchVars, allDDSchedVars, allDDChoiceVars, allDDNondetVars, ddVarNames, numModules, moduleNames, moduleDDRowVars, moduleDDColVars, numVars, varList, varDDRowVars, varDDColVars, constantValues); } else if (type == ModulesFile.STOCHASTIC) { - model = new StochModel(trans, trans01, start, reach, deadlocks, stateRewardsArray, transRewardsArray, rewardStructNames, allDDRowVars, allDDColVars, ddVarNames, + model = new StochModel(trans, start, stateRewardsArray, transRewardsArray, rewardStructNames, allDDRowVars, allDDColVars, ddVarNames, numModules, moduleNames, moduleDDRowVars, moduleDDColVars, numVars, varList, varDDRowVars, varDDColVars, constantValues); } + // do reachability (or not) + if (prism.getDoReach()) { + mainLog.print("\nComputing reachable states...\n"); + model.doReachability(prism.getExtraReachInfo()); + model.filterReachableStates(); + } + else { + mainLog.print("\nSkipping reachable state computation.\n"); + model.skipReachability(); + model.filterReachableStates(); + } + + // Print some info (if extraddinfo flag on) + if (prism.getExtraDDInfo()) { + mainLog.print("Reach: " + JDD.GetNumNodes(model.getReach()) + " nodes\n"); + } + + // find any deadlocks + model.findDeadlocks(); + // deref spare dds JDD.Deref(moduleIdentities[0]); JDD.Deref(moduleRangeDDs[0]); @@ -893,139 +884,6 @@ public class Explicit2MTBDD throw new PrismException("Error detected at line " + lineNum + " of states file \"" + statesFile + "\""); } } - - // do reachability - - private void doReachability() - { - int i; - JDDNode tmp; - - // calculate dd for initial state - start = JDD.Constant(1); - for (i = 0; i < numVars; i++) { - tmp = JDD.SetVectorElement(JDD.Constant(0), varDDRowVars[i], varList.getStart(i)-varList.getLow(i), 1); - start = JDD.And(start, tmp); - } - - // calculate 0-1 version of trans - JDD.Ref(trans); - trans01 = JDD.GreaterThan(trans, 0); - - // remove any nondeterminism - if (type == ModulesFile.NONDETERMINISTIC) { - JDD.Ref(trans01); - tmp = JDD.MaxAbstract(trans01, allDDNondetVars); - } - else { - JDD.Ref(trans01); - tmp = trans01; - } - - // compute reachable states - mainLog.print("\nComputing reachable states...\n"); - reach = PrismMTBDD.Reachability(tmp, allDDRowVars, allDDColVars, start); - JDD.Deref(tmp); - - // remove non-reachable states from transition matrix - JDD.Ref(reach); - trans = JDD.Apply(JDD.TIMES, reach, trans); - JDD.Ref(reach); - tmp = JDD.PermuteVariables(reach, allDDRowVars, allDDColVars); - trans = JDD.Apply(JDD.TIMES, tmp, trans); - - // recalculate 0-1 version of trans - JDD.Deref(trans01); - JDD.Ref(trans); - trans01 = JDD.GreaterThan(trans, 0); - - // remove non-reachable states from states rewards vector - JDD.Ref(reach); - stateRewards = JDD.Apply(JDD.TIMES, reach, stateRewards); - - // remove non-reachable states from transition reward matrix - JDD.Ref(reach); - transRewards = JDD.Apply(JDD.TIMES, reach, transRewards); - JDD.Ref(reach); - tmp = JDD.PermuteVariables(reach, allDDRowVars, allDDColVars); - transRewards = JDD.Apply(JDD.TIMES, tmp, transRewards); - } - - // this method allows you to skip the reachability phase - // there are two versions - one which actually does skip it - // and one which does it anyway but doesn't filter out the - // unreachable states from the transition matrix. - // these are only here for experimental purposes - not general use. - - // (do reach but don't filter) - -// private void skipReachability() -// { -// int i; -// JDDNode tmp; -// -// // calculate dd for initial state -// start = JDD.Constant(1); -// for (i = 0; i < numVars; i++) { -// tmp = JDD.SetVectorElement(JDD.Constant(0), varDDRowVars[i], varList.getStart(i)-varList.getLow(i), 1); -// start = JDD.And(start, tmp); -// } -// -// // calculate 0-1 version of trans -// JDD.Ref(trans); -// trans01 = JDD.GreaterThan(trans, 0); -// -// // remove any nondeterminism -// if (type == ModulesFile.NONDETERMINISTIC) { -// JDD.Ref(trans01); -// tmp = JDD.MaxAbstract(trans01, allDDNondetVars); -// } -// else { -// JDD.Ref(trans01); -// tmp = trans01; -// } -// -// // compute reachable states -// mainLog.print("\nComputing reachable states...\n"); -// reach = PrismMTBDD.Reachability(tmp, allDDRowVars, allDDColVars, start); -// JDD.Deref(tmp); -// } - -// (no reach and no filter) - - private void skipReachability() - { - int i; - JDDNode tmp; - - // calculate dd for initial state - start = JDD.Constant(1); - for (i = 0; i < numVars; i++) { - tmp = JDD.SetVectorElement(JDD.Constant(0), varDDRowVars[i], varList.getStart(i)-varList.getLow(i), 1); - start = JDD.And(start, tmp); - } - - // calculate 0-1 version of trans - JDD.Ref(trans); - trans01 = JDD.GreaterThan(trans, 0); - - // don't compute reachable states - assume all reachable - reach = JDD.Constant(1); - } - - private void findDeadlocks() - { - // find states with at least one transition - JDD.Ref(trans01); - deadlocks = JDD.ThereExists(trans01, allDDColVars); - if (type == ModulesFile.NONDETERMINISTIC) { - deadlocks = JDD.ThereExists(deadlocks, allDDNondetVars); - } - - // find reachable states with no transitions - JDD.Ref(reach); - deadlocks = JDD.And(reach, JDD.Not(deadlocks)); - } } //------------------------------------------------------------------------------ diff --git a/prism/src/prism/Model.java b/prism/src/prism/Model.java index c6f82801..e2d3f6ad 100644 --- a/prism/src/prism/Model.java +++ b/prism/src/prism/Model.java @@ -98,6 +98,11 @@ public interface Model ODDNode getODD(); + void doReachability(); + void doReachability(boolean extraReachInfo); + void skipReachability(); + void filterReachableStates(); + void findDeadlocks(); void fixDeadlocks(); void printTrans(); void printTrans01(); diff --git a/prism/src/prism/Modules2MTBDD.java b/prism/src/prism/Modules2MTBDD.java index 5012d491..1c216810 100644 --- a/prism/src/prism/Modules2MTBDD.java +++ b/prism/src/prism/Modules2MTBDD.java @@ -31,7 +31,6 @@ import java.util.HashSet; import java.util.Iterator; import jdd.*; -import mtbdd.*; import parser.*; import parser.ast.*; @@ -78,10 +77,7 @@ public class Modules2MTBDD // dds/dd vars - whole system private JDDNode trans; // transition matrix dd private JDDNode range; // dd giving range for system - private JDDNode trans01; // 0-1 transition matrix dd private JDDNode start; // dd for start state - private JDDNode reach; // dd of reachable states - private JDDNode deadlocks; // dd of deadlock states private JDDNode stateRewards[]; // dds for state rewards private JDDNode transRewards[]; // dds for transition rewards private JDDVars allDDRowVars; // all dd vars (rows) @@ -225,16 +221,8 @@ public class Modules2MTBDD mainLog.print(JDD.GetNumTerminals(trans) + " terminal)\n"); } - // do reachability (or not!) - if (prism.getDoReach()) { - doReachability(); - } - else { - skipReachability(); - } - - // find any deadlocks - findDeadlocks(); + // build bdd for initial state(s) + buildInitialStates(); // store reward struct names rewardStructNames = new String[numRewardStructs]; @@ -244,22 +232,42 @@ public class Modules2MTBDD // create new Model object to be returned if (type == ModulesFile.PROBABILISTIC) { - model = new ProbModel(trans, trans01, start, reach, deadlocks, stateRewards, transRewards, rewardStructNames, allDDRowVars, allDDColVars, ddVarNames, + model = new ProbModel(trans, start, stateRewards, transRewards, rewardStructNames, allDDRowVars, allDDColVars, ddVarNames, numModules, moduleNames, moduleDDRowVars, moduleDDColVars, numVars, varList, varDDRowVars, varDDColVars, constantValues); } else if (type == ModulesFile.NONDETERMINISTIC) { - model = new NondetModel(trans, trans01, start, reach, deadlocks, stateRewards, transRewards, rewardStructNames, allDDRowVars, allDDColVars, + model = new NondetModel(trans, start, stateRewards, transRewards, rewardStructNames, allDDRowVars, allDDColVars, allDDSynchVars, allDDSchedVars, allDDChoiceVars, allDDNondetVars, ddVarNames, numModules, moduleNames, moduleDDRowVars, moduleDDColVars, numVars, varList, varDDRowVars, varDDColVars, constantValues); } else if (type == ModulesFile.STOCHASTIC) { - model = new StochModel(trans, trans01, start, reach, deadlocks, stateRewards, transRewards, rewardStructNames, allDDRowVars, allDDColVars, ddVarNames, + model = new StochModel(trans, start, stateRewards, transRewards, rewardStructNames, allDDRowVars, allDDColVars, ddVarNames, numModules, moduleNames, moduleDDRowVars, moduleDDColVars, numVars, varList, varDDRowVars, varDDColVars, constantValues); } + // do reachability (or not) + if (prism.getDoReach()) { + mainLog.print("\nComputing reachable states...\n"); + model.doReachability(prism.getExtraReachInfo()); + model.filterReachableStates(); + } + else { + mainLog.print("\nSkipping reachable state computation.\n"); + model.skipReachability(); + model.filterReachableStates(); + } + + // Print some info (if extraddinfo flag on) + if (prism.getExtraDDInfo()) { + mainLog.print("Reach: " + JDD.GetNumNodes(model.getReach()) + " nodes\n"); + } + + // find any deadlocks + model.findDeadlocks(); + // deref spare dds globalDDRowVars.derefAll(); globalDDColVars.derefAll(); @@ -1929,15 +1937,14 @@ public class Modules2MTBDD } } } - - // do reachability - private void doReachability() throws PrismException + // calculate dd for initial state(s) + + private void buildInitialStates() throws PrismException { int i; JDDNode tmp; - // calculate dd for initial state // first, handle case where multiple initial states specified with init...endinit if (modulesFile.getInitialStates() != null) { start = translateExpression(modulesFile.getInitialStates()); @@ -1953,130 +1960,6 @@ public class Modules2MTBDD start = JDD.And(start, tmp); } } - - // calculate 0-1 version of trans - JDD.Ref(trans); - trans01 = JDD.GreaterThan(trans, 0); - - // remove any nondeterminism - if (type == ModulesFile.NONDETERMINISTIC) { - JDD.Ref(trans01); - tmp = JDD.MaxAbstract(trans01, allDDNondetVars); - } - else { - JDD.Ref(trans01); - tmp = trans01; - } - - // compute reachable states - mainLog.print("\nComputing reachable states...\n"); - reach = PrismMTBDD.Reachability(tmp, allDDRowVars, allDDColVars, start, prism.getExtraReachInfo()?1:0); - JDD.Deref(tmp); - - // Print some info (if extraddinfo flag on) - if (prism.getExtraDDInfo()) { - mainLog.print("Reach: " + JDD.GetNumNodes(reach) + " nodes\n"); - } - // remove non-reachable states from transition matrix - JDD.Ref(reach); - trans = JDD.Apply(JDD.TIMES, reach, trans); - JDD.Ref(reach); - tmp = JDD.PermuteVariables(reach, allDDRowVars, allDDColVars); - trans = JDD.Apply(JDD.TIMES, tmp, trans); - - // recalculate 0-1 version of trans - JDD.Deref(trans01); - JDD.Ref(trans); - trans01 = JDD.GreaterThan(trans, 0); - - // remove non-reachable states from state/transition rewards - for (i = 0; i < modulesFile.getNumRewardStructs(); i++) { - // state rewards vector - JDD.Ref(reach); - stateRewards[i] = JDD.Apply(JDD.TIMES, reach, stateRewards[i]); - // transition reward matrix - JDD.Ref(reach); - transRewards[i] = JDD.Apply(JDD.TIMES, reach, transRewards[i]); - JDD.Ref(reach); - tmp = JDD.PermuteVariables(reach, allDDRowVars, allDDColVars); - transRewards[i] = JDD.Apply(JDD.TIMES, tmp, transRewards[i]); - } - } - - // this method allows you to skip the reachability phase - // there are two versions - one which actually does skip it - // and one which does it anyway but doesn't filter out the - // unreachable states from the transition matrix. - // these are only here for experimental purposes - not general use. - - // (do reach but don't filter) - -// private void skipReachability() -// { -// int i; -// JDDNode tmp; -// -// // calculate dd for initial state -// start = JDD.Constant(1); -// for (i = 0; i < numVars; i++) { -// tmp = JDD.SetVectorElement(JDD.Constant(0), varDDRowVars[i], varList.getStart(i)-varList.getLow(i), 1); -// start = JDD.And(start, tmp); -// } -// -// // calculate 0-1 version of trans -// JDD.Ref(trans); -// trans01 = JDD.GreaterThan(trans, 0); -// -// // remove any nondeterminism -// if (type == ModulesFile.NONDETERMINISTIC) { -// JDD.Ref(trans01); -// tmp = JDD.MaxAbstract(trans01, allDDNondetVars); -// } -// else { -// JDD.Ref(trans01); -// tmp = trans01; -// } -// -// // compute reachable states -// mainLog.print("\nComputing reachable states...\n"); -// reach = PrismMTBDD.Reachability(tmp, allDDRowVars, allDDColVars, start); -// JDD.Deref(tmp); -// } - -// (no reach and no filter) - - private void skipReachability() - { - int i; - JDDNode tmp; - - // calculate dd for initial state - start = JDD.Constant(1); - for (i = 0; i < numVars; i++) { - tmp = JDD.SetVectorElement(JDD.Constant(0), varDDRowVars[i], varList.getStart(i)-varList.getLow(i), 1); - start = JDD.And(start, tmp); - } - - // calculate 0-1 version of trans - JDD.Ref(trans); - trans01 = JDD.GreaterThan(trans, 0); - - // don't compute reachable states - assume all reachable - reach = JDD.Constant(1); - } - - private void findDeadlocks() - { - // find states with at least one transition - JDD.Ref(trans01); - deadlocks = JDD.ThereExists(trans01, allDDColVars); - if (type == ModulesFile.NONDETERMINISTIC) { - deadlocks = JDD.ThereExists(deadlocks, allDDNondetVars); - } - - // find reachable states with no transitions - JDD.Ref(reach); - deadlocks = JDD.And(reach, JDD.Not(deadlocks)); } } diff --git a/prism/src/prism/NondetModel.java b/prism/src/prism/NondetModel.java index 36470411..2eef7ed5 100644 --- a/prism/src/prism/NondetModel.java +++ b/prism/src/prism/NondetModel.java @@ -112,28 +112,60 @@ public class NondetModel extends ProbModel public String getTransName() { - return "Transition matrix"; + return "Transition matrix"; } - + 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 s, 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) { - super(tr, tr01, s, r, dl, sr, trr, rsn, arv, acv, ddvn, nm, mn, mrv, mcv, nv, vl, vrv, vcv, cv); - + super(tr, s, sr, trr, rsn, arv, acv, ddvn, nm, mn, mrv, mcv, nv, vl, vrv, vcv, cv); + allDDSynchVars = asyv; allDDSchedVars = asv; allDDChoiceVars = achv; allDDNondetVars = andv; + } + + // do reachability + + public void doReachability(boolean extraReachInfo) + { + JDDNode tmp; + + // remove any nondeterminism + JDD.Ref(trans01); + tmp = JDD.MaxAbstract(trans01, allDDNondetVars); + + // compute reachable states + reach = PrismMTBDD.Reachability(tmp, allDDRowVars, allDDColVars, start, extraReachInfo ? 1 : 0); + JDD.Deref(tmp); + + // work out number of reachable states + numStates = JDD.GetNumMinterms(reach, allDDRowVars.n()); + // build odd + odd = ODDUtils.BuildODD(reach, allDDRowVars); + + // store reachable states in a StateList + reachStateList = new StateListMTBDD(reach, this); + } + + // remove non-reachable states from various dds + // (and calculate num transitions, etc.) + // (and build mask) + + public void filterReachableStates() + { + super.filterReachableStates(); + // build mask for nondeterminstic choices JDD.Ref(trans01); JDD.Ref(reach); @@ -144,6 +176,25 @@ public class NondetModel extends ProbModel double d = JDD.GetNumMinterms(nondetMask, getNumDDRowVars() + getNumDDNondetVars()); numChoices = ((Math.pow(2, getNumDDNondetVars())) * numStates) - d; } + + // identify any deadlock states + + public void findDeadlocks() + { + // find states with at least one transition + JDD.Ref(trans01); + deadlocks = JDD.ThereExists(trans01, allDDColVars); + deadlocks = JDD.ThereExists(deadlocks, allDDNondetVars); + + // find reachable states with no transitions + JDD.Ref(reach); + deadlocks = JDD.And(reach, JDD.Not(deadlocks)); + + // store deadlock states in a StateList + deadlockStateList = new StateListMTBDD(deadlocks, this); + } + + // remove deadlocks by adding self-loops public void fixDeadlocks() { @@ -248,8 +299,8 @@ public class NondetModel extends ProbModel if (!explicit) { // can only do explicit (sparse matrix based) export for mdps } else { - PrismSparse.ExportMDP(trans, getTransSymbol(), allDDRowVars, allDDColVars, allDDNondetVars, odd, exportType, - (file != null) ? file.getPath() : null); + PrismSparse.ExportMDP(trans, getTransSymbol(), allDDRowVars, allDDColVars, allDDNondetVars, odd, + exportType, (file != null) ? file.getPath() : null); } } diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 5465542d..eae37a3a 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -849,8 +849,7 @@ public class Prism implements PrismSettingsListener public ModulesFile parseExplicitModel(File statesFile, File transFile, int typeOverride, String initString) throws PrismException { // create Explicit2MTBDD object - exp2mtbdd = new Explicit2MTBDD(mainLog, techLog, statesFile, transFile, typeOverride, initString); - exp2mtbdd.setOption("doreach", getDoReach()); + exp2mtbdd = new Explicit2MTBDD(this, statesFile, transFile, typeOverride, initString); // build state space return exp2mtbdd.buildStates(); diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 179bc42e..6b580c72 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -534,7 +534,7 @@ public class PrismCL } // print model info - mainLog.println("\nType: " + model.getType()); + mainLog.println("\nType: " + model.getTypeString()); mainLog.print("Modules: "); for (i = 0; i < model.getNumModules(); i++) { mainLog.print(model.getModuleName(i) + " "); diff --git a/prism/src/prism/ProbModel.java b/prism/src/prism/ProbModel.java index 8aa1ddb9..f58dd2f7 100644 --- a/prism/src/prism/ProbModel.java +++ b/prism/src/prism/ProbModel.java @@ -364,30 +364,27 @@ public class ProbModel implements Model { return odd; } - + public String getTransName() { - return "Transition matrix"; + return "Transition matrix"; } - + public String getTransSymbol() { return "P"; } - + // 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) + public ProbModel(JDDNode tr, JDDNode s, 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; - reach = r; - deadlocks = dl; fixdl = JDD.Constant(0); stateRewards = sr; transRewards = trr; @@ -415,26 +412,112 @@ public class ProbModel implements Model gtol[i] = gtol[i] * gtol[i + 1]; } - // work out number of states - numStates = JDD.GetNumMinterms(reach, allDDRowVars.n()); + // calculate 0-1 version of trans + JDD.Ref(trans); + trans01 = JDD.GreaterThan(trans, 0); + + // work out number of initial states numStartStates = JDD.GetNumMinterms(start, allDDRowVars.n()); - // work out number of transitions - numTransitions = JDD.GetNumMinterms(trans01, getNumDDVarsInTrans()); + // store initial states in a StateList + startStateList = new StateListMTBDD(start, this); + } + + // do reachability + + public void doReachability() + { + doReachability(false); + } + + public void doReachability(boolean extraReachInfo) + { + // compute reachable states + reach = PrismMTBDD.Reachability(trans01, allDDRowVars, allDDColVars, start, extraReachInfo ? 1 : 0); + + // work out number of reachable states + numStates = JDD.GetNumMinterms(reach, allDDRowVars.n()); + + // build odd + odd = ODDUtils.BuildODD(reach, allDDRowVars); + + // store reachable states in a StateList + reachStateList = new StateListMTBDD(reach, this); + } + + // this method allows you to skip the reachability phase + // it is only here for experimental purposes - not general use. + + public void skipReachability() + { + // don't compute reachable states - assume all reachable + reach = JDD.Constant(1); + + // work out number of reachable states + numStates = Math.pow(2, allDDRowVars.n()); // build odd odd = ODDUtils.BuildODD(reach, allDDRowVars); // store reachable states in a StateList reachStateList = new StateListMTBDD(reach, this); + } + + // remove non-reachable states from various dds + // (and calculate num transitions) + + public void filterReachableStates() + { + int i; + JDDNode tmp; + + // remove non-reachable states from transition matrix + JDD.Ref(reach); + trans = JDD.Apply(JDD.TIMES, reach, trans); + JDD.Ref(reach); + tmp = JDD.PermuteVariables(reach, allDDRowVars, allDDColVars); + trans = JDD.Apply(JDD.TIMES, tmp, trans); + + // recalculate 0-1 version of trans + JDD.Deref(trans01); + JDD.Ref(trans); + trans01 = JDD.GreaterThan(trans, 0); + + // remove non-reachable states from state/transition rewards + for (i = 0; i < stateRewards.length; i++) { + // state rewards vector + JDD.Ref(reach); + stateRewards[i] = JDD.Apply(JDD.TIMES, reach, stateRewards[i]); + // transition reward matrix + JDD.Ref(reach); + transRewards[i] = JDD.Apply(JDD.TIMES, reach, transRewards[i]); + JDD.Ref(reach); + tmp = JDD.PermuteVariables(reach, allDDRowVars, allDDColVars); + transRewards[i] = JDD.Apply(JDD.TIMES, tmp, transRewards[i]); + } + + // work out number of transitions + numTransitions = JDD.GetNumMinterms(trans01, getNumDDVarsInTrans()); + } + + // identify any deadlock states + + public void findDeadlocks() + { + // find states with at least one transition + JDD.Ref(trans01); + deadlocks = JDD.ThereExists(trans01, allDDColVars); + + // find reachable states with no transitions + JDD.Ref(reach); + deadlocks = JDD.And(reach, JDD.Not(deadlocks)); // store deadlock states in a StateList deadlockStateList = new StateListMTBDD(deadlocks, this); - - // store initial states in a StateList - startStateList = new StateListMTBDD(start, this); } + // remove deadlocks by adding self-loops + public void fixDeadlocks() { JDDNode tmp; @@ -530,11 +613,11 @@ public class ProbModel implements Model public void exportToFile(int exportType, boolean explicit, File file) throws FileNotFoundException { if (!explicit) { - PrismMTBDD.ExportMatrix(trans, getTransSymbol(), 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); + PrismSparse.ExportMatrix(trans, getTransSymbol(), allDDRowVars, allDDColVars, odd, exportType, + (file != null) ? file.getPath() : null); } } diff --git a/prism/src/prism/StochModel.java b/prism/src/prism/StochModel.java index 3899c7c9..b2216a94 100644 --- a/prism/src/prism/StochModel.java +++ b/prism/src/prism/StochModel.java @@ -51,20 +51,20 @@ public class StochModel extends ProbModel public String getTransName() { - return "Rate matrix"; + return "Rate matrix"; } - + public String getTransSymbol() { return "R"; } - + // constructor - 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) + public StochModel(JDDNode tr, JDDNode s, 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) { - super(tr, tr01, s, r, dl, sr, trr, rsn, arv, acv, ddvn, nm, mn, mrv, mcv, nv, vl, vrv, vcv, cv); + super(tr, s, sr, trr, rsn, arv, acv, ddvn, nm, mn, mrv, mcv, nv, vl, vrv, vcv, cv); } }