diff --git a/src/storm/modelchecker/parametric/ParameterLifting.h b/src/storm/modelchecker/parametric/ParameterLifting.h index c428d1ba9..2626ce7ab 100644 --- a/src/storm/modelchecker/parametric/ParameterLifting.h +++ b/src/storm/modelchecker/parametric/ParameterLifting.h @@ -69,7 +69,8 @@ namespace storm { std::unique_ptr> parameterLiftingChecker; - std::unique_ptr> exactParameterLiftingChecker; + std::unique_ptr> exactParameterLiftingChecker; // todo: use template argument instead of rational number + //std::unique_ptr> exactParameterLiftingChecker; std::unique_ptr> instantiationChecker; mutable storm::utility::Stopwatch initializationStopwatch, instantiationCheckerStopwatch, parameterLiftingCheckerStopwatch; diff --git a/src/storm/modelchecker/parametric/SparseDtmcParameterLifting.cpp b/src/storm/modelchecker/parametric/SparseDtmcParameterLifting.cpp index 55b1406a8..021bbdd59 100644 --- a/src/storm/modelchecker/parametric/SparseDtmcParameterLifting.cpp +++ b/src/storm/modelchecker/parametric/SparseDtmcParameterLifting.cpp @@ -33,8 +33,10 @@ 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"); - this->exactParameterLiftingChecker = std::make_unique::CoefficientType>>(this->getConsideredParametricModel()); + //STORM_LOG_WARN_COND(!(std::is_same::CoefficientType) , "Exact validation is not necessarry if the original computation is already exact"); + STORM_LOG_WARN_COND(!(std::is_same::value) , "Exact validation is not necessarry if the original computation is already exact"); + //this->exactParameterLiftingChecker = std::make_unique::CoefficientType>>(this->getConsideredParametricModel()); // todo: use template argument instead of storm::Rational + this->exactParameterLiftingChecker = std::make_unique>(this->getConsideredParametricModel()); } this->parameterLiftingChecker = std::make_unique>(this->getConsideredParametricModel()); this->instantiationChecker = std::make_unique>(this->getConsideredParametricModel()); @@ -44,7 +46,8 @@ namespace storm { void SparseDtmcParameterLifting::applyHintsToExactChecker() { auto dtmcPLChecker = dynamic_cast*>(this->parameterLiftingChecker.get()); STORM_LOG_ASSERT(dtmcPLChecker, "Underlying Parameter lifting checker has unexpected type"); - auto exactDtmcPLChecker = dynamic_cast::CoefficientType>*>(this->exactParameterLiftingChecker.get()); + auto exactDtmcPLChecker = dynamic_cast*>(this->exactParameterLiftingChecker.get()); + //auto exactDtmcPLChecker = dynamic_cast::CoefficientType>*>(this->exactParameterLiftingChecker.get()); // todo: use template argument instead of storm::Rational STORM_LOG_ASSERT(exactDtmcPLChecker, "Underlying exact parameter lifting checker has unexpected type"); exactDtmcPLChecker->getCurrentMaxScheduler() = dtmcPLChecker->getCurrentMaxScheduler(); exactDtmcPLChecker->getCurrentMinScheduler() = dtmcPLChecker->getCurrentMinScheduler(); diff --git a/src/storm/modelchecker/parametric/SparseMdpParameterLifting.cpp b/src/storm/modelchecker/parametric/SparseMdpParameterLifting.cpp index 001d0d6e4..43c6db29a 100644 --- a/src/storm/modelchecker/parametric/SparseMdpParameterLifting.cpp +++ b/src/storm/modelchecker/parametric/SparseMdpParameterLifting.cpp @@ -33,8 +33,10 @@ 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"); - this->exactParameterLiftingChecker = std::make_unique::CoefficientType>>(this->getConsideredParametricModel()); + //STORM_LOG_WARN_COND(!(std::is_same::CoefficientType>::value), "Exact validation is not necessarry if the original computation is already exact"); // todo: use templated argument instead of storm::RationalNumber + STORM_LOG_WARN_COND(!(std::is_same::value), "Exact validation is not necessarry if the original computation is already exact"); + //this->exactParameterLiftingChecker = std::make_unique::CoefficientType>>(this->getConsideredParametricModel()); // todo: use templated argument instead of storm::RationalNumber + this->exactParameterLiftingChecker = std::make_unique>(this->getConsideredParametricModel()); } this->parameterLiftingChecker = std::make_unique>(this->getConsideredParametricModel()); this->instantiationChecker = std::make_unique>(this->getConsideredParametricModel()); @@ -44,7 +46,8 @@ namespace storm { void SparseMdpParameterLifting::applyHintsToExactChecker() { auto MdpPLChecker = dynamic_cast*>(this->parameterLiftingChecker.get()); STORM_LOG_ASSERT(MdpPLChecker, "Underlying Parameter lifting checker has unexpected type"); - auto exactMdpPLChecker = dynamic_cast::CoefficientType>*>(this->exactParameterLiftingChecker.get()); + auto exactMdpPLChecker = dynamic_cast*>(this->exactParameterLiftingChecker.get()); +// auto exactMdpPLChecker = dynamic_cast::CoefficientType>*>(this->exactParameterLiftingChecker.get()); // todo: use template argument instead of storm::RationalNumber STORM_LOG_ASSERT(exactMdpPLChecker, "Underlying exact parameter lifting checker has unexpected type"); exactMdpPLChecker->getCurrentMaxScheduler() = MdpPLChecker->getCurrentMaxScheduler(); exactMdpPLChecker->getCurrentMinScheduler() = MdpPLChecker->getCurrentMinScheduler();