diff --git a/prism/src/explicit/STPGModelChecker.java b/prism/src/explicit/STPGModelChecker.java index 85fc5bd54..0309751ff 100644 --- a/prism/src/explicit/STPGModelChecker.java +++ b/prism/src/explicit/STPGModelChecker.java @@ -41,6 +41,7 @@ import prism.PrismFileLog; import prism.PrismLog; import prism.PrismNotSupportedException; +import prism.PrismSettings; import prism.PrismUtils; import strat.BoundedRewardDeterministicStrategy; import strat.MemorylessDeterministicStrategy; @@ -495,6 +496,12 @@ protected ModelCheckerResult computeReachProbsValIter(STPG stpg, BitSet no, BitS if (verbosity >= 1) mainLog.println("Starting value iteration (" + (min1 ? "min" : "max") + (min2 ? "min" : "max") + ")..."); + ExportIterations iterationsExport = null; + if (settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)) { + String description = (min1 ? "Min" : "Max") + "/" + (min1 ? "Min" : "Max"); + iterationsExport = new ExportIterations("Explicit STPG ReachProbs value iteration (" + description + ")"); + } + // Store num states n = stpg.getNumStates(); @@ -546,6 +553,10 @@ protected ModelCheckerResult computeReachProbsValIter(STPG stpg, BitSet no, BitS } } + if (iterationsExport != null) { + iterationsExport.exportVector(soln); + } + // Start iterations iters = 0; done = false; @@ -559,6 +570,10 @@ protected ModelCheckerResult computeReachProbsValIter(STPG stpg, BitSet no, BitS tmpsoln = soln; soln = soln2; soln2 = tmpsoln; + + if (iterationsExport != null) { + iterationsExport.exportVector(soln); + } } // Finished value iteration @@ -568,6 +583,10 @@ protected ModelCheckerResult computeReachProbsValIter(STPG stpg, BitSet no, BitS mainLog.println(" took " + iters + " iterations and " + timer / 1000.0 + " seconds."); } + if (iterationsExport != null) { + iterationsExport.close(); + } + // Non-convergence is an error (usually) if (!done && errorOnNonConverge) { String msg = "Iterative method did not converge within " + iters + " iterations."; @@ -623,6 +642,12 @@ protected ModelCheckerResult computeReachProbsGaussSeidel(STPG stpg, BitSet no, if (verbosity >= 1) mainLog.println("Starting value iteration (" + (min1 ? "min" : "max") + (min2 ? "min" : "max") + ")..."); + ExportIterations iterationsExport = null; + if (settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)) { + String description = (min1 ? "Min" : "Max") + "/" + (min1 ? "Min" : "Max"); + iterationsExport = new ExportIterations("Explicit STPG ReachProbs Gauss Seidel (" + description + ")"); + } + // Store num states n = stpg.getNumStates(); @@ -654,6 +679,10 @@ protected ModelCheckerResult computeReachProbsGaussSeidel(STPG stpg, BitSet no, if (known != null) unknown.andNot(known); + if (iterationsExport != null) { + iterationsExport.exportVector(soln); + } + // Start iterations iters = 0; done = false; @@ -663,6 +692,10 @@ protected ModelCheckerResult computeReachProbsGaussSeidel(STPG stpg, BitSet no, maxDiff = stpg.mvMultGSMinMax(soln, min1, min2, unknown, false, termCrit == TermCrit.ABSOLUTE); // Check termination done = maxDiff < termCritParam; + + if (iterationsExport != null) { + iterationsExport.exportVector(soln); + } } // Finished Gauss-Seidel @@ -672,6 +705,10 @@ protected ModelCheckerResult computeReachProbsGaussSeidel(STPG stpg, BitSet no, mainLog.println(" took " + iters + " iterations and " + timer / 1000.0 + " seconds."); } + if (iterationsExport != null) { + iterationsExport.close(); + } + // Non-convergence is an error (usually) if (!done && errorOnNonConverge) { String msg = "Iterative method did not converge within " + iters + " iterations."; @@ -963,6 +1000,12 @@ protected ModelCheckerResult computeReachRewardsValIter(STPG stpg, STPGRewards r if (verbosity >= 1) mainLog.println("Starting value iteration (" + (min1 ? "min" : "max") + (min2 ? "min" : "max") + ")..."); + ExportIterations iterationsExport = null; + if (settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)) { + String description = (min1 ? "Min" : "Max") + "/" + (min1 ? "Min" : "Max"); + iterationsExport = new ExportIterations("Explicit STPG ReachRewards value iteration (" + description + ")"); + } + // Store num states n = stpg.getNumStates(); @@ -1017,6 +1060,10 @@ protected ModelCheckerResult computeReachRewardsValIter(STPG stpg, STPGRewards r } } + if (iterationsExport != null) { + iterationsExport.exportVector(soln); + } + // Start iterations iters = 0; done = false; @@ -1040,6 +1087,11 @@ protected ModelCheckerResult computeReachRewardsValIter(STPG stpg, STPGRewards r tmpsoln = soln; soln = soln2; soln2 = tmpsoln; + + + if (iterationsExport != null) { + iterationsExport.exportVector(soln); + } } // Finished value iteration @@ -1049,6 +1101,10 @@ protected ModelCheckerResult computeReachRewardsValIter(STPG stpg, STPGRewards r mainLog.println(" took " + iters + " iterations and " + timer / 1000.0 + " seconds."); } + if (iterationsExport != null) { + iterationsExport.close(); + } + // Print adversary if (genAdv) { PrismLog out = new PrismFileLog(exportAdvFilename); @@ -1200,7 +1256,12 @@ public ModelCheckerResult computeReachRewardsInfinity(STPG stpg, STPGRewards rew // Compute the value when rewards are nonzero switch (solnMethod) { case VALUE_ITERATION: - res = computeReachRewardsValIter(stpg, rewards, target, inf, min1, min2, init, known); + try { + ExportIterations.setDefaultFilename("iterations-upper-bound.html"); + res = computeReachRewardsValIter(stpg, rewards, target, inf, min1, min2, init, known); + } finally { + ExportIterations.resetDefaultFilename(); + } break; default: throw new PrismException("Unknown STPG solution method " + solnMethod); @@ -1590,7 +1651,13 @@ public ModelCheckerResult computeReachRewardsZero(STPG stpg, STPGRewards rewards // Get the rich man's strategy and its values // Start with computing optimal probabilities to reach the final state - ModelCheckerResult mcrprob = computeReachProbs(stpg, target, min1, min2); + ModelCheckerResult mcrprob; + try { + ExportIterations.setDefaultFilename("iterations-rich-man-probs.html"); + mcrprob = computeReachProbs(stpg, target, min1, min2); + } finally { + ExportIterations.resetDefaultFilename(); + } // Next, reweigh the rewards and make sure that only optimal actions are // taken @@ -1653,8 +1720,15 @@ public ModelCheckerResult computeReachRewardsZero(STPG stpg, STPGRewards rewards throw new PrismException("To compute expected reward I need to modify the reward structure. But I don't know how to modify" + rewards.getClass().getName()); } + // Next, compute the value for the rich man's strategy. - ModelCheckerResult mcrrich = computeReachRewards(stpg, rewardsRestricted, target, min1, min2, init, known, R_CUMULATIVE); + ModelCheckerResult mcrrich; + try { + ExportIterations.setDefaultFilename("iterations-rich-man-rewards.html"); + mcrrich = computeReachRewards(stpg, rewardsRestricted, target, min1, min2, init, known, R_CUMULATIVE); + } finally { + ExportIterations.resetDefaultFilename(); + } //System.out.println("maximal rews for rich man's strategy: " + Arrays.toString(mcrrich.soln)); // TODO generate rich man strategy. @@ -1725,6 +1799,12 @@ public ModelCheckerResult computeReachRewardsZero(STPG stpg, STPGRewards rewards // chosen by rews boolean done = false; + ExportIterations iterationsExport = null; + if (settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)) { + ExportIterations.setDefaultFilename("iterations-reach-rewards-zero-" + x + ".html"); + iterationsExport = new ExportIterations("ReachRewardsZero, reward level " + x); + } + double difference = 0; do { difference = 0; @@ -1787,7 +1867,10 @@ public ModelCheckerResult computeReachRewardsZero(STPG stpg, STPGRewards rewards difference = cDif; rews[0][s] = stateRew; - + } + + if (iterationsExport != null) { + iterationsExport.exportVector(rews[0]); } } while (difference > 10e-6); // TODO some smarter convergence @@ -1809,6 +1892,11 @@ public ModelCheckerResult computeReachRewardsZero(STPG stpg, STPGRewards rewards } } + if (iterationsExport != null) { + iterationsExport.exportVector(rews[0]); + iterationsExport.close(); + } + // shift the array double[] tmpRews = rews[kSize - 1]; for (i = kSize - 1; i >= 1; i--) {