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

Replaced the StateDuplicator with the new memory structure product

tempestpy_adaptions
TimQu 8 years ago
parent
c5f29c3761
commit
b7aaf1957e
3 changed files with 122 additions and 91 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. 2
      src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp
  2. 199
      src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp
  3. 12
      src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.h

2
src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp
View File

@ -108,7 +108,7 @@ namespace storm {
result.toMS = this->model.getTransitionMatrix().getSubmatrix(true, result.states, this->model.getMarkovianStates(), createMS);
result.toPS = this->model.getTransitionMatrix().getSubmatrix(true, result.states, probabilisticStates, false);
STORM_LOG_ASSERT(result.getNumberOfStates() == result.states.getNumberOfSetBits() && result.getNumberOfStates() == result.toMS.getRowGroupCount() && result.getNumberOfStates() == result.toPS.getRowGroupCount(), "Invalid state count for subsystem");
STORM_LOG_ASSERT(result.getNumberOfChoices() == result.choices.getNumberOfSetBits() && result.getNumberOfChoices() == result.toMS.getRowCount() && result.getNumberOfChoices() == result.toPS.getRowCount(), "Invalid state count for subsystem");
STORM_LOG_ASSERT(result.getNumberOfChoices() == result.choices.getNumberOfSetBits() && result.getNumberOfChoices() == result.toMS.getRowCount() && result.getNumberOfChoices() == result.toPS.getRowCount(), "Invalid choice count for subsystem");
result.weightedRewardVector.resize(result.getNumberOfChoices());
storm::utility::vector::selectVectorValues(result.weightedRewardVector, result.choices, weightedRewardVector);

199
src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp
View File

@ -6,7 +6,8 @@
#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/storage/MaximalEndComponentDecomposition.h"
#include "storm/transformer/StateDuplicator.h"
#include "storm/storage/memorystructure/MemoryStructureBuilder.h"
#include "storm/storage/memorystructure/SparseModelMemoryProduct.h"
#include "storm/transformer/SubsystemBuilder.h"
#include "storm/utility/macros.h"
#include "storm/utility/vector.h"
@ -26,12 +27,12 @@ namespace storm {
result.newToOldStateIndexMapping = storm::utility::vector::buildVectorForRange(0, originalModel.getNumberOfStates());
//Invoke preprocessing on the individual objectives
for(auto const& subFormula : originalFormula.getSubformulas()){
for (auto const& subFormula : originalFormula.getSubformulas()){
STORM_LOG_INFO("Preprocessing objective " << *subFormula<< ".");
result.objectives.emplace_back();
PcaaObjective<ValueType>& currentObjective = result.objectives.back();
currentObjective.originalFormula = subFormula;
if(currentObjective.originalFormula->isOperatorFormula()) {
if (currentObjective.originalFormula->isOperatorFormula()) {
preprocessOperatorFormula(currentObjective.originalFormula->asOperatorFormula(), result, currentObjective);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the subformula " << *subFormula << " of " << originalFormula << " because it is not supported");
@ -40,11 +41,11 @@ namespace storm {
// Set the query type. In case of a quantitative query, also set the index of the objective to be optimized.
// Note: If there are only zero (or one) objectives left, we should not consider a pareto query!
storm::storage::BitVector objectivesWithoutThreshold(result.objectives.size());
for(uint_fast64_t objIndex = 0; objIndex < result.objectives.size(); ++objIndex) {
for (uint_fast64_t objIndex = 0; objIndex < result.objectives.size(); ++objIndex) {
objectivesWithoutThreshold.set(objIndex, !result.objectives[objIndex].threshold);
}
uint_fast64_t numOfObjectivesWithoutThreshold = objectivesWithoutThreshold.getNumberOfSetBits();
if(numOfObjectivesWithoutThreshold == 0) {
if (numOfObjectivesWithoutThreshold == 0) {
result.queryType = ReturnType::QueryType::Achievability;
} else if (numOfObjectivesWithoutThreshold == 1) {
result.queryType = ReturnType::QueryType::Quantitative;
@ -64,9 +65,9 @@ namespace storm {
//Get actions to which a positive or negative reward is assigned for at least one objective
result.actionsWithPositiveReward = storm::storage::BitVector(result.preprocessedModel.getNumberOfChoices(), false);
result.actionsWithNegativeReward = storm::storage::BitVector(result.preprocessedModel.getNumberOfChoices(), false);
for(uint_fast64_t objIndex = 0; objIndex < result.objectives.size(); ++objIndex) {
if(!result.objectives[objIndex].upperTimeBound) {
if(result.objectives[objIndex].rewardsArePositive) {
for (uint_fast64_t objIndex = 0; objIndex < result.objectives.size(); ++objIndex) {
if (!result.objectives[objIndex].upperTimeBound) {
if (result.objectives[objIndex].rewardsArePositive) {
result.actionsWithPositiveReward |= ~storm::utility::vector::filterZero(result.preprocessedModel.getRewardModel(result.objectives[objIndex].rewardModelName).getTotalRewardVector(result.preprocessedModel.getTransitionMatrix()));
} else {
result.actionsWithNegativeReward |= ~storm::utility::vector::filterZero(result.preprocessedModel.getRewardModel(result.objectives[objIndex].rewardModelName).getTotalRewardVector(result.preprocessedModel.getTransitionMatrix()));
@ -77,7 +78,7 @@ namespace storm {
// Analyze End components and ensure reward finiteness.
// Note that this is only necessary if there is at least one objective with no upper time bound
for (auto const& obj : result.objectives) {
if(!obj.upperTimeBound) {
if (!obj.upperTimeBound) {
auto backwardTransitions = result.preprocessedModel.getBackwardTransitions();
analyzeEndComponents(result, backwardTransitions);
ensureRewardFiniteness(result, backwardTransitions);
@ -89,13 +90,36 @@ namespace storm {
template<typename SparseModelType>
void SparsePcaaPreprocessor<SparseModelType>::updatePreprocessedModel(ReturnType& result, SparseModelType& newPreprocessedModel, std::vector<uint_fast64_t>& newToOldStateIndexMapping) {
result.preprocessedModel = std::move(newPreprocessedModel);
// the given newToOldStateIndexMapping reffers to the indices of the former preprocessedModel as 'old indices'
for(auto & preprocessedModelStateIndex : newToOldStateIndexMapping){
// the given newToOldStateIndexMapping refers to the indices of the former preprocessedModel as 'old indices'
for (auto & preprocessedModelStateIndex : newToOldStateIndexMapping){
preprocessedModelStateIndex = result.newToOldStateIndexMapping[preprocessedModelStateIndex];
}
result.newToOldStateIndexMapping = std::move(newToOldStateIndexMapping);
}
template<typename SparseModelType>
void SparsePcaaPreprocessor<SparseModelType>::addMemoryToPreprocessedModel(ReturnType& result, storm::storage::MemoryStructure& memory) {
storm::storage::SparseModelMemoryProduct<ValueType> product = memory.product(result.preprocessedModel);
auto newModel = product.build();
// update the newToOldStateIndexMapping
std::vector<uint_fast64_t> updatedMapping;
updatedMapping.reserve(newModel->getNumberOfStates());
for (uint_fast64_t oldState = 0; oldState < result.preprocessedModel.getNumberOfStates(); ++oldState) {
for (uint_fast64_t memoryState = 0; memoryState < memory.getNumberOfStates(); ++memoryState) {
uint_fast64_t const& newState = product.getResultState(oldState, memoryState);
// Check if the state actually exists in the new model
if (newState < newModel->getNumberOfStates()) {
assert(newState == updatedMapping.size());
updatedMapping.push_back(result.newToOldStateIndexMapping[oldState]);
}
}
}
result.preprocessedModel = std::move(dynamic_cast<SparseModelType&>(*newModel));
result.newToOldStateIndexMapping = std::move(updatedMapping);
}
template<typename SparseModelType>
void SparsePcaaPreprocessor<SparseModelType>::preprocessOperatorFormula(storm::logic::OperatorFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective) {
@ -110,7 +134,7 @@ namespace storm {
currentObjective.rewardsArePositive = true;
bool formulaMinimizes = false;
if(formula.hasBound()) {
if (formula.hasBound()) {
currentObjective.threshold = formula.template getThresholdAs<ValueType>();
currentObjective.thresholdIsStrict = storm::logic::isStrict(formula.getBound().comparisonType);
//Note that we minimize for upper bounds since we are looking for the EXISTENCE of a satisfying scheduler
@ -120,25 +144,25 @@ namespace storm {
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Current objective " << formula << " does not specify whether to minimize or maximize");
}
if(formulaMinimizes) {
if (formulaMinimizes) {
// We negate all the values so we can consider the maximum for this objective
// Thus, all objectives will be maximized.
currentObjective.rewardsArePositive = false;
currentObjective.toOriginalValueTransformationFactor = -storm::utility::one<ValueType>();
}
if(formula.isProbabilityOperatorFormula()){
if (formula.isProbabilityOperatorFormula()){
preprocessProbabilityOperatorFormula(formula.asProbabilityOperatorFormula(), result, currentObjective);
} else if(formula.isRewardOperatorFormula()){
} else if (formula.isRewardOperatorFormula()){
preprocessRewardOperatorFormula(formula.asRewardOperatorFormula(), result, currentObjective);
} else if(formula.isTimeOperatorFormula()){
} else if (formula.isTimeOperatorFormula()){
preprocessTimeOperatorFormula(formula.asTimeOperatorFormula(), result, currentObjective);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the objective " << formula << " because it is not supported");
}
// Transform the threshold for the preprocessed Model
if(currentObjective.threshold) {
if (currentObjective.threshold) {
currentObjective.threshold = (currentObjective.threshold.get() - currentObjective.toOriginalValueTransformationOffset) / currentObjective.toOriginalValueTransformationFactor;
}
}
@ -146,13 +170,13 @@ namespace storm {
template<typename SparseModelType>
void SparsePcaaPreprocessor<SparseModelType>::preprocessProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective) {
if(formula.getSubformula().isUntilFormula()){
if (formula.getSubformula().isUntilFormula()){
preprocessUntilFormula(formula.getSubformula().asUntilFormula(), result, currentObjective);
} else if(formula.getSubformula().isBoundedUntilFormula()){
} else if (formula.getSubformula().isBoundedUntilFormula()){
preprocessBoundedUntilFormula(formula.getSubformula().asBoundedUntilFormula(), result, currentObjective);
} else if(formula.getSubformula().isGloballyFormula()){
} else if (formula.getSubformula().isGloballyFormula()){
preprocessGloballyFormula(formula.getSubformula().asGloballyFormula(), result, currentObjective);
} else if(formula.getSubformula().isEventuallyFormula()){
} else if (formula.getSubformula().isEventuallyFormula()){
preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), result, currentObjective);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported.");
@ -165,11 +189,11 @@ namespace storm {
STORM_LOG_THROW((formula.hasRewardModelName() && result.preprocessedModel.hasRewardModel(formula.getRewardModelName()))
|| result.preprocessedModel.hasUniqueRewardModel(), storm::exceptions::InvalidPropertyException, "The reward model is not unique and the formula " << formula << " does not specify a reward model.");
if(formula.getSubformula().isEventuallyFormula()){
if (formula.getSubformula().isEventuallyFormula()){
preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), result, currentObjective, formula.getOptionalRewardModelName());
} else if(formula.getSubformula().isCumulativeRewardFormula()) {
} else if (formula.getSubformula().isCumulativeRewardFormula()) {
preprocessCumulativeRewardFormula(formula.getSubformula().asCumulativeRewardFormula(), result, currentObjective, formula.getOptionalRewardModelName());
} else if(formula.getSubformula().isTotalRewardFormula()) {
} else if (formula.getSubformula().isTotalRewardFormula()) {
preprocessTotalRewardFormula(result, currentObjective, formula.getOptionalRewardModelName());
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported.");
@ -181,7 +205,7 @@ namespace storm {
// Time formulas are only supported for Markov automata
STORM_LOG_THROW(result.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton), storm::exceptions::InvalidPropertyException, "Time operator formulas are only supported for Markov automata.");
if(formula.getSubformula().isEventuallyFormula()){
if (formula.getSubformula().isEventuallyFormula()){
preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), result, currentObjective);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported.");
@ -190,37 +214,39 @@ namespace storm {
template<typename SparseModelType>
void SparsePcaaPreprocessor<SparseModelType>::preprocessUntilFormula(storm::logic::UntilFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective) {
CheckTask<storm::logic::Formula, ValueType> phiTask(formula.getLeftSubformula());
CheckTask<storm::logic::Formula, ValueType> psiTask(formula.getRightSubformula());
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> mc(result.preprocessedModel);
STORM_LOG_THROW(mc.canHandle(phiTask) && mc.canHandle(psiTask), storm::exceptions::InvalidPropertyException, "The subformulas of " << formula << " should be propositional.");
storm::storage::BitVector phiStates = mc.check(phiTask)->asExplicitQualitativeCheckResult().getTruthValuesVector();
storm::storage::BitVector psiStates = mc.check(psiTask)->asExplicitQualitativeCheckResult().getTruthValuesVector();
if(!(psiStates & result.preprocessedModel.getInitialStates()).empty() && !currentObjective.lowerTimeBound) {
// Create a memory structure that stores whether a PhiState or a PsiState has already been reached
storm::storage::MemoryStructureBuilder builder(2);
// Get a unique label that is not already present in the model
std::string memoryLabel = "obj" + std::to_string(result.objectives.size());
while (result.preprocessedModel.hasLabel(memoryLabel)) memoryLabel = "_" + memoryLabel;
builder.setLabel(0, memoryLabel);
auto negatedLeftSubFormula = std::make_shared<storm::logic::UnaryBooleanStateFormula>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, formula.getLeftSubformula().asSharedPointer());
auto targetFormula = std::make_shared<storm::logic::BinaryBooleanStateFormula>(storm::logic::BinaryBooleanStateFormula::OperatorType::Or, negatedLeftSubFormula, formula.getRightSubformula().asSharedPointer());
builder.setTransition(0, 0, std::make_shared<storm::logic::UnaryBooleanStateFormula>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, targetFormula));
builder.setTransition(0, 1, targetFormula);
builder.setTransition(1, 1, std::make_shared<storm::logic::BooleanLiteralFormula>(true));
storm::storage::MemoryStructure memory = builder.build();
addMemoryToPreprocessedModel(result, memory);
// build stateAction reward vector that gives (one*transitionProbability) reward whenever a transition leads from a memoryLabel-state to a psiState
storm::storage::BitVector const& statesWithMemoryLabel = result.preprocessedModel.getStates(memoryLabel);
if ((statesWithMemoryLabel & result.preprocessedModel.getInitialStates()).empty() && !currentObjective.lowerTimeBound) {
// The probability is always one as the initial state is a target state.
// For this special case, the transformation to an expected reward objective fails.
// We could handle this with further preprocessing steps but as this case is boring anyway, we simply reject the input.
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The Probability for the objective " << currentObjective.originalFormula << " is always one as the rhs of the until formula is true in the initial state. Please omit this objective.");
}
auto duplicatorResult = storm::transformer::StateDuplicator<SparseModelType>::transform(result.preprocessedModel, ~phiStates | psiStates);
updatePreprocessedModel(result, *duplicatorResult.model, duplicatorResult.newToOldStateIndexMapping);
storm::storage::BitVector newPsiStates(result.preprocessedModel.getNumberOfStates(), false);
for(auto const& oldPsiState : psiStates){
//note that psiStates are always located in the second copy
newPsiStates.set(duplicatorResult.secondCopyOldToNewStateIndexMapping[oldPsiState], true);
// We could handle this with further preprocessing steps but as this case is trivial anyway, we reject the input.
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The Probability for the objective " << *currentObjective.originalFormula << " is always one as the rhs of the until formula is true in the initial state. Please omit this objective.");
}
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> mc(result.preprocessedModel);
storm::storage::BitVector psiStates = mc.check(formula.getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
// build stateAction reward vector that gives (one*transitionProbability) reward whenever a transition leads from the firstCopy to a psiState
std::vector<ValueType> objectiveRewards(result.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero<ValueType>());
for (auto const& firstCopyState : duplicatorResult.firstCopy) {
for (uint_fast64_t row = result.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[firstCopyState]; row < result.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[firstCopyState + 1]; ++row) {
objectiveRewards[row] = result.preprocessedModel.getTransitionMatrix().getConstrainedRowSum(row, newPsiStates);
for (auto const& state : statesWithMemoryLabel) {
for (uint_fast64_t row = result.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state]; row < result.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state + 1]; ++row) {
objectiveRewards[row] = result.preprocessedModel.getTransitionMatrix().getConstrainedRowSum(row, psiStates);
}
}
if(!currentObjective.rewardsArePositive) {
if (!currentObjective.rewardsArePositive) {
storm::utility::vector::scaleVectorInPlace(objectiveRewards, -storm::utility::one<ValueType>());
}
result.preprocessedModel.addRewardModel(currentObjective.rewardModelName, RewardModelType(boost::none, objectiveRewards));
@ -258,43 +284,48 @@ namespace storm {
template<typename SparseModelType>
void SparsePcaaPreprocessor<SparseModelType>::preprocessEventuallyFormula(storm::logic::EventuallyFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective, boost::optional<std::string> const& optionalRewardModelName) {
if(formula.isReachabilityProbabilityFormula()){
if (formula.isReachabilityProbabilityFormula()){
preprocessUntilFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), formula.getSubformula().asSharedPointer()), result, currentObjective);
return;
}
CheckTask<storm::logic::Formula, ValueType> targetTask(formula.getSubformula());
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> mc(result.preprocessedModel);
STORM_LOG_THROW(mc.canHandle(targetTask), storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " should be propositional.");
storm::storage::BitVector targetStates = mc.check(targetTask)->asExplicitQualitativeCheckResult().getTruthValuesVector();
auto duplicatorResult = storm::transformer::StateDuplicator<SparseModelType>::transform(result.preprocessedModel, targetStates);
updatePreprocessedModel(result, *duplicatorResult.model, duplicatorResult.newToOldStateIndexMapping);
// Add a reward model that gives zero reward to the actions of states of the second copy.
// Create a memory structure that stores whether a target state has already been reached
storm::storage::MemoryStructureBuilder builder(2);
// Get a unique label that is not already present in the model
std::string memoryLabel = "obj" + std::to_string(result.objectives.size());
while (result.preprocessedModel.hasLabel(memoryLabel)) memoryLabel = "_" + memoryLabel;
builder.setLabel(0, memoryLabel);
builder.setTransition(0, 0, std::make_shared<storm::logic::UnaryBooleanStateFormula>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, formula.getSubformula().asSharedPointer()));
builder.setTransition(0, 1, formula.getSubformula().asSharedPointer());
builder.setTransition(1, 1, std::make_shared<storm::logic::BooleanLiteralFormula>(true));
storm::storage::MemoryStructure memory = builder.build();
addMemoryToPreprocessedModel(result, memory);
// Add a reward model that only gives reward to states with the memory label
RewardModelType objectiveRewards(boost::none);
if(formula.isReachabilityRewardFormula()) {
if (formula.isReachabilityRewardFormula()) {
storm::storage::BitVector statesWithoutMemoryLabel = ~result.preprocessedModel.getStates(memoryLabel);
objectiveRewards = result.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : "");
objectiveRewards.reduceToStateBasedRewards(result.preprocessedModel.getTransitionMatrix(), false);
if(objectiveRewards.hasStateRewards()) {
storm::utility::vector::setVectorValues(objectiveRewards.getStateRewardVector(), duplicatorResult.secondCopy, storm::utility::zero<ValueType>());
if (objectiveRewards.hasStateRewards()) {
storm::utility::vector::setVectorValues(objectiveRewards.getStateRewardVector(), statesWithoutMemoryLabel, storm::utility::zero<ValueType>());
}
if(objectiveRewards.hasStateActionRewards()) {
for(auto secondCopyState : duplicatorResult.secondCopy) {
std::fill_n(objectiveRewards.getStateActionRewardVector().begin() + result.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[secondCopyState], result.preprocessedModel.getTransitionMatrix().getRowGroupSize(secondCopyState), storm::utility::zero<ValueType>());
if (objectiveRewards.hasStateActionRewards()) {
for (auto state : statesWithoutMemoryLabel) {
std::fill_n(objectiveRewards.getStateActionRewardVector().begin() + result.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state], result.preprocessedModel.getTransitionMatrix().getRowGroupSize(state), storm::utility::zero<ValueType>());
}
}
} else if(formula.isReachabilityTimeFormula() && result.preprocessedModel.isOfType(storm::models::ModelType::MarkovAutomaton)) {
} else if (formula.isReachabilityTimeFormula() && result.preprocessedModel.isOfType(storm::models::ModelType::MarkovAutomaton)) {
objectiveRewards = RewardModelType(std::vector<ValueType>(result.preprocessedModel.getNumberOfStates(), storm::utility::zero<ValueType>()));
storm::utility::vector::setVectorValues(objectiveRewards.getStateRewardVector(), dynamic_cast<storm::models::sparse::MarkovAutomaton<ValueType>*>(&result.preprocessedModel)->getMarkovianStates() & duplicatorResult.firstCopy, storm::utility::one<ValueType>());
storm::utility::vector::setVectorValues(objectiveRewards.getStateRewardVector(), dynamic_cast<storm::models::sparse::MarkovAutomaton<ValueType>*>(&result.preprocessedModel)->getMarkovianStates() & result.preprocessedModel.getStates(memoryLabel), storm::utility::one<ValueType>());
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The formula " << formula << " neither considers reachability probabilities nor reachability rewards " << (result.preprocessedModel.isOfType(storm::models::ModelType::MarkovAutomaton) ? "nor reachability time" : "") << ". This is not supported.");
}
if(!currentObjective.rewardsArePositive){
if(objectiveRewards.hasStateRewards()) {
if (!currentObjective.rewardsArePositive){
if (objectiveRewards.hasStateRewards()) {
storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateRewardVector(), -storm::utility::one<ValueType>());
}
if(objectiveRewards.hasStateActionRewards()) {
if (objectiveRewards.hasStateActionRewards()) {
storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateActionRewardVector(), -storm::utility::one<ValueType>());
}
}
@ -309,11 +340,11 @@ namespace storm {
RewardModelType objectiveRewards = result.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : "");
objectiveRewards.reduceToStateBasedRewards(result.preprocessedModel.getTransitionMatrix(), false);
if(!currentObjective.rewardsArePositive){
if(objectiveRewards.hasStateRewards()) {
if (!currentObjective.rewardsArePositive){
if (objectiveRewards.hasStateRewards()) {
storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateRewardVector(), -storm::utility::one<ValueType>());
}
if(objectiveRewards.hasStateActionRewards()) {
if (objectiveRewards.hasStateActionRewards()) {
storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateActionRewardVector(), -storm::utility::one<ValueType>());
}
}
@ -324,11 +355,11 @@ namespace storm {
void SparsePcaaPreprocessor<SparseModelType>::preprocessTotalRewardFormula(ReturnType& result, PcaaObjective<ValueType>& currentObjective, boost::optional<std::string> const& optionalRewardModelName) {
RewardModelType objectiveRewards = result.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : "");
objectiveRewards.reduceToStateBasedRewards(result.preprocessedModel.getTransitionMatrix(), false);
if(!currentObjective.rewardsArePositive){
if(objectiveRewards.hasStateRewards()) {
if (!currentObjective.rewardsArePositive){
if (objectiveRewards.hasStateRewards()) {
storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateRewardVector(), -storm::utility::one<ValueType>());
}
if(objectiveRewards.hasStateActionRewards()) {
if (objectiveRewards.hasStateActionRewards()) {
storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateActionRewardVector(), -storm::utility::one<ValueType>());
}
}
@ -344,9 +375,9 @@ namespace storm {
auto mecDecomposition = storm::storage::MaximalEndComponentDecomposition<ValueType>(result.preprocessedModel.getTransitionMatrix(), backwardTransitions);
STORM_LOG_ASSERT(!mecDecomposition.empty(), "Empty maximal end component decomposition.");
ecs.reserve(mecDecomposition.size());
for(auto& mec : mecDecomposition) {
for(auto const& stateActionsPair : mec) {
for(auto const& action : stateActionsPair.second) {
for (auto& mec : mecDecomposition) {
for (auto const& stateActionsPair : mec) {
for (auto const& action : stateActionsPair.second) {
result.ecActions.set(action);
}
}
@ -356,17 +387,17 @@ namespace storm {
result.possiblyRecurrentStates = storm::storage::BitVector(result.preprocessedModel.getNumberOfStates(), false);
storm::storage::BitVector neutralActions = ~(result.actionsWithNegativeReward | result.actionsWithPositiveReward);
storm::storage::BitVector statesInCurrentECWithNeutralAction(result.preprocessedModel.getNumberOfStates(), false);
for(uint_fast64_t ecIndex = 0; ecIndex < ecs.size(); ++ecIndex) { //we will insert new ecs in the vector (thus no iterators for the loop)
for (uint_fast64_t ecIndex = 0; ecIndex < ecs.size(); ++ecIndex) { //we will insert new ecs in the vector (thus no iterators for the loop)
bool currentECIsNeutral = true;
for(auto const& stateActionsPair : ecs[ecIndex]) {
for (auto const& stateActionsPair : ecs[ecIndex]) {
bool stateHasNeutralActionWithinEC = false;
for(auto const& action : stateActionsPair.second) {
for (auto const& action : stateActionsPair.second) {
stateHasNeutralActionWithinEC |= neutralActions.get(action);
}
statesInCurrentECWithNeutralAction.set(stateActionsPair.first, stateHasNeutralActionWithinEC);
currentECIsNeutral &= stateHasNeutralActionWithinEC;
}
if(currentECIsNeutral) {
if (currentECIsNeutral) {
result.possiblyRecurrentStates |= statesInCurrentECWithNeutralAction;
}else{
// Check if the ec contains neutral sub ecs. This is done by adding the subECs to our list of ECs
@ -374,7 +405,7 @@ namespace storm {
statesInCurrentECWithNeutralAction = storm::utility::graph::performProb0E(result.preprocessedModel.getTransitionMatrix(), result.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), backwardTransitions,statesInCurrentECWithNeutralAction, ~statesInCurrentECWithNeutralAction);
auto subECs = storm::storage::MaximalEndComponentDecomposition<ValueType>(result.preprocessedModel.getTransitionMatrix(), backwardTransitions, statesInCurrentECWithNeutralAction);
ecs.reserve(ecs.size() + subECs.size());
for(auto& ec : subECs){
for (auto& ec : subECs){
ecs.push_back(std::move(ec));
}
}
@ -390,7 +421,7 @@ namespace storm {
storm::storage::BitVector statesReachingNegativeRewardsFinitelyOftenForSomeScheduler = storm::utility::graph::performProb1E(result.preprocessedModel.getTransitionMatrix(), result.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), backwardTransitions, storm::storage::BitVector(result.preprocessedModel.getNumberOfStates(), true), result.possiblyRecurrentStates);
STORM_LOG_THROW(!(statesReachingNegativeRewardsFinitelyOftenForSomeScheduler & result.preprocessedModel.getInitialStates()).empty(), storm::exceptions::InvalidPropertyException, "Infinite Rewards: For every scheduler, the induced reward for one or more of the objectives that minimize rewards is infinity.");
if(!statesReachingNegativeRewardsFinitelyOftenForSomeScheduler.full()) {
if (!statesReachingNegativeRewardsFinitelyOftenForSomeScheduler.full()) {
// Remove the states that for any scheduler have one objective with infinite expected reward.
auto subsystemBuilderResult = storm::transformer::SubsystemBuilder<SparseModelType>::transform(result.preprocessedModel, statesReachingNegativeRewardsFinitelyOftenForSomeScheduler, storm::storage::BitVector(result.preprocessedModel.getNumberOfChoices(), true));
updatePreprocessedModel(result, *subsystemBuilderResult.model, subsystemBuilderResult.newToOldStateIndexMapping);

12
src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.h
View File

@ -6,6 +6,7 @@
#include "storm/logic/Formulas.h"
#include "storm/storage/BitVector.h"
#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessorReturnType.h"
#include "storm/storage/memorystructure/MemoryStructure.h"
namespace storm {
namespace modelchecker {
@ -29,12 +30,6 @@ namespace storm {
static ReturnType preprocess(SparseModelType const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula);
private:
/*!
* Initializes the returned Information
* @param originalModel The considered model
* @param originalFormula the considered formula
*/
static ReturnType initializeResult(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel);
/*!
* Updates the preprocessed model stored in the given result to the given model.
@ -43,6 +38,11 @@ namespace storm {
*/
static void updatePreprocessedModel(ReturnType& result, SparseModelType& newPreprocessedModel, std::vector<uint_fast64_t>& newToOldStateIndexMapping);
/*!
* Updates the preprocessed model stored in the given result to the product of the model and the given memory structure.
*/
static void addMemoryToPreprocessedModel(ReturnType& result, storm::storage::MemoryStructure& memory);
/*!
* Apply the neccessary preprocessing for the given formula.
* @param formula the current (sub)formula

Write Preview
Loading…
Cancel
Save