diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
index 6ed39870f..dfc23481d 100644
--- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
+++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
@@ -108,6 +108,7 @@ namespace storm {
} else {
numericResult = helper.compute(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictLowerBound<uint64_t>(), pathFormula.getNonStrictUpperBound<uint64_t>(), checkTask.getHint(), resultMaybeStates, choiceValues);
}
+ STORM_LOG_DEBUG(numericResult);
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
}
}
@@ -119,6 +120,7 @@ namespace storm {
std::unique_ptr<CheckResult> subResultPointer = this->check(env, pathFormula.getSubformula());
ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeNextProbabilities(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector());
+ STORM_LOG_DEBUG(ret.values);
std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(ret.values)));
if(checkTask.isShieldingTask()) {
tempest::shields::createShield<ValueType>(std::make_shared<storm::models::sparse::Mdp<ValueType>>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.maybeStates), storm::storage::BitVector(ret.maybeStates.size(), true));
@@ -137,6 +139,7 @@ namespace storm {
ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet(), checkTask.getHint());
+ STORM_LOG_DEBUG(ret.values);
std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(ret.values)));
if(checkTask.isShieldingTask()) {
tempest::shields::createShield<ValueType>(std::make_shared<storm::models::sparse::Mdp<ValueType>>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.maybeStates), storm::storage::BitVector(ret.maybeStates.size(), true));
@@ -153,9 +156,11 @@ namespace storm {
std::unique_ptr<CheckResult> subResultPointer = this->check(env, pathFormula.getSubformula());
ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeGloballyProbabilities(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet());
+ STORM_LOG_DEBUG(ret.values);
std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(ret.values)));
if(checkTask.isShieldingTask()) {
- tempest::shields::createShield<ValueType>(std::make_shared<storm::models::sparse::Mdp<ValueType>>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.maybeStates), storm::storage::BitVector(ret.maybeStates.size(), true));
+ STORM_LOG_DEBUG(ret.choiceValues);
+ tempest::shields::createShield<ValueType>(std::make_shared<storm::models::sparse::Mdp<ValueType>>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(),subResult.getTruthValuesVector(), storm::storage::BitVector(ret.maybeStates.size(), true));
} else if (checkTask.isProduceSchedulersSet() && ret.scheduler) {
result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::move(ret.scheduler));
}
diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
index c80b5647f..11f3bcaca 100644
--- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
+++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
@@ -603,7 +603,7 @@ namespace storm {
// We need to identify the maybe states (states which have a probability for satisfying the until formula
// that is strictly between 0 and 1) and the states that satisfy the formula with probablity 1 and 0, respectively.
QualitativeStateSetsUntilProbabilities qualitativeStateSets = getQualitativeStateSetsUntilProbabilities(goal, transitionMatrix, backwardTransitions, phiStates, psiStates, hint);
-
+
STORM_LOG_INFO("Preprocessing: " << qualitativeStateSets.statesWithProbability1.getNumberOfSetBits() << " states with probability 1, " << qualitativeStateSets.statesWithProbability0.getNumberOfSetBits() << " with probability 0 (" << qualitativeStateSets.maybeStates.getNumberOfSetBits() << " states remaining).");
// Set values of resulting vector that are known exactly.
@@ -621,14 +621,14 @@ namespace storm {
// create multiplier and execute the calculation for 1 additional step
auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, transitionMatrix);
- uint sizeChoiceValues = 0;
+ uint sizeMaybeStateChoiceValues = 0;
for(uint counter = 0; counter < qualitativeStateSets.maybeStates.size(); counter++) {
if(qualitativeStateSets.maybeStates.get(counter)) {
- sizeChoiceValues += transitionMatrix.getRowGroupSize(counter);
+ sizeMaybeStateChoiceValues += transitionMatrix.getRowGroupSize(counter);
}
}
- std::vector<ValueType> choiceValues = std::vector<ValueType>(sizeChoiceValues, storm::utility::zero<ValueType>());
+ std::vector<ValueType> maybeStateChoiceValues = std::vector<ValueType>(sizeMaybeStateChoiceValues, storm::utility::zero<ValueType>());
// Check whether we need to compute exact probabilities for some states.
if (qualitative || maybeStatesNotRelevant || !goal.isShieldingTask()) {
@@ -681,19 +681,27 @@ namespace storm {
submatrix = transitionMatrix.getSubmatrix(true, qualitativeStateSets.maybeStates, qualitativeStateSets.maybeStates, false);
auto sub_multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, submatrix);
- sub_multiplier->multiply(env, subResult, &b, choiceValues);
-
- std::vector<ValueType> allChoices = std::vector<ValueType>(transitionMatrix.getRowGroupIndices().at(transitionMatrix.getRowGroupIndices().size() - 1), storm::utility::zero<ValueType>());
- auto choice_it = choiceValues.begin();
- for(uint state = 0; state < transitionMatrix.getRowGroupIndices().size() - 1; state++) {
- uint rowGroupSize = transitionMatrix.getRowGroupIndices().at(state + 1) - transitionMatrix.getRowGroupIndices().at(state);
- if (qualitativeStateSets.maybeStates.get(state)) {
- for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) {
- allChoices.at(transitionMatrix.getRowGroupIndices().at(state) + choice) = *choice_it;
- }
- }
- }
- choiceValues = allChoices;
+ sub_multiplier->multiply(env, subResult, &b, maybeStateChoiceValues);
+
+ }
+ }
+ }
+
+ std::vector<ValueType> choiceValues = std::vector<ValueType>(transitionMatrix.getRowGroupIndices().at(transitionMatrix.getRowGroupIndices().size() - 1), storm::utility::zero<ValueType>());
+ auto choice_it = maybeStateChoiceValues.begin();
+ for(uint state = 0; state < transitionMatrix.getRowGroupIndices().size() - 1; state++) {
+ uint rowGroupSize = transitionMatrix.getRowGroupIndices().at(state + 1) - transitionMatrix.getRowGroupIndices().at(state);
+ if (qualitativeStateSets.maybeStates.get(state)) {
+ for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) {
+ choiceValues.at(transitionMatrix.getRowGroupIndices().at(state) + choice) = *choice_it;
+ }
+ } else if (qualitativeStateSets.statesWithProbability0.get(state)) {
+ for(uint choice = 0; choice < rowGroupSize; choice++) {
+ choiceValues.at(transitionMatrix.getRowGroupIndices().at(state) + choice) = 0;
+ }
+ } else if (qualitativeStateSets.statesWithProbability1.get(state)) {
+ for(uint choice = 0; choice < rowGroupSize; choice++) {
+ choiceValues.at(transitionMatrix.getRowGroupIndices().at(state) + choice) = 1;
}
}
}