diff --git a/src/storm/modelchecker/parametric/ParameterLifting.cpp b/src/storm/modelchecker/parametric/ParameterLifting.cpp index d0ea5dc08..4db278bba 100644 --- a/src/storm/modelchecker/parametric/ParameterLifting.cpp +++ b/src/storm/modelchecker/parametric/ParameterLifting.cpp @@ -17,6 +17,7 @@ #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/CoreSettings.h" +#include "storm/settings/modules/ParametricSettings.h" namespace storm { @@ -24,8 +25,7 @@ namespace storm { namespace parametric { ParameterLiftingSettings::ParameterLiftingSettings() { - // todo: get this form settings - this->applyExactValidation = false; + this->applyExactValidation = storm::settings::getModule().isExactValidationSet(); } template @@ -126,20 +126,24 @@ namespace storm { if (numericResult == RegionCheckResult::AllSat) { if(!exactParameterLiftingChecker->check(region, this->currentCheckTask->getOptimizationDirection())->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) { // Numerical result is wrong; Check whether the region is AllViolated! + STORM_LOG_INFO("Numerical result was wrong for one region... Applying exact methods to obtain the actual result..."); if(!exactParameterLiftingChecker->check(region, storm::solver::invert(this->currentCheckTask->getOptimizationDirection()))->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) { parameterLiftingCheckerStopwatch.stop(); return RegionCheckResult::AllViolated; } else { + parameterLiftingCheckerStopwatch.stop(); return RegionCheckResult::Unknown; } } } else if (numericResult == RegionCheckResult::AllViolated) { if(exactParameterLiftingChecker->check(region, storm::solver::invert(this->currentCheckTask->getOptimizationDirection()))->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) { // Numerical result is wrong; Check whether the region is AllSat! + STORM_LOG_INFO("Numerical result was wrong for one region... Applying exact methods to obtain the actual result..."); if(exactParameterLiftingChecker->check(region, this->currentCheckTask->getOptimizationDirection())->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) { parameterLiftingCheckerStopwatch.stop(); return RegionCheckResult::AllSat; } else { + parameterLiftingCheckerStopwatch.stop(); return RegionCheckResult::Unknown; } } diff --git a/src/storm/modelchecker/parametric/SparseDtmcParameterLifting.cpp b/src/storm/modelchecker/parametric/SparseDtmcParameterLifting.cpp index 2ca6ba507..55b1406a8 100644 --- a/src/storm/modelchecker/parametric/SparseDtmcParameterLifting.cpp +++ b/src/storm/modelchecker/parametric/SparseDtmcParameterLifting.cpp @@ -33,7 +33,7 @@ namespace storm { template void SparseDtmcParameterLifting::initializeUnderlyingCheckers() { if (this->settings.applyExactValidation) { - STORM_LOG_WARN_COND((std::is_same::CoefficientType>::value) , "Exact validation is not necessarry if the original computation is already exact"); + STORM_LOG_WARN_COND(!(std::is_same::CoefficientType>::value) , "Exact validation is not necessarry if the original computation is already exact"); this->exactParameterLiftingChecker = std::make_unique::CoefficientType>>(this->getConsideredParametricModel()); } this->parameterLiftingChecker = std::make_unique>(this->getConsideredParametricModel()); diff --git a/src/storm/modelchecker/parametric/SparseMdpParameterLifting.cpp b/src/storm/modelchecker/parametric/SparseMdpParameterLifting.cpp index 25d222063..001d0d6e4 100644 --- a/src/storm/modelchecker/parametric/SparseMdpParameterLifting.cpp +++ b/src/storm/modelchecker/parametric/SparseMdpParameterLifting.cpp @@ -33,7 +33,7 @@ namespace storm { template void SparseMdpParameterLifting::initializeUnderlyingCheckers() { if (this->settings.applyExactValidation) { - STORM_LOG_WARN_COND((std::is_same::CoefficientType>::value), "Exact validation is not necessarry if the original computation is already exact"); + STORM_LOG_WARN_COND(!(std::is_same::CoefficientType>::value), "Exact validation is not necessarry if the original computation is already exact"); this->exactParameterLiftingChecker = std::make_unique::CoefficientType>>(this->getConsideredParametricModel()); } this->parameterLiftingChecker = std::make_unique>(this->getConsideredParametricModel());