From b267394a2c88fc64c61563d708166acaed4b731e Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@web.de>
Date: Sat, 9 Jul 2016 16:52:11 +0200
Subject: [PATCH] fixed the case where an objective is satisfied at the initial
state. correctly added support for lower time bounds
Former-commit-id: 4d13d5de1b6bb27cf2e6bcfc256dd7045363ab70
---
...rseMaMultiObjectiveWeightVectorChecker.cpp | 71 ++++++-----
...seMdpMultiObjectiveWeightVectorChecker.cpp | 75 ++++++++---
.../helper/SparseMultiObjectiveHelper.cpp | 4 +-
.../SparseMultiObjectivePostprocessor.cpp | 12 +-
.../SparseMultiObjectivePreprocessor.cpp | 117 ++++++++++++------
.../helper/SparseMultiObjectivePreprocessor.h | 23 ++--
.../SparseMultiObjectivePreprocessorData.h | 18 +--
...parseMultiObjectiveWeightVectorChecker.cpp | 13 +-
src/transformer/StateDuplicator.h | 21 ++--
...parseMdpMultiObjectiveModelCheckerTest.cpp | 42 +++++++
10 files changed, 270 insertions(+), 126 deletions(-)
diff --git a/src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.cpp b/src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.cpp
index 03fdaf37d..7fd8b8769 100644
--- a/src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.cpp
+++ b/src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.cpp
@@ -80,6 +80,7 @@ namespace storm {
performMSStep(MS, PS, consideredObjectives);
if(currentEpoch % 1000 == 0) {
STORM_LOG_DEBUG(currentEpoch << " digitized time steps left. Current weighted value is " << PS.weightedSolutionVector[0]);
+ std::cout << std::endl << currentEpoch << " digitized time steps left. Current weighted value is " << PS.weightedSolutionVector[0] << std::endl;
}
--currentEpoch;
} else {
@@ -256,41 +257,43 @@ namespace storm {
void SparseMaMultiObjectiveWeightVectorChecker<SparseMaModelType>::digitizeTimeBounds(TimeBoundMap& lowerTimeBounds, TimeBoundMap& upperTimeBounds, VT const& digitizationConstant) {
VT const maxRate = this->data.preprocessedModel.getMaximalExitRate();
- storm::storage::BitVector boundedObjectives = ~this->unboundedObjectives;
- for(uint_fast64_t objIndex : boundedObjectives) {
- boost::optional<VT> objLowerBound, objUpperBound;
- if(this->data.objectives[objIndex].timeBounds->which() == 0) {
- objUpperBound = storm::utility::convertNumber<VT>(boost::get<uint_fast64_t>(this->data.objectives[objIndex].timeBounds.get()));
- } else {
- auto const& pair = boost::get<std::pair<double, double>>(this->data.objectives[objIndex].timeBounds.get());
- if(!storm::utility::isZero(pair.first)) {
- objLowerBound = storm::utility::convertNumber<VT>(pair.first);
+ for(uint_fast64_t objIndex = 0; objIndex < this->data.objectives.size(); ++objIndex) {
+ auto const& obj = this->data.objectives[objIndex];
+ if(obj.timeBounds) {
+ boost::optional<VT> objLowerBound, objUpperBound;
+ if(obj.timeBounds->which() == 0) {
+ objUpperBound = storm::utility::convertNumber<VT>(boost::get<uint_fast64_t>(obj.timeBounds.get()));
+ } else {
+ auto const& pair = boost::get<std::pair<double, double>>(obj.timeBounds.get());
+ if(!storm::utility::isZero(pair.first)) {
+ objLowerBound = storm::utility::convertNumber<VT>(pair.first);
+ }
+ objUpperBound = storm::utility::convertNumber<VT>(pair.second);
+ }
+ if(objLowerBound) {
+ uint_fast64_t digitizedBound = storm::utility::convertNumber<uint_fast64_t>((*objLowerBound)/digitizationConstant);
+ auto timeBoundIt = lowerTimeBounds.insert(std::make_pair(digitizedBound, storm::storage::BitVector(this->data.objectives.size(), false))).first;
+ timeBoundIt->second.set(objIndex);
+ VT digitizationError = storm::utility::one<VT>();
+ digitizationError -= std::exp(-maxRate * (*objLowerBound)) * storm::utility::pow(storm::utility::one<VT>() + maxRate * digitizationConstant, digitizedBound);
+ this->offsetsToLowerBound[objIndex] = -digitizationError;
+
+ } else {
+ this->offsetsToLowerBound[objIndex] = storm::utility::zero<VT>();
}
- objUpperBound = storm::utility::convertNumber<VT>(pair.second);
- }
- if(objLowerBound) {
- uint_fast64_t digitizedBound = storm::utility::convertNumber<uint_fast64_t>((*objLowerBound)/digitizationConstant);
- auto timeBoundIt = lowerTimeBounds.insert(std::make_pair(digitizedBound, storm::storage::BitVector(this->data.objectives.size(), false))).first;
- timeBoundIt->second.set(objIndex);
- VT digitizationError = storm::utility::one<VT>();
- digitizationError -= std::exp(-maxRate * (*objLowerBound)) * storm::utility::pow(storm::utility::one<VT>() + maxRate * digitizationConstant, digitizedBound);
- this->offsetsToLowerBound[objIndex] = -digitizationError;
- } else {
- this->offsetsToLowerBound[objIndex] = storm::utility::zero<VT>();
- }
-
- if(objUpperBound) {
- uint_fast64_t digitizedBound = storm::utility::convertNumber<uint_fast64_t>((*objUpperBound)/digitizationConstant);
- auto timeBoundIt = upperTimeBounds.insert(std::make_pair(digitizedBound, storm::storage::BitVector(this->data.objectives.size(), false))).first;
- timeBoundIt->second.set(objIndex);
- VT digitizationError = storm::utility::one<VT>();
- digitizationError -= std::exp(-maxRate * (*objUpperBound)) * storm::utility::pow(storm::utility::one<VT>() + maxRate * digitizationConstant, digitizedBound);
- this->offsetsToUpperBound[objIndex] = digitizationError;
- } else {
- this->offsetsToUpperBound[objIndex] = storm::utility::zero<VT>();
+ if(objUpperBound) {
+ uint_fast64_t digitizedBound = storm::utility::convertNumber<uint_fast64_t>((*objUpperBound)/digitizationConstant);
+ auto timeBoundIt = upperTimeBounds.insert(std::make_pair(digitizedBound, storm::storage::BitVector(this->data.objectives.size(), false))).first;
+ timeBoundIt->second.set(objIndex);
+ VT digitizationError = storm::utility::one<VT>();
+ digitizationError -= std::exp(-maxRate * (*objUpperBound)) * storm::utility::pow(storm::utility::one<VT>() + maxRate * digitizationConstant, digitizedBound);
+ this->offsetsToUpperBound[objIndex] = digitizationError;
+ } else {
+ this->offsetsToUpperBound[objIndex] = storm::utility::zero<VT>();
+ }
+ STORM_LOG_ASSERT(this->offsetsToUpperBound[objIndex] - this->offsetsToLowerBound[objIndex] <= this->maximumLowerUpperBoundGap, "Precision not sufficient.");
}
- STORM_LOG_ASSERT(this->offsetsToUpperBound[objIndex] - this->offsetsToLowerBound[objIndex] <= this->maximumLowerUpperBoundGap, "Precision not sufficient.");
}
}
@@ -374,12 +377,14 @@ namespace storm {
// check whether the linEqSolver needs to be updated, i.e., whether the scheduler has changed
if(newOptimalChoices != optimalChoicesAtCurrentEpoch) {
- std::cout << "Scheduler changed!";
+ std::cout << "X";
optimalChoicesAtCurrentEpoch.swap(newOptimalChoices);
linEq.solver = nullptr;
storm::storage::SparseMatrix<ValueType> linEqMatrix = PS.toPS.selectRowsFromRowGroups(optimalChoicesAtCurrentEpoch, true);
linEqMatrix.convertToEquationSystem();
linEq.solver = linEq.factory.create(std::move(linEqMatrix));
+ } else {
+ std::cout << " ";
}
for(auto objIndex : consideredObjectives) {
PS.toMS.multiplyWithVector(MS.objectiveSolutionVectors[objIndex], PS.auxChoiceValues);
diff --git a/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectiveWeightVectorChecker.cpp b/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectiveWeightVectorChecker.cpp
index 476775f60..fecec0071 100644
--- a/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectiveWeightVectorChecker.cpp
+++ b/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectiveWeightVectorChecker.cpp
@@ -27,26 +27,68 @@ namespace storm {
std::vector<uint_fast64_t> optimalChoicesInCurrentEpoch(this->data.preprocessedModel.getNumberOfStates());
std::vector<ValueType> choiceValues(weightedRewardVector.size());
std::vector<ValueType> temporaryResult(this->data.preprocessedModel.getNumberOfStates());
+ std::vector<ValueType> zeroReward(weightedRewardVector.size(), storm::utility::zero<ValueType>());
// Get for each occurring timeBound the indices of the objectives with that bound.
- std::map<uint_fast64_t, storm::storage::BitVector, std::greater<uint_fast64_t>> timeBounds;
- storm::storage::BitVector boundedObjectives = ~this->unboundedObjectives;
- for(uint_fast64_t objIndex : boundedObjectives) {
- uint_fast64_t timeBound = boost::get<uint_fast64_t>(this->data.objectives[objIndex].timeBounds.get());
- auto timeBoundIt = timeBounds.insert(std::make_pair(timeBound, storm::storage::BitVector(this->data.objectives.size(), false))).first;
- timeBoundIt->second.set(objIndex);
- // There is no error for the values of these objectives.
- this->offsetsToLowerBound[objIndex] = storm::utility::zero<ValueType>();
- this->offsetsToUpperBound[objIndex] = storm::utility::zero<ValueType>();
+ std::map<uint_fast64_t, storm::storage::BitVector, std::greater<uint_fast64_t>> lowerTimeBounds;
+ std::map<uint_fast64_t, storm::storage::BitVector, std::greater<uint_fast64_t>> upperTimeBounds;
+ for(uint_fast64_t objIndex = 0; objIndex < this->data.objectives.size(); ++objIndex) {
+ auto const& obj = this->data.objectives[objIndex];
+ if(obj.timeBounds) {
+ boost::optional<uint_fast64_t> objLowerBound, objUpperBound;
+ if(obj.timeBounds->which() == 0) {
+ objUpperBound = boost::get<uint_fast64_t>(obj.timeBounds.get());
+ } else {
+ auto const& pair = boost::get<std::pair<double, double>>(obj.timeBounds.get());
+ if(!storm::utility::isZero(pair.first)) {
+ objLowerBound = storm::utility::convertNumber<uint_fast64_t>(pair.first);
+ STORM_LOG_WARN_COND(storm::utility::isZero(pair.first - (*objLowerBound)), "Rounded non-integral bound " << pair.first << " to " << *objLowerBound << ".");
+ }
+ objUpperBound = storm::utility::convertNumber<uint_fast64_t>(pair.second);
+ STORM_LOG_WARN_COND(storm::utility::isZero(pair.second - (*objUpperBound)), "Rounded non-integral bound " << pair.second << " to " << *objUpperBound << ".");
+ }
+ if(objLowerBound) {
+ auto timeBoundIt = lowerTimeBounds.insert(std::make_pair(*objLowerBound, storm::storage::BitVector(this->data.objectives.size(), false))).first;
+ timeBoundIt->second.set(objIndex);
+ }
+ if(objUpperBound) {
+ auto timeBoundIt = upperTimeBounds.insert(std::make_pair(*objUpperBound, storm::storage::BitVector(this->data.objectives.size(), false))).first;
+ timeBoundIt->second.set(objIndex);
+ }
+ // There is no error for the values of these objectives.
+ this->offsetsToLowerBound[objIndex] = storm::utility::zero<ValueType>();
+ this->offsetsToUpperBound[objIndex] = storm::utility::zero<ValueType>();
+ }
}
+
+ // Stores the objectives for which we need to compute values in the current time epoch.
storm::storage::BitVector consideredObjectives = this->unboundedObjectives;
- auto timeBoundIt = timeBounds.begin();
- for(uint_fast64_t currentEpoch = timeBoundIt->first; currentEpoch > 0; --currentEpoch) {
- if(timeBoundIt != timeBounds.end() && currentEpoch == timeBoundIt->first) {
- consideredObjectives |= timeBoundIt->second;
- for(auto objIndex : timeBoundIt->second) {
+
+ // Stores objectives for which the current epoch passed their lower bound
+ storm::storage::BitVector lowerBoundViolatedObjectives(consideredObjectives.size(), false);
+
+ auto lowerTimeBoundIt = lowerTimeBounds.begin();
+ auto upperTimeBoundIt = upperTimeBounds.begin();
+ uint_fast64_t currentEpoch = std::max(lowerTimeBounds.empty() ? 0 : lowerTimeBoundIt->first - 1, upperTimeBounds.empty() ? 0 : upperTimeBoundIt->first); // consider lowerBound - 1 since we are interested in the first epoch that passes the bound
+
+ while(currentEpoch > 0) {
+ //For lower time bounds we need to react when the currentEpoch passed the bound
+ // Hence, we substract 1 from the lower time bounds.
+ if(lowerTimeBoundIt != lowerTimeBounds.end() && currentEpoch == lowerTimeBoundIt->first - 1) {
+ lowerBoundViolatedObjectives |= lowerTimeBoundIt->second;
+ for(auto objIndex : lowerTimeBoundIt->second) {
+ // No more reward is earned for this objective.
+ storm::utility::vector::addScaledVector(weightedRewardVector, this->discreteActionRewards[objIndex], -weightVector[objIndex]);
+ }
+ ++lowerTimeBoundIt;
+ }
+
+ if(upperTimeBoundIt != upperTimeBounds.end() && currentEpoch == upperTimeBoundIt->first) {
+ consideredObjectives |= upperTimeBoundIt->second;
+ for(auto objIndex : upperTimeBoundIt->second) {
+ // This objective now plays a role in the weighted sum
storm::utility::vector::addScaledVector(weightedRewardVector, this->discreteActionRewards[objIndex], weightVector[objIndex]);
}
- ++timeBoundIt;
+ ++upperTimeBoundIt;
}
// Get values and scheduler for weighted sum of objectives
@@ -58,7 +100,7 @@ namespace storm {
// TODO we could compute the result for one of the objectives from the weighted result, the given weight vector, and the remaining objective results.
for(auto objIndex : consideredObjectives) {
std::vector<ValueType>& objectiveResult = this->objectiveResults[objIndex];
- std::vector<ValueType> objectiveRewards = this->discreteActionRewards[objIndex];
+ std::vector<ValueType> const& objectiveRewards = lowerBoundViolatedObjectives.get(objIndex) ? zeroReward : this->discreteActionRewards[objIndex];
auto rowGroupIndexIt = this->data.preprocessedModel.getTransitionMatrix().getRowGroupIndices().begin();
auto optimalChoiceIt = optimalChoicesInCurrentEpoch.begin();
for(ValueType& stateValue : temporaryResult){
@@ -72,6 +114,7 @@ namespace storm {
}
objectiveResult.swap(temporaryResult);
}
+ --currentEpoch;
}
}
diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp
index a369f1565..1c5145a20 100644
--- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp
+++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp
@@ -47,8 +47,8 @@ namespace storm {
return true;
}
for(auto const& preprocessorResult : preprocessorData.solutionsFromPreprocessing) {
- if(preprocessorResult == PreprocessorData::PreprocessorObjectiveSolution::False ||
- preprocessorResult == PreprocessorData::PreprocessorObjectiveSolution::Undefined) {
+ if(preprocessorResult.first == PreprocessorData::PreprocessorObjectiveSolution::False ||
+ preprocessorResult.first == PreprocessorData::PreprocessorObjectiveSolution::Undefined) {
return true;
}
}
diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp
index 9437bf189..0bfea1603 100644
--- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp
+++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp
@@ -54,7 +54,7 @@ namespace storm {
//Incorporate the results from prerpocessing
for(uint_fast64_t subformulaIndex = 0; subformulaIndex < preprocessorData.originalFormula.getNumberOfSubformulas(); ++subformulaIndex) {
- switch(preprocessorData.solutionsFromPreprocessing[subformulaIndex]) {
+ switch(preprocessorData.solutionsFromPreprocessing[subformulaIndex].first) {
case PreprocessorData::PreprocessorObjectiveSolution::None:
// Nothing to be done
break;
@@ -92,7 +92,7 @@ namespace storm {
//Incorporate the results from prerpocessing
boost::optional<ValueType> preprocessorNumericalResult;
for(uint_fast64_t subformulaIndex = 0; subformulaIndex < preprocessorData.originalFormula.getNumberOfSubformulas(); ++subformulaIndex) {
- switch(preprocessorData.solutionsFromPreprocessing[subformulaIndex]) {
+ switch(preprocessorData.solutionsFromPreprocessing[subformulaIndex].first) {
case PreprocessorData::PreprocessorObjectiveSolution::None:
// Nothing to be done
break;
@@ -101,9 +101,9 @@ namespace storm {
case PreprocessorData::PreprocessorObjectiveSolution::True:
// Nothing to be done
break;
- case PreprocessorData::PreprocessorObjectiveSolution::Zero:
+ case PreprocessorData::PreprocessorObjectiveSolution::Numerical:
STORM_LOG_ASSERT(!preprocessorNumericalResult, "There are multiple numerical results obtained in preprocessing");
- preprocessorNumericalResult = storm::utility::zero<ValueType>();
+ preprocessorNumericalResult = preprocessorData.solutionsFromPreprocessing[subformulaIndex].second;
break;
case PreprocessorData::PreprocessorObjectiveSolution::Unbounded:
STORM_LOG_ASSERT(!preprocessorNumericalResult, "There are multiple numerical results obtained in preprocessing");
@@ -144,7 +144,7 @@ namespace storm {
//Issue a warning for objectives that have been solved in preprocessing
for(uint_fast64_t subformulaIndex = 0; subformulaIndex < preprocessorData.originalFormula.getNumberOfSubformulas(); ++subformulaIndex) {
- switch(preprocessorData.solutionsFromPreprocessing[subformulaIndex]) {
+ switch(preprocessorData.solutionsFromPreprocessing[subformulaIndex].first) {
case PreprocessorData::PreprocessorObjectiveSolution::None:
// Nothing to be done
break;
@@ -153,7 +153,7 @@ namespace storm {
case PreprocessorData::PreprocessorObjectiveSolution::True:
// Nothing to be done
break;
- case PreprocessorData::PreprocessorObjectiveSolution::Zero:
+ case PreprocessorData::PreprocessorObjectiveSolution::Numerical:
STORM_LOG_WARN("The result of the objective " << preprocessorData.originalFormula.getSubformula(subformulaIndex) << " was obtained in preprocessing and will not be incorporated in the check result. Objective Result is zero.");
break;
case PreprocessorData::PreprocessorObjectiveSolution::Unbounded:
diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp
index 01b5c1f9f..0e87c9dbf 100644
--- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp
+++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp
@@ -44,28 +44,8 @@ namespace storm {
data.preprocessedModel.removeRewardModel(rewModel);
}
- assertRewardFiniteness(data);
-
- // set solution for objectives for which there are no rewards left
- for(uint_fast64_t objIndex = 0; objIndex < data.objectives.size(); ++objIndex) {
- if(data.solutionsFromPreprocessing[objIndex] == PreprocessorData::PreprocessorObjectiveSolution::None &&
- data.preprocessedModel.getRewardModel(data.objectives[objIndex].rewardModelName).isAllZero()) {
- if(data.objectives[objIndex].threshold) {
- if(storm::utility::zero<ValueType>() > *data.objectives[objIndex].threshold ||
- (!data.objectives[objIndex].thresholdIsStrict && storm::utility::zero<ValueType>() >= *data.objectives[objIndex].threshold) ){
- data.solutionsFromPreprocessing[objIndex] = PreprocessorData::PreprocessorObjectiveSolution::True;
- } else {
- data.solutionsFromPreprocessing[objIndex] = PreprocessorData::PreprocessorObjectiveSolution::False;
- }
- } else {
- data.solutionsFromPreprocessing[objIndex] = PreprocessorData::PreprocessorObjectiveSolution::Zero;
- }
- }
- }
-
- // Only keep the objectives for which we have no solution yet
- storm::storage::BitVector objWithNoSolution = storm::utility::vector::filter<typename PreprocessorData::PreprocessorObjectiveSolution>(data.solutionsFromPreprocessing, [&] (typename PreprocessorData::PreprocessorObjectiveSolution const& value) -> bool { return value == PreprocessorData::PreprocessorObjectiveSolution::None; });
- data.objectives = storm::utility::vector::filterVector(data.objectives, objWithNoSolution);
+ ensureRewardFiniteness(data);
+ handleObjectivesWithSolutionFromPreprocessing(data);
// Set the query type. In case of a numerical 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!
@@ -87,6 +67,16 @@ namespace storm {
return data;
}
+ template<typename SparseModelType>
+ void SparseMultiObjectivePreprocessor<SparseModelType>::updatePreprocessedModel(PreprocessorData& data, SparseModelType& newPreprocessedModel, std::vector<uint_fast64_t>& newToOldStateIndexMapping) {
+ data.preprocessedModel = std::move(newPreprocessedModel);
+ // the given newToOldStateIndexMapping reffers to the indices of the former preprocessedModel as 'old indices'
+ for(auto & preprocessedModelStateIndex : newToOldStateIndexMapping){
+ preprocessedModelStateIndex = data.newToOldStateIndexMapping[preprocessedModelStateIndex];
+ }
+ data.newToOldStateIndexMapping = std::move(newToOldStateIndexMapping);
+ }
+
template<typename SparseModelType>
void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::OperatorFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective) {
@@ -200,6 +190,13 @@ namespace storm {
storm::storage::BitVector phiStates = mc.check(phiTask)->asExplicitQualitativeCheckResult().getTruthValuesVector();
storm::storage::BitVector psiStates = mc.check(psiTask)->asExplicitQualitativeCheckResult().getTruthValuesVector();
+ if(!(psiStates & data.preprocessedModel.getInitialStates()).empty()) {
+ // The probability is always one
+ data.solutionsFromPreprocessing[data.objectives.size()-1].first = PreprocessorData::PreprocessorObjectiveSolution::Numerical;
+ data.solutionsFromPreprocessing[data.objectives.size()-1].second = currentObjective.rewardsArePositive ? storm::utility::one<ValueType>() : -storm::utility::one<ValueType>();
+ return;
+ }
+
auto duplicatorResult = storm::transformer::StateDuplicator<SparseModelType>::transform(data.preprocessedModel, ~phiStates | psiStates);
updatePreprocessedModel(data, *duplicatorResult.model, duplicatorResult.newToOldStateIndexMapping);
@@ -223,9 +220,10 @@ namespace storm {
noIncomingTransitionFromFirstCopyStates = duplicatorResult.gateStates & (~newPsiStates);
}
if((subsystemStates & data.preprocessedModel.getInitialStates()).empty()) {
- data.solutionsFromPreprocessing[data.objectives.size()-1] = PreprocessorData::PreprocessorObjectiveSolution::False;
+ data.solutionsFromPreprocessing[data.objectives.size()-1].first = PreprocessorData::PreprocessorObjectiveSolution::False;
} else {
- data.solutionsFromPreprocessing[data.objectives.size()-1] = PreprocessorData::PreprocessorObjectiveSolution::True;
+ data.solutionsFromPreprocessing[data.objectives.size()-1].first = PreprocessorData::PreprocessorObjectiveSolution::True;
+ // Get a subsystem that deletes actions for which the property would be violated
storm::storage::BitVector consideredActions(data.preprocessedModel.getTransitionMatrix().getRowCount(), true);
for(auto state : duplicatorResult.firstCopy) {
for(uint_fast64_t action = data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state]; action < data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state +1]; ++action) {
@@ -275,6 +273,8 @@ namespace storm {
currentObjective.timeBounds = formula.getIntervalBounds();
}
preprocessFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), data, currentObjective, false, false);
+ } else {
+ STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Got a boundedUntilFormula which can not be checked for the current model type.");
}
}
@@ -287,7 +287,10 @@ namespace storm {
// To transform from the value of the preprocessed model back to the value of the original model, we have to add 1 to the result.
// The transformation factor has already been set correctly.
currentObjective.toOriginalValueTransformationOffset = storm::utility::one<ValueType>();
+
auto negatedSubformula = std::make_shared<storm::logic::UnaryBooleanStateFormula>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, formula.getSubformula().asSharedPointer());
+
+ // We need to swap the two flags isProb0Formula and isProb1Formula
preprocessFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), negatedSubformula), data, currentObjective, isProb1Formula, isProb0Formula);
}
@@ -302,6 +305,14 @@ namespace storm {
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> mc(data.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();
+
+ if(!(targetStates & data.preprocessedModel.getInitialStates()).empty()) {
+ // The value is always zero
+ data.solutionsFromPreprocessing[data.objectives.size()-1].first = PreprocessorData::PreprocessorObjectiveSolution::Numerical;
+ data.solutionsFromPreprocessing[data.objectives.size()-1].second = storm::utility::zero<ValueType>();
+ return;
+ }
+
auto duplicatorResult = storm::transformer::StateDuplicator<SparseModelType>::transform(data.preprocessedModel, targetStates);
updatePreprocessedModel(data, *duplicatorResult.model, duplicatorResult.newToOldStateIndexMapping);
@@ -340,7 +351,7 @@ namespace storm {
data.preprocessedModel.getStateLabeling().setStates(data.prob1StatesLabel, data.preprocessedModel.getStateLabeling().getStates(data.prob1StatesLabel) & duplicatorResult.secondCopy);
storm::storage::BitVector subsystemStates = duplicatorResult.secondCopy | storm::utility::graph::performProb1E(data.preprocessedModel, data.preprocessedModel.getBackwardTransitions(), duplicatorResult.firstCopy, duplicatorResult.gateStates);
if((subsystemStates & data.preprocessedModel.getInitialStates()).empty()) {
- data.solutionsFromPreprocessing[data.objectives.size()-1] = PreprocessorData::PreprocessorObjectiveSolution::Undefined;
+ data.solutionsFromPreprocessing[data.objectives.size()-1].first = PreprocessorData::PreprocessorObjectiveSolution::Undefined;
} else if(!subsystemStates.full()) {
auto subsystemBuilderResult = storm::transformer::SubsystemBuilder<SparseModelType>::transform(data.preprocessedModel, subsystemStates, storm::storage::BitVector(data.preprocessedModel.getTransitionMatrix().getRowCount(), true));
updatePreprocessedModel(data, *subsystemBuilderResult.model, subsystemBuilderResult.newToOldStateIndexMapping);
@@ -384,7 +395,7 @@ namespace storm {
template<typename SparseModelType>
- void SparseMultiObjectivePreprocessor<SparseModelType>::assertRewardFiniteness(PreprocessorData& data) {
+ void SparseMultiObjectivePreprocessor<SparseModelType>::ensureRewardFiniteness(PreprocessorData& data) {
bool negativeRewardsOccur = false;
bool positiveRewardsOccur = false;
for(auto& obj : data.objectives) {
@@ -395,17 +406,17 @@ namespace storm {
}
storm::storage::BitVector actionsWithNegativeReward;
if(negativeRewardsOccur) {
- actionsWithNegativeReward = assertNegativeRewardFiniteness(data);
+ actionsWithNegativeReward = ensureNegativeRewardFiniteness(data);
} else {
actionsWithNegativeReward = storm::storage::BitVector(data.preprocessedModel.getTransitionMatrix().getRowCount(), false);
}
if(positiveRewardsOccur) {
- assertPositiveRewardFiniteness(data, actionsWithNegativeReward);
+ ensurePositiveRewardFiniteness(data, actionsWithNegativeReward);
}
}
template<typename SparseModelType>
- storm::storage::BitVector SparseMultiObjectivePreprocessor<SparseModelType>::assertNegativeRewardFiniteness(PreprocessorData& data) {
+ storm::storage::BitVector SparseMultiObjectivePreprocessor<SparseModelType>::ensureNegativeRewardFiniteness(PreprocessorData& data) {
storm::storage::BitVector actionsWithNonNegativeReward(data.preprocessedModel.getTransitionMatrix().getRowCount(), true);
storm::storage::BitVector objectivesWithNegativeReward(data.objectives.size(), false);
@@ -436,9 +447,9 @@ namespace storm {
STORM_LOG_WARN("For every scheduler, the induced reward for one or more of the objectives that minimize rewards is infinity.");
for(auto objIndex : objectivesWithNegativeReward) {
if(data.objectives[objIndex].threshold) {
- data.solutionsFromPreprocessing[objIndex] = PreprocessorData::PreprocessorObjectiveSolution::False;
+ data.solutionsFromPreprocessing[objIndex].first = PreprocessorData::PreprocessorObjectiveSolution::False;
} else {
- data.solutionsFromPreprocessing[objIndex] = PreprocessorData::PreprocessorObjectiveSolution::Unbounded;
+ data.solutionsFromPreprocessing[objIndex].first = PreprocessorData::PreprocessorObjectiveSolution::Unbounded;
}
}
} else if(!statesReachingNegativeRewardsFinitelyOftenForSomeScheduler.full()) {
@@ -450,10 +461,10 @@ namespace storm {
}
template<typename SparseModelType>
- void SparseMultiObjectivePreprocessor<SparseModelType>::assertPositiveRewardFiniteness(PreprocessorData& data, storm::storage::BitVector const& actionsWithNegativeReward) {
+ void SparseMultiObjectivePreprocessor<SparseModelType>::ensurePositiveRewardFiniteness(PreprocessorData& data, storm::storage::BitVector const& actionsWithNegativeReward) {
storm::utility::Stopwatch sw;
auto mecDecomposition = storm::storage::MaximalEndComponentDecomposition<ValueType>(data.preprocessedModel.getTransitionMatrix(), data.preprocessedModel.getBackwardTransitions());
- STORM_LOG_DEBUG("Maximal end component decomposition for asserting positive reward finiteness took " << sw << " seconds.");
+ STORM_LOG_DEBUG("Maximal end component decomposition for ensuring positive reward finiteness took " << sw << " seconds.");
if(mecDecomposition.empty()) {
return;
}
@@ -474,9 +485,9 @@ namespace storm {
}
if(ecHasActionWithPositiveReward) {
if(obj.threshold) {
- data.solutionsFromPreprocessing[objIndex] = PreprocessorData::PreprocessorObjectiveSolution::True;
+ data.solutionsFromPreprocessing[objIndex].first = PreprocessorData::PreprocessorObjectiveSolution::True;
} else {
- data.solutionsFromPreprocessing[objIndex] = PreprocessorData::PreprocessorObjectiveSolution::Unbounded;
+ data.solutionsFromPreprocessing[objIndex].first = PreprocessorData::PreprocessorObjectiveSolution::Unbounded;
}
break;
}
@@ -486,15 +497,39 @@ namespace storm {
}
template<typename SparseModelType>
- void SparseMultiObjectivePreprocessor<SparseModelType>::updatePreprocessedModel(PreprocessorData& data, SparseModelType& newPreprocessedModel, std::vector<uint_fast64_t>& newToOldStateIndexMapping) {
- data.preprocessedModel = std::move(newPreprocessedModel);
- // the given newToOldStateIndexMapping reffers to the indices of the former preprocessedModel as 'old indices'
- for(auto & preprocessedModelStateIndex : newToOldStateIndexMapping){
- preprocessedModelStateIndex = data.newToOldStateIndexMapping[preprocessedModelStateIndex];
+ void SparseMultiObjectivePreprocessor<SparseModelType>::handleObjectivesWithSolutionFromPreprocessing(PreprocessorData& data) {
+ // Set solution for objectives for which there are no rewards left
+ for(uint_fast64_t objIndex = 0; objIndex < data.objectives.size(); ++objIndex) {
+ if(data.solutionsFromPreprocessing[objIndex].first == PreprocessorData::PreprocessorObjectiveSolution::None &&
+ data.preprocessedModel.getRewardModel(data.objectives[objIndex].rewardModelName).isAllZero()) {
+ data.solutionsFromPreprocessing[objIndex].first = PreprocessorData::PreprocessorObjectiveSolution::Numerical;
+ data.solutionsFromPreprocessing[objIndex].second = storm::utility::zero<ValueType>();
+ }
}
- data.newToOldStateIndexMapping = std::move(newToOldStateIndexMapping);
+
+ // Translate numerical solutions from preprocessing to Truth values (if the objective specifies a threshold) or to values for the original model (otherwise).
+ for(uint_fast64_t objIndex = 0; objIndex < data.objectives.size(); ++objIndex) {
+ if(data.solutionsFromPreprocessing[objIndex].first == PreprocessorData::PreprocessorObjectiveSolution::Numerical) {
+ ValueType& value = data.solutionsFromPreprocessing[objIndex].second;
+ ObjectiveInformation const& obj = data.objectives[objIndex];
+ if(obj.threshold) {
+ if((obj.thresholdIsStrict && value > (*obj.threshold)) || (!obj.thresholdIsStrict && value >= (*obj.threshold))) {
+ data.solutionsFromPreprocessing[objIndex].first = PreprocessorData::PreprocessorObjectiveSolution::True;
+ } else {
+ data.solutionsFromPreprocessing[objIndex].first = PreprocessorData::PreprocessorObjectiveSolution::False;
+ }
+ } else {
+ value = value * obj.toOriginalValueTransformationFactor + obj.toOriginalValueTransformationOffset;
+ }
+ }
+ }
+
+ // Only keep the objectives for which we have no solution yet
+ storm::storage::BitVector objWithNoSolution = storm::utility::vector::filter<std::pair<typename PreprocessorData::PreprocessorObjectiveSolution, ValueType>>(data.solutionsFromPreprocessing, [&] (std::pair<typename PreprocessorData::PreprocessorObjectiveSolution, ValueType> const& value) -> bool { return value.first == PreprocessorData::PreprocessorObjectiveSolution::None; });
+ data.objectives = storm::utility::vector::filterVector(data.objectives, objWithNoSolution);
}
+
template class SparseMultiObjectivePreprocessor<storm::models::sparse::Mdp<double>>;
template class SparseMultiObjectivePreprocessor<storm::models::sparse::MarkovAutomaton<double>>;
diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h
index 248a2c4fd..133501dd4 100644
--- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h
+++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h
@@ -31,6 +31,13 @@ namespace storm {
private:
+ /*!
+ * Updates the preprocessed model stored in the given data to the given model.
+ * The given newToOldStateIndexMapping should give for each state in the newPreprocessedModel
+ * the index of the state in the current data.preprocessedModel.
+ */
+ static void updatePreprocessedModel(PreprocessorData& data, SparseModelType& newPreprocessedModel, std::vector<uint_fast64_t>& newToOldStateIndexMapping);
+
/*!
* Apply the neccessary preprocessing for the given formula.
* @param formula the current (sub)formula
@@ -64,25 +71,27 @@ namespace storm {
* For reward properties that minimize, all states from which only infinite reward is possible are removed.
* Note that this excludes solutions of numerical queries where the minimum is infinity...
*/
- static void assertRewardFiniteness(PreprocessorData& data);
+ static void ensureRewardFiniteness(PreprocessorData& data);
/*!
* Checks reward finiteness for the negative rewards and returns the set of actions in the
* preprocessedModel that give negative rewards for some objective
*/
- static storm::storage::BitVector assertNegativeRewardFiniteness(PreprocessorData& data);
+ static storm::storage::BitVector ensureNegativeRewardFiniteness(PreprocessorData& data);
/*!
* Checks reward finiteness for the positive rewards
*/
- static void assertPositiveRewardFiniteness(PreprocessorData& data, storm::storage::BitVector const& actionsWithNegativeReward);
+ static void ensurePositiveRewardFiniteness(PreprocessorData& data, storm::storage::BitVector const& actionsWithNegativeReward);
/*!
- * Updates the preprocessed model stored in the given data to the given model.
- * The given newToOldStateIndexMapping should give for each state in the newPreprocessedModel
- * the index of the state in the current data.preprocessedModel.
+ * Handles the objectives for which a solution has been found in preprocessing, that is:
+ * * Set the solution for objectives for which no reward is left to zero
+ * * Translate numerical solutions for objectives with a threshold to either True or False
+ * * Translate numerical solutions for objectives without a threshold to a value for the original model
+ * * Only keep the objectives for which there is no solution yet
*/
- static void updatePreprocessedModel(PreprocessorData& data, SparseModelType& newPreprocessedModel, std::vector<uint_fast64_t>& newToOldStateIndexMapping);
+ static void handleObjectivesWithSolutionFromPreprocessing(PreprocessorData& data);
};
diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h
index 8b6a38a55..b9982b2de 100644
--- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h
+++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h
@@ -12,6 +12,7 @@
#include "src/models/sparse/MarkovAutomaton.h"
#include "src/storage/BitVector.h"
#include "src/utility/macros.h"
+#include "src/utility/constants.h"
#include "src/exceptions/UnexpectedException.h"
@@ -23,10 +24,13 @@ namespace storm {
struct SparseMultiObjectivePreprocessorData {
enum class QueryType { Achievability, Numerical, Pareto };
- enum class PreprocessorObjectiveSolution { None, False, True, Zero, Unbounded, Undefined };
+ enum class PreprocessorObjectiveSolution { None, False, True, Numerical, Unbounded, Undefined };
storm::logic::MultiObjectiveFormula const& originalFormula;
- std::vector<PreprocessorObjectiveSolution> solutionsFromPreprocessing;
+
+ // Stores the result for this objective obtained from preprocessing.
+ // In case of a numerical result, the value is store in the second entry of the pair. Otherwise, the second entry can be ignored.
+ std::vector<std::pair<PreprocessorObjectiveSolution, typename SparseModelType::ValueType>> solutionsFromPreprocessing;
SparseModelType const& originalModel;
SparseModelType preprocessedModel;
@@ -39,7 +43,7 @@ namespace storm {
bool produceSchedulers;
- SparseMultiObjectivePreprocessorData(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel, SparseModelType&& preprocessedModel, std::vector<uint_fast64_t>&& newToOldStateIndexMapping) : originalFormula(originalFormula), solutionsFromPreprocessing(originalFormula.getNumberOfSubformulas(), PreprocessorObjectiveSolution::None), originalModel(originalModel), preprocessedModel(preprocessedModel), newToOldStateIndexMapping(newToOldStateIndexMapping), produceSchedulers(false) {
+ SparseMultiObjectivePreprocessorData(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel, SparseModelType&& preprocessedModel, std::vector<uint_fast64_t>&& newToOldStateIndexMapping) : originalFormula(originalFormula), solutionsFromPreprocessing(originalFormula.getNumberOfSubformulas(), std::make_pair(PreprocessorObjectiveSolution::None, storm::utility::zero<typename SparseModelType::ValueType>())), originalModel(originalModel), preprocessedModel(preprocessedModel), newToOldStateIndexMapping(newToOldStateIndexMapping), produceSchedulers(false) {
// get a unique name for the labels of states that have to be reached with probability 1 and add the label
this->prob1StatesLabel = "prob1";
@@ -72,13 +76,13 @@ namespace storm {
out << "\t" << originalFormula << std::endl;
bool hasOneObjectiveSolvedInPreprocessing = false;
for(uint_fast64_t subformulaIndex = 0; subformulaIndex < originalFormula.getNumberOfSubformulas(); ++subformulaIndex) {
- if(!hasOneObjectiveSolvedInPreprocessing && solutionsFromPreprocessing[subformulaIndex]!= PreprocessorObjectiveSolution::None) {
+ if(!hasOneObjectiveSolvedInPreprocessing && solutionsFromPreprocessing[subformulaIndex].first != PreprocessorObjectiveSolution::None) {
hasOneObjectiveSolvedInPreprocessing = true;
out << std::endl;
out << "Solutions of objectives obtained from Preprocessing: " << std::endl;
out << "--------------------------------------------------------------" << std::endl;
}
- switch(solutionsFromPreprocessing[subformulaIndex]) {
+ switch(solutionsFromPreprocessing[subformulaIndex].first) {
case PreprocessorObjectiveSolution::None:
break;
case PreprocessorObjectiveSolution::False:
@@ -87,8 +91,8 @@ namespace storm {
case PreprocessorObjectiveSolution::True:
out<< "\t" << subformulaIndex << ": " << originalFormula.getSubformula(subformulaIndex) << " \t= true" << std::endl;
break;
- case PreprocessorObjectiveSolution::Zero:
- out<< "\t" << subformulaIndex << ": " << originalFormula.getSubformula(subformulaIndex) << " \t= zero" << std::endl;
+ case PreprocessorObjectiveSolution::Numerical:
+ out<< "\t" << subformulaIndex << ": " << originalFormula.getSubformula(subformulaIndex) << " \t= " << solutionsFromPreprocessing[subformulaIndex].second << std::endl;
break;
case PreprocessorObjectiveSolution::Unbounded:
out<< "\t" << subformulaIndex << ": " << originalFormula.getSubformula(subformulaIndex) << " \t= unbounded" << std::endl;
diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp
index 4741f2a0a..3d9ef373c 100644
--- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp
+++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp
@@ -42,10 +42,13 @@ namespace storm {
storm::utility::vector::addScaledVector(weightedRewardVector, discreteActionRewards[objIndex], weightVector[objIndex]);
}
unboundedWeightedPhase(weightedRewardVector);
- STORM_LOG_DEBUG("Unbounded weighted phase result: " << weightedResult[data.preprocessedModel.getInitialStates().getNextSetIndex(0)] << " (value in initial state).");
unboundedIndividualPhase(weightVector);
- if(!this->unboundedObjectives.full()) {
- boundedPhase(weightVector, weightedRewardVector);
+ // Only invoke boundedPhase if necessarry, i.e., if there is at least one objective with a time bound
+ for(auto const& obj : this->data.objectives) {
+ if(obj.timeBounds) {
+ boundedPhase(weightVector, weightedRewardVector);
+ break;
+ }
}
STORM_LOG_DEBUG("Weight vector check done. Lower bounds for results in initial state: " << storm::utility::vector::convertNumericVector<double>(getLowerBoundsOfInitialStateResults()));
}
@@ -87,7 +90,9 @@ namespace storm {
template <class SparseModelType>
storm::storage::TotalScheduler const& SparseMultiObjectiveWeightVectorChecker<SparseModelType>::getScheduler() const {
STORM_LOG_THROW(this->checkHasBeenCalled, storm::exceptions::IllegalFunctionCallException, "Tried to retrieve results but check(..) has not been called before.");
- STORM_LOG_THROW(this->unboundedObjectives.full(), storm::exceptions::NotImplementedException, "Scheduler retrival is not implemented for timeBounded objectives.");
+ for(auto const& obj : this->data.objectives) {
+ STORM_LOG_THROW(!obj.timeBounds, storm::exceptions::NotImplementedException, "Scheduler retrival is not implemented for timeBounded objectives.");
+ }
return scheduler;
}
diff --git a/src/transformer/StateDuplicator.h b/src/transformer/StateDuplicator.h
index 094e3e5ec..65d4527b5 100644
--- a/src/transformer/StateDuplicator.h
+++ b/src/transformer/StateDuplicator.h
@@ -44,7 +44,8 @@ namespace storm {
*
* Note that only reachable states are kept.
* Gate states will always belong to the second copy.
- * Rewards and labels are duplicated accordingly, but the states in the second copy will not get the label for initial states.
+ * Rewards and labels are duplicated accordingly.
+ * However, the non-gate-states in the second copy will not get the label for initial states.
*
* @param originalModel The model to be duplicated
* @param gateStates The states for which the incoming transitions are redirected
@@ -57,18 +58,18 @@ namespace storm {
initializeTransformation(originalModel, gateStates, result);
// Transform the ingedients of the model
- storm::storage::SparseMatrix<typename SparseModelType::ValueType> matrix = transformMatrix(originalModel.getTransitionMatrix(), result);
+ storm::storage::SparseMatrix<typename SparseModelType::ValueType> matrix = transformMatrix(originalModel.getTransitionMatrix(), result, gateStates);
storm::models::sparse::StateLabeling labeling(matrix.getRowGroupCount());
for(auto const& label : originalModel.getStateLabeling().getLabels()){
storm::storage::BitVector newBitVectorForLabel = transformStateBitVector(originalModel.getStateLabeling().getStates(label), result);
if(label=="init"){
- newBitVectorForLabel &=result.firstCopy;
+ newBitVectorForLabel &= (result.firstCopy | result.gateStates);
}
labeling.addLabel(label, std::move(newBitVectorForLabel));
}
std::unordered_map<std::string, typename SparseModelType::RewardModelType> rewardModels;
for(auto const& rewardModel : originalModel.getRewardModels()){
- rewardModels.insert(std::make_pair(rewardModel.first, transformRewardModel(rewardModel.second, originalModel.getTransitionMatrix().getRowGroupIndices(), result)));
+ rewardModels.insert(std::make_pair(rewardModel.first, transformRewardModel(rewardModel.second, originalModel.getTransitionMatrix().getRowGroupIndices(), result, gateStates)));
}
boost::optional<std::vector<storm::models::sparse::LabelSet>> choiceLabeling;
if(originalModel.hasChoiceLabeling()){
@@ -99,8 +100,6 @@ namespace storm {
result.firstCopy.resize(numStates, false); // the new states do NOT belong to the first copy
result.secondCopy = (statesForSecondCopy & (~statesForFirstCopy)) % result.reachableStates; // only consider reachable states
result.secondCopy.resize(numStates, true); // the new states DO belong to the second copy
- result.gateStates = gateStates;
- result.gateStates.resize(numStates, false); // there are no duplicated gateStates
STORM_LOG_ASSERT((result.firstCopy^result.secondCopy).full(), "firstCopy and secondCopy do not partition the state space.");
// Get the state mappings.
@@ -127,11 +126,13 @@ namespace storm {
++newState;
}
STORM_LOG_ASSERT(newState == numStates, "Unexpected state Indices");
+
+ result.gateStates = transformStateBitVector(gateStates, result);
}
template<typename ValueType = typename SparseModelType::ValueType, typename RewardModelType = typename SparseModelType::RewardModelType>
static typename std::enable_if<std::is_same<RewardModelType, storm::models::sparse::StandardRewardModel<ValueType>>::value, RewardModelType>::type
- transformRewardModel(RewardModelType const& originalRewardModel, std::vector<uint_fast64_t> const& originalRowGroupIndices, StateDuplicatorReturnType const& result) {
+ transformRewardModel(RewardModelType const& originalRewardModel, std::vector<uint_fast64_t> const& originalRowGroupIndices, StateDuplicatorReturnType const& result, storm::storage::BitVector const& gateStates) {
boost::optional<std::vector<ValueType>> stateRewardVector;
boost::optional<std::vector<ValueType>> stateActionRewardVector;
boost::optional<storm::storage::SparseMatrix<ValueType>> transitionRewardMatrix;
@@ -142,13 +143,13 @@ namespace storm {
stateActionRewardVector = transformActionValueVector(originalRewardModel.getStateActionRewardVector(), originalRowGroupIndices, result);
}
if(originalRewardModel.hasTransitionRewards()){
- transitionRewardMatrix = transformMatrix(originalRewardModel.getTransitionRewardMatrix(), result);
+ transitionRewardMatrix = transformMatrix(originalRewardModel.getTransitionRewardMatrix(), result, gateStates);
}
return RewardModelType(std::move(stateRewardVector), std::move(stateActionRewardVector), std::move(transitionRewardMatrix));
}
template<typename ValueType = typename SparseModelType::ValueType>
- static storm::storage::SparseMatrix<ValueType> transformMatrix(storm::storage::SparseMatrix<ValueType> const& originalMatrix, StateDuplicatorReturnType const& result) {
+ static storm::storage::SparseMatrix<ValueType> transformMatrix(storm::storage::SparseMatrix<ValueType> const& originalMatrix, StateDuplicatorReturnType const& result, storm::storage::BitVector const& gateStates) {
// Build the builder
uint_fast64_t numStates = result.newToOldStateIndexMapping.size();
uint_fast64_t numRows = 0;
@@ -168,7 +169,7 @@ namespace storm {
uint_fast64_t oldState = result.newToOldStateIndexMapping[newState];
for (uint_fast64_t oldRow = originalMatrix.getRowGroupIndices()[oldState]; oldRow < originalMatrix.getRowGroupIndices()[oldState+1]; ++oldRow){
for(auto const& entry : originalMatrix.getRow(oldRow)){
- if(result.firstCopy.get(newState) && !result.gateStates.get(entry.getColumn())){
+ if(result.firstCopy.get(newState) && !gateStates.get(entry.getColumn())){
builder.addNextValue(newRow, result.firstCopyOldToNewStateIndexMapping[entry.getColumn()], entry.getValue());
} else if (!result.duplicatedStates.get(entry.getColumn())){
builder.addNextValue(newRow, result.secondCopyOldToNewStateIndexMapping[entry.getColumn()], entry.getValue());
diff --git a/test/functional/modelchecker/SparseMdpMultiObjectiveModelCheckerTest.cpp b/test/functional/modelchecker/SparseMdpMultiObjectiveModelCheckerTest.cpp
index a8fd4aeca..4cafe9afa 100644
--- a/test/functional/modelchecker/SparseMdpMultiObjectiveModelCheckerTest.cpp
+++ b/test/functional/modelchecker/SparseMdpMultiObjectiveModelCheckerTest.cpp
@@ -80,6 +80,14 @@ TEST(SparseMdpMultiObjectiveModelCheckerTest, preprocessorResultsTest) {
formulasAsString += "; \n multi(Rmax=? [ C ]) ";
formulasAsString += "; \n multi(R>1 [ C ]) ";
formulasAsString += "; \n multi(R<1 [ C ]) ";
+ formulasAsString += "; \n multi(Pmax=? [ G true ]) ";
+ formulasAsString += "; \n multi(Pmin=? [ G true ]) ";
+ formulasAsString += "; \n multi(P>0.9 [ G true ]) ";
+ formulasAsString += "; \n multi(P>1 [ G true ]) ";
+ formulasAsString += "; \n multi(Pmax=? [ G false ]) ";
+ formulasAsString += "; \n multi(P>0 [ G false ]) ";
+ formulasAsString += "; \n multi(Pmin=? [ F \"init\" ]) ";
+ formulasAsString += "; \n multi(P>0.5 [ F \"init\" ]) ";
// programm, model, formula
storm::prism::Program program = storm::parseProgram(programFile);
@@ -138,6 +146,40 @@ TEST(SparseMdpMultiObjectiveModelCheckerTest, preprocessorResultsTest) {
result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula>(*formulas[11], true));
ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]);
+
+ result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula>(*formulas[12], true));
+ ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+ EXPECT_EQ(storm::utility::one<double>(), result->asExplicitQuantitativeCheckResult<double>()[initState]);
+
+ result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula>(*formulas[13], true));
+ ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+ EXPECT_EQ(storm::utility::one<double>(), result->asExplicitQuantitativeCheckResult<double>()[initState]);
+
+ result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula>(*formulas[14], true));
+ ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
+ EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]);
+
+ result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula>(*formulas[15], true));
+ ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
+ EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]);
+
+ result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula>(*formulas[16], true));
+ ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+ EXPECT_EQ(storm::utility::zero<double>(), result->asExplicitQuantitativeCheckResult<double>()[initState]);
+
+ result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula>(*formulas[17], true));
+ ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
+ EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]);
+
+ result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula>(*formulas[18], true));
+ ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
+ EXPECT_EQ(storm::utility::one<double>(), result->asExplicitQuantitativeCheckResult<double>()[initState]);
+
+ result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula>(*formulas[19], true));
+ ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
+ EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]);
+
+
}
TEST(SparseMdpMultiObjectiveModelCheckerTest, consensus) {