sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

fixed shield handling for MDP Next and BoundedGlobally

tempestpy_adaptions
Lukas Posch 3 years ago
committed by Stefan Pranger
parent
591e63e11e
commit
7cbe2886eb
4 changed files with 62 additions and 48 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. 59
      src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp
  2. 13
      src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
  3. 27
      src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
  4. 3
      src/storm/solver/Multiplier.cpp

59
src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp
View File

@ -63,18 +63,67 @@ namespace storm {
if (lowerBound == 0) {
if(goal.isShieldingTask())
{
multiplier->repeatedMultiplyAndReduceWithChoices(env, goal.direction(), subresult, &b, upperBound, nullptr, choiceValues, transitionMatrix.getRowGroupIndices());
std::vector<storm::storage::SparseMatrix<double>::index_type> rowGroupIndices = transitionMatrix.getRowGroupIndices();
std::vector<storm::storage::SparseMatrix<double>::index_type> reducedRowGroupIndices;
uint sizeChoiceValues = 0;
for(uint counter = 0; counter < maybeStates.size(); counter++) {
if(maybeStates.get(counter)) {
sizeChoiceValues += transitionMatrix.getRowGroupSize(counter);
reducedRowGroupIndices.push_back(rowGroupIndices.at(counter));
}
}
choiceValues = std::vector<ValueType>(sizeChoiceValues, storm::utility::zero<ValueType>());
multiplier->repeatedMultiplyAndReduceWithChoices(env, goal.direction(), subresult, &b, upperBound, nullptr, choiceValues, reducedRowGroupIndices);
// fill up choicesValues for shields
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 (maybeStates.get(state)) {
for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) {
allChoices.at(transitionMatrix.getRowGroupIndices().at(state) + choice) = *choice_it;
}
}
}
choiceValues = allChoices;
} else {
multiplier->repeatedMultiplyAndReduce(env, goal.direction(), subresult, &b, upperBound);
}
} else {
if(goal.isShieldingTask())
{
multiplier->repeatedMultiplyAndReduceWithChoices(env, goal.direction(), subresult, &b, upperBound - lowerBound + 1, nullptr, choiceValues, transitionMatrix.getRowGroupIndices());
std::vector<storm::storage::SparseMatrix<double>::index_type> rowGroupIndices = transitionMatrix.getRowGroupIndices();
std::vector<storm::storage::SparseMatrix<double>::index_type> reducedRowGroupIndices;
uint sizeChoiceValues = 0;
for(uint counter = 0; counter < maybeStates.size(); counter++) {
if(maybeStates.get(counter)) {
sizeChoiceValues += transitionMatrix.getRowGroupSize(counter);
reducedRowGroupIndices.push_back(rowGroupIndices.at(counter));
}
}
choiceValues = std::vector<ValueType>(sizeChoiceValues, storm::utility::zero<ValueType>());
multiplier->repeatedMultiplyAndReduceWithChoices(env, goal.direction(), subresult, &b, upperBound - lowerBound + 1, nullptr, choiceValues, reducedRowGroupIndices);
storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, false);
auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, submatrix);
b = std::vector<ValueType>(b.size(), storm::utility::zero<ValueType>());
multiplier->repeatedMultiplyAndReduceWithChoices(env, goal.direction(), subresult, &b, lowerBound - 1, nullptr, choiceValues, transitionMatrix.getRowGroupIndices());
multiplier->repeatedMultiplyAndReduceWithChoices(env, goal.direction(), subresult, &b, lowerBound - 1, nullptr, choiceValues, reducedRowGroupIndices);
// fill up choicesValues for shields
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 (maybeStates.get(state)) {
for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) {
allChoices.at(transitionMatrix.getRowGroupIndices().at(state) + choice) = *choice_it;
}
}
}
choiceValues = allChoices;
} else {
multiplier->repeatedMultiplyAndReduce(env, goal.direction(), subresult, &b, upperBound - lowerBound + 1);
storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, false);
@ -90,11 +139,7 @@ namespace storm {
storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one<ValueType>());
}
//TODO: check if this works with nullptr as default for resultMaybeStates
if(!resultMaybeStates.empty())
{
resultMaybeStates = maybeStates;
}
return result;
}

13
src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
View File

@ -98,15 +98,13 @@ namespace storm {
storm::modelchecker::helper::SparseNondeterministicStepBoundedHorizonHelper<ValueType> helper;
std::vector<ValueType> numericResult;
//TODO: this does not work with nullptr as defaults for resultMaybeStates and choiceValues
//This works only with empty vectors, no nullptr
storm::storage::BitVector resultMaybeStates;
std::vector<ValueType> choiceValues;
//TODO: check the result for shields
if(checkTask.isShieldingTask()) {
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);
tempest::shields::createShield<ValueType>(std::make_shared<storm::models::sparse::Mdp<ValueType>>(this->getModel()), std::move(choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(resultMaybeStates), storm::storage::BitVector(resultMaybeStates.size(), false));
tempest::shields::createShield<ValueType>(std::make_shared<storm::models::sparse::Mdp<ValueType>>(this->getModel()), std::move(choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(resultMaybeStates), storm::storage::BitVector(resultMaybeStates.size(), true));
} 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);
}
@ -123,8 +121,7 @@ namespace storm {
auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeNextProbabilities(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector());
std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(ret.values)));
if(checkTask.isShieldingTask()) {
//TODO: creating a shield for NEXT does not work
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(), false));
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));
} else if (checkTask.isProduceSchedulersSet() && ret.scheduler) {
result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::move(ret.scheduler));
}
@ -142,7 +139,7 @@ namespace storm {
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());
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.values), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.maybeStates), storm::storage::BitVector(ret.maybeStates.size(), false));
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));
} else if (checkTask.isProduceSchedulersSet() && ret.scheduler) {
result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::move(ret.scheduler));
}
@ -158,7 +155,7 @@ namespace storm {
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());
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.values), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.maybeStates), storm::storage::BitVector(ret.maybeStates.size(), false));
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));
} else if (checkTask.isProduceSchedulersSet() && ret.scheduler) {
result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::move(ret.scheduler));
}

27
src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
View File

@ -671,9 +671,6 @@ namespace storm {
}
}
if (goal.isShieldingTask()) {
STORM_LOG_DEBUG("SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities: Before multiply()");
STORM_LOG_DEBUG(result);
std::vector<ValueType> subResult;
uint sizeChoiceValues = 0;
for(uint counter = 0; counter < qualitativeStateSets.maybeStates.size(); counter++) {
@ -682,21 +679,9 @@ namespace storm {
}
}
STORM_LOG_DEBUG(subResult);
STORM_LOG_DEBUG(choiceValues);
//std::vector<ValueType> b_complete = transitionMatrix.getConstrainedRowGroupSumVector(storm::storage::BitVector(qualitativeStateSets.maybeStates.size(), true), qualitativeStateSets.statesWithProbability1);
submatrix = transitionMatrix.getSubmatrix(true, qualitativeStateSets.maybeStates, qualitativeStateSets.maybeStates, false);
//STORM_LOG_DEBUG(b_complete);
auto sub_multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, submatrix);
sub_multiplier->multiply(env, subResult, &b, choiceValues);
STORM_LOG_DEBUG(choiceValues);
std::vector<ValueType> allChoices = std::vector<ValueType>(transitionMatrix.getRowGroupIndices().at(transitionMatrix.getRowGroupIndices().size() - 1), storm::utility::zero<ValueType>());
auto choice_it = choiceValues.begin();
@ -709,12 +694,6 @@ namespace storm {
}
}
choiceValues = allChoices;
STORM_LOG_DEBUG(choiceValues);
//TODO: fill up choiceValues with Zeros (dimension!)
}
}
}
@ -745,7 +724,6 @@ namespace storm {
statesInPsiMecs.set(stateActionsPair.first, true);
}
}
return computeUntilProbabilities(env, std::move(goal), transitionMatrix, backwardTransitions, psiStates, statesInPsiMecs, qualitative, produceScheduler);
} else {
goal.oneMinus();
@ -1242,10 +1220,7 @@ namespace storm {
STORM_LOG_ASSERT((!produceScheduler && !scheduler) || scheduler->isDeterministicScheduler(), "Expected a deterministic scheduler");
STORM_LOG_ASSERT((!produceScheduler && !scheduler) || scheduler->isMemorylessScheduler(), "Expected a memoryless scheduler");
//TODO: keep nullvector for choiceValues in computeReachabilityRewardsHelper? - nullptr causes ERROR
//std::vector<ValueType> choiceValues = std::vector<ValueType>(transitionMatrix.getRowCount(), storm::utility::zero<ValueType>());
std::vector<ValueType> choiceValues = std::vector<ValueType>();
std::vector<ValueType> choiceValues;
return MDPSparseModelCheckingHelperReturnType<ValueType>(std::move(result), std::move(qualitativeStateSets.maybeStates), std::move(scheduler), std::move(choiceValues));
}

3
src/storm/solver/Multiplier.cpp
View File

@ -74,11 +74,8 @@ namespace storm {
progress.setMaxCount(n);
progress.startNewMeasurement(0);
for (uint64_t i = 0; i < n; ++i) {
multiply(env, x, b, choiceValues);
reduce(env, dir, choiceValues, rowGroupIndices, x);
multiplyAndReduce(env, dir, x, b, x);
if (storm::utility::resources::isTerminate()) {
STORM_LOG_WARN("Aborting after " << i << " of " << n << " multiplications");
break;

Write Preview
Loading…
Cancel
Save