diff --git a/prism/src/explicit/CTMCModelChecker.java b/prism/src/explicit/CTMCModelChecker.java index f9ba97c4..11d8e36b 100644 --- a/prism/src/explicit/CTMCModelChecker.java +++ b/prism/src/explicit/CTMCModelChecker.java @@ -38,11 +38,8 @@ import prism.*; /** * Explicit-state model checker for continuous-time Markov chains (CTMCs). - * - * This uses various bits of functionality of DTMCModelChecker, so we inherit from that. - * (This way DTMCModelChecker picks up any options set on this one.) */ -public class CTMCModelChecker extends DTMCModelChecker +public class CTMCModelChecker extends ProbModelChecker { /** * Create a new CTMCModelChecker, inherit basic state from parent (unless null). @@ -57,28 +54,24 @@ public class CTMCModelChecker extends DTMCModelChecker @Override protected StateValues checkProbPathFormulaLTL(Model model, Expression expr, boolean qual, MinMax minMax, BitSet statesOfInterest) throws PrismException { + // Construct embedded DTMC and do computation on that mainLog.println("Building embedded DTMC..."); DTMC dtmcEmb = ((CTMC)model).getImplicitEmbeddedDTMC(); - - // use superclass (DTMCModelChecker) method on the embedded DTMC - return super.checkProbPathFormulaLTL(dtmcEmb, expr, qual, minMax, statesOfInterest); + return createDTMCModelChecker().checkProbPathFormulaLTL(dtmcEmb, expr, qual, minMax, statesOfInterest); } @Override protected StateValues checkRewardCoSafeLTL(Model model, Rewards modelRewards, Expression expr, MinMax minMax, BitSet statesOfInterest) throws PrismException { + // Construct embedded DTMC (and convert rewards for it) and do computation on that mainLog.println("Building embedded DTMC..."); DTMC dtmcEmb = ((CTMC)model).getImplicitEmbeddedDTMC(); - - // Convert rewards int n = model.getNumStates(); StateRewardsArray rewEmb = new StateRewardsArray(n); for (int i = 0; i < n; i++) { rewEmb.setStateReward(i, ((MCRewards) modelRewards).getStateReward(i) / ((CTMC)model).getExitRate(i)); } - - // use superclass (DTMCModelChecker) method on the embedded DTMC - return super.checkRewardCoSafeLTL(dtmcEmb, rewEmb, expr, minMax, statesOfInterest); + return createDTMCModelChecker().checkRewardCoSafeLTL(dtmcEmb, rewEmb, expr, minMax, statesOfInterest); } @Override @@ -138,11 +131,11 @@ public class CTMCModelChecker extends DTMCModelChecker // check for special case of lTime == 0, this is actually an unbounded until if (lTime == 0) { // compute probs - res = computeUntilProbs((DTMC) model, b1, b2); + res = createDTMCModelChecker().computeUntilProbs((DTMC) model, b1, b2); probs = StateValues.createFromDoubleArray(res.soln, model); } else { // compute unbounded until probs - tmpRes = computeUntilProbs((DTMC) model, b1, b2); + tmpRes = createDTMCModelChecker().computeUntilProbs((DTMC) model, b1, b2); // compute bounded until probs res = computeTransientBackwardsProbs((CTMC) model, b1, b1, lTime, tmpRes.soln); probs = StateValues.createFromDoubleArray(res.soln, model); @@ -243,9 +236,10 @@ public class CTMCModelChecker extends DTMCModelChecker */ public ModelCheckerResult computeNextProbs(CTMC ctmc, BitSet target) throws PrismException { + // Construct embedded DTMC and do computation on that mainLog.println("Building embedded DTMC..."); DTMC dtmcEmb = ctmc.getImplicitEmbeddedDTMC(); - return super.computeNextProbs(dtmcEmb, target); + return createDTMCModelChecker().computeNextProbs(dtmcEmb, target); } /** @@ -256,9 +250,10 @@ public class CTMCModelChecker extends DTMCModelChecker */ public ModelCheckerResult computeReachProbs(CTMC ctmc, BitSet target) throws PrismException { + // Construct embedded DTMC and do computation on that mainLog.println("Building embedded DTMC..."); DTMC dtmcEmb = ctmc.getImplicitEmbeddedDTMC(); - return super.computeReachProbs(dtmcEmb, target); + return createDTMCModelChecker().computeReachProbs(dtmcEmb, target); } /** @@ -271,9 +266,10 @@ public class CTMCModelChecker extends DTMCModelChecker */ public ModelCheckerResult computeUntilProbs(CTMC ctmc, BitSet remain, BitSet target) throws PrismException { + // Construct embedded DTMC and do computation on that mainLog.println("Building embedded DTMC..."); DTMC dtmcEmb = ctmc.getImplicitEmbeddedDTMC(); - return super.computeUntilProbs(dtmcEmb, remain, target); + return createDTMCModelChecker().computeUntilProbs(dtmcEmb, remain, target); } /** @@ -289,9 +285,10 @@ public class CTMCModelChecker extends DTMCModelChecker */ public ModelCheckerResult computeReachProbs(CTMC ctmc, BitSet remain, BitSet target, double init[], BitSet known) throws PrismException { + // Construct embedded DTMC and do computation on that mainLog.println("Building embedded DTMC..."); DTMC dtmcEmb = ctmc.getImplicitEmbeddedDTMC(); - return super.computeReachProbs(dtmcEmb, remain, target, init, known); + return createDTMCModelChecker().computeReachProbs(dtmcEmb, remain, target, init, known); } /** @@ -571,8 +568,7 @@ public class CTMCModelChecker extends DTMCModelChecker * @param mcRewards The rewards * @param t Time bound */ - @Override - public ModelCheckerResult computeInstantaneousRewards(DTMC dtmc, MCRewards mcRewards, double t) throws PrismException + public ModelCheckerResult computeInstantaneousRewards(CTMC ctmc, MCRewards mcRewards, double t) throws PrismException { ModelCheckerResult res = null; int i, n, iters; @@ -584,12 +580,12 @@ public class CTMCModelChecker extends DTMCModelChecker double q, qt, acc, weights[], totalWeight; // Store num states - n = dtmc.getNumStates(); + n = ctmc.getNumStates(); // Optimisation: If t = 0, this is easy. if (t == 0) { res = new ModelCheckerResult(); - res.soln = new double[dtmc.getNumStates()]; + res.soln = new double[ctmc.getNumStates()]; for (i = 0; i < n; i++) res.soln[i] = mcRewards.getStateReward(i); return res; @@ -599,8 +595,6 @@ public class CTMCModelChecker extends DTMCModelChecker timer = System.currentTimeMillis(); mainLog.println("\nStarting backwards instantaneous rewards computation..."); - CTMC ctmc = (CTMC) dtmc; - // Get uniformisation rate; do Fox-Glynn q = ctmc.getDefaultUniformisationRate(); qt = q * t; @@ -621,7 +615,7 @@ public class CTMCModelChecker extends DTMCModelChecker mainLog.println("Fox-Glynn (" + acc + "): left = " + left + ", right = " + right); // Build (implicit) uniformised DTMC - dtmc = ctmc.buildImplicitUniformisedDTMC(q); + DTMC dtmcUnif = ctmc.buildImplicitUniformisedDTMC(q); // Create solution vector(s) soln = new double[n]; @@ -641,7 +635,7 @@ public class CTMCModelChecker extends DTMCModelChecker iters = 1; while (iters <= right) { // Matrix-vector multiply - dtmc.mvMult(soln, soln2, null, false); + dtmcUnif.mvMult(soln, soln2, null, false); // Swap vectors for next iter tmpsoln = soln; soln = soln2; @@ -688,7 +682,7 @@ public class CTMCModelChecker extends DTMCModelChecker rewEmb.setStateReward(i, mcRewards.getStateReward(i) / ctmc.getExitRate(i)); } // Do computation on DTMC - return super.computeReachRewards(dtmcEmb, rewEmb, target); + return createDTMCModelChecker().computeReachRewards(dtmcEmb, rewEmb, target); } /** @@ -790,6 +784,18 @@ public class CTMCModelChecker extends DTMCModelChecker return res; } + // Utility methods + + /** + * Create a new DTMC model checker with the same settings as this one. + */ + private DTMCModelChecker createDTMCModelChecker() throws PrismException + { + DTMCModelChecker mcDTMC = new DTMCModelChecker(this); + mcDTMC.inheritSettings(this); + return mcDTMC; + } + /** * Simple test program. */ diff --git a/prism/src/explicit/CTMDPModelChecker.java b/prism/src/explicit/CTMDPModelChecker.java index 3b832e3b..16681a7d 100644 --- a/prism/src/explicit/CTMDPModelChecker.java +++ b/prism/src/explicit/CTMDPModelChecker.java @@ -27,19 +27,18 @@ package explicit; import java.util.BitSet; +import java.util.List; import java.util.Map; import parser.ast.ExpressionTemporal; import prism.PrismComponent; import prism.PrismException; +import prism.PrismNotSupportedException; /** * Explicit-state model checker for continuous-time Markov decision processes (CTMDPs). - * - * This uses various bits of functionality of MDPModelChecker, so we inherit from that. - * (This way MDPModelChecker picks up any options set on this one.) */ -public class CTMDPModelChecker extends MDPModelChecker +public class CTMDPModelChecker extends ProbModelChecker { /** * Create a new CTMDPModelChecker, inherit basic state from parent (unless null). @@ -243,6 +242,33 @@ public class CTMDPModelChecker extends MDPModelChecker return res; } + /** + * Compute reachability probabilities. + * i.e. compute the min/max probability of reaching a state in {@code target}. + * @param ctmdp The CTMDP + * @param target Target states + * @param min Min or max probabilities (true=min, false=max) + */ + public ModelCheckerResult computeReachProbs(CTMDP ctmdp, BitSet target, boolean min) throws PrismException + { + throw new PrismNotSupportedException("Not implemented yet"); + } + + /** + * Construct strategy information for min/max reachability probabilities. + * (More precisely, list of indices of choices resulting in min/max.) + * (Note: indices are guaranteed to be sorted in ascending order.) + * @param ctmdp The CTMDP + * @param state The state to generate strategy info for + * @param target The set of target states to reach + * @param min Min or max probabilities (true=min, false=max) + * @param lastSoln Vector of values from which to recompute in one iteration + */ + public List probReachStrategy(CTMDP ctmdp, int state, BitSet target, boolean min, double lastSoln[]) throws PrismException + { + throw new PrismNotSupportedException("Not implemented yet"); + } + /** * Simple test program. */ diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index ffdcc88a..837ff9e8 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -36,7 +36,6 @@ import parser.VarList; import parser.ast.Declaration; import parser.ast.DeclarationIntUnbounded; import parser.ast.Expression; -import parser.type.TypeDouble; import prism.Prism; import prism.PrismComponent; import prism.PrismException; @@ -395,47 +394,6 @@ public class DTMCModelChecker extends ProbModelChecker throw new PrismNotSupportedException("Not implemented yet"); } - // Utility methods for probability distributions - - /** - * Generate a probability distribution, stored as a StateValues object, from a file. - * If {@code distFile} is null, so is the return value. - */ - public StateValues readDistributionFromFile(File distFile, Model model) throws PrismException - { - StateValues dist = null; - - if (distFile != null) { - mainLog.println("\nImporting probability distribution from file \"" + distFile + "\"..."); - // Build an empty vector - dist = new StateValues(TypeDouble.getInstance(), model); - // Populate vector from file - dist.readFromFile(distFile); - } - - return dist; - } - - /** - * Build a probability distribution, stored as a StateValues object, - * from the initial states info of the current model: either probability 1 for - * the (single) initial state or equiprobable over multiple initial states. - */ - public StateValues buildInitialDistribution(Model model) throws PrismException - { - StateValues dist = null; - - // Build an empty vector - dist = new StateValues(TypeDouble.getInstance(), model); - // Populate vector (equiprobable over initial states) - double d = 1.0 / model.getNumInitialStates(); - for (int in : model.getInitialStates()) { - dist.setDoubleValue(in, d); - } - - return dist; - } - // Numerical computation functions /** diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index 61546902..18114f17 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -26,6 +26,7 @@ package explicit; +import java.io.File; import java.util.BitSet; import parser.ast.Coalition; @@ -1124,4 +1125,45 @@ public class ProbModelChecker extends NonProbModelChecker } return StateValues.createFromDoubleArray(res.soln, model); } + + // Utility methods for probability distributions + + /** + * Generate a probability distribution, stored as a StateValues object, from a file. + * If {@code distFile} is null, so is the return value. + */ + public StateValues readDistributionFromFile(File distFile, Model model) throws PrismException + { + StateValues dist = null; + + if (distFile != null) { + mainLog.println("\nImporting probability distribution from file \"" + distFile + "\"..."); + // Build an empty vector + dist = new StateValues(TypeDouble.getInstance(), model); + // Populate vector from file + dist.readFromFile(distFile); + } + + return dist; + } + + /** + * Build a probability distribution, stored as a StateValues object, + * from the initial states info of the current model: either probability 1 for + * the (single) initial state or equiprobable over multiple initial states. + */ + public StateValues buildInitialDistribution(Model model) throws PrismException + { + StateValues dist = null; + + // Build an empty vector + dist = new StateValues(TypeDouble.getInstance(), model); + // Populate vector (equiprobable over initial states) + double d = 1.0 / model.getNumInitialStates(); + for (int in : model.getInitialStates()) { + dist.setDoubleValue(in, d); + } + + return dist; + } } diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index bbb55f18..73a8eae8 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/prism/src/explicit/StateModelChecker.java @@ -186,6 +186,7 @@ public class StateModelChecker extends PrismComponent */ public void inheritSettings(StateModelChecker other) { + setModulesFileAndPropertiesFile(other.modulesFile, other.propertiesFile); setLog(other.getLog()); setVerbosity(other.getVerbosity()); setExportTarget(other.getExportTarget()); @@ -350,7 +351,8 @@ public class StateModelChecker extends PrismComponent this.propertiesFile = propertiesFile; // Get combined constant values from model/properties constantValues = new Values(); - constantValues.addValues(modulesFile.getConstantValues()); + if (modulesFile != null) + constantValues.addValues(modulesFile.getConstantValues()); if (propertiesFile != null) constantValues.addValues(propertiesFile.getConstantValues()); }