diff --git a/src/logic/MultiObjectiveFormula.cpp b/src/logic/MultiObjectiveFormula.cpp index 4717fd1e4..e3bfe3078 100644 --- a/src/logic/MultiObjectiveFormula.cpp +++ b/src/logic/MultiObjectiveFormula.cpp @@ -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 { diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp index f2c04ea1d..75b2c5839 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp @@ -22,22 +22,38 @@ namespace storm { resultData.overApproximation() = storm::storage::geometry::Polytope::createUniversalPolytope(); resultData.underApproximation() = storm::storage::geometry::Polytope::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 + bool SparseMultiObjectiveHelper::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 void SparseMultiObjectiveHelper::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> 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()); } } + // Note: If we have a single objective (i.e., no objectives with thresholds), thresholdsAsPolytope gets no constraints auto thresholdsAsPolytope = storm::storage::geometry::Polytope::create(thresholdConstraints); WeightVector directionOfOptimizingObjective(preprocessorData.objectives.size(), storm::utility::zero()); directionOfOptimizingObjective[optimizingObjIndex] = storm::utility::one(); diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.h index 4ada316e5..c1746eda0 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.h +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.h @@ -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); diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp index 837141a1d..5f2bdf8f7 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp @@ -19,41 +19,106 @@ namespace storm { template typename std::unique_ptr SparseMultiObjectivePostprocessor::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(new ExplicitQualitativeCheckResult());; } template typename std::unique_ptr SparseMultiObjectivePostprocessor::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(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(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(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(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(new ExplicitQualitativeCheckResult(initState, resultData.isThresholdsAreAchievableSet() &&resultData.getThresholdsAreAchievable())); } template typename std::unique_ptr SparseMultiObjectivePostprocessor::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() * optimizingObjective.toOriginalValueTransformationFactor + optimizingObjective.toOriginalValueTransformationOffset; - STORM_LOG_WARN_COND(resultData.getTargetPrecisionReached(), "The target precision for numerical queries has not been reached."); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(initState, resultForOriginalModel)); + + //Incorporate the results from prerpocessing + boost::optional 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(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(); + break; + case PreprocessorData::PreprocessorObjectiveSolution::Unbounded: + STORM_LOG_ASSERT(!preprocessorNumericalResult, "There are multiple numerical results obtained in preprocessing"); + preprocessorNumericalResult = storm::utility::infinity(); + break; + case PreprocessorData::PreprocessorObjectiveSolution::Undefined: + STORM_LOG_ERROR("The result for the objective " << preprocessorData.originalFormula.getSubformula(subformulaIndex) << " is not defined."); + return std::unique_ptr(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(new ExplicitQuantitativeCheckResult(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() * optimizingObjective.toOriginalValueTransformationFactor + optimizingObjective.toOriginalValueTransformationOffset; + STORM_LOG_WARN_COND(resultData.getTargetPrecisionReached(), "The target precision for numerical queries has not been reached."); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(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(new ExplicitQualitativeCheckResult(initState, false)); } } diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp index f1de554ea..f658268e9 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp @@ -23,13 +23,6 @@ namespace storm { typename SparseMultiObjectivePreprocessor::PreprocessorData SparseMultiObjectivePreprocessor::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() > *data.objectives[objIndex].threshold || + (!data.objectives[objIndex].thresholdIsStrict && storm::utility::zero() >= *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(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::transform(data.preprocessedModel, subsystemStates, consideredActions); + updatePreprocessedModel(data, *subsystemBuilderResult.model, subsystemBuilderResult.newToOldStateIndexMapping); + } } - auto subsystemBuilderResult = storm::transformer::SubsystemBuilder::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 objectiveRewards(data.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero()); @@ -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::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::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 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::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::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 @@ -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; } } diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h index 71827e633..89255cd33 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h @@ -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 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&& 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&& 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) { diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveResultData.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveResultData.h index 5ba05020e..b9ebba998 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveResultData.h +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveResultData.h @@ -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> 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 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 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; }; } } diff --git a/src/transformer/SubsystemBuilder.h b/src/transformer/SubsystemBuilder.h index 254ecabba..46878204a 100644 --- a/src/transformer/SubsystemBuilder.h +++ b/src/transformer/SubsystemBuilder.h @@ -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(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; diff --git a/src/utility/vector.h b/src/utility/vector.h index 4b5a26687..f8bbf1e78 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -755,10 +755,20 @@ namespace storm { } template - bool hasNegativeEntries(std::vector const& v){ + bool hasNegativeEntry(std::vector const& v){ return std::any_of(v.begin(), v.end(), [](T value){return value < storm::utility::zero();}); } + template + bool hasPositiveEntry(std::vector const& v){ + return std::any_of(v.begin(), v.end(), [](T value){return value > storm::utility::zero();}); + } + + template + bool hasNonZeroEntry(std::vector const& v){ + return std::any_of(v.begin(), v.end(), [](T value){return !storm::utility::isZero(value);}); + } + /*! * Output vector as string. * diff --git a/test/functional/modelchecker/SparseMdpMultiObjectiveModelCheckerTest.cpp b/test/functional/modelchecker/SparseMdpMultiObjectiveModelCheckerTest.cpp index b1169f3a5..66ed8808e 100644 --- a/test/functional/modelchecker/SparseMdpMultiObjectiveModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseMdpMultiObjectiveModelCheckerTest.cpp @@ -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> formulas = storm::parseFormulasForProgram(formulasAsString, program); + typename storm::builder::ExplicitPrismModelBuilder::Options options = storm::builder::ExplicitPrismModelBuilder::Options(formulas); + std::shared_ptr> mdp = storm::builder::ExplicitPrismModelBuilder(program, options).translate()->as>(); + uint_fast64_t const initState = *mdp->getInitialStates().begin(); + + storm::modelchecker::SparseMdpMultiObjectiveModelChecker> checker(*mdp); + + std::unique_ptr result = checker.check(storm::modelchecker::CheckTask(*formulas[0], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_NEAR(7.647058824, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); + + result = checker.check(storm::modelchecker::CheckTask(*formulas[1], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_NEAR(7.647058824, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().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> formulas = storm::parseFormulasForProgram(formulasAsString, program); + typename storm::builder::ExplicitPrismModelBuilder::Options options = storm::builder::ExplicitPrismModelBuilder::Options(formulas); + std::shared_ptr> mdp = storm::builder::ExplicitPrismModelBuilder(program, options).translate()->as>(); + uint_fast64_t const initState = *mdp->getInitialStates().begin(); + + storm::modelchecker::SparseMdpMultiObjectiveModelChecker> checker(*mdp); + + std::unique_ptr result = checker.check(storm::modelchecker::CheckTask(*formulas[0], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_NEAR(0.0, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); + + result = checker.check(storm::modelchecker::CheckTask(*formulas[1], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_NEAR(0.0, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); + +} + TEST(SparseMdpMultiObjectiveModelCheckerTest, consensus) { std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/mdp/consensus/consensus2_3_2.nm"; diff --git a/test/functional/modelchecker/multiobjective1.nm b/test/functional/modelchecker/multiobjective1.nm new file mode 100644 index 000000000..1db60ec50 --- /dev/null +++ b/test/functional/modelchecker/multiobjective1.nm @@ -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 +