24 STORM_LOG_THROW(this->currentCheckTask, storm::exceptions::InvalidStateException,
"Checking has been invoked but no property has been specified before.");
25 auto const& instantiatedModel = modelInstantiator.instantiate(valuation);
26 STORM_LOG_THROW(instantiatedModel.getTransitionMatrix().isProbabilistic(), storm::exceptions::InvalidArgumentException,
27 "Instantiation point is invalid as the transition matrix becomes non-stochastic.");
32 return checkReachabilityProbabilityFormula(env, modelChecker);
38 return checkReachabilityRewardFormula(env, modelChecker);
46 return checkBoundedUntilFormula(env, modelChecker);
48 return modelChecker.
check(env, *this->currentCheckTask);
55 if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) {
60 if (this->getInstantiationsAreGraphPreserving() && !hint.
hasMaybeStates()) {
62 std::vector<ConstantType> qualitativeResult;
63 if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
64 auto newCheckTask = *this->currentCheckTask;
65 newCheckTask.setQualitative(
true);
66 newCheckTask.setOnlyInitialStatesRelevant(
false);
67 qualitativeResult = modelChecker.check(env, newCheckTask)->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
69 auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula());
70 newCheckTask.setQualitative(
true);
71 newCheckTask.setOnlyInitialStatesRelevant(
false);
73 modelChecker.computeProbabilities(env, newCheckTask)->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
75 storm::storage::BitVector maybeStates = storm::utility::vector::filter<ConstantType>(qualitativeResult, [](ConstantType
const& value) ->
bool {
76 return !(storm::utility::isZero<ConstantType>(value) || storm::utility::isOne<ConstantType>(value));
83 std::unique_ptr<CheckResult> result;
86 if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
87 result = modelChecker.check(env, *this->currentCheckTask);
88 hint.
setResultHint(result->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector());
90 auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula())
91 .setOnlyInitialStatesRelevant(
false);
92 std::unique_ptr<CheckResult> quantitativeResult = modelChecker.computeProbabilities(env, newCheckTask);
93 result = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().compareAgainstBound(
94 this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(),
95 this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs<ConstantType>());
96 hint.
setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()));
105 if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) {
110 if (this->getInstantiationsAreGraphPreserving() && !hint.
hasMaybeStates()) {
112 std::vector<ConstantType> qualitativeResult;
113 if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
114 auto newCheckTask = *this->currentCheckTask;
115 newCheckTask.setQualitative(
true);
116 newCheckTask.setOnlyInitialStatesRelevant(
false);
117 qualitativeResult = modelChecker.check(env, newCheckTask)->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
119 auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula());
120 newCheckTask.setQualitative(
true);
121 newCheckTask.setOnlyInitialStatesRelevant(
false);
122 qualitativeResult = modelChecker.computeRewards(env, newCheckTask)->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
124 storm::storage::BitVector maybeStates = storm::utility::vector::filter<ConstantType>(qualitativeResult, [](ConstantType
const& value) ->
bool {
125 return !(storm::utility::isZero<ConstantType>(value) || storm::utility::isInfinity<ConstantType>(value));
132 std::unique_ptr<CheckResult> result;
136 if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
137 result = modelChecker.check(env, *this->currentCheckTask);
138 this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>().setResultHint(
139 result->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector());
141 auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula())
142 .setOnlyInitialStatesRelevant(
false);
143 std::unique_ptr<CheckResult> quantitativeResult = modelChecker.computeRewards(env, newCheckTask);
144 result = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().compareAgainstBound(
145 this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(),
146 this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs<ConstantType>());
147 this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>().setResultHint(
148 std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()));
157 if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) {
160 std::unique_ptr<CheckResult> result;
163 if (this->getInstantiationsAreGraphPreserving() && !hint.
hasMaybeStates()) {
166 if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
167 result = modelChecker.check(env, *this->currentCheckTask);
168 hint.
setResultHint(result->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector());
170 auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula())
171 .setOnlyInitialStatesRelevant(
false);
172 std::unique_ptr<CheckResult> quantitativeResult = modelChecker.computeProbabilities(env, newCheckTask);
173 result = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().compareAgainstBound(
174 this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(),
175 this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs<ConstantType>());
176 hint.
setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()));
182 std::unique_ptr<CheckResult> subFormulaResult =
183 modelChecker.check(env, this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asBoundedUntilFormula().getRightSubformula());
184 maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector());
188 result = modelChecker.check(env, *this->currentCheckTask);