//============================================================================== // // Copyright (c) 2002- // Authors: // * Dave Parker (University of Oxford) // //------------------------------------------------------------------------------ // // This file is part of PRISM. // // PRISM is free software; you can redistribute it and/or modify // it under the terms of the GNU General Public License as published by // the Free Software Foundation; either version 2 of the License, or // (at your option) any later version. // // PRISM is distributed in the hope that it will be useful, // but WITHOUT ANY WARRANTY; without even the implied warranty of // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the // GNU General Public License for more details. // // You should have received a copy of the GNU General Public License // along with PRISM; if not, write to the Free Software Foundation, // Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA // //============================================================================== package explicit; import java.util.*; import explicit.rewards.MCRewards; import explicit.rewards.MCRewardsStateArray; import parser.ast.ExpressionTemporal; 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 { // Model checking functions protected StateValues checkProbBoundedUntil(Model model, ExpressionTemporal expr) throws PrismException { // TODO: handle until case double time; BitSet b1, b2; StateValues probs = null; ModelCheckerResult res = null; // get info from bounded until time = expr.getUpperBound().evaluateDouble(constantValues, null); if (time < 0) { String bound = expr.upperBoundIsStrict() ? "<" + (time + 1) : "<=" + time; throw new PrismException("Invalid bound " + bound + " in bounded until formula"); } // model check operands first b1 = (BitSet) checkExpression(model, expr.getOperand1()); b2 = (BitSet) checkExpression(model, expr.getOperand2()); // compute probabilities // a trivial case: "U<=0" if (time == 0) { // prob is 1 in b2 states, 0 otherwise probs = StateValues.createFromBitSetAsDoubles(model.getNumStates(), b2); } else { res = computeTimeBoundedUntilProbs((CTMC) model, b2, time); probs = StateValues.createFromDoubleArray(res.soln); } return probs; } // Numerical computation functions /** * Compute reachability/until probabilities. * i.e. compute the min/max probability of reaching a state in {@code target}, * while remaining in those in @{code remain}. * @param dtmc The CTMC * @param remain Remain in these states (optional: null means "all") * @param target Target states * @param init Optionally, an initial solution vector (may be overwritten) * @param known Optionally, a set of states for which the exact answer is known * Note: if 'known' is specified (i.e. is non-null, 'init' must also be given and is used for the exact values. */ public ModelCheckerResult computeReachProbs(DTMC dtmc, BitSet remain, BitSet target, double init[], BitSet known) throws PrismException { mainLog.println("Building embedded DTMC..."); DTMC dtmcEmb = ((CTMC) dtmc).buildImplicitEmbeddedDTMC(); return super.computeReachProbs(dtmcEmb, null, target, init, known); } /** * Compute time-bounded until probabilities. * i.e. compute the probability of reaching a state in {@code target}, * within time t, and while remaining in states in @{code remain}. * @param ctmc The CTMC * @param target Target states * @param t Time bound */ public ModelCheckerResult computeTimeBoundedUntilProbs(CTMC ctmc, BitSet target, double t) throws PrismException { return computeTimeBoundedUntilProbs(ctmc, target, t, null); } /** * Compute time-bounded until probabilities. * i.e. compute the probability of reaching a state in {@code target}, * within time t, and while remaining in states in @{code remain}. * @param ctmc The CTMC * @param target Target states * @param t Time bound * @param init Initial solution vector - pass null for default */ public ModelCheckerResult computeTimeBoundedUntilProbs(CTMC ctmc, BitSet target, double t, double init[]) throws PrismException { ModelCheckerResult res = null; int i, n, iters; double soln[], soln2[], tmpsoln[], sum[]; DTMC dtmc; long timer; // Fox-Glynn stuff FoxGlynn fg; int left, right; double q, qt, acc, weights[], totalWeight; // Start bounded probabilistic reachability timer = System.currentTimeMillis(); mainLog.println("Starting time-bounded probabilistic reachability..."); // Store num states n = ctmc.getNumStates(); // Get uniformisation rate; do Fox-Glynn q = ctmc.getDefaultUniformisationRate(); qt = q * t; mainLog.println("\nUniformisation: q.t = " + q + " x " + t + " = " + qt); acc = termCritParam / 8.0; fg = new FoxGlynn(qt, 1e-300, 1e+300, acc); left = fg.getLeftTruncationPoint(); right = fg.getRightTruncationPoint(); if (right < 0) { throw new PrismException("Overflow in Fox-Glynn computation (time bound too big?)"); } weights = fg.getWeights(); totalWeight = fg.getTotalWeight(); for (i = left; i <= right; i++) { weights[i - left] /= totalWeight; } mainLog.println("Fox-Glynn (" + acc + "): left = " + left + ", right = " + right); // Build (implicit) uniformised DTMC dtmc = ctmc.buildImplicitUniformisedDTMC(q); // Create solution vector(s) soln = new double[n]; soln2 = (init == null) ? new double[n] : init; sum = new double[n]; // Initialise solution vectors. Use passed in initial vector, if present if (init != null) { for (i = 0; i < n; i++) soln[i] = soln2[i] = target.get(i) ? 1.0 : init[i]; } else { for (i = 0; i < n; i++) soln[i] = soln2[i] = target.get(i) ? 1.0 : 0.0; } for (i = 0; i < n; i++) sum[i] = 0.0; // If necessary, do 0th element of summation (doesn't require any matrix powers) if (left == 0) for (i = 0; i < n; i++) sum[i] += weights[0] * soln[i]; // Start iterations iters = 1; while (iters <= right) { // Matrix-vector multiply dtmc.mvMult(soln, soln2, target, true); // Swap vectors for next iter tmpsoln = soln; soln = soln2; soln2 = tmpsoln; // Add to sum if (iters >= left) { for (i = 0; i < n; i++) sum[i] += weights[iters - left] * soln[i]; } iters++; } // Finished bounded probabilistic reachability timer = System.currentTimeMillis() - timer; mainLog.print("Time-bounded probabilistic reachability"); mainLog.println(" took " + iters + " iters and " + timer / 1000.0 + " seconds."); // Return results res = new ModelCheckerResult(); res.soln = sum; res.lastSoln = soln2; res.numIters = iters; res.timeTaken = timer / 1000.0; res.timePre = 0.0; return res; } /** * Compute expected reachability rewards. * @param dtmc The CTMC * @param mcRewards The rewards * @param target Target states */ public ModelCheckerResult computeReachRewards(DTMC dtmc, MCRewards mcRewards, BitSet target) throws PrismException { int i, n; // Build embedded DTMC mainLog.println("Building embedded DTMC..."); DTMC dtmcEmb = ((CTMC) dtmc).buildImplicitEmbeddedDTMC(); // Convert rewards n = dtmc.getNumStates(); MCRewardsStateArray rewEmb = new MCRewardsStateArray(n); for (i = 0; i < n; i++) { rewEmb.setStateReward(i, mcRewards.getStateReward(i) * ((CTMC) dtmc).getExitRate(i)); } // Do computation on DTMC return super.computeReachRewards(dtmcEmb, rewEmb, target); } /** * Simple test program. */ public static void main(String args[]) { CTMCModelChecker mc; CTMCSimple ctmc; ModelCheckerResult res; BitSet target; Map labels; try { mc = new CTMCModelChecker(); ctmc = new CTMCSimple(); ctmc.buildFromPrismExplicit(args[0]); //System.out.println(dtmc); labels = mc.loadLabelsFile(args[1]); //System.out.println(labels); target = labels.get(args[2]); if (target == null) throw new PrismException("Unknown label \"" + args[2] + "\""); for (int i = 4; i < args.length; i++) { if (args[i].equals("-nopre")) mc.setPrecomp(false); } res = mc.computeTimeBoundedUntilProbs(ctmc, target, Double.parseDouble(args[3])); System.out.println(res.soln[0]); } catch (PrismException e) { System.out.println(e); } } }