diff --git a/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp b/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp index 5de3d8fd3..9ea15c4f9 100644 --- a/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp +++ b/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp @@ -42,8 +42,31 @@ namespace storm { this->currentCheckTask->setHint(std::make_shared>()); } ExplicitModelCheckerHint& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint(); - std::unique_ptr result; + if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { + // Perform purely qualitative analysis once + std::vector qualitativeResult; + if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { + auto newCheckTask = *this->currentCheckTask; + newCheckTask.setQualitative(true); + newCheckTask.setOnlyInitialStatesRelevant(false); + qualitativeResult = modelChecker.check(env, newCheckTask)->template asExplicitQuantitativeCheckResult().getValueVector(); + } else { + auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()); + newCheckTask.setQualitative(true); + newCheckTask.setOnlyInitialStatesRelevant(false); + qualitativeResult = modelChecker.computeProbabilities(env, newCheckTask)->template asExplicitQuantitativeCheckResult().getValueVector(); + } + std::cout << storm::utility::vector::toString(qualitativeResult) << std::endl; + storm::storage::BitVector maybeStates = storm::utility::vector::filter(qualitativeResult, + [] (ConstantType const& value) -> bool { return !(storm::utility::isZero(value) || storm::utility::isOne(value)); }); + std::cout < result; // Check the formula and store the result as a hint for the next call. // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { @@ -56,15 +79,6 @@ namespace storm { hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult().getValueVector())); } - if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { - // Extract the maybe states from the current result. - assert(hint.hasResultHint()); - storm::storage::BitVector maybeStates = ~storm::utility::vector::filter(hint.getResultHint(), - [] (ConstantType const& value) -> bool { return storm::utility::isZero(value) || storm::utility::isOne(value); }); - hint.setMaybeStates(std::move(maybeStates)); - hint.setComputeOnlyMaybeStates(true); - } - return result; } @@ -75,6 +89,28 @@ namespace storm { this->currentCheckTask->setHint(std::make_shared>()); } ExplicitModelCheckerHint& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint(); + + if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { + // Perform purely qualitative analysis once + std::vector qualitativeResult; + if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { + auto newCheckTask = *this->currentCheckTask; + newCheckTask.setQualitative(true); + newCheckTask.setOnlyInitialStatesRelevant(false); + qualitativeResult = modelChecker.check(env, newCheckTask)->template asExplicitQuantitativeCheckResult().getValueVector(); + } else { + auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()); + newCheckTask.setQualitative(true); + newCheckTask.setOnlyInitialStatesRelevant(false); + qualitativeResult = modelChecker.computeRewards(env, this->currentCheckTask->getFormula().asRewardOperatorFormula().getMeasureType(), newCheckTask)->template asExplicitQuantitativeCheckResult().getValueVector(); + } + storm::storage::BitVector maybeStates = storm::utility::vector::filter(qualitativeResult, + [] (ConstantType const& value) -> bool { return !(storm::utility::isZero(value) || storm::utility::isInfinity(value)); }); + hint.setMaybeStates(std::move(maybeStates)); + hint.setResultHint(std::move(qualitativeResult)); + hint.setComputeOnlyMaybeStates(true); + } + std::unique_ptr result; // Check the formula and store the result as a hint for the next call. @@ -89,18 +125,6 @@ namespace storm { this->currentCheckTask->getHint().template asExplicitModelCheckerHint().setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult().getValueVector())); } - if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { - // Extract the maybe states from the current result. - assert(hint.hasResultHint()); - storm::storage::BitVector maybeStates = ~storm::utility::vector::filterInfinity(hint.getResultHint()); - // We need to exclude the target states from the maybe states. - // Note that we can not consider the states with reward zero since a valuation might set a reward to zero - std::unique_ptr subFormulaResult = modelChecker.check(env, this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asEventuallyFormula().getSubformula()); - maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector()); - hint.setMaybeStates(std::move(maybeStates)); - hint.setComputeOnlyMaybeStates(true); - } - return result; } diff --git a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp index 3dc4866d3..0f1e8b9ac 100644 --- a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp +++ b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp @@ -47,8 +47,31 @@ namespace storm { this->currentCheckTask->setHint(std::make_shared>()); } ExplicitModelCheckerHint& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint(); - std::unique_ptr result; + if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { + // Perform purely qualitative analysis once + std::vector qualitativeResult; + if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { + auto newCheckTask = *this->currentCheckTask; + newCheckTask.setQualitative(true); + newCheckTask.setOnlyInitialStatesRelevant(false); + qualitativeResult = modelChecker.check(env, newCheckTask)->template asExplicitQuantitativeCheckResult().getValueVector(); + } else { + auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()); + newCheckTask.setQualitative(true); + newCheckTask.setOnlyInitialStatesRelevant(false); + qualitativeResult = modelChecker.computeProbabilities(env, newCheckTask)->template asExplicitQuantitativeCheckResult().getValueVector(); + } + std::cout << storm::utility::vector::toString(qualitativeResult) << std::endl; + storm::storage::BitVector maybeStates = storm::utility::vector::filter(qualitativeResult, + [] (ConstantType const& value) -> bool { return !(storm::utility::isZero(value) || storm::utility::isOne(value)); }); + std::cout < result; // Check the formula and store the result as a hint for the next call. // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { @@ -65,21 +88,6 @@ namespace storm { hint.setSchedulerHint(std::move(dynamic_cast&>(scheduler))); } - if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { - // Extract the maybe states from the current result. - assert(hint.hasResultHint()); - storm::storage::BitVector maybeStates = ~storm::utility::vector::filter(hint.getResultHint(), - [] (ConstantType const& value) -> bool { return storm::utility::isZero(value) || storm::utility::isOne(value); }); - hint.setMaybeStates(std::move(maybeStates)); - hint.setComputeOnlyMaybeStates(true); - - // Check if there can be end components within the maybestates - if (storm::solver::minimize(this->currentCheckTask->getOptimizationDirection()) || - storm::utility::graph::performProb1A(instantiatedModel.getTransitionMatrix(), instantiatedModel.getTransitionMatrix().getRowGroupIndices(), instantiatedModel.getBackwardTransitions(), hint.getMaybeStates(), ~hint.getMaybeStates()).full()) { - hint.setNoEndComponentsInMaybeStates(true); - } - } - return result; } @@ -92,8 +100,29 @@ namespace storm { this->currentCheckTask->setHint(std::make_shared>()); } ExplicitModelCheckerHint& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint(); - std::unique_ptr result; + if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { + // Perform purely qualitative analysis once + std::vector qualitativeResult; + if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { + auto newCheckTask = *this->currentCheckTask; + newCheckTask.setQualitative(true); + newCheckTask.setOnlyInitialStatesRelevant(false); + qualitativeResult = modelChecker.check(env, newCheckTask)->template asExplicitQuantitativeCheckResult().getValueVector(); + } else { + auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()); + newCheckTask.setQualitative(true); + newCheckTask.setOnlyInitialStatesRelevant(false); + qualitativeResult = modelChecker.computeRewards(env, this->currentCheckTask->getFormula().asRewardOperatorFormula().getMeasureType(), newCheckTask)->template asExplicitQuantitativeCheckResult().getValueVector(); + } + storm::storage::BitVector maybeStates = storm::utility::vector::filter(qualitativeResult, + [] (ConstantType const& value) -> bool { return !(storm::utility::isZero(value) || storm::utility::isInfinity(value)); }); + hint.setMaybeStates(std::move(maybeStates)); + hint.setResultHint(std::move(qualitativeResult)); + hint.setComputeOnlyMaybeStates(true); + } + + std::unique_ptr result; // Check the formula and store the result as a hint for the next call. // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula if(this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { @@ -110,23 +139,6 @@ namespace storm { hint.setSchedulerHint(std::move(dynamic_cast&>(scheduler))); } - if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { - // Extract the maybe states from the current result. - assert(hint.hasResultHint()); - storm::storage::BitVector maybeStates = ~storm::utility::vector::filterInfinity(hint.getResultHint()); - // We need to exclude the target states from the maybe states. - // Note that we can not consider the states with reward zero since a valuation might set a reward to zero - std::unique_ptr subFormulaResult = modelChecker.check(env, this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asEventuallyFormula().getSubformula()); - maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector()); - hint.setMaybeStates(std::move(maybeStates)); - hint.setComputeOnlyMaybeStates(true); - - // Check if there can be end components within the maybestates - if (storm::solver::maximize(this->currentCheckTask->getOptimizationDirection()) || - storm::utility::graph::performProb1A(instantiatedModel.getTransitionMatrix(), instantiatedModel.getTransitionMatrix().getRowGroupIndices(), instantiatedModel.getBackwardTransitions(), hint.getMaybeStates(), ~hint.getMaybeStates()).full()) { - hint.setNoEndComponentsInMaybeStates(true); - } - } return result; } diff --git a/src/storm/modelchecker/CheckTask.h b/src/storm/modelchecker/CheckTask.h index 45f2a9bc3..898795fda 100644 --- a/src/storm/modelchecker/CheckTask.h +++ b/src/storm/modelchecker/CheckTask.h @@ -207,6 +207,14 @@ namespace storm { bool isQualitativeSet() const { return qualitative; } + + /*! + * sets whether the computation only needs to be performed qualitatively, because the values will only + * be compared to 0/1. + */ + void setQualitative(bool value) { + qualitative = value; + } /*! * Sets whether to produce schedulers (if supported).