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

fixed the case where an objective is satisfied at the initial state. 

correctly added support for lower time bounds


Former-commit-id: 4d13d5de1b
main
TimQu 9 years ago
parent
45434556e2
commit
b267394a2c
10 changed files with 270 additions and 126 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 17
      src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.cpp
  2. 67
      src/modelchecker/multiobjective/helper/SparseMdpMultiObjectiveWeightVectorChecker.cpp
  3. 4
      src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp
  4. 12
      src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp
  5. 117
      src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp
  6. 23
      src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h
  7. 18
      src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h
  8. 11
      src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp
  9. 21
      src/transformer/StateDuplicator.h
  10. 42
      test/functional/modelchecker/SparseMdpMultiObjectiveModelCheckerTest.cpp

17
src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.cpp
View File

@ -80,6 +80,7 @@ namespace storm {
performMSStep(MS, PS, consideredObjectives); performMSStep(MS, PS, consideredObjectives);
if(currentEpoch % 1000 == 0) { if(currentEpoch % 1000 == 0) {
STORM_LOG_DEBUG(currentEpoch << " digitized time steps left. Current weighted value is " << PS.weightedSolutionVector[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; --currentEpoch;
} else { } else {
@ -256,13 +257,14 @@ namespace storm {
void SparseMaMultiObjectiveWeightVectorChecker<SparseMaModelType>::digitizeTimeBounds(TimeBoundMap& lowerTimeBounds, TimeBoundMap& upperTimeBounds, VT const& digitizationConstant) { void SparseMaMultiObjectiveWeightVectorChecker<SparseMaModelType>::digitizeTimeBounds(TimeBoundMap& lowerTimeBounds, TimeBoundMap& upperTimeBounds, VT const& digitizationConstant) {
VT const maxRate = this->data.preprocessedModel.getMaximalExitRate(); VT const maxRate = this->data.preprocessedModel.getMaximalExitRate();
storm::storage::BitVector boundedObjectives = ~this->unboundedObjectives;
for(uint_fast64_t objIndex : boundedObjectives) {
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; 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()));
if(obj.timeBounds->which() == 0) {
objUpperBound = storm::utility::convertNumber<VT>(boost::get<uint_fast64_t>(obj.timeBounds.get()));
} else { } else {
auto const& pair = boost::get<std::pair<double, double>>(this->data.objectives[objIndex].timeBounds.get());
auto const& pair = boost::get<std::pair<double, double>>(obj.timeBounds.get());
if(!storm::utility::isZero(pair.first)) { if(!storm::utility::isZero(pair.first)) {
objLowerBound = storm::utility::convertNumber<VT>(pair.first); objLowerBound = storm::utility::convertNumber<VT>(pair.first);
} }
@ -293,6 +295,7 @@ namespace storm {
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.");
} }
} }
}
template <class SparseMaModelType> template <class SparseMaModelType>
template <typename VT, typename std::enable_if<!storm::NumberTraits<VT>::SupportsExponential, int>::type> template <typename VT, typename std::enable_if<!storm::NumberTraits<VT>::SupportsExponential, int>::type>
@ -374,12 +377,14 @@ namespace storm {
// check whether the linEqSolver needs to be updated, i.e., whether the scheduler has changed // check whether the linEqSolver needs to be updated, i.e., whether the scheduler has changed
if(newOptimalChoices != optimalChoicesAtCurrentEpoch) { if(newOptimalChoices != optimalChoicesAtCurrentEpoch) {
std::cout << "Scheduler changed!";
std::cout << "X";
optimalChoicesAtCurrentEpoch.swap(newOptimalChoices); optimalChoicesAtCurrentEpoch.swap(newOptimalChoices);
linEq.solver = nullptr; linEq.solver = nullptr;
storm::storage::SparseMatrix<ValueType> linEqMatrix = PS.toPS.selectRowsFromRowGroups(optimalChoicesAtCurrentEpoch, true); storm::storage::SparseMatrix<ValueType> linEqMatrix = PS.toPS.selectRowsFromRowGroups(optimalChoicesAtCurrentEpoch, true);
linEqMatrix.convertToEquationSystem(); linEqMatrix.convertToEquationSystem();
linEq.solver = linEq.factory.create(std::move(linEqMatrix)); linEq.solver = linEq.factory.create(std::move(linEqMatrix));
} else {
std::cout << " ";
} }
for(auto objIndex : consideredObjectives) { for(auto objIndex : consideredObjectives) {
PS.toMS.multiplyWithVector(MS.objectiveSolutionVectors[objIndex], PS.auxChoiceValues); PS.toMS.multiplyWithVector(MS.objectiveSolutionVectors[objIndex], PS.auxChoiceValues);

67
src/modelchecker/multiobjective/helper/SparseMdpMultiObjectiveWeightVectorChecker.cpp
View File

@ -27,26 +27,68 @@ namespace storm {
std::vector<uint_fast64_t> optimalChoicesInCurrentEpoch(this->data.preprocessedModel.getNumberOfStates()); std::vector<uint_fast64_t> optimalChoicesInCurrentEpoch(this->data.preprocessedModel.getNumberOfStates());
std::vector<ValueType> choiceValues(weightedRewardVector.size()); std::vector<ValueType> choiceValues(weightedRewardVector.size());
std::vector<ValueType> temporaryResult(this->data.preprocessedModel.getNumberOfStates()); 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. // 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;
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); 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. // There is no error for the values of these objectives.
this->offsetsToLowerBound[objIndex] = storm::utility::zero<ValueType>(); this->offsetsToLowerBound[objIndex] = storm::utility::zero<ValueType>();
this->offsetsToUpperBound[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; 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]); storm::utility::vector::addScaledVector(weightedRewardVector, this->discreteActionRewards[objIndex], weightVector[objIndex]);
} }
++timeBoundIt;
++upperTimeBoundIt;
} }
// Get values and scheduler for weighted sum of objectives // 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. // 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) { for(auto objIndex : consideredObjectives) {
std::vector<ValueType>& objectiveResult = this->objectiveResults[objIndex]; 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 rowGroupIndexIt = this->data.preprocessedModel.getTransitionMatrix().getRowGroupIndices().begin();
auto optimalChoiceIt = optimalChoicesInCurrentEpoch.begin(); auto optimalChoiceIt = optimalChoicesInCurrentEpoch.begin();
for(ValueType& stateValue : temporaryResult){ for(ValueType& stateValue : temporaryResult){
@ -72,6 +114,7 @@ namespace storm {
} }
objectiveResult.swap(temporaryResult); objectiveResult.swap(temporaryResult);
} }
--currentEpoch;
} }
} }

4
src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp
View File

@ -47,8 +47,8 @@ namespace storm {
return true; return true;
} }
for(auto const& preprocessorResult : preprocessorData.solutionsFromPreprocessing) { 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; return true;
} }
} }

12
src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp
View File

@ -54,7 +54,7 @@ namespace storm {
//Incorporate the results from prerpocessing //Incorporate the results from prerpocessing
for(uint_fast64_t subformulaIndex = 0; subformulaIndex < preprocessorData.originalFormula.getNumberOfSubformulas(); ++subformulaIndex) { for(uint_fast64_t subformulaIndex = 0; subformulaIndex < preprocessorData.originalFormula.getNumberOfSubformulas(); ++subformulaIndex) {
switch(preprocessorData.solutionsFromPreprocessing[subformulaIndex]) {
switch(preprocessorData.solutionsFromPreprocessing[subformulaIndex].first) {
case PreprocessorData::PreprocessorObjectiveSolution::None: case PreprocessorData::PreprocessorObjectiveSolution::None:
// Nothing to be done // Nothing to be done
break; break;
@ -92,7 +92,7 @@ namespace storm {
//Incorporate the results from prerpocessing //Incorporate the results from prerpocessing
boost::optional<ValueType> preprocessorNumericalResult; boost::optional<ValueType> preprocessorNumericalResult;
for(uint_fast64_t subformulaIndex = 0; subformulaIndex < preprocessorData.originalFormula.getNumberOfSubformulas(); ++subformulaIndex) { for(uint_fast64_t subformulaIndex = 0; subformulaIndex < preprocessorData.originalFormula.getNumberOfSubformulas(); ++subformulaIndex) {
switch(preprocessorData.solutionsFromPreprocessing[subformulaIndex]) {
switch(preprocessorData.solutionsFromPreprocessing[subformulaIndex].first) {
case PreprocessorData::PreprocessorObjectiveSolution::None: case PreprocessorData::PreprocessorObjectiveSolution::None:
// Nothing to be done // Nothing to be done
break; break;
@ -101,9 +101,9 @@ namespace storm {
case PreprocessorData::PreprocessorObjectiveSolution::True: case PreprocessorData::PreprocessorObjectiveSolution::True:
// Nothing to be done // Nothing to be done
break; break;
case PreprocessorData::PreprocessorObjectiveSolution::Zero:
case PreprocessorData::PreprocessorObjectiveSolution::Numerical:
STORM_LOG_ASSERT(!preprocessorNumericalResult, "There are multiple numerical results obtained in preprocessing"); STORM_LOG_ASSERT(!preprocessorNumericalResult, "There are multiple numerical results obtained in preprocessing");
preprocessorNumericalResult = storm::utility::zero<ValueType>();
preprocessorNumericalResult = preprocessorData.solutionsFromPreprocessing[subformulaIndex].second;
break; break;
case PreprocessorData::PreprocessorObjectiveSolution::Unbounded: case PreprocessorData::PreprocessorObjectiveSolution::Unbounded:
STORM_LOG_ASSERT(!preprocessorNumericalResult, "There are multiple numerical results obtained in preprocessing"); 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 //Issue a warning for objectives that have been solved in preprocessing
for(uint_fast64_t subformulaIndex = 0; subformulaIndex < preprocessorData.originalFormula.getNumberOfSubformulas(); ++subformulaIndex) { for(uint_fast64_t subformulaIndex = 0; subformulaIndex < preprocessorData.originalFormula.getNumberOfSubformulas(); ++subformulaIndex) {
switch(preprocessorData.solutionsFromPreprocessing[subformulaIndex]) {
switch(preprocessorData.solutionsFromPreprocessing[subformulaIndex].first) {
case PreprocessorData::PreprocessorObjectiveSolution::None: case PreprocessorData::PreprocessorObjectiveSolution::None:
// Nothing to be done // Nothing to be done
break; break;
@ -153,7 +153,7 @@ namespace storm {
case PreprocessorData::PreprocessorObjectiveSolution::True: case PreprocessorData::PreprocessorObjectiveSolution::True:
// Nothing to be done // Nothing to be done
break; 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."); 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; break;
case PreprocessorData::PreprocessorObjectiveSolution::Unbounded: case PreprocessorData::PreprocessorObjectiveSolution::Unbounded:

117
src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp
View File

@ -44,28 +44,8 @@ namespace storm {
data.preprocessedModel.removeRewardModel(rewModel); 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. // 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! // 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; 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> template<typename SparseModelType>
void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::OperatorFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective) { 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 phiStates = mc.check(phiTask)->asExplicitQualitativeCheckResult().getTruthValuesVector();
storm::storage::BitVector psiStates = mc.check(psiTask)->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); auto duplicatorResult = storm::transformer::StateDuplicator<SparseModelType>::transform(data.preprocessedModel, ~phiStates | psiStates);
updatePreprocessedModel(data, *duplicatorResult.model, duplicatorResult.newToOldStateIndexMapping); updatePreprocessedModel(data, *duplicatorResult.model, duplicatorResult.newToOldStateIndexMapping);
@ -223,9 +220,10 @@ namespace storm {
noIncomingTransitionFromFirstCopyStates = duplicatorResult.gateStates & (~newPsiStates); noIncomingTransitionFromFirstCopyStates = duplicatorResult.gateStates & (~newPsiStates);
} }
if((subsystemStates & data.preprocessedModel.getInitialStates()).empty()) { 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 { } 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); storm::storage::BitVector consideredActions(data.preprocessedModel.getTransitionMatrix().getRowCount(), true);
for(auto state : duplicatorResult.firstCopy) { for(auto state : duplicatorResult.firstCopy) {
for(uint_fast64_t action = data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state]; action < data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state +1]; ++action) { 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(); currentObjective.timeBounds = formula.getIntervalBounds();
} }
preprocessFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), data, currentObjective, false, false); 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. // 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. // The transformation factor has already been set correctly.
currentObjective.toOriginalValueTransformationOffset = storm::utility::one<ValueType>(); currentObjective.toOriginalValueTransformationOffset = storm::utility::one<ValueType>();
auto negatedSubformula = std::make_shared<storm::logic::UnaryBooleanStateFormula>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, formula.getSubformula().asSharedPointer()); 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); 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::modelchecker::SparsePropositionalModelChecker<SparseModelType> mc(data.preprocessedModel);
STORM_LOG_THROW(mc.canHandle(targetTask), storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " should be propositional."); 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(); 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); auto duplicatorResult = storm::transformer::StateDuplicator<SparseModelType>::transform(data.preprocessedModel, targetStates);
updatePreprocessedModel(data, *duplicatorResult.model, duplicatorResult.newToOldStateIndexMapping); 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); 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); 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()) { 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()) { } else if(!subsystemStates.full()) {
auto subsystemBuilderResult = storm::transformer::SubsystemBuilder<SparseModelType>::transform(data.preprocessedModel, subsystemStates, storm::storage::BitVector(data.preprocessedModel.getTransitionMatrix().getRowCount(), true)); auto subsystemBuilderResult = storm::transformer::SubsystemBuilder<SparseModelType>::transform(data.preprocessedModel, subsystemStates, storm::storage::BitVector(data.preprocessedModel.getTransitionMatrix().getRowCount(), true));
updatePreprocessedModel(data, *subsystemBuilderResult.model, subsystemBuilderResult.newToOldStateIndexMapping); updatePreprocessedModel(data, *subsystemBuilderResult.model, subsystemBuilderResult.newToOldStateIndexMapping);
@ -384,7 +395,7 @@ namespace storm {
template<typename SparseModelType> template<typename SparseModelType>
void SparseMultiObjectivePreprocessor<SparseModelType>::assertRewardFiniteness(PreprocessorData& data) {
void SparseMultiObjectivePreprocessor<SparseModelType>::ensureRewardFiniteness(PreprocessorData& data) {
bool negativeRewardsOccur = false; bool negativeRewardsOccur = false;
bool positiveRewardsOccur = false; bool positiveRewardsOccur = false;
for(auto& obj : data.objectives) { for(auto& obj : data.objectives) {
@ -395,17 +406,17 @@ namespace storm {
} }
storm::storage::BitVector actionsWithNegativeReward; storm::storage::BitVector actionsWithNegativeReward;
if(negativeRewardsOccur) { if(negativeRewardsOccur) {
actionsWithNegativeReward = assertNegativeRewardFiniteness(data);
actionsWithNegativeReward = ensureNegativeRewardFiniteness(data);
} else { } else {
actionsWithNegativeReward = storm::storage::BitVector(data.preprocessedModel.getTransitionMatrix().getRowCount(), false); actionsWithNegativeReward = storm::storage::BitVector(data.preprocessedModel.getTransitionMatrix().getRowCount(), false);
} }
if(positiveRewardsOccur) { if(positiveRewardsOccur) {
assertPositiveRewardFiniteness(data, actionsWithNegativeReward);
ensurePositiveRewardFiniteness(data, actionsWithNegativeReward);
} }
} }
template<typename SparseModelType> 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 actionsWithNonNegativeReward(data.preprocessedModel.getTransitionMatrix().getRowCount(), true);
storm::storage::BitVector objectivesWithNegativeReward(data.objectives.size(), false); 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."); 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) { for(auto objIndex : objectivesWithNegativeReward) {
if(data.objectives[objIndex].threshold) { if(data.objectives[objIndex].threshold) {
data.solutionsFromPreprocessing[objIndex] = PreprocessorData::PreprocessorObjectiveSolution::False;
data.solutionsFromPreprocessing[objIndex].first = PreprocessorData::PreprocessorObjectiveSolution::False;
} else { } else {
data.solutionsFromPreprocessing[objIndex] = PreprocessorData::PreprocessorObjectiveSolution::Unbounded;
data.solutionsFromPreprocessing[objIndex].first = PreprocessorData::PreprocessorObjectiveSolution::Unbounded;
} }
} }
} else if(!statesReachingNegativeRewardsFinitelyOftenForSomeScheduler.full()) { } else if(!statesReachingNegativeRewardsFinitelyOftenForSomeScheduler.full()) {
@ -450,10 +461,10 @@ namespace storm {
} }
template<typename SparseModelType> 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; storm::utility::Stopwatch sw;
auto mecDecomposition = storm::storage::MaximalEndComponentDecomposition<ValueType>(data.preprocessedModel.getTransitionMatrix(), data.preprocessedModel.getBackwardTransitions()); 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()) { if(mecDecomposition.empty()) {
return; return;
} }
@ -474,9 +485,9 @@ namespace storm {
} }
if(ecHasActionWithPositiveReward) { if(ecHasActionWithPositiveReward) {
if(obj.threshold) { if(obj.threshold) {
data.solutionsFromPreprocessing[objIndex] = PreprocessorData::PreprocessorObjectiveSolution::True;
data.solutionsFromPreprocessing[objIndex].first = PreprocessorData::PreprocessorObjectiveSolution::True;
} else { } else {
data.solutionsFromPreprocessing[objIndex] = PreprocessorData::PreprocessorObjectiveSolution::Unbounded;
data.solutionsFromPreprocessing[objIndex].first = PreprocessorData::PreprocessorObjectiveSolution::Unbounded;
} }
break; break;
} }
@ -486,15 +497,39 @@ namespace storm {
} }
template<typename SparseModelType> 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::Mdp<double>>;
template class SparseMultiObjectivePreprocessor<storm::models::sparse::MarkovAutomaton<double>>; template class SparseMultiObjectivePreprocessor<storm::models::sparse::MarkovAutomaton<double>>;

23
src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h
View File

@ -31,6 +31,13 @@ namespace storm {
private: 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. * Apply the neccessary preprocessing for the given formula.
* @param formula the current (sub)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. * 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... * 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 * Checks reward finiteness for the negative rewards and returns the set of actions in the
* preprocessedModel that give negative rewards for some objective * 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 * 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);
}; };

18
src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h
View File

@ -12,6 +12,7 @@
#include "src/models/sparse/MarkovAutomaton.h" #include "src/models/sparse/MarkovAutomaton.h"
#include "src/storage/BitVector.h" #include "src/storage/BitVector.h"
#include "src/utility/macros.h" #include "src/utility/macros.h"
#include "src/utility/constants.h"
#include "src/exceptions/UnexpectedException.h" #include "src/exceptions/UnexpectedException.h"
@ -23,10 +24,13 @@ namespace storm {
struct SparseMultiObjectivePreprocessorData { struct SparseMultiObjectivePreprocessorData {
enum class QueryType { Achievability, Numerical, Pareto }; 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; 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 const& originalModel;
SparseModelType preprocessedModel; SparseModelType preprocessedModel;
@ -39,7 +43,7 @@ namespace storm {
bool produceSchedulers; 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 // get a unique name for the labels of states that have to be reached with probability 1 and add the label
this->prob1StatesLabel = "prob1"; this->prob1StatesLabel = "prob1";
@ -72,13 +76,13 @@ namespace storm {
out << "\t" << originalFormula << std::endl; out << "\t" << originalFormula << std::endl;
bool hasOneObjectiveSolvedInPreprocessing = false; bool hasOneObjectiveSolvedInPreprocessing = false;
for(uint_fast64_t subformulaIndex = 0; subformulaIndex < originalFormula.getNumberOfSubformulas(); ++subformulaIndex) { 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; hasOneObjectiveSolvedInPreprocessing = true;
out << std::endl; out << std::endl;
out << "Solutions of objectives obtained from Preprocessing: " << std::endl; out << "Solutions of objectives obtained from Preprocessing: " << std::endl;
out << "--------------------------------------------------------------" << std::endl; out << "--------------------------------------------------------------" << std::endl;
} }
switch(solutionsFromPreprocessing[subformulaIndex]) {
switch(solutionsFromPreprocessing[subformulaIndex].first) {
case PreprocessorObjectiveSolution::None: case PreprocessorObjectiveSolution::None:
break; break;
case PreprocessorObjectiveSolution::False: case PreprocessorObjectiveSolution::False:
@ -87,8 +91,8 @@ namespace storm {
case PreprocessorObjectiveSolution::True: case PreprocessorObjectiveSolution::True:
out<< "\t" << subformulaIndex << ": " << originalFormula.getSubformula(subformulaIndex) << " \t= true" << std::endl; out<< "\t" << subformulaIndex << ": " << originalFormula.getSubformula(subformulaIndex) << " \t= true" << std::endl;
break; 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; break;
case PreprocessorObjectiveSolution::Unbounded: case PreprocessorObjectiveSolution::Unbounded:
out<< "\t" << subformulaIndex << ": " << originalFormula.getSubformula(subformulaIndex) << " \t= unbounded" << std::endl; out<< "\t" << subformulaIndex << ": " << originalFormula.getSubformula(subformulaIndex) << " \t= unbounded" << std::endl;

11
src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp
View File

@ -42,10 +42,13 @@ namespace storm {
storm::utility::vector::addScaledVector(weightedRewardVector, discreteActionRewards[objIndex], weightVector[objIndex]); storm::utility::vector::addScaledVector(weightedRewardVector, discreteActionRewards[objIndex], weightVector[objIndex]);
} }
unboundedWeightedPhase(weightedRewardVector); unboundedWeightedPhase(weightedRewardVector);
STORM_LOG_DEBUG("Unbounded weighted phase result: " << weightedResult[data.preprocessedModel.getInitialStates().getNextSetIndex(0)] << " (value in initial state).");
unboundedIndividualPhase(weightVector); unboundedIndividualPhase(weightVector);
if(!this->unboundedObjectives.full()) {
// 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); boundedPhase(weightVector, weightedRewardVector);
break;
}
} }
STORM_LOG_DEBUG("Weight vector check done. Lower bounds for results in initial state: " << storm::utility::vector::convertNumericVector<double>(getLowerBoundsOfInitialStateResults())); 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> template <class SparseModelType>
storm::storage::TotalScheduler const& SparseMultiObjectiveWeightVectorChecker<SparseModelType>::getScheduler() const { 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->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; return scheduler;
} }

21
src/transformer/StateDuplicator.h
View File

@ -44,7 +44,8 @@ namespace storm {
* *
* Note that only reachable states are kept. * Note that only reachable states are kept.
* Gate states will always belong to the second copy. * 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 originalModel The model to be duplicated
* @param gateStates The states for which the incoming transitions are redirected * @param gateStates The states for which the incoming transitions are redirected
@ -57,18 +58,18 @@ namespace storm {
initializeTransformation(originalModel, gateStates, result); initializeTransformation(originalModel, gateStates, result);
// Transform the ingedients of the model // 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()); storm::models::sparse::StateLabeling labeling(matrix.getRowGroupCount());
for(auto const& label : originalModel.getStateLabeling().getLabels()){ for(auto const& label : originalModel.getStateLabeling().getLabels()){
storm::storage::BitVector newBitVectorForLabel = transformStateBitVector(originalModel.getStateLabeling().getStates(label), result); storm::storage::BitVector newBitVectorForLabel = transformStateBitVector(originalModel.getStateLabeling().getStates(label), result);
if(label=="init"){ if(label=="init"){
newBitVectorForLabel &=result.firstCopy;
newBitVectorForLabel &= (result.firstCopy | result.gateStates);
} }
labeling.addLabel(label, std::move(newBitVectorForLabel)); labeling.addLabel(label, std::move(newBitVectorForLabel));
} }
std::unordered_map<std::string, typename SparseModelType::RewardModelType> rewardModels; std::unordered_map<std::string, typename SparseModelType::RewardModelType> rewardModels;
for(auto const& rewardModel : originalModel.getRewardModels()){ 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; boost::optional<std::vector<storm::models::sparse::LabelSet>> choiceLabeling;
if(originalModel.hasChoiceLabeling()){ 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.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 = (statesForSecondCopy & (~statesForFirstCopy)) % result.reachableStates; // only consider reachable states
result.secondCopy.resize(numStates, true); // the new states DO belong to the second copy 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."); STORM_LOG_ASSERT((result.firstCopy^result.secondCopy).full(), "firstCopy and secondCopy do not partition the state space.");
// Get the state mappings. // Get the state mappings.
@ -127,11 +126,13 @@ namespace storm {
++newState; ++newState;
} }
STORM_LOG_ASSERT(newState == numStates, "Unexpected state Indices"); STORM_LOG_ASSERT(newState == numStates, "Unexpected state Indices");
result.gateStates = transformStateBitVector(gateStates, result);
} }
template<typename ValueType = typename SparseModelType::ValueType, typename RewardModelType = typename SparseModelType::RewardModelType> 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 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>> stateRewardVector;
boost::optional<std::vector<ValueType>> stateActionRewardVector; boost::optional<std::vector<ValueType>> stateActionRewardVector;
boost::optional<storm::storage::SparseMatrix<ValueType>> transitionRewardMatrix; boost::optional<storm::storage::SparseMatrix<ValueType>> transitionRewardMatrix;
@ -142,13 +143,13 @@ namespace storm {
stateActionRewardVector = transformActionValueVector(originalRewardModel.getStateActionRewardVector(), originalRowGroupIndices, result); stateActionRewardVector = transformActionValueVector(originalRewardModel.getStateActionRewardVector(), originalRowGroupIndices, result);
} }
if(originalRewardModel.hasTransitionRewards()){ 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)); return RewardModelType(std::move(stateRewardVector), std::move(stateActionRewardVector), std::move(transitionRewardMatrix));
} }
template<typename ValueType = typename SparseModelType::ValueType> 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 // Build the builder
uint_fast64_t numStates = result.newToOldStateIndexMapping.size(); uint_fast64_t numStates = result.newToOldStateIndexMapping.size();
uint_fast64_t numRows = 0; uint_fast64_t numRows = 0;
@ -168,7 +169,7 @@ namespace storm {
uint_fast64_t oldState = result.newToOldStateIndexMapping[newState]; uint_fast64_t oldState = result.newToOldStateIndexMapping[newState];
for (uint_fast64_t oldRow = originalMatrix.getRowGroupIndices()[oldState]; oldRow < originalMatrix.getRowGroupIndices()[oldState+1]; ++oldRow){ for (uint_fast64_t oldRow = originalMatrix.getRowGroupIndices()[oldState]; oldRow < originalMatrix.getRowGroupIndices()[oldState+1]; ++oldRow){
for(auto const& entry : originalMatrix.getRow(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()); builder.addNextValue(newRow, result.firstCopyOldToNewStateIndexMapping[entry.getColumn()], entry.getValue());
} else if (!result.duplicatedStates.get(entry.getColumn())){ } else if (!result.duplicatedStates.get(entry.getColumn())){
builder.addNextValue(newRow, result.secondCopyOldToNewStateIndexMapping[entry.getColumn()], entry.getValue()); builder.addNextValue(newRow, result.secondCopyOldToNewStateIndexMapping[entry.getColumn()], entry.getValue());

42
test/functional/modelchecker/SparseMdpMultiObjectiveModelCheckerTest.cpp
View File

@ -80,6 +80,14 @@ TEST(SparseMdpMultiObjectiveModelCheckerTest, preprocessorResultsTest) {
formulasAsString += "; \n multi(Rmax=? [ C ]) "; formulasAsString += "; \n multi(Rmax=? [ C ]) ";
formulasAsString += "; \n multi(R>1 [ C ]) "; formulasAsString += "; \n multi(R>1 [ 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 // programm, model, formula
storm::prism::Program program = storm::parseProgram(programFile); 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)); result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula>(*formulas[11], true));
ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); 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) { TEST(SparseMdpMultiObjectiveModelCheckerTest, consensus) {

Write Preview
Loading…
Cancel
Save