diff --git a/resources/examples/testfiles/dtmc/test_conditional.pm b/resources/examples/testfiles/dtmc/test_conditional.pm index 57b8ba44c6..ffa12b1c54 100644 --- a/resources/examples/testfiles/dtmc/test_conditional.pm +++ b/resources/examples/testfiles/dtmc/test_conditional.pm @@ -14,5 +14,6 @@ rewards s=2 : 1; endrewards +label "unreachable" = false; label "condition" = s=2; label "target" = s=3; diff --git a/resources/examples/testfiles/dtmc/test_conditional_multiple_initial.pm b/resources/examples/testfiles/dtmc/test_conditional_multiple_initial.pm new file mode 100644 index 0000000000..68ba7f6049 --- /dev/null +++ b/resources/examples/testfiles/dtmc/test_conditional_multiple_initial.pm @@ -0,0 +1,24 @@ +dtmc + +module test + s : [0 .. 3]; + + [] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2); + [] s=1 -> 1 : true; + [] s=2 -> 1 : (s'=3); + [] s=3 -> 1 : true; + +endmodule + +// The condition is reachable from state 0, but not from state 1. +init + s=0 | s=1 +endinit + +rewards + s=2 : 1; +endrewards + +label "start" = s=0; +label "condition" = s=2; +label "target" = s=3; diff --git a/src/storm/modelchecker/helper/conditional/ConditionalHelper.cpp b/src/storm/modelchecker/helper/conditional/ConditionalHelper.cpp index 2204d48e7e..c8c71092bc 100644 --- a/src/storm/modelchecker/helper/conditional/ConditionalHelper.cpp +++ b/src/storm/modelchecker/helper/conditional/ConditionalHelper.cpp @@ -8,6 +8,7 @@ #include "storm/environment/modelchecker/ConditionalModelCheckerEnvironment.h" #include "storm/environment/modelchecker/ModelCheckerEnvironment.h" #include "storm/environment/solver/MinMaxSolverEnvironment.h" +#include "storm/exceptions/InvalidPropertyException.h" #include "storm/exceptions/NotImplementedException.h" #include "storm/exceptions/NotSupportedException.h" #include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h" @@ -1252,7 +1253,7 @@ std::optional handleTrivialCases(uint64_t const initialState, Norm if (normalForm.conditionStates.get(initialState)) { return normalForm.getTargetValue(initialState); // The value is already known, nothing to do. } else { - STORM_LOG_THROW(!normalForm.universalObservationFailureStates.get(initialState), storm::exceptions::NotSupportedException, + STORM_LOG_THROW(!normalForm.universalObservationFailureStates.get(initialState), storm::exceptions::InvalidPropertyException, "Trying to compute undefined conditional probability: the condition has probability 0 under all policies."); // The last case for a terminal initial state is that it is already target and the condition is reachable with non-zero probability. // In this case, all schedulers induce a conditional probability of 1 (or do not reach the condition, i.e., have undefined value) diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 8075d75414..f563d4b426 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -858,35 +858,39 @@ std::vector SparseDtmcPrctlHelper) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support computing conditional probabilities with interval models."); } else { + // The conditional value is only defined for states that reach the condition with positive probability. + storm::storage::BitVector const conditionProbGreater0States = + storm::utility::graph::performProbGreater0(backwardTransitions, storm::storage::BitVector(conditionStates.size(), true), conditionStates); + STORM_LOG_THROW(goal.hasRelevantValues() ? goal.relevantValues().isSubsetOf(conditionProbGreater0States) : !conditionProbGreater0States.empty(), + storm::exceptions::InvalidPropertyException, "Trying to compute an undefined conditional value: the condition is not reachable."); + // Prepare result vector. std::vector result(transitionMatrix.getRowCount(), storm::utility::infinity()); - if (!conditionStates.empty()) { - BaierTransformedModel transformedModel = - computeBaierTransformation(env, transitionMatrix, backwardTransitions, targetStates, conditionStates, boost::none); - - if (transformedModel.noTargetStates) { - storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, storm::utility::zero()); + BaierTransformedModel transformedModel = + computeBaierTransformation(env, transitionMatrix, backwardTransitions, targetStates, conditionStates, boost::none); + + if (transformedModel.noTargetStates) { + storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, storm::utility::zero()); + } else { + // At this point, we do not need to check whether there are 'before' states, since the condition + // states were non-empty so there is at least one state with a positive probability of satisfying + // the condition. + + // Now compute reachability probabilities in the transformed model. + storm::storage::SparseMatrix const& newTransitionMatrix = transformedModel.transitionMatrix.get(); + storm::storage::BitVector newRelevantValues; + if (goal.hasRelevantValues()) { + newRelevantValues = transformedModel.getNewRelevantStates(goal.relevantValues()); } else { - // At this point, we do not need to check whether there are 'before' states, since the condition - // states were non-empty so there is at least one state with a positive probability of satisfying - // the condition. - - // Now compute reachability probabilities in the transformed model. - storm::storage::SparseMatrix const& newTransitionMatrix = transformedModel.transitionMatrix.get(); - storm::storage::BitVector newRelevantValues; - if (goal.hasRelevantValues()) { - newRelevantValues = transformedModel.getNewRelevantStates(goal.relevantValues()); - } else { - newRelevantValues = transformedModel.getNewRelevantStates(); - } - goal.setRelevantValues(std::move(newRelevantValues)); - std::vector conditionalProbabilities = computeUntilProbabilities( - env, std::move(goal), newTransitionMatrix, newTransitionMatrix.transpose(), - storm::storage::BitVector(newTransitionMatrix.getRowCount(), true), transformedModel.targetStates.get(), qualitative); - - storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, conditionalProbabilities); + newRelevantValues = transformedModel.getNewRelevantStates(); } + goal.setRelevantValues(std::move(newRelevantValues)); + std::vector conditionalProbabilities = + computeUntilProbabilities(env, std::move(goal), newTransitionMatrix, newTransitionMatrix.transpose(), + storm::storage::BitVector(newTransitionMatrix.getRowCount(), true), transformedModel.targetStates.get(), qualitative); + + storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, conditionalProbabilities); } return result; @@ -901,34 +905,38 @@ std::vector SparseDtmcPrctlHelper) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support computing conditional rewards with interval models."); } else { + // The conditional value is only defined for states that reach the condition with positive probability. + storm::storage::BitVector const conditionProbGreater0States = + storm::utility::graph::performProbGreater0(backwardTransitions, storm::storage::BitVector(conditionStates.size(), true), conditionStates); + STORM_LOG_THROW(goal.hasRelevantValues() ? goal.relevantValues().isSubsetOf(conditionProbGreater0States) : !conditionProbGreater0States.empty(), + storm::exceptions::InvalidPropertyException, "Trying to compute an undefined conditional value: the condition is not reachable."); + // Prepare result vector. std::vector result(transitionMatrix.getRowCount(), storm::utility::infinity()); - if (!conditionStates.empty()) { - BaierTransformedModel transformedModel = computeBaierTransformation(env, transitionMatrix, backwardTransitions, targetStates, conditionStates, - rewardModel.getTotalRewardVector(transitionMatrix)); - - if (transformedModel.noTargetStates) { - storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, storm::utility::zero()); + BaierTransformedModel transformedModel = computeBaierTransformation(env, transitionMatrix, backwardTransitions, targetStates, conditionStates, + rewardModel.getTotalRewardVector(transitionMatrix)); + + if (transformedModel.noTargetStates) { + storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, storm::utility::zero()); + } else { + // At this point, we do not need to check whether there are 'before' states, since the condition + // states were non-empty so there is at least one state with a positive probability of satisfying + // the condition. + + // Now compute reachability probabilities in the transformed model. + storm::storage::SparseMatrix const& newTransitionMatrix = transformedModel.transitionMatrix.get(); + storm::storage::BitVector newRelevantValues; + if (goal.hasRelevantValues()) { + newRelevantValues = transformedModel.getNewRelevantStates(goal.relevantValues()); } else { - // At this point, we do not need to check whether there are 'before' states, since the condition - // states were non-empty so there is at least one state with a positive probability of satisfying - // the condition. - - // Now compute reachability probabilities in the transformed model. - storm::storage::SparseMatrix const& newTransitionMatrix = transformedModel.transitionMatrix.get(); - storm::storage::BitVector newRelevantValues; - if (goal.hasRelevantValues()) { - newRelevantValues = transformedModel.getNewRelevantStates(goal.relevantValues()); - } else { - newRelevantValues = transformedModel.getNewRelevantStates(); - } - goal.setRelevantValues(std::move(newRelevantValues)); - std::vector conditionalRewards = - computeReachabilityRewards(env, std::move(goal), newTransitionMatrix, newTransitionMatrix.transpose(), transformedModel.stateRewards.get(), - transformedModel.targetStates.get(), qualitative); - storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, conditionalRewards); + newRelevantValues = transformedModel.getNewRelevantStates(); } + goal.setRelevantValues(std::move(newRelevantValues)); + std::vector conditionalRewards = + computeReachabilityRewards(env, std::move(goal), newTransitionMatrix, newTransitionMatrix.transpose(), transformedModel.stateRewards.get(), + transformedModel.targetStates.get(), qualitative); + storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, conditionalRewards); } return result; diff --git a/src/test/storm/modelchecker/prctl/dtmc/ConditionalDtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/dtmc/ConditionalDtmcPrctlModelCheckerTest.cpp index 73c4d213ee..c711a13a6e 100644 --- a/src/test/storm/modelchecker/prctl/dtmc/ConditionalDtmcPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/dtmc/ConditionalDtmcPrctlModelCheckerTest.cpp @@ -7,6 +7,7 @@ #include "storm/environment/solver/EigenSolverEnvironment.h" #include "storm/environment/solver/GmmxxSolverEnvironment.h" #include "storm/environment/solver/NativeSolverEnvironment.h" +#include "storm/exceptions/InvalidPropertyException.h" #include "storm/logic/Formulas.h" #include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" @@ -165,6 +166,10 @@ TYPED_TEST(ConditionalDtmcPrctlModelCheckerTest, Conditional) { storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(storm::utility::one(), quantitativeResult2[0], this->precision()); + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"target\" || F \"unreachable\"]"); + + STORM_SILENT_EXPECT_THROW(checker.check(this->env(), *formula), storm::exceptions::InvalidPropertyException); + formula = formulaParser.parseSingleFormulaFromString("R=? [F \"target\"]"); result = checker.check(this->env(), *formula); @@ -176,5 +181,54 @@ TYPED_TEST(ConditionalDtmcPrctlModelCheckerTest, Conditional) { result = checker.check(this->env(), *formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(storm::utility::one(), quantitativeResult4[0], this->precision()); + + formula = formulaParser.parseSingleFormulaFromString("R=? [F \"target\" || F \"unreachable\"]"); + + STORM_SILENT_EXPECT_THROW(checker.check(this->env(), *formula), storm::exceptions::InvalidPropertyException); +} + +TYPED_TEST(ConditionalDtmcPrctlModelCheckerTest, ConditionalUnreachableFromInitialState) { + typedef typename TestFixture::ValueType ValueType; + + // In this model, the condition is reachable from one of the two initial states only. + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/test_conditional_multiple_initial.pm"); + + storm::generator::NextStateGeneratorOptions options; + options.setBuildAllLabels().setBuildAllRewardModels(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).build(); + ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc); + ASSERT_EQ(4ul, model->getNumberOfStates()); + + std::shared_ptr> dtmc = model->template as>(); + ASSERT_EQ(2ul, dtmc->getInitialStates().getNumberOfSetBits()); + storm::storage::BitVector initialStatesWithoutCondition = dtmc->getInitialStates() & ~dtmc->getStates("start"); + ASSERT_EQ(1ul, initialStatesWithoutCondition.getNumberOfSetBits()); + + storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc); + + auto expManager = std::make_shared(); + storm::parser::FormulaParser formulaParser(expManager); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"target\" || F \"condition\"]"); + + // If we are only interested in the initial states, the value is undefined for the initial state that cannot reach the condition. + STORM_SILENT_EXPECT_THROW(checker.check(this->env(), storm::modelchecker::CheckTask(*formula, true)), + storm::exceptions::InvalidPropertyException); + + // If all states are relevant, the undefined values are reported as infinity. + std::unique_ptr result = checker.check(this->env(), *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(storm::utility::one(), quantitativeResult1[*dtmc->getStates("start").begin()], this->precision()); + EXPECT_EQ(storm::utility::infinity(), quantitativeResult1[*initialStatesWithoutCondition.begin()]); + + formula = formulaParser.parseSingleFormulaFromString("R=? [F \"target\" || F \"condition\"]"); + + STORM_SILENT_EXPECT_THROW(checker.check(this->env(), storm::modelchecker::CheckTask(*formula, true)), + storm::exceptions::InvalidPropertyException); + + result = checker.check(this->env(), *formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(storm::utility::one(), quantitativeResult2[*dtmc->getStates("start").begin()], this->precision()); + EXPECT_EQ(storm::utility::infinity(), quantitativeResult2[*initialStatesWithoutCondition.begin()]); } } // namespace