Skip to content

STPGModelChecker iteration export #3

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
kleinj wants to merge 1 commit into
base: master
Choose a base branch
from
Open

STPGModelChecker iteration export #3

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
96 changes: 92 additions & 4 deletions prism/src/explicit/STPGModelChecker.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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();

Expand Down Expand Up @@ -546,6 +553,10 @@ protected ModelCheckerResult computeReachProbsValIter(STPG stpg, BitSet no, BitS
}
}

if (iterationsExport != null) {
iterationsExport.exportVector(soln);
}

// Start iterations
iters = 0;
done = false;
Expand All @@ -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
Expand All @@ -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.";
Expand Down Expand Up @@ -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();

Expand Down Expand Up @@ -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;
Expand All @@ -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
Expand All @@ -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.";
Expand Down Expand Up @@ -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();

Expand Down Expand Up @@ -1017,6 +1060,10 @@ protected ModelCheckerResult computeReachRewardsValIter(STPG stpg, STPGRewards r
}
}

if (iterationsExport != null) {
iterationsExport.exportVector(soln);
}

// Start iterations
iters = 0;
done = false;
Expand All @@ -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
Expand All @@ -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);
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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
Expand All @@ -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--) {
Expand Down