diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 8dcd741e1b..1e81947d93 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -1302,7 +1302,7 @@ void verifyModel(std::shared_ptr> const& std::unique_ptr filter; if (filterForInitialStates) { - filter = std::make_unique(sparseModel->getInitialStates()); + filter = std::make_unique>(sparseModel->getInitialStates()); } else if (!states->isTrueFormula()) { // No need to apply filter if it is the formula 'true' filter = storm::api::verifyWithSparseEngine(mpi.env, sparseModel, storm::api::createTask(states, false)); } @@ -1348,6 +1348,13 @@ void verifyModel(std::shared_ptr> const& auto const& paretoRes = result->template asExplicitParetoCurveCheckResult(); storm::api::exportParetoScheduler(sparseModel, paretoRes.getPoints(), paretoRes.getSchedulers(), schedulerExportPath.string()); } + } else if (result->isExplicitQualitativeCheckResult()) { + if constexpr (storm::IsIntervalType) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Scheduler export for interval models is not supported."); + } else { + storm::api::exportScheduler(sparseModel, result->template asExplicitQualitativeCheckResult().getScheduler(), + schedulerExportPath.string()); + } } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Scheduler export not supported for this value type."); } diff --git a/src/storm-counterexamples/api/counterexamples.cpp b/src/storm-counterexamples/api/counterexamples.cpp index 6738bf2239..af0104a901 100644 --- a/src/storm-counterexamples/api/counterexamples.cpp +++ b/src/storm-counterexamples/api/counterexamples.cpp @@ -45,7 +45,7 @@ std::shared_ptr computeKShortestPathCoun storm::logic::EventuallyFormula const& eventuallyFormula = subformula.asEventuallyFormula(); std::unique_ptr subResult = modelchecker.check(env, eventuallyFormula.getSubformula()); - storm::modelchecker::ExplicitQualitativeCheckResult const& subQualitativeResult = subResult->asExplicitQualitativeCheckResult(); + storm::modelchecker::ExplicitQualitativeCheckResult const& subQualitativeResult = subResult->template asExplicitQualitativeCheckResult(); // Check if counterexample is even possible storm::storage::BitVector phiStates(model->getNumberOfStates(), true); diff --git a/src/storm-counterexamples/counterexamples/MILPMinimalLabelSetGenerator.h b/src/storm-counterexamples/counterexamples/MILPMinimalLabelSetGenerator.h index cdd057d069..e14a490411 100644 --- a/src/storm-counterexamples/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/storm-counterexamples/counterexamples/MILPMinimalLabelSetGenerator.h @@ -1023,8 +1023,8 @@ class MILPMinimalLabelSetGenerator { std::unique_ptr leftResult = modelchecker.check(env, untilFormula.getLeftSubformula()); std::unique_ptr rightResult = modelchecker.check(env, untilFormula.getRightSubformula()); - storm::modelchecker::ExplicitQualitativeCheckResult const& leftQualitativeResult = leftResult->asExplicitQualitativeCheckResult(); - storm::modelchecker::ExplicitQualitativeCheckResult const& rightQualitativeResult = rightResult->asExplicitQualitativeCheckResult(); + storm::modelchecker::ExplicitQualitativeCheckResult const& leftQualitativeResult = leftResult->template asExplicitQualitativeCheckResult(); + storm::modelchecker::ExplicitQualitativeCheckResult const& rightQualitativeResult = rightResult->template asExplicitQualitativeCheckResult(); phiStates = leftQualitativeResult.getTruthValuesVector(); psiStates = rightQualitativeResult.getTruthValuesVector(); @@ -1033,7 +1033,7 @@ class MILPMinimalLabelSetGenerator { std::unique_ptr subResult = modelchecker.check(env, eventuallyFormula.getSubformula()); - storm::modelchecker::ExplicitQualitativeCheckResult const& subQualitativeResult = subResult->asExplicitQualitativeCheckResult(); + storm::modelchecker::ExplicitQualitativeCheckResult const& subQualitativeResult = subResult->template asExplicitQualitativeCheckResult(); phiStates = storm::storage::BitVector(mdp.getNumberOfStates(), true); psiStates = subQualitativeResult.getTruthValuesVector(); diff --git a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h index 4cf453c738..5a837289ae 100644 --- a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h +++ b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h @@ -2157,8 +2157,8 @@ class SMTMinimalLabelSetGenerator { std::unique_ptr leftResult = modelchecker.check(env, untilFormula.getLeftSubformula()); std::unique_ptr rightResult = modelchecker.check(env, untilFormula.getRightSubformula()); - storm::modelchecker::ExplicitQualitativeCheckResult const& leftQualitativeResult = leftResult->asExplicitQualitativeCheckResult(); - storm::modelchecker::ExplicitQualitativeCheckResult const& rightQualitativeResult = rightResult->asExplicitQualitativeCheckResult(); + storm::modelchecker::ExplicitQualitativeCheckResult const& leftQualitativeResult = leftResult->template asExplicitQualitativeCheckResult(); + storm::modelchecker::ExplicitQualitativeCheckResult const& rightQualitativeResult = rightResult->template asExplicitQualitativeCheckResult(); result.phiStates = leftQualitativeResult.getTruthValuesVector(); result.psiStates = rightQualitativeResult.getTruthValuesVector(); @@ -2167,7 +2167,7 @@ class SMTMinimalLabelSetGenerator { std::unique_ptr subResult = modelchecker.check(env, eventuallyFormula.getSubformula()); - storm::modelchecker::ExplicitQualitativeCheckResult const& subQualitativeResult = subResult->asExplicitQualitativeCheckResult(); + storm::modelchecker::ExplicitQualitativeCheckResult const& subQualitativeResult = subResult->template asExplicitQualitativeCheckResult(); result.phiStates = storm::storage::BitVector(model.getNumberOfStates(), true); result.psiStates = subQualitativeResult.getTruthValuesVector(); diff --git a/src/storm-dft/modelchecker/DFTModelChecker.cpp b/src/storm-dft/modelchecker/DFTModelChecker.cpp index 6dbbc1f31a..e56ed46673 100644 --- a/src/storm-dft/modelchecker/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/DFTModelChecker.cpp @@ -461,7 +461,7 @@ std::vector DFTModelChecker::checkModel(std::shared_ptr(model, storm::api::createTask(property, true))); if (result) { - result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); + result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); ValueType resultValue = result->asExplicitQuantitativeCheckResult().getValueMap().begin()->second; results.push_back(resultValue); } else { diff --git a/src/storm-pars-cli/sampling.h b/src/storm-pars-cli/sampling.h index 622f806415..b163dabe3f 100644 --- a/src/storm-pars-cli/sampling.h +++ b/src/storm-pars-cli/sampling.h @@ -115,7 +115,7 @@ void verifyPropertiesAtSamplePoints(ModelType const& model, cli::SymbolicInput c valuationWatch.stop(); if (result) { - result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model.getInitialStates())); + result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model.getInitialStates())); } printInitialStatesResult(result, &valuationWatch, &valuation); diff --git a/src/storm-pars-cli/solutionFunctions.h b/src/storm-pars-cli/solutionFunctions.h index 294c50c56b..8c74e278ff 100644 --- a/src/storm-pars-cli/solutionFunctions.h +++ b/src/storm-pars-cli/solutionFunctions.h @@ -31,7 +31,7 @@ void computeSolutionFunctionsWithSparseEngine(std::shared_ptr result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(formula, true)); if (result) { - result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); + result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); } return result; }, diff --git a/src/storm-pars/derivative/SparseDerivativeInstantiationModelChecker.cpp b/src/storm-pars/derivative/SparseDerivativeInstantiationModelChecker.cpp index 5bf5ec4f12..8f57bb92f7 100644 --- a/src/storm-pars/derivative/SparseDerivativeInstantiationModelChecker.cpp +++ b/src/storm-pars/derivative/SparseDerivativeInstantiationModelChecker.cpp @@ -143,20 +143,20 @@ void SparseDerivativeInstantiationModelChecker::spec if (this->currentFormula->isRewardOperatorFormula()) { auto subformula = modelchecker::CheckTask( this->currentFormula->asRewardOperatorFormula().getSubformula().asEventuallyFormula().getSubformula()); - target = propositionalChecker.check(subformula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + target = propositionalChecker.check(subformula)->template asExplicitQualitativeCheckResult().getTruthValuesVector(); } else { if (this->currentFormula->asProbabilityOperatorFormula().getSubformula().isUntilFormula()) { auto rightSubformula = modelchecker::CheckTask( this->currentFormula->asProbabilityOperatorFormula().getSubformula().asUntilFormula().getRightSubformula()); auto leftSubformula = modelchecker::CheckTask( this->currentFormula->asProbabilityOperatorFormula().getSubformula().asUntilFormula().getLeftSubformula()); - target = propositionalChecker.check(rightSubformula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); - avoid = propositionalChecker.check(leftSubformula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + target = propositionalChecker.check(rightSubformula)->template asExplicitQualitativeCheckResult().getTruthValuesVector(); + avoid = propositionalChecker.check(leftSubformula)->template asExplicitQualitativeCheckResult().getTruthValuesVector(); avoid.complement(); } else { auto subformula = modelchecker::CheckTask( this->currentFormula->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula()); - target = propositionalChecker.check(subformula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + target = propositionalChecker.check(subformula)->template asExplicitQualitativeCheckResult().getTruthValuesVector(); } } initialStateModel = model.getStates("init").getNextSetIndex(0); diff --git a/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp b/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp index 6b7387b67c..6551db7209 100644 --- a/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp +++ b/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp @@ -181,7 +181,7 @@ std::unique_ptr SparseDtmcInstantiationModelChecker0 steps std::unique_ptr subFormulaResult = modelChecker.check(env, this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asBoundedUntilFormula().getRightSubformula()); - maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector()); + maybeStates = maybeStates & ~(subFormulaResult->template asExplicitQualitativeCheckResult().getTruthValuesVector()); hint.setMaybeStates(std::move(maybeStates)); hint.setComputeOnlyMaybeStates(true); } else { diff --git a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp index dc75828481..d866cc858b 100644 --- a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp +++ b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp @@ -220,7 +220,7 @@ std::unique_ptr SparseMdpInstantiationModelChecker0 steps std::unique_ptr subFormulaResult = modelChecker.check(env, this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asBoundedUntilFormula().getRightSubformula()); - maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector()); + maybeStates = maybeStates & ~(subFormulaResult->template asExplicitQualitativeCheckResult().getTruthValuesVector()); hint.setMaybeStates(std::move(maybeStates)); hint.setComputeOnlyMaybeStates(true); } else { diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp index 11ada9bdd9..002151ac7c 100644 --- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp @@ -150,10 +150,12 @@ void SparseDtmcParameterLiftingModelCheckerasExplicitQualitativeCheckResult().getTruthValuesVector()); - storm::storage::BitVector psiStates = - std::move(propositionalChecker.check(checkTask.getFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector()); + storm::storage::BitVector phiStates = std::move(propositionalChecker.check(checkTask.getFormula().getLeftSubformula()) + ->template asExplicitQualitativeCheckResult() + .getTruthValuesVector()); + storm::storage::BitVector psiStates = std::move(propositionalChecker.check(checkTask.getFormula().getRightSubformula()) + ->template asExplicitQualitativeCheckResult() + .getTruthValuesVector()); // get the maybeStates maybeStates = storm::utility::graph::performProbGreater0(this->parametricModel->getBackwardTransitions(), phiStates, psiStates, true, *stepBound); @@ -192,10 +194,12 @@ void SparseDtmcParameterLiftingModelCheckerasExplicitQualitativeCheckResult().getTruthValuesVector()); - storm::storage::BitVector psiStates = - std::move(propositionalChecker.check(checkTask.getFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector()); + storm::storage::BitVector phiStates = std::move(propositionalChecker.check(checkTask.getFormula().getLeftSubformula()) + ->template asExplicitQualitativeCheckResult() + .getTruthValuesVector()); + storm::storage::BitVector psiStates = std::move(propositionalChecker.check(checkTask.getFormula().getRightSubformula()) + ->template asExplicitQualitativeCheckResult() + .getTruthValuesVector()); // get the maybeStates std::pair statesWithProbability01 = @@ -264,8 +268,9 @@ void SparseDtmcParameterLiftingModelChecker propositionalChecker(*this->parametricModel); STORM_LOG_THROW(propositionalChecker.canHandle(checkTask.getFormula().getSubformula()), storm::exceptions::NotSupportedException, "Parameter lifting with non-propositional subformulas is not supported"); - storm::storage::BitVector targetStates = - std::move(propositionalChecker.check(checkTask.getFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector()); + storm::storage::BitVector targetStates = std::move(propositionalChecker.check(checkTask.getFormula().getSubformula()) + ->template asExplicitQualitativeCheckResult() + .getTruthValuesVector()); // get the maybeStates storm::storage::BitVector infinityStates = storm::utility::graph::performProb1( this->parametricModel->getBackwardTransitions(), storm::storage::BitVector(this->parametricModel->getNumberOfStates(), true), targetStates); diff --git a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp index 9e9c2f366f..4294ad72b5 100644 --- a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp @@ -109,10 +109,12 @@ void SparseMdpParameterLiftingModelChecker::speci STORM_LOG_THROW(propositionalChecker.canHandle(checkTask.getFormula().getLeftSubformula()) && propositionalChecker.canHandle(checkTask.getFormula().getRightSubformula()), storm::exceptions::NotSupportedException, "Parameter lifting with non-propositional subformulas is not supported"); - storm::storage::BitVector phiStates = - std::move(propositionalChecker.check(checkTask.getFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector()); - storm::storage::BitVector psiStates = - std::move(propositionalChecker.check(checkTask.getFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector()); + storm::storage::BitVector phiStates = std::move(propositionalChecker.check(checkTask.getFormula().getLeftSubformula()) + ->template asExplicitQualitativeCheckResult() + .getTruthValuesVector()); + storm::storage::BitVector psiStates = std::move(propositionalChecker.check(checkTask.getFormula().getRightSubformula()) + ->template asExplicitQualitativeCheckResult() + .getTruthValuesVector()); // get the maybeStates maybeStates = storm::solver::minimize(checkTask.getOptimizationDirection()) @@ -152,10 +154,12 @@ void SparseMdpParameterLiftingModelChecker::speci STORM_LOG_THROW(propositionalChecker.canHandle(checkTask.getFormula().getLeftSubformula()) && propositionalChecker.canHandle(checkTask.getFormula().getRightSubformula()), storm::exceptions::NotSupportedException, "Parameter lifting with non-propositional subformulas is not supported"); - storm::storage::BitVector phiStates = - std::move(propositionalChecker.check(checkTask.getFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector()); - storm::storage::BitVector psiStates = - std::move(propositionalChecker.check(checkTask.getFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector()); + storm::storage::BitVector phiStates = std::move(propositionalChecker.check(checkTask.getFormula().getLeftSubformula()) + ->template asExplicitQualitativeCheckResult() + .getTruthValuesVector()); + storm::storage::BitVector psiStates = std::move(propositionalChecker.check(checkTask.getFormula().getRightSubformula()) + ->template asExplicitQualitativeCheckResult() + .getTruthValuesVector()); // get the maybeStates std::pair statesWithProbability01 = @@ -203,8 +207,9 @@ void SparseMdpParameterLiftingModelChecker::speci storm::modelchecker::SparsePropositionalModelChecker propositionalChecker(*this->parametricModel); STORM_LOG_THROW(propositionalChecker.canHandle(checkTask.getFormula().getSubformula()), storm::exceptions::NotSupportedException, "Parameter lifting with non-propositional subformulas is not supported"); - storm::storage::BitVector targetStates = - std::move(propositionalChecker.check(checkTask.getFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector()); + storm::storage::BitVector targetStates = std::move(propositionalChecker.check(checkTask.getFormula().getSubformula()) + ->template asExplicitQualitativeCheckResult() + .getTruthValuesVector()); // get the maybeStates storm::storage::BitVector infinityStates = diff --git a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp index 69964a1cff..0cb3c6a252 100644 --- a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp @@ -101,15 +101,16 @@ RegionResult SparseParameterLiftingModelChecker:: (result == RegionResult::Unknown || result == RegionResult::ExistsIllDefined || result == RegionResult::CenterIllDefined)) { auto const center = region.region.getCenterPoint(); if (getInstantiationChecker(false).isWellDefined(center)) { - result = getInstantiationChecker(false).check(env, center)->asExplicitQualitativeCheckResult()[getUniqueInitialState()] + result = getInstantiationChecker(false).check(env, center)->template asExplicitQualitativeCheckResult()[getUniqueInitialState()] ? RegionResult::CenterSat : RegionResult::CenterViolated; } else { auto const lowerCorner = region.region.getLowerBoundaries(); if (getInstantiationChecker(false).isWellDefined(lowerCorner)) { - result = getInstantiationChecker(false).check(env, lowerCorner)->asExplicitQualitativeCheckResult()[getUniqueInitialState()] - ? RegionResult::ExistsSat - : RegionResult::ExistsViolated; + result = + getInstantiationChecker(false).check(env, lowerCorner)->template asExplicitQualitativeCheckResult()[getUniqueInitialState()] + ? RegionResult::ExistsSat + : RegionResult::ExistsViolated; } else { result = RegionResult::CenterIllDefined; } @@ -143,7 +144,7 @@ RegionResult SparseParameterLiftingModelChecker:: auto const valuation = getOptimalValuationForMonotonicity(region.region, globalMonotonicity->getMonotonicityResult(), dirToCheck); STORM_LOG_ASSERT(valuation.size() == region.region.getVariables().size(), "Not all parameters seem to be monotonic."); auto& checker = existsSat ? getInstantiationCheckerSAT(false) : getInstantiationCheckerVIO(false); - bool const monCheckResult = checker.check(env, valuation)->asExplicitQualitativeCheckResult()[getUniqueInitialState()]; + bool const monCheckResult = checker.check(env, valuation)->template asExplicitQualitativeCheckResult()[getUniqueInitialState()]; if (existsSat == monCheckResult) { result = existsSat ? RegionResult::AllSat : RegionResult::AllViolated; STORM_LOG_INFO("Region " << region.region << " is " << result << ", discovered with instantiation checker on " << valuation @@ -165,7 +166,7 @@ RegionResult SparseParameterLiftingModelChecker:: // Try to prove AllSat or AllViolated through parameterLifting auto const checkResult = this->check(env, region, dirToCheck); if (checkResult) { - bool const value = checkResult->asExplicitQualitativeCheckResult()[getUniqueInitialState()]; + bool const value = checkResult->template asExplicitQualitativeCheckResult()[getUniqueInitialState()]; if ((dirToCheck == dirForSat) == value) { result = (dirToCheck == dirForSat) ? RegionResult::AllSat : RegionResult::AllViolated; } else if (sampleVerticesOfRegion) { @@ -196,7 +197,7 @@ RegionResult SparseParameterLiftingModelChecker:: auto vertices = region.getVerticesOfRegion(region.getVariables()); auto vertexIt = vertices.begin(); while (vertexIt != vertices.end() && !(hasSatPoint && hasViolatedPoint)) { - if (getInstantiationChecker(false).check(env, *vertexIt)->asExplicitQualitativeCheckResult()[getUniqueInitialState()]) { + if (getInstantiationChecker(false).check(env, *vertexIt)->template asExplicitQualitativeCheckResult()[getUniqueInitialState()]) { hasSatPoint = true; } else { hasViolatedPoint = true; diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp index 05fa65ef00..184b549475 100644 --- a/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp @@ -91,8 +91,9 @@ RegionResult ValidatingSparseParameterLiftingModelCheckerasExplicitQualitativeCheckResult()[*preciseChecker.getConsideredParametricModel().getInitialStates().begin()]; + bool preciseResult = + preciseChecker.check(env, region, parameterOptDir) + ->template asExplicitQualitativeCheckResult()[*preciseChecker.getConsideredParametricModel().getInitialStates().begin()]; bool preciseResultAgrees = preciseResult == (currentResult == RegionResult::AllSat); if (!preciseResultAgrees) { @@ -103,8 +104,9 @@ RegionResult ValidatingSparseParameterLiftingModelCheckerasExplicitQualitativeCheckResult()[*preciseChecker.getConsideredParametricModel().getInitialStates().begin()]; + preciseResult = + preciseChecker.check(env, region, parameterOptDir) + ->template asExplicitQualitativeCheckResult()[*preciseChecker.getConsideredParametricModel().getInitialStates().begin()]; if (preciseResult && parameterOptDir == preciseChecker.getCurrentCheckTask().getOptimizationDirection()) { currentResult = RegionResult::AllSat; } else if (!preciseResult && parameterOptDir == storm::solver::invert(preciseChecker.getCurrentCheckTask().getOptimizationDirection())) { diff --git a/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.cpp b/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.cpp index 90cabf4968..a57d2d9ead 100644 --- a/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.cpp +++ b/src/storm-pars/modelchecker/region/monotonicity/OrderExtender.cpp @@ -102,16 +102,16 @@ std::shared_ptr OrderExtender::getBottomTopOrder assert(formula->isProbabilityOperatorFormula()); if (formula->asProbabilityOperatorFormula().getSubformula().isUntilFormula()) { phiStates = propositionalChecker.check(formula->asProbabilityOperatorFormula().getSubformula().asUntilFormula().getLeftSubformula()) - ->asExplicitQualitativeCheckResult() + ->template asExplicitQualitativeCheckResult() .getTruthValuesVector(); psiStates = propositionalChecker.check(formula->asProbabilityOperatorFormula().getSubformula().asUntilFormula().getRightSubformula()) - ->asExplicitQualitativeCheckResult() + ->template asExplicitQualitativeCheckResult() .getTruthValuesVector(); } else { assert(formula->asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()); phiStates = storage::BitVector(numberOfStates, true); psiStates = propositionalChecker.check(formula->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula()) - ->asExplicitQualitativeCheckResult() + ->template asExplicitQualitativeCheckResult() .getTruthValuesVector(); } // Get the maybeStates diff --git a/src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp b/src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp index 7258cbb5b2..2910fa4881 100644 --- a/src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp +++ b/src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp @@ -29,10 +29,12 @@ bool SparseParametricDtmcSimplifier::simplifyForUntilProbabilit STORM_LOG_DEBUG("Can not simplify when Until-formula has non-propositional subformula(s). Formula: " << formula); return false; } - storm::storage::BitVector phiStates = std::move( - propositionalChecker.check(formula.getSubformula().asUntilFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector()); - storm::storage::BitVector psiStates = std::move( - propositionalChecker.check(formula.getSubformula().asUntilFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector()); + storm::storage::BitVector phiStates = std::move(propositionalChecker.check(formula.getSubformula().asUntilFormula().getLeftSubformula()) + ->template asExplicitQualitativeCheckResult() + .getTruthValuesVector()); + storm::storage::BitVector psiStates = std::move(propositionalChecker.check(formula.getSubformula().asUntilFormula().getRightSubformula()) + ->template asExplicitQualitativeCheckResult() + .getTruthValuesVector()); std::pair statesWithProbability01 = storm::utility::graph::performProb01(this->originalModel, phiStates, psiStates); // Only consider the maybestates that are reachable from one initial state without hopping over a target (i.e., prob1) state @@ -97,10 +99,10 @@ bool SparseParametricDtmcSimplifier::simplifyForBoundedUntilPro return false; } storm::storage::BitVector phiStates = std::move(propositionalChecker.check(formula.getSubformula().asBoundedUntilFormula().getLeftSubformula()) - ->asExplicitQualitativeCheckResult() + ->template asExplicitQualitativeCheckResult() .getTruthValuesVector()); storm::storage::BitVector psiStates = std::move(propositionalChecker.check(formula.getSubformula().asBoundedUntilFormula().getRightSubformula()) - ->asExplicitQualitativeCheckResult() + ->template asExplicitQualitativeCheckResult() .getTruthValuesVector()); storm::storage::BitVector probGreater0States = storm::utility::graph::performProbGreater0(this->originalModel.getBackwardTransitions(), phiStates, psiStates, true, upperStepBound); @@ -151,8 +153,9 @@ bool SparseParametricDtmcSimplifier::simplifyForReachabilityRew STORM_LOG_DEBUG("Can not simplify when reachability reward formula has non-propositional subformula(s). Formula: " << formula); return false; } - storm::storage::BitVector targetStates = std::move( - propositionalChecker.check(formula.getSubformula().asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector()); + storm::storage::BitVector targetStates = std::move(propositionalChecker.check(formula.getSubformula().asEventuallyFormula().getSubformula()) + ->template asExplicitQualitativeCheckResult() + .getTruthValuesVector()); // The set of target states can be extended by the states that reach target with probability 1 without collecting any reward targetStates = storm::utility::graph::performProb1(this->originalModel.getBackwardTransitions(), originalRewardModel.getStatesWithZeroReward(this->originalModel.getTransitionMatrix()), targetStates); diff --git a/src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp b/src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp index 375690682f..ed9ac1efbe 100644 --- a/src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp +++ b/src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp @@ -34,10 +34,12 @@ bool SparseParametricMdpSimplifier::simplifyForUntilProbabiliti STORM_LOG_DEBUG("Can not simplify when Until-formula has non-propositional subformula(s). Formula: " << formula); return false; } - storm::storage::BitVector phiStates = std::move( - propositionalChecker.check(formula.getSubformula().asUntilFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector()); - storm::storage::BitVector psiStates = std::move( - propositionalChecker.check(formula.getSubformula().asUntilFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector()); + storm::storage::BitVector phiStates = std::move(propositionalChecker.check(formula.getSubformula().asUntilFormula().getLeftSubformula()) + ->template asExplicitQualitativeCheckResult() + .getTruthValuesVector()); + storm::storage::BitVector psiStates = std::move(propositionalChecker.check(formula.getSubformula().asUntilFormula().getRightSubformula()) + ->template asExplicitQualitativeCheckResult() + .getTruthValuesVector()); std::pair statesWithProbability01 = minimizing ? storm::utility::graph::performProb01Min(this->originalModel, phiStates, psiStates) : storm::utility::graph::performProb01Max(this->originalModel, phiStates, psiStates); @@ -121,10 +123,10 @@ bool SparseParametricMdpSimplifier::simplifyForBoundedUntilProb return false; } storm::storage::BitVector phiStates = std::move(propositionalChecker.check(formula.getSubformula().asBoundedUntilFormula().getLeftSubformula()) - ->asExplicitQualitativeCheckResult() + ->template asExplicitQualitativeCheckResult() .getTruthValuesVector()); storm::storage::BitVector psiStates = std::move(propositionalChecker.check(formula.getSubformula().asBoundedUntilFormula().getRightSubformula()) - ->asExplicitQualitativeCheckResult() + ->template asExplicitQualitativeCheckResult() .getTruthValuesVector()); storm::storage::BitVector probGreater0States = minimizing ? storm::utility::graph::performProbGreater0A(this->originalModel.getTransitionMatrix(), @@ -181,8 +183,9 @@ bool SparseParametricMdpSimplifier::simplifyForReachabilityRewa STORM_LOG_DEBUG("Can not simplify when reachability reward formula has non-propositional subformula(s). Formula: " << formula); return false; } - storm::storage::BitVector targetStates = std::move( - propositionalChecker.check(formula.getSubformula().asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector()); + storm::storage::BitVector targetStates = std::move(propositionalChecker.check(formula.getSubformula().asEventuallyFormula().getSubformula()) + ->template asExplicitQualitativeCheckResult() + .getTruthValuesVector()); // The set of target states can be extended by the states that reach target with probability 1 without collecting any reward // TODO for the call of Prob1E we could restrict the analysis to actions with zero reward instead of states with zero reward targetStates = diff --git a/src/storm-permissive/analysis/PermissiveSchedulers.cpp b/src/storm-permissive/analysis/PermissiveSchedulers.cpp index 5ce205bc4d..a73a11c45f 100644 --- a/src/storm-permissive/analysis/PermissiveSchedulers.cpp +++ b/src/storm-permissive/analysis/PermissiveSchedulers.cpp @@ -20,8 +20,9 @@ boost::optional> computePermissiveSchedulerViaMILP storm::modelchecker::SparsePropositionalModelChecker> propMC(mdp); STORM_LOG_ASSERT(safeProp.getSubformula().isEventuallyFormula(), "No eventually formula."); auto backwardTransitions = mdp.getBackwardTransitions(); - storm::storage::BitVector goalstates = - propMC.check(safeProp.getSubformula().asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + storm::storage::BitVector goalstates = propMC.check(safeProp.getSubformula().asEventuallyFormula().getSubformula()) + ->template asExplicitQualitativeCheckResult() + .getTruthValuesVector(); goalstates = storm::utility::graph::performProb1A(mdp, backwardTransitions, storm::storage::BitVector(goalstates.size(), true), goalstates); storm::storage::BitVector sinkstates = storm::utility::graph::performProb0A(backwardTransitions, storm::storage::BitVector(goalstates.size(), true), goalstates); @@ -49,8 +50,9 @@ boost::optional> computePermissiveSchedulerViaSMT( storm::modelchecker::SparsePropositionalModelChecker> propMC(mdp); STORM_LOG_ASSERT(safeProp.getSubformula().isEventuallyFormula(), "No eventually formula."); auto backwardTransitions = mdp.getBackwardTransitions(); - storm::storage::BitVector goalstates = - propMC.check(safeProp.getSubformula().asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + storm::storage::BitVector goalstates = propMC.check(safeProp.getSubformula().asEventuallyFormula().getSubformula()) + ->template asExplicitQualitativeCheckResult() + .getTruthValuesVector(); goalstates = storm::utility::graph::performProb1A(mdp, backwardTransitions, storm::storage::BitVector(goalstates.size(), true), goalstates); storm::storage::BitVector sinkstates = storm::utility::graph::performProb0A(backwardTransitions, storm::storage::BitVector(goalstates.size(), true), goalstates); diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp index 45805c4cc7..45f5595dcb 100644 --- a/src/storm-pomdp-cli/storm-pomdp.cpp +++ b/src/storm-pomdp-cli/storm-pomdp.cpp @@ -273,7 +273,7 @@ bool performAnalysis(std::shared_ptr> co storm::api::createTask(formula.asSharedPointer(), true)); if (resultPtr) { auto result = resultPtr->template asExplicitQuantitativeCheckResult(); - result.filter(storm::modelchecker::ExplicitQualitativeCheckResult(pomdp->getInitialStates())); + result.filter(storm::modelchecker::ExplicitQualitativeCheckResult(pomdp->getInitialStates())); if (storm::utility::resources::isTerminate()) { STORM_PRINT_AND_LOG("\nResult till abort: "); } else { diff --git a/src/storm-pomdp/analysis/FormulaInformation.cpp b/src/storm-pomdp/analysis/FormulaInformation.cpp index 3b7ad31bbf..62aaee7078 100644 --- a/src/storm-pomdp/analysis/FormulaInformation.cpp +++ b/src/storm-pomdp/analysis/FormulaInformation.cpp @@ -114,7 +114,7 @@ template storm::storage::BitVector getStates(storm::logic::Formula const& propositionalFormula, bool formulaInverted, PomdpType const& pomdp) { storm::modelchecker::SparsePropositionalModelChecker mc(pomdp); auto checkResult = mc.check(propositionalFormula); - storm::storage::BitVector resultBitVector(checkResult->asExplicitQualitativeCheckResult().getTruthValuesVector()); + storm::storage::BitVector resultBitVector(checkResult->template asExplicitQualitativeCheckResult().getTruthValuesVector()); if (formulaInverted) { resultBitVector.complement(); } diff --git a/src/storm-pomdp/analysis/QualitativeAnalysisOnGraphs.cpp b/src/storm-pomdp/analysis/QualitativeAnalysisOnGraphs.cpp index 3f0f71845c..5a9a6fcea5 100644 --- a/src/storm-pomdp/analysis/QualitativeAnalysisOnGraphs.cpp +++ b/src/storm-pomdp/analysis/QualitativeAnalysisOnGraphs.cpp @@ -202,7 +202,7 @@ storm::storage::BitVector QualitativeAnalysisOnGraphs::checkPropositi storm::modelchecker::SparsePropositionalModelChecker> mc(pomdp); STORM_LOG_THROW(mc.canHandle(propositionalFormula), storm::exceptions::InvalidPropertyException, "Propositional model checker can not handle formula " << propositionalFormula); - return mc.check(propositionalFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + return mc.check(propositionalFormula)->template asExplicitQualitativeCheckResult().getTruthValuesVector(); } template class QualitativeAnalysisOnGraphs; diff --git a/src/storm-pomdp/transformer/GlobalPomdpMecChoiceEliminator.cpp b/src/storm-pomdp/transformer/GlobalPomdpMecChoiceEliminator.cpp index a357cc5917..a8f1f388a6 100644 --- a/src/storm-pomdp/transformer/GlobalPomdpMecChoiceEliminator.cpp +++ b/src/storm-pomdp/transformer/GlobalPomdpMecChoiceEliminator.cpp @@ -234,7 +234,7 @@ storm::storage::BitVector GlobalPomdpMecChoiceEliminator::checkPropos storm::modelchecker::SparsePropositionalModelChecker> mc(pomdp); STORM_LOG_THROW(mc.canHandle(propositionalFormula), storm::exceptions::InvalidPropertyException, "Propositional model checker can not handle formula " << propositionalFormula); - return mc.check(propositionalFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + return mc.check(propositionalFormula)->template asExplicitQualitativeCheckResult().getTruthValuesVector(); } template class GlobalPomdpMecChoiceEliminator; diff --git a/src/storm/api/export.h b/src/storm/api/export.h index c24ea4ce33..baff690a6b 100644 --- a/src/storm/api/export.h +++ b/src/storm/api/export.h @@ -115,7 +115,8 @@ inline void exportCheckResultToJson(std::shared_ptrisExplicitQualitativeCheckResult()) { - auto j = checkResult->asExplicitQualitativeCheckResult().toJson(model->getOptionalStateValuations(), model->getStateLabeling()); + auto j = checkResult->template asExplicitQualitativeCheckResult().template toJson(model->getOptionalStateValuations(), + model->getStateLabeling()); stream << storm::dumpJson(j); } else { STORM_LOG_THROW(checkResult->isExplicitQuantitativeCheckResult(), storm::exceptions::NotSupportedException, diff --git a/src/storm/modelchecker/AbstractModelChecker.cpp b/src/storm/modelchecker/AbstractModelChecker.cpp index f81331c3d2..6b42c5be6c 100644 --- a/src/storm/modelchecker/AbstractModelChecker.cpp +++ b/src/storm/modelchecker/AbstractModelChecker.cpp @@ -150,7 +150,7 @@ std::unique_ptr AbstractModelChecker::computeStateFormul std::unique_ptr resultPointer = this->check(env, checkTask.getFormula()); if (resultPointer->isExplicitQualitativeCheckResult()) { STORM_LOG_ASSERT(ModelType::Representation == storm::models::ModelRepresentation::Sparse, "Unexpected model type."); - return std::make_unique>(resultPointer->asExplicitQualitativeCheckResult()); + return std::make_unique>(resultPointer->template asExplicitQualitativeCheckResult()); } else { STORM_LOG_ASSERT(resultPointer->isSymbolicQualitativeCheckResult(), "Unexpected result type."); STORM_LOG_ASSERT(ModelType::Representation != storm::models::ModelRepresentation::Sparse, "Unexpected model type."); diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 8a5e847156..b36579b09c 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -57,8 +57,8 @@ std::unique_ptr SparseCtmcCslModelChecker::com storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr leftResultPointer = this->check(env, pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); - ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); - ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->template asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->template asExplicitQualitativeCheckResult(); STORM_LOG_THROW(pathFormula.getTimeBoundReference().isTimeBound(), storm::exceptions::NotImplementedException, "Currently step-bounded or reward-bounded properties on CTMCs are not supported."); @@ -86,7 +86,7 @@ std::unique_ptr SparseCtmcCslModelChecker::com Environment const& env, CheckTask const& checkTask) { storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(env, pathFormula.getSubformula()); - ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->template asExplicitQualitativeCheckResult(); std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeNextProbabilities( env, this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), subResult.getTruthValuesVector()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); @@ -97,7 +97,7 @@ std::unique_ptr SparseCtmcCslModelChecker::com Environment const& env, CheckTask const& checkTask) { storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(env, pathFormula.getSubformula()); - ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->template asExplicitQualitativeCheckResult(); auto probabilisticTransitions = this->getModel().computeProbabilityMatrix(); std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeGloballyProbabilities( env, storm::solver::SolveGoal(this->getModel(), checkTask), probabilisticTransitions, probabilisticTransitions.transpose(), @@ -111,8 +111,8 @@ std::unique_ptr SparseCtmcCslModelChecker::com storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr leftResultPointer = this->check(env, pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); - ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); - ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->template asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->template asExplicitQualitativeCheckResult(); std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeUntilProbabilities( env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), @@ -130,7 +130,7 @@ std::unique_ptr SparseCtmcCslModelChecker::com storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); auto formulaChecker = [&](storm::logic::Formula const& formula) { - return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + return this->check(env, formula)->template asExplicitQualitativeCheckResult().getTruthValuesVector(); }; auto apSets = helper.computeApSets(pathFormula.getAPMapping(), formulaChecker); std::vector numericResult = helper.computeDAProductProbabilities(env, *pathFormula.readAutomaton(), apSets); @@ -148,7 +148,7 @@ std::unique_ptr SparseCtmcCslModelChecker::com storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); auto formulaChecker = [&](storm::logic::Formula const& formula) { - return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + return this->check(env, formula)->template asExplicitQualitativeCheckResult().getTruthValuesVector(); }; std::vector numericResult = helper.computeLTLProbabilities(env, pathFormula, formulaChecker); @@ -196,7 +196,7 @@ std::unique_ptr SparseCtmcCslModelChecker::com Environment const& env, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(env, eventuallyFormula.getSubformula()); - ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->template asExplicitQualitativeCheckResult(); auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeReachabilityRewards( env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), @@ -220,7 +220,7 @@ std::unique_ptr SparseCtmcCslModelChecker::com Environment const& env, CheckTask const& checkTask) { storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(env, stateFormula); - ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->template asExplicitQualitativeCheckResult(); auto probabilisticTransitions = this->getModel().computeProbabilityMatrix(); storm::modelchecker::helper::SparseDeterministicInfiniteHorizonHelper helper(probabilisticTransitions, this->getModel().getExitRateVector()); @@ -246,7 +246,7 @@ std::unique_ptr SparseCtmcCslModelChecker::com Environment const& env, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(env, eventuallyFormula.getSubformula()); - ExplicitQualitativeCheckResult& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult& subResult = subResultPointer->template asExplicitQualitativeCheckResult(); std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeReachabilityTimes( env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), @@ -269,8 +269,8 @@ std::vector SparseCtmcCslModelChecker leftResultPointer = this->check(env, pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); - ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); - ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->template asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->template asExplicitQualitativeCheckResult(); std::vector result = storm::modelchecker::helper::SparseCtmcCslHelper::computeAllTransientProbabilities( env, this->getModel().getTransitionMatrix(), this->getModel().getInitialStates(), leftResult.getTruthValuesVector(), diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 203cbce8f1..f5aa67bc85 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -72,10 +72,10 @@ std::unique_ptr SparseMarkovAutomatonCslModelCheckergetModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute time-bounded reachability probabilities in non-closed Markov automaton."); std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); - ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->template asExplicitQualitativeCheckResult(); std::unique_ptr leftResultPointer = this->check(env, pathFormula.getLeftSubformula()); - ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->template asExplicitQualitativeCheckResult(); STORM_LOG_THROW(pathFormula.getTimeBoundReference().isTimeBound(), storm::exceptions::NotImplementedException, "Currently step-bounded and reward-bounded properties on MAs are not supported."); @@ -103,7 +103,7 @@ std::unique_ptr SparseMarkovAutomatonCslModelChecker subResultPointer = this->check(env, pathFormula.getSubformula()); - ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->template asExplicitQualitativeCheckResult(); std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeNextProbabilities( env, checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); @@ -116,7 +116,7 @@ std::unique_ptr SparseMarkovAutomatonCslModelChecker subResultPointer = this->check(env, pathFormula.getSubformula()); - ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->template asExplicitQualitativeCheckResult(); auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeGloballyProbabilities( env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet()); @@ -135,8 +135,8 @@ std::unique_ptr SparseMarkovAutomatonCslModelChecker leftResultPointer = this->check(env, pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); - ExplicitQualitativeCheckResult& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); - ExplicitQualitativeCheckResult& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult& leftResult = leftResultPointer->template asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult& rightResult = rightResultPointer->template asExplicitQualitativeCheckResult(); auto ret = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeUntilProbabilities( env, checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), @@ -157,7 +157,7 @@ std::unique_ptr SparseMarkovAutomatonCslModelCheckergetModel()); auto formulaChecker = [&](storm::logic::Formula const& formula) { - return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + return this->check(env, formula)->template asExplicitQualitativeCheckResult().getTruthValuesVector(); }; auto apSets = helper.computeApSets(pathFormula.getAPMapping(), formulaChecker); std::vector numericResult = helper.computeDAProductProbabilities(env, *pathFormula.readAutomaton(), apSets); @@ -183,7 +183,7 @@ std::unique_ptr SparseMarkovAutomatonCslModelCheckergetModel()); auto formulaChecker = [&](storm::logic::Formula const& formula) { - return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + return this->check(env, formula)->template asExplicitQualitativeCheckResult().getTruthValuesVector(); }; std::vector numericResult = helper.computeLTLProbabilities(env, pathFormula, formulaChecker); @@ -205,7 +205,7 @@ std::unique_ptr SparseMarkovAutomatonCslModelCheckergetModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute reachability rewards in non-closed Markov automaton."); std::unique_ptr subResultPointer = this->check(env, eventuallyFormula.getSubformula()); - ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->template asExplicitQualitativeCheckResult(); auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); auto ret = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeReachabilityRewards( @@ -247,7 +247,7 @@ std::unique_ptr SparseMarkovAutomatonCslModelCheckergetModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute long-run average in non-closed Markov automaton."); std::unique_ptr subResultPointer = this->check(env, stateFormula); - ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->template asExplicitQualitativeCheckResult(); storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper helper( this->getModel().getTransitionMatrix(), this->getModel().getMarkovianStates(), this->getModel().getExitRates()); @@ -291,7 +291,7 @@ std::unique_ptr SparseMarkovAutomatonCslModelCheckergetModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute expected times in non-closed Markov automaton."); std::unique_ptr subResultPointer = this->check(env, eventuallyFormula.getSubformula()); - ExplicitQualitativeCheckResult& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult& subResult = subResultPointer->template asExplicitQualitativeCheckResult(); auto ret = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeReachabilityTimes( env, checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), diff --git a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp index 225b7b12f5..4bfd4de17f 100644 --- a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp +++ b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp @@ -34,7 +34,7 @@ template std::unique_ptr SparseCbAchievabilityQuery::check(Environment const& env) { bool result = this->checkAchievability(); - return std::unique_ptr(new ExplicitQualitativeCheckResult(this->originalModel.getInitialStates().getNextSetIndex(0), result)); + return std::unique_ptr(new ExplicitQualitativeCheckResult(this->originalModel.getInitialStates().getNextSetIndex(0), result)); } template diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsAchievabilityChecker.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsAchievabilityChecker.cpp index cedca9edfe..75bdfe5c8b 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsAchievabilityChecker.cpp +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsAchievabilityChecker.cpp @@ -63,13 +63,13 @@ std::unique_ptr DeterministicSchedsAchievabilityCheckercheck(env, thresholdPolytope, eps); bool const isAchievable = achievingPoint.has_value(); + using ValueType = typename SparseModelType::ValueType; if (isAchievable) { STORM_LOG_INFO( "Found achievable point: " << storm::utility::vector::toString(achievingPoint->first) << " ( approx. " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector(achievingPoint->first)) << " )."); if (optimizingObjectiveIndex.has_value()) { - using ValueType = typename SparseModelType::ValueType; // Average between obtained lower- and upper bounds auto result = storm::utility::convertNumber(achievingPoint->first[*optimizingObjectiveIndex] + achievingPoint->second); @@ -80,7 +80,7 @@ std::unique_ptr DeterministicSchedsAchievabilityChecker>(originalModelInitialState, result); } } - return std::make_unique(originalModelInitialState, isAchievable); + return std::make_unique>(originalModelInitialState, isAchievable); } template class DeterministicSchedsAchievabilityChecker, storm::RationalNumber>; diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp index 0346b41e4f..c1d03129b9 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp @@ -39,7 +39,7 @@ storm::storage::BitVector evaluatePropositionalFormula(ModelType const& model, s auto checkResult = mc.check(formula); STORM_LOG_THROW(checkResult && checkResult->isExplicitQualitativeCheckResult(), storm::exceptions::UnexpectedException, "Unexpected type of check result for subformula " << formula << "."); - return checkResult->asExplicitQualitativeCheckResult().getTruthValuesVector(); + return checkResult->template asExplicitQualitativeCheckResult().getTruthValuesVector(); } template diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp index 9271fe33e6..562f4dbfc5 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp @@ -51,7 +51,8 @@ std::unique_ptr SparsePcaaAchievabilityQuerycheckAchievability(env); - return std::unique_ptr(new ExplicitQualitativeCheckResult(this->originalModel.getInitialStates().getNextSetIndex(0), result)); + return std::unique_ptr( + new ExplicitQualitativeCheckResult(this->originalModel.getInitialStates().getNextSetIndex(0), result)); } template diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp index c13762c22e..e4e613f69a 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp @@ -91,7 +91,8 @@ std::unique_ptr SparsePcaaQuantitativeQuery(new ExplicitQuantitativeCheckResult( this->originalModel.getInitialStates().getNextSetIndex(0), resultForOriginalModel)); } else { - return std::unique_ptr(new ExplicitQualitativeCheckResult(this->originalModel.getInitialStates().getNextSetIndex(0), false)); + return std::unique_ptr( + new ExplicitQualitativeCheckResult(this->originalModel.getInitialStates().getNextSetIndex(0), false)); } } diff --git a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp index 6eabbd6bda..91dc7be1b2 100644 --- a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp @@ -128,8 +128,10 @@ void SparseMultiObjectivePreprocessor::removeIrrelevantStates(s auto const& pathFormula = opFormula->asOperatorFormula().getSubformula(); if (opFormula->isProbabilityOperatorFormula()) { if (pathFormula.isUntilFormula()) { - auto lhs = mc.check(pathFormula.asUntilFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); - auto rhs = mc.check(pathFormula.asUntilFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + auto lhs = + mc.check(pathFormula.asUntilFormula().getLeftSubformula())->template asExplicitQualitativeCheckResult().getTruthValuesVector(); + auto rhs = + mc.check(pathFormula.asUntilFormula().getRightSubformula())->template asExplicitQualitativeCheckResult().getTruthValuesVector(); absorbingStatesForSubformula = storm::utility::graph::performProb0A(backwardTransitions, lhs, rhs); absorbingStatesForSubformula |= getOnlyReachableViaPhi(*model, ~lhs | rhs); } else if (pathFormula.isBoundedUntilFormula()) { @@ -138,10 +140,12 @@ void SparseMultiObjectivePreprocessor::removeIrrelevantStates(s storm::storage::BitVector absorbingStatesForSubSubformula; for (uint64_t i = 0; i < pathFormula.asBoundedUntilFormula().getDimension(); ++i) { auto subPathFormula = pathFormula.asBoundedUntilFormula().restrictToDimension(i); - auto lhs = - mc.check(pathFormula.asBoundedUntilFormula().getLeftSubformula(i))->asExplicitQualitativeCheckResult().getTruthValuesVector(); - auto rhs = - mc.check(pathFormula.asBoundedUntilFormula().getRightSubformula(i))->asExplicitQualitativeCheckResult().getTruthValuesVector(); + auto lhs = mc.check(pathFormula.asBoundedUntilFormula().getLeftSubformula(i)) + ->template asExplicitQualitativeCheckResult() + .getTruthValuesVector(); + auto rhs = mc.check(pathFormula.asBoundedUntilFormula().getRightSubformula(i)) + ->template asExplicitQualitativeCheckResult() + .getTruthValuesVector(); absorbingStatesForSubSubformula = storm::utility::graph::performProb0A(backwardTransitions, lhs, rhs); if (pathFormula.asBoundedUntilFormula().hasLowerBound(i)) { absorbingStatesForSubSubformula |= getOnlyReachableViaPhi(*model, ~lhs); @@ -151,8 +155,12 @@ void SparseMultiObjectivePreprocessor::removeIrrelevantStates(s absorbingStatesForSubformula &= absorbingStatesForSubSubformula; } } else { - auto lhs = mc.check(pathFormula.asBoundedUntilFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); - auto rhs = mc.check(pathFormula.asBoundedUntilFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + auto lhs = mc.check(pathFormula.asBoundedUntilFormula().getLeftSubformula()) + ->template asExplicitQualitativeCheckResult() + .getTruthValuesVector(); + auto rhs = mc.check(pathFormula.asBoundedUntilFormula().getRightSubformula()) + ->template asExplicitQualitativeCheckResult() + .getTruthValuesVector(); absorbingStatesForSubformula = storm::utility::graph::performProb0A(backwardTransitions, lhs, rhs); if (pathFormula.asBoundedUntilFormula().hasLowerBound()) { absorbingStatesForSubformula |= getOnlyReachableViaPhi(*model, ~lhs); @@ -161,12 +169,14 @@ void SparseMultiObjectivePreprocessor::removeIrrelevantStates(s } } } else if (pathFormula.isGloballyFormula()) { - auto phi = mc.check(pathFormula.asGloballyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + auto phi = + mc.check(pathFormula.asGloballyFormula().getSubformula())->template asExplicitQualitativeCheckResult().getTruthValuesVector(); auto notPhi = ~phi; absorbingStatesForSubformula = storm::utility::graph::performProb0A(backwardTransitions, phi, notPhi); absorbingStatesForSubformula |= getOnlyReachableViaPhi(*model, notPhi); } else if (pathFormula.isEventuallyFormula()) { - auto phi = mc.check(pathFormula.asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + auto phi = + mc.check(pathFormula.asEventuallyFormula().getSubformula())->template asExplicitQualitativeCheckResult().getTruthValuesVector(); absorbingStatesForSubformula = storm::utility::graph::performProb0A(backwardTransitions, ~phi, phi); absorbingStatesForSubformula |= getOnlyReachableViaPhi(*model, phi); } else { @@ -181,7 +191,8 @@ void SparseMultiObjectivePreprocessor::removeIrrelevantStates(s storm::storage::BitVector statesWithoutReward = rewardModel.get().getStatesWithZeroReward(model->getTransitionMatrix()); // Make states that can not reach a state with non-zero reward absorbing absorbingStatesForSubformula = storm::utility::graph::performProb0A(backwardTransitions, statesWithoutReward, ~statesWithoutReward); - auto phi = mc.check(pathFormula.asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + auto phi = + mc.check(pathFormula.asEventuallyFormula().getSubformula())->template asExplicitQualitativeCheckResult().getTruthValuesVector(); // Make states that reach phi with prob 1 while only visiting states with reward 0 absorbing absorbingStatesForSubformula |= storm::utility::graph::performProb1A( model->getTransitionMatrix(), model->getTransitionMatrix().getRowGroupIndices(), backwardTransitions, statesWithoutReward, phi); @@ -210,13 +221,14 @@ void SparseMultiObjectivePreprocessor::removeIrrelevantStates(s } } else if (opFormula->isTimeOperatorFormula()) { if (pathFormula.isEventuallyFormula()) { - auto phi = mc.check(pathFormula.asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + auto phi = + mc.check(pathFormula.asEventuallyFormula().getSubformula())->template asExplicitQualitativeCheckResult().getTruthValuesVector(); absorbingStatesForSubformula = getOnlyReachableViaPhi(*model, phi); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << pathFormula << " is not supported."); } } else if (opFormula->isLongRunAverageOperatorFormula()) { - auto lraStates = mc.check(pathFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + auto lraStates = mc.check(pathFormula)->template asExplicitQualitativeCheckResult().getTruthValuesVector(); // Compute Sat(Forall F (Forall G not "lraStates")) auto forallGloballyNotLraStates = storm::utility::graph::performProb0A(backwardTransitions, ~lraStates, lraStates); absorbingStatesForSubformula = storm::utility::graph::performProb1A(model->getTransitionMatrix(), model->getNondeterministicChoiceIndices(), @@ -432,7 +444,8 @@ void SparseMultiObjectivePreprocessor::preprocessLongRunAverage // Create and add the new reward model that only gives one reward for goal states storm::modelchecker::SparsePropositionalModelChecker mc(*data.model); - storm::storage::BitVector subFormulaResult = mc.check(formula.getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + storm::storage::BitVector subFormulaResult = + mc.check(formula.getSubformula())->template asExplicitQualitativeCheckResult().getTruthValuesVector(); std::vector lraRewards(data.model->getNumberOfStates(), storm::utility::zero()); storm::utility::vector::setVectorValues(lraRewards, subFormulaResult, storm::utility::one()); data.model->addRewardModel(rewardModelName, typename SparseModelType::RewardModelType(std::move(lraRewards))); @@ -445,7 +458,8 @@ void SparseMultiObjectivePreprocessor::preprocessUntilFormula(s // Try to transform the formula to expected total (or cumulative) rewards storm::modelchecker::SparsePropositionalModelChecker mc(*data.model); - storm::storage::BitVector rightSubformulaResult = mc.check(formula.getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + storm::storage::BitVector rightSubformulaResult = + mc.check(formula.getRightSubformula())->template asExplicitQualitativeCheckResult().getTruthValuesVector(); // Check if the formula is already satisfied in the initial state because then the transformation to expected rewards will fail. // TODO: Handle this case more properly STORM_LOG_THROW((data.model->getInitialStates() & rightSubformulaResult).empty(), storm::exceptions::NotImplementedException, @@ -455,7 +469,8 @@ void SparseMultiObjectivePreprocessor::preprocessUntilFormula(s // Whenever a state that violates the left subformula or satisfies the right subformula is reached, the objective is 'decided', i.e., no more reward should // be collected from there - storm::storage::BitVector notLeftOrRight = mc.check(formula.getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + storm::storage::BitVector notLeftOrRight = + mc.check(formula.getLeftSubformula())->template asExplicitQualitativeCheckResult().getTruthValuesVector(); notLeftOrRight.complement(); notLeftOrRight |= rightSubformulaResult; @@ -542,7 +557,8 @@ void SparseMultiObjectivePreprocessor::preprocessEventuallyForm // Analyze the subformula storm::modelchecker::SparsePropositionalModelChecker mc(*data.model); - storm::storage::BitVector subFormulaResult = mc.check(formula.getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + storm::storage::BitVector subFormulaResult = + mc.check(formula.getSubformula())->template asExplicitQualitativeCheckResult().getTruthValuesVector(); // Get the states that are reachable from a goal state storm::storage::BitVector allStates(data.model->getNumberOfStates(), true), noStates(data.model->getNumberOfStates(), false); diff --git a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp index 344766e323..81815a9d85 100644 --- a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp @@ -176,7 +176,7 @@ std::unique_ptr HybridMdpPrctlModelChecker::checkMultiOb // Convert the explicit result if (explicitResult->isExplicitQualitativeCheckResult()) { - if (explicitResult->asExplicitQualitativeCheckResult()[*sparseModel->getInitialStates().begin()]) { + if (explicitResult->template asExplicitQualitativeCheckResult()[*sparseModel->getInitialStates().begin()]) { return std::unique_ptr(new storm::modelchecker::SymbolicQualitativeCheckResult( this->getModel().getReachableStates(), this->getModel().getInitialStates(), this->getModel().getManager().getBddOne())); } else { diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 1686bbe010..431039c622 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -92,8 +92,8 @@ std::unique_ptr SparseDtmcPrctlModelChecker::c STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper step bound."); std::unique_ptr leftResultPointer = this->check(env, pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); - ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); - ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->template asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->template asExplicitQualitativeCheckResult(); storm::modelchecker::helper::SparseDeterministicStepBoundedHorizonHelper helper; std::vector numericResult = helper.compute(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), @@ -109,7 +109,7 @@ std::unique_ptr SparseDtmcPrctlModelChecker::c Environment const& env, CheckTask const& checkTask) { storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(env, pathFormula.getSubformula()); - ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->template asExplicitQualitativeCheckResult(); std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeNextProbabilities( env, this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); @@ -121,8 +121,8 @@ std::unique_ptr SparseDtmcPrctlModelChecker::c storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr leftResultPointer = this->check(env, pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); - ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); - ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->template asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->template asExplicitQualitativeCheckResult(); std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeUntilProbabilities( env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), @@ -135,7 +135,7 @@ std::unique_ptr SparseDtmcPrctlModelChecker::c Environment const& env, CheckTask const& checkTask) { storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(env, pathFormula.getSubformula()); - ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->template asExplicitQualitativeCheckResult(); std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeGloballyProbabilities( env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet()); @@ -151,7 +151,7 @@ std::unique_ptr SparseDtmcPrctlModelChecker::c storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); auto formulaChecker = [&](storm::logic::Formula const& formula) { - return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + return this->check(env, formula)->template asExplicitQualitativeCheckResult().getTruthValuesVector(); }; auto apSets = helper.computeApSets(pathFormula.getAPMapping(), formulaChecker); std::vector numericResult = helper.computeDAProductProbabilities(env, *pathFormula.readAutomaton(), apSets); @@ -168,7 +168,7 @@ std::unique_ptr SparseDtmcPrctlModelChecker::c storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); auto formulaChecker = [&](storm::logic::Formula const& formula) { - return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + return this->check(env, formula)->template asExplicitQualitativeCheckResult().getTruthValuesVector(); }; std::vector numericResult = helper.computeLTLProbabilities(env, pathFormula, formulaChecker); @@ -236,7 +236,7 @@ std::unique_ptr SparseDtmcPrctlModelChecker::c Environment const& env, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(env, eventuallyFormula.getSubformula()); - ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->template asExplicitQualitativeCheckResult(); auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards( env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), @@ -249,7 +249,7 @@ std::unique_ptr SparseDtmcPrctlModelChecker::c Environment const& env, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(env, eventuallyFormula.getSubformula()); - ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->template asExplicitQualitativeCheckResult(); std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityTimes( env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.getHint()); @@ -290,7 +290,7 @@ std::unique_ptr SparseDtmcPrctlModelChecker::c Environment const& env, CheckTask const& checkTask) { storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(env, stateFormula); - ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->template asExplicitQualitativeCheckResult(); storm::modelchecker::helper::SparseDeterministicInfiniteHorizonHelper helper(this->getModel().getTransitionMatrix()); storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); @@ -320,8 +320,8 @@ std::unique_ptr SparseDtmcPrctlModelChecker::c std::unique_ptr leftResultPointer = this->check(env, conditionalFormula.getSubformula().asEventuallyFormula().getSubformula()); std::unique_ptr rightResultPointer = this->check(env, conditionalFormula.getConditionFormula().asEventuallyFormula().getSubformula()); - ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); - ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->template asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->template asExplicitQualitativeCheckResult(); std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeConditionalProbabilities( env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), @@ -340,8 +340,8 @@ std::unique_ptr SparseDtmcPrctlModelChecker::c std::unique_ptr leftResultPointer = this->check(env, conditionalFormula.getSubformula().asReachabilityRewardFormula().getSubformula()); std::unique_ptr rightResultPointer = this->check(env, conditionalFormula.getConditionFormula().asEventuallyFormula().getSubformula()); - ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); - ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->template asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->template asExplicitQualitativeCheckResult(); std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeConditionalRewards( env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index e532228189..8d19c3dea6 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -139,8 +139,8 @@ std::unique_ptr SparseMdpPrctlModelChecker::com "Formula needs to have discrete upper time bound."); std::unique_ptr leftResultPointer = this->check(env, pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); - ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); - ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->template asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->template asExplicitQualitativeCheckResult(); storm::modelchecker::helper::SparseNondeterministicStepBoundedHorizonHelper helper; std::vector numericResult = helper.compute(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), @@ -158,7 +158,7 @@ std::unique_ptr SparseMdpPrctlModelChecker::com STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(env, pathFormula.getSubformula()); - ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->template asExplicitQualitativeCheckResult(); std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeNextProbabilities( env, checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); @@ -172,8 +172,8 @@ std::unique_ptr SparseMdpPrctlModelChecker::com "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr leftResultPointer = this->check(env, pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); - ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); - ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->template asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->template asExplicitQualitativeCheckResult(); auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities( env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), @@ -192,7 +192,7 @@ std::unique_ptr SparseMdpPrctlModelChecker::com STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(env, pathFormula.getSubformula()); - ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->template asExplicitQualitativeCheckResult(); auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeGloballyProbabilities( env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet()); @@ -215,7 +215,7 @@ std::unique_ptr SparseMdpPrctlModelChecker::com storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel()); auto formulaChecker = [&](storm::logic::Formula const& formula) { - return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + return this->check(env, formula)->template asExplicitQualitativeCheckResult().getTruthValuesVector(); }; auto apSets = helper.computeApSets(pathFormula.getAPMapping(), formulaChecker); std::vector numericResult = helper.computeDAProductProbabilities(env, *pathFormula.readAutomaton(), apSets); @@ -245,7 +245,7 @@ std::unique_ptr SparseMdpPrctlModelChecker::com storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel()); auto formulaChecker = [&](storm::logic::Formula const& formula) { - return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + return this->check(env, formula)->template asExplicitQualitativeCheckResult().getTruthValuesVector(); }; std::vector numericResult = helper.computeLTLProbabilities(env, pathFormula, formulaChecker); @@ -276,8 +276,8 @@ std::unique_ptr SparseMdpPrctlModelChecker::com std::unique_ptr leftResultPointer = this->check(env, conditionalFormula.getSubformula().asEventuallyFormula().getSubformula()); std::unique_ptr rightResultPointer = this->check(env, conditionalFormula.getConditionFormula().asEventuallyFormula().getSubformula()); - ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); - ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->template asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->template asExplicitQualitativeCheckResult(); if constexpr (std::is_same_v) { throw exceptions::NotImplementedException() << "Conditional Probabilities are not supported with interval models"; } else { @@ -363,7 +363,7 @@ std::unique_ptr SparseMdpPrctlModelChecker::com STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(env, eventuallyFormula.getSubformula()); - ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->template asExplicitQualitativeCheckResult(); auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeReachabilityRewards( env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), @@ -383,7 +383,7 @@ std::unique_ptr SparseMdpPrctlModelChecker::com STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(env, eventuallyFormula.getSubformula()); - ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->template asExplicitQualitativeCheckResult(); auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeReachabilityTimes( env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet(), @@ -446,7 +446,7 @@ std::unique_ptr SparseMdpPrctlModelChecker::com STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(env, stateFormula); - ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->template asExplicitQualitativeCheckResult(); storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper helper(this->getModel().getTransitionMatrix()); storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel()); @@ -499,7 +499,7 @@ std::unique_ptr SparseMdpPrctlModelChecker::che STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented lexicographic model checking with intervals"); } else { auto formulaChecker = [&](storm::logic::Formula const& formula) { - return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + return this->check(env, formula)->template asExplicitQualitativeCheckResult().getTruthValuesVector(); }; auto ret = lexicographic::check(env, this->getModel(), checkTask, formulaChecker); std::unique_ptr result(new LexicographicCheckResult(ret.values, *this->getModel().getInitialStates().begin())); diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.cpp index 7bb836cc88..ccc196db4e 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.cpp +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.cpp @@ -132,9 +132,12 @@ storm::storage::MemoryStructure ProductModel::computeMemoryStructure( for (auto dim : objectiveDimensions[objIndex]) { auto const& dimension = dimensions[dim]; STORM_LOG_ASSERT(dimension.formula->isBoundedUntilFormula(), "Unexpected Formula type"); - constraintStates &= - (mc.check(dimension.formula->asBoundedUntilFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector() | - mc.check(dimension.formula->asBoundedUntilFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector()); + constraintStates &= (mc.check(dimension.formula->asBoundedUntilFormula().getLeftSubformula()) + ->template asExplicitQualitativeCheckResult() + .getTruthValuesVector() | + mc.check(dimension.formula->asBoundedUntilFormula().getRightSubformula()) + ->template asExplicitQualitativeCheckResult() + .getTruthValuesVector()); } // Build the transitions between the memory states @@ -155,7 +158,8 @@ storm::storage::MemoryStructure ProductModel::computeMemoryStructure( storm::logic::BinaryBooleanStateFormula::OperatorType::And, transitionFormula, subObjFormula); } - storm::storage::BitVector transitionStates = mc.check(*transitionFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + storm::storage::BitVector transitionStates = + mc.check(*transitionFormula)->template asExplicitQualitativeCheckResult().getTruthValuesVector(); if (memStatePrimeBV.empty()) { transitionStates |= ~constraintStates; } else { @@ -426,9 +430,11 @@ std::vector> ProductModel::computeObjectiveRew } } - storm::storage::BitVector relevantStates = mc.check(*relevantStatesFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + storm::storage::BitVector relevantStates = + mc.check(*relevantStatesFormula)->template asExplicitQualitativeCheckResult().getTruthValuesVector(); storm::storage::BitVector relevantChoices = getProduct().getTransitionMatrix().getRowFilter(relevantStates); - storm::storage::BitVector goalStates = mc.check(*goalStatesFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + storm::storage::BitVector goalStates = + mc.check(*goalStatesFormula)->template asExplicitQualitativeCheckResult().getTruthValuesVector(); for (auto choice : relevantChoices) { objRew[choice] += getProduct().getTransitionMatrix().getConstrainedRowSum(choice, goalStates); } diff --git a/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp b/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp index 094a2332cf..8fa08b56c7 100644 --- a/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp +++ b/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp @@ -35,9 +35,9 @@ std::unique_ptr SparsePropositionalModelChecker::c Environment const& env, CheckTask const& checkTask) { storm::logic::BooleanLiteralFormula const& stateFormula = checkTask.getFormula(); if (stateFormula.isTrueFormula()) { - return std::unique_ptr(new ExplicitQualitativeCheckResult(storm::storage::BitVector(model.getNumberOfStates(), true))); + return std::unique_ptr(new ExplicitQualitativeCheckResult(storm::storage::BitVector(model.getNumberOfStates(), true))); } else { - return std::unique_ptr(new ExplicitQualitativeCheckResult(storm::storage::BitVector(model.getNumberOfStates()))); + return std::unique_ptr(new ExplicitQualitativeCheckResult(storm::storage::BitVector(model.getNumberOfStates()))); } } @@ -47,7 +47,7 @@ std::unique_ptr SparsePropositionalModelChecker::c storm::logic::AtomicLabelFormula const& stateFormula = checkTask.getFormula(); STORM_LOG_THROW(model.hasLabel(stateFormula.getLabel()), storm::exceptions::InvalidPropertyException, "The property refers to unknown label '" << stateFormula.getLabel() << "'."); - return std::unique_ptr(new ExplicitQualitativeCheckResult(model.getStates(stateFormula.getLabel()))); + return std::unique_ptr(new ExplicitQualitativeCheckResult(model.getStates(stateFormula.getLabel()))); } template diff --git a/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 43296a4d13..506f03b3ff 100644 --- a/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -55,7 +55,7 @@ std::unique_ptr SparseDtmcEliminationModelChecker const& checkTask) { storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(stateFormula); - storm::storage::BitVector const& psiStates = subResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); + storm::storage::BitVector const& psiStates = subResultPointer->template asExplicitQualitativeCheckResult().getTruthValuesVector(); storm::storage::SparseMatrix const& transitionMatrix = this->getModel().getTransitionMatrix(); uint_fast64_t numberOfStates = transitionMatrix.getRowCount(); @@ -112,7 +112,7 @@ std::unique_ptr SparseDtmcEliminationModelCheckerfilter(ExplicitQualitativeCheckResult(initialStates)); + checkResult->filter(ExplicitQualitativeCheckResult(initialStates)); } return checkResult; } @@ -177,7 +177,7 @@ std::unique_ptr SparseDtmcEliminationModelCheckerfilter(ExplicitQualitativeCheckResult(initialStates)); + checkResult->filter(ExplicitQualitativeCheckResult(initialStates)); } return checkResult; } @@ -350,8 +350,8 @@ std::unique_ptr SparseDtmcEliminationModelChecker leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); - storm::storage::BitVector const& phiStates = leftResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); - storm::storage::BitVector const& psiStates = rightResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); + storm::storage::BitVector const& phiStates = leftResultPointer->template asExplicitQualitativeCheckResult().getTruthValuesVector(); + storm::storage::BitVector const& psiStates = rightResultPointer->template asExplicitQualitativeCheckResult().getTruthValuesVector(); // Start by determining the states that have a non-zero probability of reaching the target states within the // time bound. @@ -444,7 +444,7 @@ std::unique_ptr SparseDtmcEliminationModelCheckerfilter(ExplicitQualitativeCheckResult(this->getModel().getInitialStates() | psiStates)); + checkResult->filter(ExplicitQualitativeCheckResult(this->getModel().getInitialStates() | psiStates)); } return checkResult; } @@ -457,8 +457,8 @@ std::unique_ptr SparseDtmcEliminationModelChecker leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); - storm::storage::BitVector const& phiStates = leftResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); - storm::storage::BitVector const& psiStates = rightResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); + storm::storage::BitVector const& phiStates = leftResultPointer->template asExplicitQualitativeCheckResult().getTruthValuesVector(); + storm::storage::BitVector const& psiStates = rightResultPointer->template asExplicitQualitativeCheckResult().getTruthValuesVector(); return computeUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getInitialStates(), phiStates, psiStates, checkTask.isOnlyInitialStatesRelevantSet()); @@ -538,7 +538,7 @@ std::unique_ptr SparseDtmcEliminationModelChecker subResultPointer = this->check(eventuallyFormula.getSubformula()); storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); - storm::storage::BitVector const& targetStates = subResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); + storm::storage::BitVector const& targetStates = subResultPointer->template asExplicitQualitativeCheckResult().getTruthValuesVector(); // Do some sanity checks to establish some required properties. RewardModelType const& rewardModel = this->getModel().getRewardModel(checkTask.isRewardModelSet() ? checkTask.getRewardModel() : ""); @@ -650,8 +650,8 @@ std::unique_ptr SparseDtmcEliminationModelChecker leftResultPointer = this->check(conditionalFormula.getSubformula().asEventuallyFormula().getSubformula()); std::unique_ptr rightResultPointer = this->check(conditionalFormula.getConditionFormula().asEventuallyFormula().getSubformula()); - storm::storage::BitVector phiStates = leftResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); - storm::storage::BitVector psiStates = rightResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); + storm::storage::BitVector phiStates = leftResultPointer->template asExplicitQualitativeCheckResult().getTruthValuesVector(); + storm::storage::BitVector psiStates = rightResultPointer->template asExplicitQualitativeCheckResult().getTruthValuesVector(); storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); // Do some sanity checks to establish some required properties. diff --git a/src/storm/modelchecker/results/CheckResult.cpp b/src/storm/modelchecker/results/CheckResult.cpp index 8549ce26d0..c43c2cf441 100644 --- a/src/storm/modelchecker/results/CheckResult.cpp +++ b/src/storm/modelchecker/results/CheckResult.cpp @@ -82,12 +82,14 @@ bool CheckResult::isHybridQuantitativeCheckResult() const { return false; } -ExplicitQualitativeCheckResult& CheckResult::asExplicitQualitativeCheckResult() { - return dynamic_cast(*this); +template +ExplicitQualitativeCheckResult& CheckResult::asExplicitQualitativeCheckResult() { + return dynamic_cast&>(*this); } -ExplicitQualitativeCheckResult const& CheckResult::asExplicitQualitativeCheckResult() const { - return dynamic_cast(*this); +template +ExplicitQualitativeCheckResult const& CheckResult::asExplicitQualitativeCheckResult() const { + return dynamic_cast const&>(*this); } template @@ -188,6 +190,8 @@ template QuantitativeCheckResult const& CheckResult::asQuantitativeCheck template ExplicitQuantitativeCheckResult& CheckResult::asExplicitQuantitativeCheckResult(); template ExplicitQuantitativeCheckResult const& CheckResult::asExplicitQuantitativeCheckResult() const; +template ExplicitQualitativeCheckResult& CheckResult::asExplicitQualitativeCheckResult(); +template ExplicitQualitativeCheckResult const& CheckResult::asExplicitQualitativeCheckResult() const; template ExplicitParetoCurveCheckResult& CheckResult::asExplicitParetoCurveCheckResult(); template ExplicitParetoCurveCheckResult const& CheckResult::asExplicitParetoCurveCheckResult() const; template LexicographicCheckResult& CheckResult::asLexicographicCheckResult(); @@ -221,6 +225,8 @@ template QuantitativeCheckResult const& CheckResult::asQu template ExplicitQuantitativeCheckResult& CheckResult::asExplicitQuantitativeCheckResult(); template ExplicitQuantitativeCheckResult const& CheckResult::asExplicitQuantitativeCheckResult() const; +template ExplicitQualitativeCheckResult& CheckResult::asExplicitQualitativeCheckResult(); +template ExplicitQualitativeCheckResult const& CheckResult::asExplicitQualitativeCheckResult() const; template QuantitativeCheckResult& CheckResult::asQuantitativeCheckResult(); template QuantitativeCheckResult const& CheckResult::asQuantitativeCheckResult() const; @@ -228,6 +234,9 @@ template QuantitativeCheckResult const& CheckResult::as template ExplicitQuantitativeCheckResult& CheckResult::asExplicitQuantitativeCheckResult(); template ExplicitQuantitativeCheckResult const& CheckResult::asExplicitQuantitativeCheckResult() const; +template ExplicitQualitativeCheckResult& CheckResult::asExplicitQualitativeCheckResult(); +template ExplicitQualitativeCheckResult const& CheckResult::asExplicitQualitativeCheckResult() const; + template ExplicitParetoCurveCheckResult& CheckResult::asExplicitParetoCurveCheckResult(); template ExplicitParetoCurveCheckResult const& CheckResult::asExplicitParetoCurveCheckResult() const; @@ -235,5 +244,10 @@ template LexicographicCheckResult& CheckResult::asLexicog template LexicographicCheckResult const& CheckResult::asLexicographicCheckResult() const; #endif + +// Instantiation for storm::Interval (carl::Interval) +template ExplicitQualitativeCheckResult& CheckResult::asExplicitQualitativeCheckResult(); +template ExplicitQualitativeCheckResult const& CheckResult::asExplicitQualitativeCheckResult() const; + } // namespace modelchecker } // namespace storm diff --git a/src/storm/modelchecker/results/CheckResult.h b/src/storm/modelchecker/results/CheckResult.h index f46e1abcf9..c8ba918329 100644 --- a/src/storm/modelchecker/results/CheckResult.h +++ b/src/storm/modelchecker/results/CheckResult.h @@ -13,6 +13,7 @@ namespace modelchecker { class QualitativeCheckResult; template class QuantitativeCheckResult; +template class ExplicitQualitativeCheckResult; template @@ -77,8 +78,11 @@ class CheckResult { template QuantitativeCheckResult const& asQuantitativeCheckResult() const; - ExplicitQualitativeCheckResult& asExplicitQualitativeCheckResult(); - ExplicitQualitativeCheckResult const& asExplicitQualitativeCheckResult() const; + template + ExplicitQualitativeCheckResult& asExplicitQualitativeCheckResult(); + + template + ExplicitQualitativeCheckResult const& asExplicitQualitativeCheckResult() const; template ExplicitQuantitativeCheckResult& asExplicitQuantitativeCheckResult(); diff --git a/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp b/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp index a9d59197a5..ac58ec1fc2 100644 --- a/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp +++ b/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp @@ -56,8 +56,8 @@ void ExplicitParetoCurveCheckResult::filter(QualitativeCheckResult co STORM_LOG_THROW(filter.isExplicitQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot filter explicit check result with non-explicit filter."); STORM_LOG_THROW(filter.isResultForAllStates(), storm::exceptions::InvalidOperationException, "Cannot filter check result with non-complete filter."); - ExplicitQualitativeCheckResult const& explicitFilter = filter.asExplicitQualitativeCheckResult(); - ExplicitQualitativeCheckResult::vector_type const& filterTruthValues = explicitFilter.getTruthValuesVector(); + ExplicitQualitativeCheckResult const& explicitFilter = filter.template asExplicitQualitativeCheckResult(); + typename ExplicitQualitativeCheckResult::vector_type const& filterTruthValues = explicitFilter.getTruthValuesVector(); STORM_LOG_THROW(filterTruthValues.getNumberOfSetBits() == 1 && filterTruthValues.get(state), storm::exceptions::InvalidOperationException, "The check result fails to contain some results referred to by the filter."); diff --git a/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.cpp b/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.cpp index f608a3065b..f39ac58a74 100644 --- a/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.cpp @@ -3,53 +3,70 @@ #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/adapters/JsonAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/exceptions/InvalidOperationException.h" #include "storm/utility/macros.h" namespace storm { namespace modelchecker { -ExplicitQualitativeCheckResult::ExplicitQualitativeCheckResult() : truthValues(map_type()) { + +template +ExplicitQualitativeCheckResult::ExplicitQualitativeCheckResult() : truthValues(map_type()) { // Intentionally left empty. } -ExplicitQualitativeCheckResult::ExplicitQualitativeCheckResult(map_type const& map) : truthValues(map) { +template +ExplicitQualitativeCheckResult::ExplicitQualitativeCheckResult(map_type const& map) : truthValues(map) { // Intentionally left empty. } -ExplicitQualitativeCheckResult::ExplicitQualitativeCheckResult(map_type&& map) : truthValues(map) { +template +ExplicitQualitativeCheckResult::ExplicitQualitativeCheckResult(map_type&& map) : truthValues(map) { // Intentionally left empty. } -ExplicitQualitativeCheckResult::ExplicitQualitativeCheckResult(storm::storage::sparse::state_type state, bool value) : truthValues(map_type()) { +template +ExplicitQualitativeCheckResult::ExplicitQualitativeCheckResult(storm::storage::sparse::state_type state, bool value) : truthValues(map_type()) { boost::get(truthValues)[state] = value; } -ExplicitQualitativeCheckResult::ExplicitQualitativeCheckResult(storm::storage::BitVector const& truthValues) : truthValues(truthValues) { +template +ExplicitQualitativeCheckResult::ExplicitQualitativeCheckResult(storm::storage::BitVector const& truthValues) : truthValues(truthValues) { // Intentionally left empty. } -ExplicitQualitativeCheckResult::ExplicitQualitativeCheckResult(storm::storage::BitVector&& truthValues) : truthValues(std::move(truthValues)) { +template +ExplicitQualitativeCheckResult::ExplicitQualitativeCheckResult(storm::storage::BitVector&& truthValues) : truthValues(std::move(truthValues)) { // Intentionally left empty. } -ExplicitQualitativeCheckResult::ExplicitQualitativeCheckResult(boost::variant const& truthValues) : truthValues(truthValues) { +template +ExplicitQualitativeCheckResult::ExplicitQualitativeCheckResult(boost::variant const& truthValues, + boost::optional>> scheduler) + : truthValues(truthValues), scheduler(scheduler) { // Intentionally left empty. } -ExplicitQualitativeCheckResult::ExplicitQualitativeCheckResult(boost::variant&& truthValues) : truthValues(std::move(truthValues)) { +template +ExplicitQualitativeCheckResult::ExplicitQualitativeCheckResult(boost::variant&& truthValues, + boost::optional>> scheduler) + : truthValues(std::move(truthValues)), scheduler(scheduler) { // Intentionally left empty. } -std::unique_ptr ExplicitQualitativeCheckResult::clone() const { - return std::make_unique(this->truthValues); +template +std::unique_ptr ExplicitQualitativeCheckResult::clone() const { + return std::make_unique>(this->truthValues); } -void ExplicitQualitativeCheckResult::performLogicalOperation(ExplicitQualitativeCheckResult& first, QualitativeCheckResult const& second, bool logicalAnd) { +template +void ExplicitQualitativeCheckResult::performLogicalOperation(ExplicitQualitativeCheckResult& first, QualitativeCheckResult const& second, + bool logicalAnd) { STORM_LOG_THROW(second.isExplicitQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot perform logical 'and' on check results of incompatible type."); STORM_LOG_THROW(first.isResultForAllStates() == second.isResultForAllStates(), storm::exceptions::InvalidOperationException, "Cannot perform logical 'and' on check results of incompatible type."); - ExplicitQualitativeCheckResult const& secondCheckResult = static_cast(second); + ExplicitQualitativeCheckResult const& secondCheckResult = static_cast const&>(second); if (first.isResultForAllStates()) { if (logicalAnd) { boost::get(first.truthValues) &= boost::get(secondCheckResult.truthValues); @@ -78,17 +95,20 @@ void ExplicitQualitativeCheckResult::performLogicalOperation(ExplicitQualitative } } -QualitativeCheckResult& ExplicitQualitativeCheckResult::operator&=(QualitativeCheckResult const& other) { +template +QualitativeCheckResult& ExplicitQualitativeCheckResult::operator&=(QualitativeCheckResult const& other) { performLogicalOperation(*this, other, true); return *this; } -QualitativeCheckResult& ExplicitQualitativeCheckResult::operator|=(QualitativeCheckResult const& other) { +template +QualitativeCheckResult& ExplicitQualitativeCheckResult::operator|=(QualitativeCheckResult const& other) { performLogicalOperation(*this, other, false); return *this; } -bool ExplicitQualitativeCheckResult::existsTrue() const { +template +bool ExplicitQualitativeCheckResult::existsTrue() const { if (this->isResultForAllStates()) { return !boost::get(truthValues).empty(); } else { @@ -100,7 +120,9 @@ bool ExplicitQualitativeCheckResult::existsTrue() const { return false; } } -bool ExplicitQualitativeCheckResult::forallTrue() const { + +template +bool ExplicitQualitativeCheckResult::forallTrue() const { if (this->isResultForAllStates()) { return boost::get(truthValues).full(); } else { @@ -113,7 +135,8 @@ bool ExplicitQualitativeCheckResult::forallTrue() const { } } -uint64_t ExplicitQualitativeCheckResult::count() const { +template +uint64_t ExplicitQualitativeCheckResult::count() const { if (this->isResultForAllStates()) { return boost::get(truthValues).getNumberOfSetBits(); } else { @@ -127,7 +150,8 @@ uint64_t ExplicitQualitativeCheckResult::count() const { } } -bool ExplicitQualitativeCheckResult::operator[](storm::storage::sparse::state_type state) const { +template +bool ExplicitQualitativeCheckResult::operator[](storm::storage::sparse::state_type state) const { if (this->isResultForAllStates()) { return boost::get(truthValues).get(state); } else { @@ -138,15 +162,18 @@ bool ExplicitQualitativeCheckResult::operator[](storm::storage::sparse::state_ty } } -ExplicitQualitativeCheckResult::vector_type const& ExplicitQualitativeCheckResult::getTruthValuesVector() const { +template +typename ExplicitQualitativeCheckResult::vector_type const& ExplicitQualitativeCheckResult::getTruthValuesVector() const { return boost::get(truthValues); } -ExplicitQualitativeCheckResult::map_type const& ExplicitQualitativeCheckResult::getTruthValuesMap() const { +template +typename ExplicitQualitativeCheckResult::map_type const& ExplicitQualitativeCheckResult::getTruthValuesMap() const { return boost::get(truthValues); } -void ExplicitQualitativeCheckResult::complement() { +template +void ExplicitQualitativeCheckResult::complement() { if (this->isResultForAllStates()) { boost::get(truthValues).complement(); } else { @@ -156,19 +183,23 @@ void ExplicitQualitativeCheckResult::complement() { } } -bool ExplicitQualitativeCheckResult::isExplicit() const { +template +bool ExplicitQualitativeCheckResult::isExplicit() const { return true; } -bool ExplicitQualitativeCheckResult::isResultForAllStates() const { +template +bool ExplicitQualitativeCheckResult::isResultForAllStates() const { return truthValues.which() == 0; } -bool ExplicitQualitativeCheckResult::isExplicitQualitativeCheckResult() const { +template +bool ExplicitQualitativeCheckResult::isExplicitQualitativeCheckResult() const { return true; } -std::ostream& ExplicitQualitativeCheckResult::writeToStream(std::ostream& out) const { +template +std::ostream& ExplicitQualitativeCheckResult::writeToStream(std::ostream& out) const { if (this->isResultForAllStates()) { vector_type const& vector = boost::get(truthValues); bool allTrue = vector.full(); @@ -211,11 +242,12 @@ std::ostream& ExplicitQualitativeCheckResult::writeToStream(std::ostream& out) c return out; } -void ExplicitQualitativeCheckResult::filter(QualitativeCheckResult const& filter) { +template +void ExplicitQualitativeCheckResult::filter(QualitativeCheckResult const& filter) { STORM_LOG_THROW(filter.isExplicitQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot filter explicit check result with non-explicit filter."); STORM_LOG_THROW(filter.isResultForAllStates(), storm::exceptions::InvalidOperationException, "Cannot filter check result with non-complete filter."); - ExplicitQualitativeCheckResult const& explicitFilter = filter.asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& explicitFilter = filter.template asExplicitQualitativeCheckResult(); vector_type const& filterTruthValues = explicitFilter.getTruthValuesVector(); if (this->isResultForAllStates()) { @@ -241,6 +273,28 @@ void ExplicitQualitativeCheckResult::filter(QualitativeCheckResult const& filter } } +template +bool ExplicitQualitativeCheckResult::hasScheduler() const { + return static_cast(scheduler); +} + +template +void ExplicitQualitativeCheckResult::setScheduler(std::unique_ptr>&& scheduler) { + this->scheduler = std::move(scheduler); +} + +template +storm::storage::Scheduler const& ExplicitQualitativeCheckResult::getScheduler() const { + STORM_LOG_THROW(this->hasScheduler(), storm::exceptions::InvalidOperationException, "Unable to retrieve non-existing scheduler."); + return *scheduler.get(); +} + +template +storm::storage::Scheduler& ExplicitQualitativeCheckResult::getScheduler() { + STORM_LOG_THROW(this->hasScheduler(), storm::exceptions::InvalidOperationException, "Unable to retrieve non-existing scheduler."); + return *scheduler.get(); +} + template void insertJsonEntry(storm::json& json, uint64_t const& id, bool value, std::optional const& stateValuations = std::nullopt, @@ -259,9 +313,10 @@ void insertJsonEntry(storm::json& json, uint64_t const& id, bo json.push_back(std::move(entry)); } +template template -storm::json ExplicitQualitativeCheckResult::toJson(std::optional const& stateValuations, - std::optional const& stateLabels) const { +storm::json ExplicitQualitativeCheckResult::toJson(std::optional const& stateValuations, + std::optional const& stateLabels) const { storm::json result; if (this->isResultForAllStates()) { vector_type const& valuesAsVector = boost::get(truthValues); @@ -277,10 +332,33 @@ storm::json ExplicitQualitativeCheckResult::toJson(std::option return result; } -template storm::json ExplicitQualitativeCheckResult::toJson(std::optional const&, - std::optional const&) const; -template storm::json ExplicitQualitativeCheckResult::toJson( +// Explicit template instantiations +template class ExplicitQualitativeCheckResult; +template storm::json ExplicitQualitativeCheckResult::toJson(std::optional const&, + std::optional const&) const; + +#ifdef STORM_HAVE_CARL +template storm::json ExplicitQualitativeCheckResult::toJson( + std::optional const&, std::optional const&) const; + +template class ExplicitQualitativeCheckResult; +template storm::json ExplicitQualitativeCheckResult::toJson( + std::optional const&, std::optional const&) const; +template storm::json ExplicitQualitativeCheckResult::toJson( + std::optional const&, std::optional const&) const; + +template class ExplicitQualitativeCheckResult; +template storm::json ExplicitQualitativeCheckResult::toJson( + std::optional const&, std::optional const&) const; +template storm::json ExplicitQualitativeCheckResult::toJson( + std::optional const&, std::optional const&) const; + +template class ExplicitQualitativeCheckResult; +template storm::json ExplicitQualitativeCheckResult::toJson(std::optional const&, + std::optional const&) const; +template storm::json ExplicitQualitativeCheckResult::toJson( std::optional const&, std::optional const&) const; +#endif } // namespace modelchecker } // namespace storm diff --git a/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.h b/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.h index 8e13acbef7..14d781ef86 100644 --- a/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.h +++ b/src/storm/modelchecker/results/ExplicitQualitativeCheckResult.h @@ -9,12 +9,15 @@ #include "storm/modelchecker/results/QualitativeCheckResult.h" #include "storm/models/sparse/StateLabeling.h" #include "storm/storage/BitVector.h" +#include "storm/storage/Scheduler.h" #include "storm/storage/sparse/StateType.h" #include "storm/storage/sparse/StateValuations.h" namespace storm { namespace modelchecker { + +template class ExplicitQualitativeCheckResult : public QualitativeCheckResult { public: typedef storm::storage::BitVector vector_type; @@ -27,8 +30,10 @@ class ExplicitQualitativeCheckResult : public QualitativeCheckResult { ExplicitQualitativeCheckResult(storm::storage::sparse::state_type state, bool value); ExplicitQualitativeCheckResult(vector_type const& truthValues); ExplicitQualitativeCheckResult(vector_type&& truthValues); - ExplicitQualitativeCheckResult(boost::variant const& truthValues); - ExplicitQualitativeCheckResult(boost::variant&& truthValues); + ExplicitQualitativeCheckResult(boost::variant const& truthValues, + boost::optional>> scheduler = boost::none); + ExplicitQualitativeCheckResult(boost::variant&& truthValues, + boost::optional>> scheduler = boost::none); ExplicitQualitativeCheckResult(ExplicitQualitativeCheckResult const& other) = default; ExplicitQualitativeCheckResult& operator=(ExplicitQualitativeCheckResult const& other) = default; @@ -60,6 +65,11 @@ class ExplicitQualitativeCheckResult : public QualitativeCheckResult { virtual void filter(QualitativeCheckResult const& filter) override; + virtual bool hasScheduler() const override; + void setScheduler(std::unique_ptr>&& scheduler); + storm::storage::Scheduler const& getScheduler() const; + storm::storage::Scheduler& getScheduler(); + template storm::json toJson(std::optional const& stateValuations = std::nullopt, std::optional const& stateLabels = std::nullopt) const; @@ -69,6 +79,9 @@ class ExplicitQualitativeCheckResult : public QualitativeCheckResult { // The values of the quantitative check result. boost::variant truthValues; + + // An optional scheduler that accompanies the values. + boost::optional>> scheduler; }; } // namespace modelchecker } // namespace storm diff --git a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp index 3464ee9381..f9dc8f2bef 100644 --- a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp @@ -61,7 +61,7 @@ ExplicitQuantitativeCheckResult::ExplicitQuantitativeCheckResult(boos } template -ExplicitQuantitativeCheckResult::ExplicitQuantitativeCheckResult(ExplicitQualitativeCheckResult const& other) { +ExplicitQuantitativeCheckResult::ExplicitQuantitativeCheckResult(ExplicitQualitativeCheckResult const& other) { if (other.isResultForAllStates()) { storm::storage::BitVector const& bvValues = other.getTruthValuesVector(); @@ -73,7 +73,7 @@ ExplicitQuantitativeCheckResult::ExplicitQuantitativeCheckResult(Expl values = newVector; } else { - ExplicitQualitativeCheckResult::map_type const& bitMap = other.getTruthValuesMap(); + typename ExplicitQualitativeCheckResult::map_type const& bitMap = other.getTruthValuesMap(); map_type newMap; for (auto const& e : bitMap) { @@ -109,8 +109,8 @@ void ExplicitQuantitativeCheckResult::filter(QualitativeCheckResult c STORM_LOG_THROW(filter.isExplicitQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot filter explicit check result with non-explicit filter."); STORM_LOG_THROW(filter.isResultForAllStates(), storm::exceptions::InvalidOperationException, "Cannot filter check result with non-complete filter."); - ExplicitQualitativeCheckResult const& explicitFilter = filter.asExplicitQualitativeCheckResult(); - ExplicitQualitativeCheckResult::vector_type const& filterTruthValues = explicitFilter.getTruthValuesVector(); + ExplicitQualitativeCheckResult const& explicitFilter = filter.template asExplicitQualitativeCheckResult(); + typename ExplicitQualitativeCheckResult::vector_type const& filterTruthValues = explicitFilter.getTruthValuesVector(); if (this->isResultForAllStates()) { map_type newMap; @@ -369,7 +369,7 @@ std::unique_ptr ExplicitQuantitativeCheckResult::compare } break; } - return std::unique_ptr(new ExplicitQualitativeCheckResult(std::move(result))); + return std::unique_ptr(new ExplicitQualitativeCheckResult(std::move(result), std::move(scheduler))); } else { map_type const& valuesAsMap = boost::get(values); std::map result; @@ -395,7 +395,7 @@ std::unique_ptr ExplicitQuantitativeCheckResult::compare } break; } - return std::unique_ptr(new ExplicitQualitativeCheckResult(std::move(result))); + return std::unique_ptr(new ExplicitQualitativeCheckResult(std::move(result), std::move(scheduler))); } } diff --git a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h index e9c9ac487d..125752ca14 100644 --- a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h +++ b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h @@ -16,6 +16,7 @@ namespace storm { namespace modelchecker { // Forward declaration +template class ExplicitQualitativeCheckResult; template @@ -39,7 +40,7 @@ class ExplicitQuantitativeCheckResult : public QuantitativeCheckResult const& other); virtual ~ExplicitQuantitativeCheckResult() = default; diff --git a/src/storm/modelchecker/results/LexicographicCheckResult.cpp b/src/storm/modelchecker/results/LexicographicCheckResult.cpp index 027f21f3ef..0206554088 100644 --- a/src/storm/modelchecker/results/LexicographicCheckResult.cpp +++ b/src/storm/modelchecker/results/LexicographicCheckResult.cpp @@ -43,8 +43,8 @@ void LexicographicCheckResult::filter(QualitativeCheckResult const& f STORM_LOG_THROW(filter.isExplicitQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot filter explicit check result with non-explicit filter."); STORM_LOG_THROW(filter.isResultForAllStates(), storm::exceptions::InvalidOperationException, "Cannot filter check result with non-complete filter."); - ExplicitQualitativeCheckResult const& explicitFilter = filter.asExplicitQualitativeCheckResult(); - ExplicitQualitativeCheckResult::vector_type const& filterTruthValues = explicitFilter.getTruthValuesVector(); + ExplicitQualitativeCheckResult const& explicitFilter = filter.template asExplicitQualitativeCheckResult(); + typename ExplicitQualitativeCheckResult::vector_type const& filterTruthValues = explicitFilter.getTruthValuesVector(); STORM_LOG_THROW(filterTruthValues.getNumberOfSetBits() == 1 && filterTruthValues.get(state), storm::exceptions::InvalidOperationException, "The check result fails to contain some results referred to by the filter."); diff --git a/src/storm/storage/bisimulation/BisimulationDecomposition.cpp b/src/storm/storage/bisimulation/BisimulationDecomposition.cpp index 4828c13ef7..2f3206ac29 100644 --- a/src/storm/storage/bisimulation/BisimulationDecomposition.cpp +++ b/src/storm/storage/bisimulation/BisimulationDecomposition.cpp @@ -160,8 +160,8 @@ void BisimulationDecomposition::Options::checkAndSetMe storm::modelchecker::SparsePropositionalModelChecker checker(model); std::unique_ptr phiStatesCheckResult = checker.check(*leftSubformula); std::unique_ptr psiStatesCheckResult = checker.check(*rightSubformula); - phiStates = phiStatesCheckResult->asExplicitQualitativeCheckResult().getTruthValuesVector(); - psiStates = psiStatesCheckResult->asExplicitQualitativeCheckResult().getTruthValuesVector(); + phiStates = phiStatesCheckResult->template asExplicitQualitativeCheckResult().getTruthValuesVector(); + psiStates = psiStatesCheckResult->template asExplicitQualitativeCheckResult().getTruthValuesVector(); } else { optimalityType = boost::none; } diff --git a/src/storm/transformer/MemoryIncorporation.cpp b/src/storm/transformer/MemoryIncorporation.cpp index a0d894e6a3..14554ec711 100644 --- a/src/storm/transformer/MemoryIncorporation.cpp +++ b/src/storm/transformer/MemoryIncorporation.cpp @@ -27,7 +27,8 @@ storm::storage::MemoryStructure getGoalMemory(SparseModelType const& model, stor "The subformula " << propositionalGoalStateFormula << " should be propositional."); storm::modelchecker::SparsePropositionalModelChecker mc(model); - storm::storage::BitVector goalStates = mc.check(propositionalGoalStateFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + storm::storage::BitVector goalStates = + mc.check(propositionalGoalStateFormula)->template asExplicitQualitativeCheckResult().getTruthValuesVector(); // Check if the formula is already satisfied for all initial states. In such a case the trivial memory structure suffices. if (model.getInitialStates().isSubsetOf(goalStates)) { diff --git a/src/test/storm-pars/modelchecker/region/monotonicity/MonotonicityCheckerTest.cpp b/src/test/storm-pars/modelchecker/region/monotonicity/MonotonicityCheckerTest.cpp index ceab40c2fe..9a78b6f47c 100644 --- a/src/test/storm-pars/modelchecker/region/monotonicity/MonotonicityCheckerTest.cpp +++ b/src/test/storm-pars/modelchecker/region/monotonicity/MonotonicityCheckerTest.cpp @@ -52,7 +52,8 @@ TEST_F(MonotonicityCheckerTest, Simple1_larger_region) { storm::storage::BitVector psiStates; phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true); storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula(); - psiStates = propositionalChecker.check(formula.getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + psiStates = + propositionalChecker.check(formula.getSubformula())->template asExplicitQualitativeCheckResult().getTruthValuesVector(); // Get the maybeStates std::pair statesWithProbability01 = storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates); @@ -100,7 +101,8 @@ TEST_F(MonotonicityCheckerTest, Simple1_small_region) { storm::storage::BitVector psiStates; phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true); storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula(); - psiStates = propositionalChecker.check(formula.getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + psiStates = + propositionalChecker.check(formula.getSubformula())->template asExplicitQualitativeCheckResult().getTruthValuesVector(); // Get the maybeStates std::pair statesWithProbability01 = storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates); @@ -149,7 +151,8 @@ TEST_F(MonotonicityCheckerTest, Casestudy1) { storm::storage::BitVector psiStates; phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true); storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula(); - psiStates = propositionalChecker.check(formula.getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + psiStates = + propositionalChecker.check(formula.getSubformula())->template asExplicitQualitativeCheckResult().getTruthValuesVector(); // Get the maybeStates std::pair statesWithProbability01 = storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates); @@ -202,7 +205,8 @@ TEST_F(MonotonicityCheckerTest, Casestudy2) { storm::storage::BitVector psiStates; phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true); storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula(); - psiStates = propositionalChecker.check(formula.getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + psiStates = + propositionalChecker.check(formula.getSubformula())->template asExplicitQualitativeCheckResult().getTruthValuesVector(); // Get the maybeStates std::pair statesWithProbability01 = storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates); @@ -256,7 +260,8 @@ TEST_F(MonotonicityCheckerTest, Casestudy3) { storm::storage::BitVector psiStates; phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true); storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula(); - psiStates = propositionalChecker.check(formula.getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + psiStates = + propositionalChecker.check(formula.getSubformula())->template asExplicitQualitativeCheckResult().getTruthValuesVector(); // Get the maybeStates std::pair statesWithProbability01 = storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates); diff --git a/src/test/storm-pars/modelchecker/region/monotonicity/OrderExtenderTest.cpp b/src/test/storm-pars/modelchecker/region/monotonicity/OrderExtenderTest.cpp index 0c865a12ea..a50109532e 100644 --- a/src/test/storm-pars/modelchecker/region/monotonicity/OrderExtenderTest.cpp +++ b/src/test/storm-pars/modelchecker/region/monotonicity/OrderExtenderTest.cpp @@ -144,7 +144,8 @@ TEST_F(OrderExtenderTest, Brp_with_bisimulation_on_matrix) { storm::storage::BitVector psiStates; phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true); storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula(); - psiStates = propositionalChecker.check(formula.getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + psiStates = + propositionalChecker.check(formula.getSubformula())->template asExplicitQualitativeCheckResult().getTruthValuesVector(); // Get the maybeStates std::pair statesWithProbability01 = storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates); @@ -191,7 +192,8 @@ TEST_F(OrderExtenderTest, Brp_without_bisimulation_on_matrix) { storm::storage::BitVector psiStates; phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true); storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula(); - psiStates = propositionalChecker.check(formula.getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + psiStates = + propositionalChecker.check(formula.getSubformula())->template asExplicitQualitativeCheckResult().getTruthValuesVector(); // Get the maybeStates std::pair statesWithProbability01 = storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates); @@ -268,7 +270,8 @@ TEST_F(OrderExtenderTest, simple1_on_matrix) { storm::storage::BitVector psiStates; phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true); storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula(); - psiStates = propositionalChecker.check(formula.getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + psiStates = + propositionalChecker.check(formula.getSubformula())->template asExplicitQualitativeCheckResult().getTruthValuesVector(); // Get the maybeStates std::pair statesWithProbability01 = storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates); @@ -359,7 +362,8 @@ TEST_F(OrderExtenderTest, casestudy1_on_matrix) { storm::storage::BitVector psiStates; phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true); storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula(); - psiStates = propositionalChecker.check(formula.getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + psiStates = + propositionalChecker.check(formula.getSubformula())->template asExplicitQualitativeCheckResult().getTruthValuesVector(); // Get the maybeStates std::pair statesWithProbability01 = storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates); @@ -412,7 +416,8 @@ TEST_F(OrderExtenderTest, casestudy2_on_matrix) { storm::storage::BitVector psiStates; phiStates = storm::storage::BitVector(model->getTransitionMatrix().getRowCount(), true); storm::logic::EventuallyFormula formula = formulas[0]->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula(); - psiStates = propositionalChecker.check(formula.getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + psiStates = + propositionalChecker.check(formula.getSubformula())->template asExplicitQualitativeCheckResult().getTruthValuesVector(); // Get the maybeStates std::pair statesWithProbability01 = storm::utility::graph::performProb01(model->getBackwardTransitions(), phiStates, psiStates); diff --git a/src/test/storm-pars/transformer/IntervalEndComponentPreserverCheckTest.cpp b/src/test/storm-pars/transformer/IntervalEndComponentPreserverCheckTest.cpp index bdc748e6e0..6fd2a97347 100644 --- a/src/test/storm-pars/transformer/IntervalEndComponentPreserverCheckTest.cpp +++ b/src/test/storm-pars/transformer/IntervalEndComponentPreserverCheckTest.cpp @@ -53,7 +53,7 @@ void testModelInterval(std::string programFile, std::string formulaAsString, std storm::modelchecker::SparsePropositionalModelChecker> propositionalChecker(*dtmc); storm::storage::BitVector psiStates = propositionalChecker.check(checkTask.getFormula().asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula()) - ->asExplicitQualitativeCheckResult() + ->template asExplicitQualitativeCheckResult() .getTruthValuesVector(); std::vector target(model->getNumberOfStates(), storm::utility::zero()); diff --git a/src/test/storm-permissive/analysis/MilpPermissiveSchedulerTest.cpp b/src/test/storm-permissive/analysis/MilpPermissiveSchedulerTest.cpp index b3c587afd2..46ab3d299b 100644 --- a/src/test/storm-permissive/analysis/MilpPermissiveSchedulerTest.cpp +++ b/src/test/storm-permissive/analysis/MilpPermissiveSchedulerTest.cpp @@ -55,7 +55,7 @@ TEST(MilpPermissiveSchedulerTest, DieSelection) { storm::modelchecker::SparseMdpPrctlModelChecker> checker0(*mdp); std::unique_ptr result0 = checker0.check(env, formula02); - storm::modelchecker::ExplicitQualitativeCheckResult& qualitativeResult0 = result0->asExplicitQualitativeCheckResult(); + storm::modelchecker::ExplicitQualitativeCheckResult& qualitativeResult0 = result0->template asExplicitQualitativeCheckResult(); ASSERT_FALSE(qualitativeResult0[0]); @@ -63,7 +63,7 @@ TEST(MilpPermissiveSchedulerTest, DieSelection) { storm::modelchecker::SparseMdpPrctlModelChecker> checker1(submdp); std::unique_ptr result1 = checker1.check(env, formula02); - storm::modelchecker::ExplicitQualitativeCheckResult& qualitativeResult1 = result1->asExplicitQualitativeCheckResult(); + storm::modelchecker::ExplicitQualitativeCheckResult& qualitativeResult1 = result1->template asExplicitQualitativeCheckResult(); EXPECT_TRUE(qualitativeResult1[0]); } diff --git a/src/test/storm-permissive/analysis/SmtPermissiveSchedulerTest.cpp b/src/test/storm-permissive/analysis/SmtPermissiveSchedulerTest.cpp index 84594a1389..99aa4fa1b8 100644 --- a/src/test/storm-permissive/analysis/SmtPermissiveSchedulerTest.cpp +++ b/src/test/storm-permissive/analysis/SmtPermissiveSchedulerTest.cpp @@ -49,7 +49,7 @@ TEST(SmtPermissiveSchedulerTest, DieSelection) { storm::modelchecker::SparseMdpPrctlModelChecker> checker0(*mdp); std::unique_ptr result0 = checker0.check(env, formula02b); - storm::modelchecker::ExplicitQualitativeCheckResult& qualitativeResult0 = result0->asExplicitQualitativeCheckResult(); + storm::modelchecker::ExplicitQualitativeCheckResult& qualitativeResult0 = result0->template asExplicitQualitativeCheckResult(); ASSERT_FALSE(qualitativeResult0[0]); @@ -57,7 +57,7 @@ TEST(SmtPermissiveSchedulerTest, DieSelection) { storm::modelchecker::SparseMdpPrctlModelChecker> checker1(submdp); std::unique_ptr result1 = checker1.check(env, formula02b); - storm::modelchecker::ExplicitQualitativeCheckResult& qualitativeResult1 = result1->asExplicitQualitativeCheckResult(); + storm::modelchecker::ExplicitQualitativeCheckResult& qualitativeResult1 = result1->template asExplicitQualitativeCheckResult(); EXPECT_TRUE(qualitativeResult1[0]); diff --git a/src/test/storm/modelchecker/csl/CtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/csl/CtmcCslModelCheckerTest.cpp index e546e33be6..2692e8c546 100644 --- a/src/test/storm/modelchecker/csl/CtmcCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/csl/CtmcCslModelCheckerTest.cpp @@ -318,7 +318,7 @@ class CtmcCslModelCheckerTest : public ::testing::Test { std::unique_ptr getInitialStateFilter(std::shared_ptr> const& model) const { if (isSparseModel()) { - return std::make_unique(model->template as()->getInitialStates()); + return std::make_unique>(model->template as()->getInitialStates()); } else { return std::make_unique>( model->template as()->getReachableStates(), model->template as()->getInitialStates()); diff --git a/src/test/storm/modelchecker/csl/LraCtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/csl/LraCtmcCslModelCheckerTest.cpp index c7273dd2a4..36e162ab5b 100644 --- a/src/test/storm/modelchecker/csl/LraCtmcCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/csl/LraCtmcCslModelCheckerTest.cpp @@ -381,7 +381,7 @@ class LraCtmcCslModelCheckerTest : public ::testing::Test { std::unique_ptr getInitialStateFilter(std::shared_ptr> const& model) const { if (isSparseModel()) { - return std::make_unique(model->template as()->getInitialStates()); + return std::make_unique>(model->template as()->getInitialStates()); } else { return std::make_unique>( model->template as()->getReachableStates(), model->template as()->getInitialStates()); diff --git a/src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp b/src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp index 4010abee25..3a398d1b1e 100644 --- a/src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp @@ -245,7 +245,7 @@ class MarkovAutomatonCslModelCheckerTest : public ::testing::Test { std::unique_ptr getInitialStateFilter(std::shared_ptr> const& model) const { if (isSparseModel()) { - return std::make_unique(model->template as()->getInitialStates()); + return std::make_unique>(model->template as()->getInitialStates()); } else { return std::make_unique>( model->template as()->getReachableStates(), model->template as()->getInitialStates()); diff --git a/src/test/storm/modelchecker/multiobjective/MultiObjectiveSchedRestModelCheckerTest.cpp b/src/test/storm/modelchecker/multiobjective/MultiObjectiveSchedRestModelCheckerTest.cpp index 755a60f403..42fd7aa01e 100644 --- a/src/test/storm/modelchecker/multiobjective/MultiObjectiveSchedRestModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/multiobjective/MultiObjectiveSchedRestModelCheckerTest.cpp @@ -274,13 +274,13 @@ TYPED_TEST(MultiObjectiveSchedRestModelCheckerTest, steps) { { auto result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[formulaIndex]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[*mdp->getInitialStates().begin()]); + EXPECT_TRUE(result->template asExplicitQualitativeCheckResult()[*mdp->getInitialStates().begin()]); } ++formulaIndex; { auto result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[formulaIndex]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[*mdp->getInitialStates().begin()]); + EXPECT_FALSE(result->template asExplicitQualitativeCheckResult()[*mdp->getInitialStates().begin()]); } ++formulaIndex; { @@ -293,7 +293,7 @@ TYPED_TEST(MultiObjectiveSchedRestModelCheckerTest, steps) { { auto result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[formulaIndex]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[*mdp->getInitialStates().begin()]); + EXPECT_FALSE(result->template asExplicitQualitativeCheckResult()[*mdp->getInitialStates().begin()]); } } @@ -359,7 +359,7 @@ TYPED_TEST(MultiObjectiveSchedRestModelCheckerTest, mecs) { } else { auto result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[formulaIndex]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[*mdp->getInitialStates().begin()]); + EXPECT_TRUE(result->template asExplicitQualitativeCheckResult()[*mdp->getInitialStates().begin()]); } } ++formulaIndex; @@ -371,7 +371,7 @@ TYPED_TEST(MultiObjectiveSchedRestModelCheckerTest, mecs) { } else { auto result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[formulaIndex]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[*mdp->getInitialStates().begin()]); + EXPECT_FALSE(result->template asExplicitQualitativeCheckResult()[*mdp->getInitialStates().begin()]); } } } diff --git a/src/test/storm/modelchecker/multiobjective/SparseMaCbMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/multiobjective/SparseMaCbMultiObjectiveModelCheckerTest.cpp index 94df68f83b..074797ec94 100644 --- a/src/test/storm/modelchecker/multiobjective/SparseMaCbMultiObjectiveModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/multiobjective/SparseMaCbMultiObjectiveModelCheckerTest.cpp @@ -43,9 +43,9 @@ TEST_F(SparseMaCbMultiObjectiveModelCheckerTest, server) { result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[0]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); + EXPECT_TRUE(result->template asExplicitQualitativeCheckResult()[initState]); result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[1]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); + EXPECT_FALSE(result->template asExplicitQualitativeCheckResult()[initState]); } diff --git a/src/test/storm/modelchecker/multiobjective/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/multiobjective/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp index 74a47f3f6a..f4a19f9597 100644 --- a/src/test/storm/modelchecker/multiobjective/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/multiobjective/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp @@ -172,12 +172,12 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_achievability_3Obj std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[0]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); + EXPECT_TRUE(result->template asExplicitQualitativeCheckResult()[initState]); std::unique_ptr result2 = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[1]->asMultiObjectiveFormula()); ASSERT_TRUE(result2->isExplicitQualitativeCheckResult()); - EXPECT_FALSE(result2->asExplicitQualitativeCheckResult()[initState]); + EXPECT_FALSE(result2->template asExplicitQualitativeCheckResult()[initState]); } TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_quantitative_3Obj) { @@ -210,7 +210,7 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_quantitative_3Obj) std::unique_ptr result2 = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[1]->asMultiObjectiveFormula()); ASSERT_TRUE(result2->isExplicitQualitativeCheckResult()); - EXPECT_FALSE(result2->asExplicitQualitativeCheckResult()[initState]); + EXPECT_FALSE(result2->template asExplicitQualitativeCheckResult()[initState]); } TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_pareto_2Obj) { diff --git a/src/test/storm/modelchecker/multiobjective/SparseMdpCbMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/multiobjective/SparseMdpCbMultiObjectiveModelCheckerTest.cpp index baa4726654..16250a581f 100644 --- a/src/test/storm/modelchecker/multiobjective/SparseMdpCbMultiObjectiveModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/multiobjective/SparseMdpCbMultiObjectiveModelCheckerTest.cpp @@ -43,11 +43,11 @@ TEST_F(SparseMdpCbMultiObjectiveModelCheckerTest, consensus) { result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[1]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); + EXPECT_TRUE(result->template asExplicitQualitativeCheckResult()[initState]); result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[2]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); + EXPECT_FALSE(result->template asExplicitQualitativeCheckResult()[initState]); } TEST_F(SparseMdpCbMultiObjectiveModelCheckerTest, zeroconf) { @@ -69,7 +69,7 @@ TEST_F(SparseMdpCbMultiObjectiveModelCheckerTest, zeroconf) { std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); + EXPECT_TRUE(result->template asExplicitQualitativeCheckResult()[initState]); } /* This test takes a little bit too long ... @@ -88,6 +88,6 @@ formulas)->as>(); uint_fast64_ std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula()) ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); + EXPECT_FALSE(result->template asExplicitQualitativeCheckResult()[initState]); } */ diff --git a/src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp index d08c62033d..8a40aa4161 100644 --- a/src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp @@ -228,11 +228,11 @@ TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, consensus) { result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[1]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); + EXPECT_TRUE(result->template asExplicitQualitativeCheckResult()[initState]); result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[2]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); + EXPECT_FALSE(result->template asExplicitQualitativeCheckResult()[initState]); } TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, zeroconf) { @@ -304,7 +304,7 @@ TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, tiny_rewards_negative) { std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula()); - EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); + EXPECT_TRUE(result->template asExplicitQualitativeCheckResult()[initState]); } TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, scheduler) { @@ -328,7 +328,7 @@ TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, scheduler) { std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula()); - EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); + EXPECT_TRUE(result->template asExplicitQualitativeCheckResult()[initState]); } TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, dpm) { diff --git a/src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp index 5083138f3b..a5a8fe0e26 100644 --- a/src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp @@ -644,7 +644,7 @@ class DtmcPrctlModelCheckerTest : public ::testing::Test { std::unique_ptr getInitialStateFilter(std::shared_ptr> const& model) const { if (isSparseModel()) { - return std::make_unique(model->template as()->getInitialStates()); + return std::make_unique>(model->template as()->getInitialStates()); } else { return std::make_unique>( model->template as()->getReachableStates(), model->template as()->getInitialStates()); diff --git a/src/test/storm/modelchecker/prctl/mdp/MdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/MdpPrctlModelCheckerTest.cpp index 8c01df8684..26d4b4622e 100644 --- a/src/test/storm/modelchecker/prctl/mdp/MdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/MdpPrctlModelCheckerTest.cpp @@ -670,7 +670,7 @@ class MdpPrctlModelCheckerTest : public ::testing::Test { std::unique_ptr getInitialStateFilter(std::shared_ptr> const& model) const { if (isSparseModel()) { - return std::make_unique(model->template as()->getInitialStates()); + return std::make_unique>(model->template as()->getInitialStates()); } else { return std::make_unique>( model->template as()->getReachableStates(), model->template as()->getInitialStates()); diff --git a/src/test/storm/modelchecker/prctl/mdp/QuantileQueryTest.cpp b/src/test/storm/modelchecker/prctl/mdp/QuantileQueryTest.cpp index 635b352b69..c2204c444d 100644 --- a/src/test/storm/modelchecker/prctl/mdp/QuantileQueryTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/QuantileQueryTest.cpp @@ -164,7 +164,7 @@ class QuantileQueryTest : public ::testing::Test { std::unique_ptr getInitialStateFilter( std::shared_ptr> const& model) const { - return std::make_unique(model->getInitialStates()); + return std::make_unique>(model->getInitialStates()); } }; diff --git a/src/test/storm/modelchecker/prctl/mdp/RobustMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/RobustMdpPrctlModelCheckerTest.cpp index 27a9254a16..3d509f2fbc 100644 --- a/src/test/storm/modelchecker/prctl/mdp/RobustMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/RobustMdpPrctlModelCheckerTest.cpp @@ -17,11 +17,11 @@ std::unique_ptr getInitialStateFilter( std::shared_ptr> const& model) { - return std::make_unique(model->getInitialStates()); + return std::make_unique>(model->getInitialStates()); } std::unique_ptr getInitialStateFilter(std::shared_ptr> const& model) { - return std::make_unique(model->getInitialStates()); + return std::make_unique>(model->getInitialStates()); } double getQuantitativeResultAtInitialState(std::shared_ptr> const& model,