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

Some tests, correct handling of results obtained in preprocessing, fixes 

Former-commit-id: e7eb1f67cb
main
TimQu 9 years ago
parent
ce9a6b415c
commit
3cd198c5e3
11 changed files with 333 additions and 99 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 10
      src/logic/MultiObjectiveFormula.cpp
  2. 43
      src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp
  3. 7
      src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.h
  4. 107
      src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp
  5. 102
      src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp
  6. 52
      src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h
  7. 22
      src/modelchecker/multiobjective/helper/SparseMultiObjectiveResultData.h
  8. 5
      src/transformer/SubsystemBuilder.h
  9. 12
      src/utility/vector.h
  10. 52
      test/functional/modelchecker/SparseMdpMultiObjectiveModelCheckerTest.cpp
  11. 20
      test/functional/modelchecker/multiobjective1.nm

10
src/logic/MultiObjectiveFormula.cpp
View File

@ -33,16 +33,16 @@ namespace storm {
}
bool MultiObjectiveFormula::hasNumericalResult() const {
bool hasExactlyOneQualitativeSubformula = false;
bool hasExactlyOneQuantitativeSubformula = false;
for(auto const& subformula : this->subformulas){
if(subformula->hasQualitativeResult()){
if(hasExactlyOneQualitativeSubformula){
if(subformula->hasQuantitativeResult()){
if(hasExactlyOneQuantitativeSubformula){
return false;
}
hasExactlyOneQualitativeSubformula=true;
hasExactlyOneQuantitativeSubformula=true;
}
}
return hasExactlyOneQualitativeSubformula;
return hasExactlyOneQuantitativeSubformula;
}
bool MultiObjectiveFormula::hasParetoCurveResult() const {

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

@ -22,22 +22,38 @@ namespace storm {
resultData.overApproximation() = storm::storage::geometry::Polytope<RationalNumberType>::createUniversalPolytope();
resultData.underApproximation() = storm::storage::geometry::Polytope<RationalNumberType>::createEmptyPolytope();
switch(preprocessorData.queryType) {
case PreprocessorData::QueryType::Achievability:
achievabilityQuery(preprocessorData, resultData);
break;
case PreprocessorData::QueryType::Numerical:
numericalQuery(preprocessorData, resultData);
break;
case PreprocessorData::QueryType::Pareto:
paretoQuery(preprocessorData, resultData);
break;
default:
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unknown Query Type");
if(!checkIfPreprocessingWasConclusive(preprocessorData)) {
switch(preprocessorData.queryType) {
case PreprocessorData::QueryType::Achievability:
achievabilityQuery(preprocessorData, resultData);
break;
case PreprocessorData::QueryType::Numerical:
numericalQuery(preprocessorData, resultData);
break;
case PreprocessorData::QueryType::Pareto:
paretoQuery(preprocessorData, resultData);
break;
default:
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unknown Query Type");
}
}
return resultData;
}
template <class SparseModelType, typename RationalNumberType>
bool SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::checkIfPreprocessingWasConclusive(PreprocessorData const& preprocessorData) {
if(preprocessorData.objectives.empty()) {
return true;
}
for(auto const& preprocessorResult : preprocessorData.solutionsFromPreprocessing) {
if(preprocessorResult == PreprocessorData::PreprocessorObjectiveSolution::False ||
preprocessorResult == PreprocessorData::PreprocessorObjectiveSolution::Undefined) {
return true;
}
}
return false;
}
template <class SparseModelType, typename RationalNumberType>
void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::achievabilityQuery(PreprocessorData const& preprocessorData, ResultData& resultData) {
Point thresholds;
@ -68,7 +84,7 @@ namespace storm {
uint_fast64_t optimizingObjIndex = *preprocessorData.indexOfOptimizingObjective;
Point thresholds;
thresholds.reserve(preprocessorData.objectives.size());
storm::storage::BitVector strictThresholds(preprocessorData.objectives.size());
storm::storage::BitVector strictThresholds(preprocessorData.objectives.size(), false);
std::vector<storm::storage::geometry::Halfspace<RationalNumberType>> thresholdConstraints;
thresholdConstraints.reserve(preprocessorData.objectives.size()-1);
for(uint_fast64_t objIndex = 0; objIndex < preprocessorData.objectives.size(); ++objIndex) {
@ -82,6 +98,7 @@ namespace storm {
thresholds.push_back(storm::utility::zero<RationalNumberType>());
}
}
// Note: If we have a single objective (i.e., no objectives with thresholds), thresholdsAsPolytope gets no constraints
auto thresholdsAsPolytope = storm::storage::geometry::Polytope<RationalNumberType>::create(thresholdConstraints);
WeightVector directionOfOptimizingObjective(preprocessorData.objectives.size(), storm::utility::zero<RationalNumberType>());
directionOfOptimizingObjective[optimizingObjIndex] = storm::utility::one<RationalNumberType>();

7
src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.h
View File

@ -27,6 +27,13 @@ namespace storm {
private:
/*
* Checks whether the preprocessing was already conclusive, e.g., the result for one objective is undefined or false
*
* @return true iff preprocessing was conclusive
*/
static bool checkIfPreprocessingWasConclusive(PreprocessorData const& preprocessorData);
static void achievabilityQuery(PreprocessorData const& preprocessorData, ResultData& resultData);
static void numericalQuery(PreprocessorData const& preprocessorData, ResultData& resultData);
static void paretoQuery(PreprocessorData const& preprocessorData, ResultData& resultData);

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

@ -19,41 +19,106 @@ namespace storm {
template<typename SparseModelType, typename RationalNumberType>
typename std::unique_ptr<CheckResult> SparseMultiObjectivePostprocessor<SparseModelType, RationalNumberType>::postprocess(PreprocessorData const& preprocessorData, ResultData const& resultData) {
STORM_LOG_ASSERT(preprocessorData.originalModel.getInitialStates().getNumberOfSetBits() == 1, "Multi Objective Model checking on model with multiple initial states is not supported.");
STORM_LOG_WARN_COND(!resultData.getMaxStepsPerformed(), "Multi-objective model checking has been aborted since the maximum number of refinement steps has been performed. The results are most likely incorrect.");
switch(preprocessorData.queryType) {
case PreprocessorData::QueryType::Achievability:
return postprocessAchievabilityQuery(preprocessorData, resultData);
case PreprocessorData::QueryType::Numerical:
return postprocessNumericalQuery(preprocessorData, resultData);
case PreprocessorData::QueryType::Pareto:
return postprocessParetoQuery(preprocessorData, resultData);
default:
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unknown Query Type");
if(preprocessorData.originalFormula.hasQualitativeResult()) {
return postprocessAchievabilityQuery(preprocessorData, resultData);
} else if(preprocessorData.originalFormula.hasNumericalResult()){
return postprocessNumericalQuery(preprocessorData, resultData);
} else if (preprocessorData.originalFormula.hasParetoCurveResult()) {
return postprocessParetoQuery(preprocessorData, resultData);
} else {
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unknown Query Type");
}
return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult());;
}
template<typename SparseModelType, typename RationalNumberType>
typename std::unique_ptr<CheckResult> SparseMultiObjectivePostprocessor<SparseModelType, RationalNumberType>::postprocessAchievabilityQuery(PreprocessorData const& preprocessorData, ResultData const& resultData) {
STORM_LOG_ERROR_COND(resultData.isThresholdsAreAchievableSet(), "Could not find out whether the thresholds are achievable.");
STORM_LOG_ASSERT(preprocessorData.queryType == PreprocessorData::QueryType::Achievability, "Expected an achievability query.");
uint_fast64_t initState = preprocessorData.originalModel.getInitialStates().getNextSetIndex(0);
return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(initState, resultData.getThresholdsAreAchievable()));
//Incorporate the results from prerpocessing
for(uint_fast64_t subformulaIndex = 0; subformulaIndex < preprocessorData.originalFormula.getNumberOfSubformulas(); ++subformulaIndex) {
switch(preprocessorData.solutionsFromPreprocessing[subformulaIndex]) {
case PreprocessorData::PreprocessorObjectiveSolution::None:
// Nothing to be done
break;
case PreprocessorData::PreprocessorObjectiveSolution::False:
return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(initState, false));
case PreprocessorData::PreprocessorObjectiveSolution::True:
// Nothing to be done
break;
case PreprocessorData::PreprocessorObjectiveSolution::Undefined:
STORM_LOG_ERROR("The result for the objective " << preprocessorData.originalFormula.getSubformula(subformulaIndex) << " is not defined.");
return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(initState, false));
default:
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected type of solution obtained in preprocessing.");
}
}
if(preprocessorData.objectives.empty()) {
return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(initState, true));
}
// This might be due to reaching the max. number of refinement steps (so no exception is thrown)
STORM_LOG_ERROR_COND(resultData.isThresholdsAreAchievableSet(), "Could not find out whether the thresholds are achievable.");
return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(initState, resultData.isThresholdsAreAchievableSet() &&resultData.getThresholdsAreAchievable()));
}
template<typename SparseModelType, typename RationalNumberType>
typename std::unique_ptr<CheckResult> SparseMultiObjectivePostprocessor<SparseModelType, RationalNumberType>::postprocessNumericalQuery(PreprocessorData const& preprocessorData, ResultData const& resultData) {
//The queryType might be achievability (when the numerical result was obtained in preprocessing)
STORM_LOG_ASSERT(preprocessorData.queryType == PreprocessorData::QueryType::Numerical ||
preprocessorData.queryType == PreprocessorData::QueryType::Achievability, "Expected a numerical or an achievability query.");
uint_fast64_t initState = preprocessorData.originalModel.getInitialStates().getNextSetIndex(0);
if(resultData.isThresholdsAreAchievableSet() && resultData.getThresholdsAreAchievable()) {
STORM_LOG_ASSERT(resultData.isNumericalResultSet(), "Postprocessing for numerical query invoked, but no numerical result is given");
STORM_LOG_ASSERT(preprocessorData.indexOfOptimizingObjective, "Postprocessing for numerical query invoked, but no index of optimizing objective is specified");
ObjectiveInformation optimizingObjective = preprocessorData.objectives[*preprocessorData.indexOfOptimizingObjective];
ValueType resultForOriginalModel = resultData.template getNumericalResult<ValueType>() * optimizingObjective.toOriginalValueTransformationFactor + optimizingObjective.toOriginalValueTransformationOffset;
STORM_LOG_WARN_COND(resultData.getTargetPrecisionReached(), "The target precision for numerical queries has not been reached.");
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(initState, resultForOriginalModel));
//Incorporate the results from prerpocessing
boost::optional<ValueType> preprocessorNumericalResult;
for(uint_fast64_t subformulaIndex = 0; subformulaIndex < preprocessorData.originalFormula.getNumberOfSubformulas(); ++subformulaIndex) {
switch(preprocessorData.solutionsFromPreprocessing[subformulaIndex]) {
case PreprocessorData::PreprocessorObjectiveSolution::None:
// Nothing to be done
break;
case PreprocessorData::PreprocessorObjectiveSolution::False:
return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(initState, false));
case PreprocessorData::PreprocessorObjectiveSolution::True:
// Nothing to be done
break;
case PreprocessorData::PreprocessorObjectiveSolution::Zero:
STORM_LOG_ASSERT(!preprocessorNumericalResult, "There are multiple numerical results obtained in preprocessing");
preprocessorNumericalResult = storm::utility::zero<ValueType>();
break;
case PreprocessorData::PreprocessorObjectiveSolution::Unbounded:
STORM_LOG_ASSERT(!preprocessorNumericalResult, "There are multiple numerical results obtained in preprocessing");
preprocessorNumericalResult = storm::utility::infinity<ValueType>();
break;
case PreprocessorData::PreprocessorObjectiveSolution::Undefined:
STORM_LOG_ERROR("The result for the objective " << preprocessorData.originalFormula.getSubformula(subformulaIndex) << " is not defined.");
return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(initState, false));
default:
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected solution obtained in preprocessing.");
}
}
// Check whether the given thresholds are achievable
if(preprocessorData.objectives.empty() || (resultData.isThresholdsAreAchievableSet() && resultData.getThresholdsAreAchievable())) {
// Get the numerical result
if(preprocessorNumericalResult) {
STORM_LOG_ASSERT(!resultData.isNumericalResultSet(), "Result was found in preprocessing but there is also one in the resultData");
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(initState, *preprocessorNumericalResult));
} else {
STORM_LOG_ASSERT(resultData.isNumericalResultSet(), "Postprocessing for numerical query invoked, but no numerical result is given");
STORM_LOG_ASSERT(preprocessorData.indexOfOptimizingObjective, "Postprocessing for numerical query invoked, but no index of optimizing objective is specified");
ObjectiveInformation const& optimizingObjective = preprocessorData.objectives[*preprocessorData.indexOfOptimizingObjective];
ValueType resultForOriginalModel = resultData.template getNumericalResult<ValueType>() * optimizingObjective.toOriginalValueTransformationFactor + optimizingObjective.toOriginalValueTransformationOffset;
STORM_LOG_WARN_COND(resultData.getTargetPrecisionReached(), "The target precision for numerical queries has not been reached.");
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(initState, resultForOriginalModel));
}
} else {
STORM_LOG_ERROR_COND(resultData.isThresholdsAreAchievableSet(), "Could not find out whether the thresholds are achievable.");
STORM_LOG_ERROR_COND(resultData.isThresholdsAreAchievableSet(), "Could not find out whether the thresholds are achievable."); // This might be due to reaching the max. number of refinement steps (so no exception is thrown)
return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(initState, false));
}
}

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

@ -23,13 +23,6 @@ namespace storm {
typename SparseMultiObjectivePreprocessor<SparseModelType>::PreprocessorData SparseMultiObjectivePreprocessor<SparseModelType>::preprocess(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel) {
PreprocessorData data(originalFormula, originalModel, SparseModelType(originalModel), storm::utility::vector::buildVectorForRange(0, originalModel.getNumberOfStates()));
data.objectivesSolvedInPreprocessing = storm::storage::BitVector(originalFormula.getNumberOfSubformulas(), false);
// get a unique name for the labels of states that have to be reached with probability 1 and add the label
data.prob1StatesLabel = "prob1";
while(data.preprocessedModel.hasLabel(data.prob1StatesLabel)) {
data.prob1StatesLabel = "_" + data.prob1StatesLabel;
}
data.preprocessedModel.getStateLabeling().addLabel(data.prob1StatesLabel, storm::storage::BitVector(data.preprocessedModel.getNumberOfStates(), true));
//Invoke preprocessing on the individual objectives
for(auto const& subFormula : originalFormula.getSubFormulas()){
@ -52,9 +45,29 @@ namespace storm {
assertRewardFiniteness(data);
data.objectives = storm::utility::vector::filterVector(data.objectives, ~data.objectivesSolvedInPreprocessing);
// 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 &&
!storm::utility::vector::hasNonZeroEntry(data.preprocessedModel.getRewardModel(data.objectives[objIndex].rewardModelName).getStateActionRewardVector())) {
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);
//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!
storm::storage::BitVector objectivesWithoutThreshold(data.objectives.size());
for(uint_fast64_t objIndex = 0; objIndex < data.objectives.size(); ++objIndex) {
objectivesWithoutThreshold.set(objIndex, !data.objectives[objIndex].threshold);
@ -183,7 +196,7 @@ namespace storm {
storm::storage::BitVector noIncomingTransitionFromFirstCopyStates;
if(isProb0Formula) {
storm::storage::BitVector statesReachableInSecondCopy = storm::utility::graph::getReachableStates(data.preprocessedModel.getTransitionMatrix(), duplicatorResult.gateStates & (~newPsiStates), duplicatorResult.secondCopy, storm::storage::BitVector(data.preprocessedModel.getNumberOfStates(), false));
subsystemStates = statesReachableInSecondCopy | storm::utility::graph::performProb0E(data.preprocessedModel, data.preprocessedModel.getBackwardTransitions(), duplicatorResult.firstCopy, newPsiStates);
subsystemStates = statesReachableInSecondCopy | (duplicatorResult.firstCopy & storm::utility::graph::performProb0E(data.preprocessedModel, data.preprocessedModel.getBackwardTransitions(), duplicatorResult.firstCopy, newPsiStates));
noIncomingTransitionFromFirstCopyStates = newPsiStates;
} else {
storm::storage::BitVector statesReachableInSecondCopy = storm::utility::graph::getReachableStates(data.preprocessedModel.getTransitionMatrix(), newPsiStates, duplicatorResult.secondCopy, storm::storage::BitVector(data.preprocessedModel.getNumberOfStates(), false));
@ -191,20 +204,26 @@ namespace storm {
subsystemStates = statesReachableInSecondCopy | storm::utility::graph::performProb1E(data.preprocessedModel, data.preprocessedModel.getBackwardTransitions(), duplicatorResult.firstCopy, newPsiStates);
noIncomingTransitionFromFirstCopyStates = duplicatorResult.gateStates & (~newPsiStates);
}
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) {
for(auto const& entry : data.preprocessedModel.getTransitionMatrix().getRow(action)) {
if(noIncomingTransitionFromFirstCopyStates.get(entry.getColumn())) {
consideredActions.set(action, false);
break;
if((subsystemStates & data.preprocessedModel.getInitialStates()).empty()) {
data.solutionsFromPreprocessing[data.objectives.size()-1] = PreprocessorData::PreprocessorObjectiveSolution::False;
} else {
data.solutionsFromPreprocessing[data.objectives.size()-1] = PreprocessorData::PreprocessorObjectiveSolution::True;
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) {
for(auto const& entry : data.preprocessedModel.getTransitionMatrix().getRow(action)) {
if(noIncomingTransitionFromFirstCopyStates.get(entry.getColumn())) {
consideredActions.set(action, false);
break;
}
}
}
}
if(!subsystemStates.full() || !consideredActions.full()) {
auto subsystemBuilderResult = storm::transformer::SubsystemBuilder<SparseModelType>::transform(data.preprocessedModel, subsystemStates, consideredActions);
updatePreprocessedModel(data, *subsystemBuilderResult.model, subsystemBuilderResult.newToOldStateIndexMapping);
}
}
auto subsystemBuilderResult = storm::transformer::SubsystemBuilder<SparseModelType>::transform(data.preprocessedModel, subsystemStates, consideredActions);
updatePreprocessedModel(data, *subsystemBuilderResult.model, subsystemBuilderResult.newToOldStateIndexMapping);
data.objectivesSolvedInPreprocessing.set(data.objectives.size());
} else {
// build stateAction reward vector that gives (one*transitionProbability) reward whenever a transition leads from the firstCopy to a psiState
std::vector<ValueType> objectiveRewards(data.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero<ValueType>());
@ -276,7 +295,9 @@ namespace storm {
// We also need to enforce that the second copy will be reached eventually with prob 1.
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.full()) {
if((subsystemStates & data.preprocessedModel.getInitialStates()).empty()) {
data.solutionsFromPreprocessing[data.objectives.size()-1] = 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);
}
@ -333,10 +354,12 @@ namespace storm {
storm::storage::BitVector SparseMultiObjectivePreprocessor<SparseModelType>::assertNegativeRewardFiniteness(PreprocessorData& data) {
storm::storage::BitVector actionsWithNonNegativeReward(data.preprocessedModel.getTransitionMatrix().getRowCount(), true);
for(auto& obj : data.objectives) {
if (!obj.rewardFinitenessChecked && !obj.rewardsArePositive) {
obj.rewardFinitenessChecked = true;
actionsWithNonNegativeReward &= storm::utility::vector::filterZero(data.preprocessedModel.getRewardModel(obj.rewardModelName).getStateActionRewardVector());
storm::storage::BitVector objectivesWithNegativeReward(data.objectives.size(), false);
for(uint_fast64_t objIndex = 0; objIndex < data.objectives.size(); ++objIndex) {
if (!data.objectives[objIndex].rewardFinitenessChecked && !data.objectives[objIndex].rewardsArePositive) {
data.objectives[objIndex].rewardFinitenessChecked = true;
actionsWithNonNegativeReward &= storm::utility::vector::filterZero(data.preprocessedModel.getRewardModel(data.objectives[objIndex].rewardModelName).getStateActionRewardVector());
objectivesWithNegativeReward.set(objIndex, true);
}
}
@ -350,15 +373,21 @@ namespace storm {
storm::storage::SparseMatrix<ValueType> transitionsWithNonNegativeReward = data.preprocessedModel.getTransitionMatrix().restrictRows(actionsWithNonNegativeReward);
storm::storage::BitVector statesNeverReachingNegativeRewardForSomeScheduler = storm::utility::graph::performProb0E(transitionsWithNonNegativeReward, transitionsWithNonNegativeReward.getRowGroupIndices(), transitionsWithNonNegativeReward.transpose(true), allStates, statesWithNegativeRewardForAllChoices);
storm::storage::BitVector statesReachingNegativeRewardsFinitelyOftenForSomeScheduler = storm::utility::graph::performProb1E(data.preprocessedModel.getTransitionMatrix(), data.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), data.preprocessedModel.getBackwardTransitions(), allStates, statesNeverReachingNegativeRewardForSomeScheduler);
auto subsystemBuilderResult = storm::transformer::SubsystemBuilder<SparseModelType>::transform(data.preprocessedModel, statesReachingNegativeRewardsFinitelyOftenForSomeScheduler, storm::storage::BitVector(data.preprocessedModel.getTransitionMatrix().getRowCount(), true));
data.preprocessedModel = std::move(*subsystemBuilderResult.model);
// subsystemBuilderResult.newToOldStateIndexMapping now reffers to the indices of the model we had before building the subsystem
for(auto & originalModelStateIndex : subsystemBuilderResult.newToOldStateIndexMapping){
originalModelStateIndex = data.newToOldStateIndexMapping[originalModelStateIndex];
if((statesReachingNegativeRewardsFinitelyOftenForSomeScheduler & data.preprocessedModel.getInitialStates()).empty()) {
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;
} else {
data.solutionsFromPreprocessing[objIndex] = PreprocessorData::PreprocessorObjectiveSolution::Unbounded;
}
}
} else if(!statesReachingNegativeRewardsFinitelyOftenForSomeScheduler.full()) {
auto subsystemBuilderResult = storm::transformer::SubsystemBuilder<SparseModelType>::transform(data.preprocessedModel, statesReachingNegativeRewardsFinitelyOftenForSomeScheduler, storm::storage::BitVector(data.preprocessedModel.getTransitionMatrix().getRowCount(), true));
updatePreprocessedModel(data, *subsystemBuilderResult.model, subsystemBuilderResult.newToOldStateIndexMapping);
return (~actionsWithNonNegativeReward) % subsystemBuilderResult.subsystemActions;
}
data.newToOldStateIndexMapping = std::move(subsystemBuilderResult.newToOldStateIndexMapping);
return (~actionsWithNonNegativeReward) % subsystemBuilderResult.subsystemActions;
return ~actionsWithNonNegativeReward;
}
template<typename SparseModelType>
@ -385,8 +414,11 @@ namespace storm {
}
}
if(ecHasActionWithPositiveReward) {
STORM_LOG_DEBUG("Found end component that contains positive rewards for current objective " << *obj.originalFormula << ".");
data.objectivesSolvedInPreprocessing.set(objIndex);
if(obj.threshold) {
data.solutionsFromPreprocessing[objIndex] = PreprocessorData::PreprocessorObjectiveSolution::True;
} else {
data.solutionsFromPreprocessing[objIndex] = PreprocessorData::PreprocessorObjectiveSolution::Unbounded;
}
break;
}
}

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

@ -9,6 +9,9 @@
#include "src/logic/Formulas.h"
#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveObjectiveInformation.h"
#include "src/storage/BitVector.h"
#include "src/utility/macros.h"
#include "src/exceptions/UnexpectedException.h"
namespace storm {
namespace modelchecker {
@ -18,9 +21,10 @@ namespace storm {
struct SparseMultiObjectivePreprocessorData {
enum class QueryType { Achievability, Numerical, Pareto };
enum class PreprocessorObjectiveSolution { None, False, True, Zero, Unbounded, Undefined };
storm::logic::MultiObjectiveFormula const& originalFormula;
storm::storage::BitVector objectivesSolvedInPreprocessing;
std::vector<PreprocessorObjectiveSolution> solutionsFromPreprocessing;
SparseModelType const& originalModel;
SparseModelType preprocessedModel;
@ -33,8 +37,14 @@ namespace storm {
bool produceSchedulers;
SparseMultiObjectivePreprocessorData(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel, SparseModelType&& preprocessedModel, std::vector<uint_fast64_t>&& newToOldStateIndexMapping) : originalFormula(originalFormula), originalModel(originalModel), preprocessedModel(preprocessedModel), newToOldStateIndexMapping(newToOldStateIndexMapping), produceSchedulers(false) {
//Intentionally left empty
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) {
// get a unique name for the labels of states that have to be reached with probability 1 and add the label
this->prob1StatesLabel = "prob1";
while(this->preprocessedModel.hasLabel(this->prob1StatesLabel)) {
this->prob1StatesLabel = "_" + this->prob1StatesLabel;
}
this->preprocessedModel.getStateLabeling().addLabel(this->prob1StatesLabel, storm::storage::BitVector(this->preprocessedModel.getNumberOfStates(), true));
}
void printToStream(std::ostream& out) {
@ -45,15 +55,37 @@ namespace storm {
out << "Original Formula: " << std::endl;
out << "--------------------------------------------------------------" << std::endl;
out << "\t" << originalFormula << std::endl;
out << std::endl;
if(!objectivesSolvedInPreprocessing.empty()) {
out << "Objectives solved while preprocessing: " << std::endl;
out << "--------------------------------------------------------------" << std::endl;
for(auto const& subFIndex : objectivesSolvedInPreprocessing) {
out<< "\t" << subFIndex << ": \t" << originalFormula.getSubformula(subFIndex) << std::endl;
bool hasOneObjectiveSolvedInPreprocessing = false;
for(uint_fast64_t subformulaIndex = 0; subformulaIndex < originalFormula.getNumberOfSubformulas(); ++subformulaIndex) {
if(!hasOneObjectiveSolvedInPreprocessing && solutionsFromPreprocessing[subformulaIndex]!= PreprocessorObjectiveSolution::None) {
hasOneObjectiveSolvedInPreprocessing = true;
out << std::endl;
out << "Solutions of objectives obtained from Preprocessing: " << std::endl;
out << "--------------------------------------------------------------" << std::endl;
}
switch(solutionsFromPreprocessing[subformulaIndex]) {
case PreprocessorObjectiveSolution::None:
break;
case PreprocessorObjectiveSolution::False:
out<< "\t" << subformulaIndex << ": " << originalFormula.getSubformula(subformulaIndex) << " \t= false" << std::endl;
break;
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;
break;
case PreprocessorObjectiveSolution::Unbounded:
out<< "\t" << subformulaIndex << ": " << originalFormula.getSubformula(subformulaIndex) << " \t= unbounded" << std::endl;
break;
case PreprocessorObjectiveSolution::Undefined:
out<< "\t" << subformulaIndex << ": " << originalFormula.getSubformula(subformulaIndex) << " \t= undefined" << std::endl;
break;
default:
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "no case for PreprocessorObjectiveSolution.");
}
out << std::endl;
}
out << std::endl;
out << "Objectives:" << std::endl;
out << "--------------------------------------------------------------" << std::endl;
for (auto const& obj : objectives) {

22
src/modelchecker/multiobjective/helper/SparseMultiObjectiveResultData.h
View File

@ -41,14 +41,14 @@ namespace storm {
}
void setThresholdsAreAchievable(bool value) {
thresholdsAreAchievable = value ? Tribool::TT : Tribool::FF;
thresholdsAreAchievable = value ? Tribool::True : Tribool::False;
}
bool isThresholdsAreAchievableSet() const {
return thresholdsAreAchievable != Tribool::INDETERMINATE;
return thresholdsAreAchievable != Tribool::Indeterminate;
}
bool getThresholdsAreAchievable() const {
STORM_LOG_THROW(isThresholdsAreAchievableSet(), storm::exceptions::InvalidStateException, "Could not retrieve whether thresholds are acheivable: value not set.");
return thresholdsAreAchievable == Tribool::TT;
return thresholdsAreAchievable == Tribool::True;
}
void setNumericalResult(RationalNumberType value) {
@ -63,14 +63,14 @@ namespace storm {
}
void setOptimumIsAchievable(bool value) {
optimumIsAchievable = value ? Tribool::TT : Tribool::FF;
optimumIsAchievable = value ? Tribool::True : Tribool::False;
}
bool isOptimumIsAchievableSet() const {
return optimumIsAchievable != Tribool::INDETERMINATE;
return optimumIsAchievable != Tribool::Indeterminate;
}
bool getOptimumIsAchievableAchievable() const {
STORM_LOG_THROW(isOptimumIsAchievableSet(), storm::exceptions::InvalidStateException, "Could not retrieve whether the computed optimum is acheivable: value not set.");
return optimumIsAchievable == Tribool::TT;
return optimumIsAchievable == Tribool::True;
}
void setPrecisionOfResult(RationalNumberType value) {
@ -100,7 +100,7 @@ namespace storm {
private:
enum class Tribool { FF, TT, INDETERMINATE };
enum class Tribool { False, True, Indeterminate };
//Stores the results for the individual iterations
std::vector<SparseMultiObjectiveRefinementStep<RationalNumberType>> steps;
@ -111,21 +111,21 @@ namespace storm {
// Stores the result of an achievability query (if applicable).
// For a numerical query, stores whether there is one feasible solution.
Tribool thresholdsAreAchievable = Tribool::INDETERMINATE;
Tribool thresholdsAreAchievable = Tribool::Indeterminate;
//Stores the result of a numerical query (if applicable).
boost::optional<RationalNumberType> numericalResult;
//For numerical queries, this is true iff there is an actual scheduler that induces the computed supremum (i.e., supremum == maximum)
Tribool optimumIsAchievable = Tribool::INDETERMINATE;
Tribool optimumIsAchievable = Tribool::Indeterminate;
//Stores the achieved precision for numerical and pareto queries
boost::optional<RationalNumberType> precisionOfResult;
//Stores whether the precision of the result is sufficient (only applicable to numerical and pareto queries)
bool targetPrecisionReached;
bool targetPrecisionReached = true;
//Stores whether the computation was aborted due to performing too many refinement steps
bool maxStepsPerformed;
bool maxStepsPerformed = false;
};
}
}

5
src/transformer/SubsystemBuilder.h
View File

@ -53,7 +53,7 @@ namespace storm {
uint_fast64_t subsystemStateCount = subsystem.getNumberOfSetBits();
STORM_LOG_THROW(subsystemStateCount != 0, storm::exceptions::InvalidArgumentException, "Invoked SubsystemBuilder for an empty subsystem.");
if(subsystemStateCount == subsystem.size()) {
if(subsystemStateCount == subsystem.size() && consideredActions.full()) {
result.model = std::make_shared<SparseModelType>(originalModel);
result.newToOldStateIndexMapping = storm::utility::vector::buildVectorForRange(0, result.model->getNumberOfStates());
result.subsystemActions = storm::storage::BitVector(result.model->getTransitionMatrix().getRowCount(), true);
@ -61,13 +61,12 @@ namespace storm {
}
result.newToOldStateIndexMapping.reserve(subsystemStateCount);
result.subsystemActions = storm::storage::BitVector(result.model->getTransitionMatrix().getRowCount(), false);
result.subsystemActions = storm::storage::BitVector(originalModel.getTransitionMatrix().getRowCount(), false);
for(auto subsysState : subsystem) {
result.newToOldStateIndexMapping.push_back(subsysState);
bool stateHasOneChoiceLeft = false;
for(uint_fast64_t row = consideredActions.getNextSetIndex(originalModel.getTransitionMatrix().getRowGroupIndices()[subsysState]); row < originalModel.getTransitionMatrix().getRowGroupIndices()[subsysState+1]; row = consideredActions.getNextSetIndex(row+1)) {
bool allRowEntriesStayInSubsys = true;
result.subsystemActions.set(row, true);
for(auto const& entry : originalModel.getTransitionMatrix().getRow(row)) {
if(!subsystem.get(entry.getColumn())) {
allRowEntriesStayInSubsys = false;

12
src/utility/vector.h
View File

@ -755,10 +755,20 @@ namespace storm {
}
template<typename T>
bool hasNegativeEntries(std::vector<T> const& v){
bool hasNegativeEntry(std::vector<T> const& v){
return std::any_of(v.begin(), v.end(), [](T value){return value < storm::utility::zero<T>();});
}
template<typename T>
bool hasPositiveEntry(std::vector<T> const& v){
return std::any_of(v.begin(), v.end(), [](T value){return value > storm::utility::zero<T>();});
}
template<typename T>
bool hasNonZeroEntry(std::vector<T> const& v){
return std::any_of(v.begin(), v.end(), [](T value){return !storm::utility::isZero(value);});
}
/*!
* Output vector as string.
*

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

@ -13,6 +13,58 @@
TEST(SparseMdpMultiObjectiveModelCheckerTest, probEqual1Objective) {
std::string programFile = STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/multiobjective1.nm";
std::string formulasAsString = "multi(Rmax=? [ F s=2 ], P>=1 [ s=0 U s=1 ]) ";
formulasAsString += "; \n multi(Rmax=? [ F s=2 ], P>=1 [ F s=1 ]) ";
// programm, model, formula
storm::prism::Program program = storm::parseProgram(programFile);
program.checkValidity();
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulasAsString, program);
typename storm::builder::ExplicitPrismModelBuilder<double>::Options options = storm::builder::ExplicitPrismModelBuilder<double>::Options(formulas);
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitPrismModelBuilder<double>(program, options).translate()->as<storm::models::sparse::Mdp<double>>();
uint_fast64_t const initState = *mdp->getInitialStates().begin();
storm::modelchecker::SparseMdpMultiObjectiveModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula>(*formulas[0], true));
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
EXPECT_NEAR(7.647058824, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula>(*formulas[1], true));
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
EXPECT_NEAR(7.647058824, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
}
TEST(SparseMdpMultiObjectiveModelCheckerTest, probEqual0Objective) {
std::string programFile = STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/multiobjective1.nm";
std::string formulasAsString = "multi(Rmax=? [ F s=2 ], P<=0 [ s=0 U s=1 ]) ";
formulasAsString += "; \n multi(Rmax=? [ F s=2 ], P<=0 [ F s=1 ]) ";
// programm, model, formula
storm::prism::Program program = storm::parseProgram(programFile);
program.checkValidity();
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulasAsString, program);
typename storm::builder::ExplicitPrismModelBuilder<double>::Options options = storm::builder::ExplicitPrismModelBuilder<double>::Options(formulas);
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitPrismModelBuilder<double>(program, options).translate()->as<storm::models::sparse::Mdp<double>>();
uint_fast64_t const initState = *mdp->getInitialStates().begin();
storm::modelchecker::SparseMdpMultiObjectiveModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula>(*formulas[0], true));
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
EXPECT_NEAR(0.0, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
result = checker.check(storm::modelchecker::CheckTask<storm::logic::Formula>(*formulas[1], true));
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
EXPECT_NEAR(0.0, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
}
TEST(SparseMdpMultiObjectiveModelCheckerTest, consensus) {
std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/mdp/consensus/consensus2_3_2.nm";

20
test/functional/modelchecker/multiobjective1.nm
View File

@ -0,0 +1,20 @@
mdp
module module1
// local state
s : [0..2] init 0;
[A] s=0 -> 0.6 : (s'=1) + 0.4 : (s'=2);
[B] s=0 -> 0.3 : (s'=0) + 0.7 : (s'=1);
[C] s=0 -> 0.2 : (s'=0) + 0.8 : (s'=2);
[D] s=1 -> 0.25 : (s'=0) + 0.75 : (s'=2);
[] s=2 -> 1 : (s'=s);
endmodule
rewards "rew"
[A] true : 10;
[D] true : 4;
endrewards
Write Preview
Loading…
Cancel
Save