s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

imported patch ex-dtmc-weights-support-negative-rewards.patch

tud-infrastructure-2018-10-12
Joachim Klein 7 years ago
parent
38a64f0406
commit
2ed6c9486e
2 changed files with 89 additions and 35 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 114
      prism/src/explicit/DTMCModelChecker.java
  2. 10
      prism/src/explicit/ProbModelChecker.java

114
prism/src/explicit/DTMCModelChecker.java
View File

@ -43,6 +43,7 @@ import parser.ast.DeclarationIntUnbounded;
import parser.ast.Expression;
import prism.ModelType;
import prism.OptionsIntervalIteration;
import prism.Pair;
import prism.Prism;
import prism.PrismComponent;
import prism.PrismException;
@ -60,6 +61,7 @@ import explicit.LTLModelChecker.LTLProduct;
import explicit.modelviews.DTMCAlteredDistributions;
import explicit.modelviews.MDPFromDTMC;
import explicit.rewards.MCRewards;
import explicit.rewards.MCRewardsPositive;
import explicit.rewards.MDPRewards;
import explicit.rewards.Rewards;
@ -355,6 +357,10 @@ public class DTMCModelChecker extends ProbModelChecker
throw new PrismNotSupportedException("Interval iteration for total rewards is currently not supported");
}
if (mcRewards.hasNegativeRewards()) {
throw new PrismNotSupportedException("Total reward computation in DTMC with negative rewards is currently not supported");
}
// Switch to a supported method, if necessary
if (!(linEqMethod == LinEqMethod.POWER)) {
linEqMethod = LinEqMethod.POWER;
@ -1339,19 +1345,21 @@ public class DTMCModelChecker extends ProbModelChecker
}
/**
* Compute upper bound for maximum expected reward, using the variant specified in the settings.
* Compute upper and/or lower bound for maximum expected reward, using the variant specified in the settings.
* @param dtmc the model
* @param mcRewards the rewards
* @param upper compute upper bound?
* @param lower compute lower bound?
* @param target the target states
* @param unknown the states that are not target or infinity states
* @param inf the infinity states
* @return upper bound on R=?[ F target ] for all states
* @return pair of upper (first) and lower (second) bounds on R=?[ F target ] for all states
*/
double computeReachRewardsUpperBound(DTMC dtmc, MCRewards mcRewards, BitSet target, BitSet unknown, BitSet inf) throws PrismException
Pair<Double,Double> computeReachRewardsBound(DTMC dtmc, MCRewards mcRewards, boolean upper, boolean lower, BitSet target, BitSet unknown, BitSet inf) throws PrismException
{
if (unknown.isEmpty()) {
mainLog.println("Skipping upper bound computation, no unknown states...");
return 0;
mainLog.println("Skipping bound computation, no unknown states...");
return new Pair<Double,Double>(0.0,0.0);
}
// inf and target states become trap states (with self-loops)
@ -1359,21 +1367,47 @@ public class DTMCModelChecker extends ProbModelChecker
trapStates.or(inf);
DTMCAlteredDistributions cleanedDTMC = DTMCAlteredDistributions.addSelfLoops(dtmc, trapStates);
double upperBound = 0.0, lowerBound = 0.0;
if (upper) {
if (mcRewards.hasPositiveRewards()) {
MCRewards mcRewPos = mcRewards.hasNegativeRewards() ? new MCRewardsPositive(mcRewards) : mcRewards;
upperBound = computeReachRewardsBound(cleanedDTMC, mcRewPos, true, target, unknown, inf);
} else {
// no positive rewards: upper bound 0.0 is fine
mainLog.println("Upper bound for expectation: " + upperBound + " (no positive rewards)");
}
}
if (lower) {
if (mcRewards.hasNegativeRewards()) {
// negated and then restricted to positive rewards
MCRewards mcRewPos = new MCRewardsPositive(mcRewards, true);
lowerBound = computeReachRewardsBound(cleanedDTMC, mcRewPos, false, target, unknown, inf);
} else {
// no positive rewards: lower bound 0.0 is fine
mainLog.println("Lower bound for expectation: " + lowerBound + " (no negative rewards)");
}
}
return new Pair<>(upperBound, lowerBound);
}
private double computeReachRewardsBound(DTMC cleanedDTMC, MCRewards mcRewardsPositive, boolean upper, BitSet target, BitSet unknown, BitSet inf) throws PrismException
{
OptionsIntervalIteration iiOptions = OptionsIntervalIteration.from(this);
double upperBound = 0.0;
double bound = 0.0;
String method = null;
switch (iiOptions.getBoundMethod()) {
case VARIANT_1_COARSE:
upperBound = computeReachRewardsUpperBoundVariant1Coarse(cleanedDTMC, mcRewards, target, unknown, inf);
bound = computeReachRewardsUpperBoundVariant1Coarse(cleanedDTMC, mcRewardsPositive, upper, target, unknown, inf);
method = "variant 1, coarse";
break;
case VARIANT_1_FINE:
upperBound = computeReachRewardsUpperBoundVariant1Fine(cleanedDTMC, mcRewards, target, unknown, inf);
bound = computeReachRewardsUpperBoundVariant1Fine(cleanedDTMC, mcRewardsPositive, upper, target, unknown, inf);
method = "variant 1, fine";
break;
case VARIANT_2:
upperBound = computeReachRewardsUpperBoundVariant2(cleanedDTMC, mcRewards, target, unknown, inf);
bound = computeReachRewardsUpperBoundVariant2(cleanedDTMC, mcRewardsPositive, upper, target, unknown, inf);
method = "variant 2";
break;
case DEFAULT:
@ -1385,7 +1419,7 @@ public class DTMCModelChecker extends ProbModelChecker
@Override
public double getStateReward(int s)
{
return mcRewards.getStateReward(s);
return mcRewardsPositive.getStateReward(s);
}
@Override
@ -1418,19 +1452,28 @@ public class DTMCModelChecker extends ProbModelChecker
return false;
}
};
upperBound = DijkstraSweepMPI.computeUpperBound(this, mdp, mdpRewards, target, unknown);
if (!upper) {
mainLog.println("Computing lower bound via upper bound for negated negative rewards...");
}
bound = DijkstraSweepMPI.computeUpperBound(this, mdp, mdpRewards, target, unknown);
method = "Dijkstra Sweep MPI";
break;
}
}
if (method == null) {
throw new PrismException("Unknown upper bound heuristic");
throw new PrismException("Unknown bound heuristic");
}
mainLog.println("Upper bound for expectation (" + method + "): " + upperBound);
if (upper) {
mainLog.println("Upper bound for expectation (" + method + "): " + bound);
} else {
// lower bound: we have to negate to get the actual bound
bound = -bound;
mainLog.println("Lower bound for expectation (" + method + "): " + bound);
}
return upperBound;
return bound;
}
/**
@ -1439,18 +1482,19 @@ public class DTMCModelChecker extends ProbModelChecker
* Uses Rs = S, i.e., does not take reachability into account.
* @param dtmc the model
* @param mcRewards the rewards
* @param upper computing an upper bound?
* @param target the target states
* @param unknown the states that are not target or infinity states
* @param inf the infinity states
* @return upper bound on R=?[ F target ] for all states
*/
double computeReachRewardsUpperBoundVariant1Coarse(DTMC dtmc, MCRewards mcRewards, BitSet target, BitSet unknown, BitSet inf) throws PrismException
double computeReachRewardsUpperBoundVariant1Coarse(DTMC dtmc, MCRewards mcRewards, boolean upper, BitSet target, BitSet unknown, BitSet inf) throws PrismException
{
double[] boundsOnExpectedVisits = new double[dtmc.getNumStates()];
int[] Ct = new int[dtmc.getNumStates()];
StopWatch timer = new StopWatch(getLog());
timer.start("computing an upper bound for expected reward");
timer.start("computing " + (upper ? "an upper" : "a lower") +" bound for expected reward");
SCCInfo sccs = SCCComputer.computeTopologicalOrdering(this, dtmc, true, null);
BitSet trivial = new BitSet();
@ -1523,7 +1567,7 @@ public class DTMCModelChecker extends ProbModelChecker
timer.stop();
if (OptionsIntervalIteration.from(this).isBoundComputationVerbose()) {
mainLog.println("Upper bound for max expectation computation (variant 1, coarse):");
mainLog.println((upper ? "Upper" : "Lower") +" bound for max expectation computation (variant 1, coarse):");
mainLog.println("p = " + p);
mainLog.println("q = " + q);
mainLog.println("|Ct| = " + Arrays.toString(Ct));
@ -1531,7 +1575,7 @@ public class DTMCModelChecker extends ProbModelChecker
}
if (!Double.isFinite(upperBound)) {
throw new PrismException("Problem computing an upper bound for the expectation, did not get finite result");
throw new PrismException("Problem computing " + (upper ? "an upper" : "a lower") +" bound for the expectation, did not get finite result");
}
return upperBound;
@ -1543,12 +1587,13 @@ public class DTMCModelChecker extends ProbModelChecker
* Uses Rs = S, i.e., does not take reachability into account.
* @param dtmc the model
* @param mcRewards the rewards
* @param upper computing an upper bound?
* @param target the target states
* @param unknown the states that are not target or infinity states
* @param inf the infinity states
* @return upper bound on R=?[ F target ] for all states
*/
double computeReachRewardsUpperBoundVariant1Fine(DTMC dtmc, MCRewards mcRewards, BitSet target, BitSet unknown, BitSet inf) throws PrismException
double computeReachRewardsUpperBoundVariant1Fine(DTMC dtmc, MCRewards mcRewards, boolean upper, BitSet target, BitSet unknown, BitSet inf) throws PrismException
{
double[] boundsOnExpectedVisits = new double[dtmc.getNumStates()];
double[] qt = new double[dtmc.getNumStates()];
@ -1556,7 +1601,7 @@ public class DTMCModelChecker extends ProbModelChecker
int[] Ct = new int[dtmc.getNumStates()];
StopWatch timer = new StopWatch(getLog());
timer.start("computing an upper bound for expected reward");
timer.start("computing " + (upper ? "an upper" : "a lower") + " bound for expected reward");
SCCInfo sccs = SCCComputer.computeTopologicalOrdering(this, dtmc, true, null);
BitSet trivial = new BitSet();
@ -1628,7 +1673,7 @@ public class DTMCModelChecker extends ProbModelChecker
timer.stop();
if (OptionsIntervalIteration.from(this).isBoundComputationVerbose()) {
mainLog.println("Upper bound for max expectation computation (variant 1, fine):");
mainLog.println((upper ? "Upper" : "Lower") + " bound for max expectation computation (variant 1, fine):");
mainLog.println("pt = " + Arrays.toString(pt));
mainLog.println("qt = " + Arrays.toString(qt));
mainLog.println("|Ct| = " + Arrays.toString(Ct));
@ -1636,7 +1681,7 @@ public class DTMCModelChecker extends ProbModelChecker
}
if (!Double.isFinite(upperBound)) {
throw new PrismException("Problem computing an upper bound for the expectation, did not get finite result");
throw new PrismException("Problem computing " + (upper ? "an upper" : "lower") + " bound for the expectation, did not get finite result");
}
return upperBound;
@ -1648,18 +1693,19 @@ public class DTMCModelChecker extends ProbModelChecker
* Uses Rs = S, i.e., does not take reachability into account.
* @param dtmc the model
* @param mcRewards the rewards
* @param upper computing an upper bound?
* @param target the target states
* @param unknown the states that are not target or infinity states
* @param inf the infinity states
* @return upper bound on R=?[ F target ] for all states
*/
double computeReachRewardsUpperBoundVariant2(DTMC dtmc, MCRewards mcRewards, BitSet target, BitSet unknown, BitSet inf) throws PrismException
double computeReachRewardsUpperBoundVariant2(DTMC dtmc, MCRewards mcRewards, boolean upper, BitSet target, BitSet unknown, BitSet inf) throws PrismException
{
double[] dt = new double[dtmc.getNumStates()];
double[] boundsOnExpectedVisits = new double[dtmc.getNumStates()];
StopWatch timer = new StopWatch(getLog());
timer.start("computing an upper bound for expected reward");
timer.start("computing " + (upper ? "an upper" : "a lower") + " bound for expected reward");
SCCInfo sccs = SCCComputer.computeTopologicalOrdering(this, dtmc, true, unknown::get);
@ -1717,13 +1763,13 @@ public class DTMCModelChecker extends ProbModelChecker
timer.stop();
if (OptionsIntervalIteration.from(this).isBoundComputationVerbose()) {
mainLog.println("Upper bound for max expectation computation (variant 2):");
mainLog.println((upper ? "Upper" : "Lower") + " bound for max expectation computation (variant 2):");
mainLog.println("d_t = " + Arrays.toString(dt));
mainLog.println("ζ* = " + Arrays.toString(boundsOnExpectedVisits));
}
if (!Double.isFinite(upperBound)) {
throw new PrismException("Problem computing an upper bound for the expectation, did not get finite result");
throw new PrismException("Problem computing " + (upper ? "an upper" : "a lower") + " bound for the expectation, did not get finite result");
}
return upperBound;
@ -2067,20 +2113,22 @@ public class DTMCModelChecker extends ProbModelChecker
OptionsIntervalIteration iiOptions = OptionsIntervalIteration.from(this);
double upperBound;
Double upperBound = null, lowerBound = null;
if (iiOptions.hasManualUpperBound()) {
upperBound = iiOptions.getManualUpperBound();
getLog().printWarning("Upper bound for interval iteration manually set to " + upperBound);
} else {
upperBound = computeReachRewardsUpperBound(dtmc, mcRewards, target, unknown, inf);
}
double lowerBound;
if (iiOptions.hasManualLowerBound()) {
lowerBound = iiOptions.getManualLowerBound();
getLog().printWarning("Lower bound for interval iteration manually set to " + lowerBound);
} else {
lowerBound = 0.0;
}
if (upperBound == null || lowerBound == null) {
Pair<Double, Double> computedBounds = computeReachRewardsBound(dtmc, mcRewards, upperBound==null, lowerBound==null, target, unknown, inf);
if (upperBound == null)
upperBound = computedBounds.first;
if (lowerBound == null)
lowerBound = computedBounds.second;
}
// Start value iteration

10
prism/src/explicit/ProbModelChecker.java
View File

@ -49,6 +49,7 @@ import parser.type.TypeDouble;
import parser.type.TypePathBool;
import parser.type.TypePathDouble;
import prism.IntegerBound;
import prism.ModelType;
import prism.OpRelOpBound;
import prism.Prism;
import prism.PrismComponent;
@ -872,7 +873,9 @@ public class ProbModelChecker extends NonProbModelChecker
// Build rewards
int r = expr.getRewardStructIndexByIndexObject(modelInfo, constantValues);
mainLog.println("Building reward structure...");
Rewards rewards = constructRewards(model, r);
// we allow negative (and positive) rewards for DTMCs
boolean allowNegative = model.getModelType() == ModelType.DTMC;
Rewards rewards = constructRewards(model, r, allowNegative);
// Compute rewards
StateValues rews = checkRewardFormula(model, rewards, expr.getExpression(), minMax, statesOfInterest);
@ -1276,7 +1279,10 @@ public class ProbModelChecker extends NonProbModelChecker
throw new PrismNotSupportedException("Exporting state rewards in the requested format is currently not supported by the explicit engine");
}
Rewards modelRewards = constructRewards(model, r);
// we allow negative (and positive) rewards for DTMCs
boolean allowNegative = model.getModelType() == ModelType.DTMC;
Rewards modelRewards = constructRewards(model, r, allowNegative);
switch (model.getModelType()) {
case DTMC:
case CTMC:

Write Preview
Loading…
Cancel
Save