diff --git a/src/storm-dft/transformations/DftInstantiator.h b/src/storm-dft/transformations/DftInstantiator.h index 2753d6424..3fbc98cf8 100644 --- a/src/storm-dft/transformations/DftInstantiator.h +++ b/src/storm-dft/transformations/DftInstantiator.h @@ -48,7 +48,7 @@ class DftInstantiator { template typename std::enable_if::value, ConstantType>::type instantiate_helper( ParametricType const& function, storm::utility::parametric::Valuation const& valuation) { - return storm::utility::convertNumber(storm::utility::parametric::evaluate(function, valuation)); + return storm::utility::parametric::evaluate(function, valuation); } /*! diff --git a/src/storm-pars/derivative/SparseDerivativeInstantiationModelChecker.cpp b/src/storm-pars/derivative/SparseDerivativeInstantiationModelChecker.cpp index 5f632cba2..95e83e1d2 100644 --- a/src/storm-pars/derivative/SparseDerivativeInstantiationModelChecker.cpp +++ b/src/storm-pars/derivative/SparseDerivativeInstantiationModelChecker.cpp @@ -63,10 +63,10 @@ std::unique_ptr> Spa // Write results into the placeholders for (auto& functionResult : this->functionsUnderived) { - functionResult.second = storm::utility::convertNumber(storm::utility::parametric::evaluate(functionResult.first, valuation)); + functionResult.second = storm::utility::parametric::evaluate(functionResult.first, valuation); } for (auto& functionResult : this->functionsDerived.at(parameter)) { - functionResult.second = storm::utility::convertNumber(storm::utility::parametric::evaluate(functionResult.first, valuation)); + functionResult.second = storm::utility::parametric::evaluate(functionResult.first, valuation); } auto deltaConstrainedMatrixInstantiated = deltaConstrainedMatricesInstantiated->at(parameter); @@ -81,7 +81,7 @@ std::unique_ptr> Spa std::vector instantiatedDerivedOutputVec(derivedOutputVecs->at(parameter).size()); for (uint_fast64_t i = 0; i < derivedOutputVecs->at(parameter).size(); i++) { - instantiatedDerivedOutputVec[i] = utility::convertNumber(derivedOutputVecs->at(parameter)[i].evaluate(valuation)); + instantiatedDerivedOutputVec[i] = storm::utility::parametric::evaluate(derivedOutputVecs->at(parameter)[i], valuation); } instantiationWatch.stop(); diff --git a/src/storm-pars/transformer/ParameterLifter.cpp b/src/storm-pars/transformer/ParameterLifter.cpp index 7207f9dd8..841adaaf2 100644 --- a/src/storm-pars/transformer/ParameterLifter.cpp +++ b/src/storm-pars/transformer/ParameterLifter.cpp @@ -355,9 +355,9 @@ void ParameterLifter::FunctionValuationCollector:: ConstantType& placeholder = collectedFunctionValuationPlaceholder.second; auto concreteValuations = abstrValuation.getConcreteValuations(region); auto concreteValuationIt = concreteValuations.begin(); - placeholder = storm::utility::convertNumber(storm::utility::parametric::evaluate(function, *concreteValuationIt)); + placeholder = storm::utility::parametric::evaluate(function, *concreteValuationIt); for (++concreteValuationIt; concreteValuationIt != concreteValuations.end(); ++concreteValuationIt) { - ConstantType currentResult = storm::utility::convertNumber(storm::utility::parametric::evaluate(function, *concreteValuationIt)); + ConstantType currentResult = storm::utility::parametric::evaluate(function, *concreteValuationIt); if (storm::solver::minimize(dirForUnspecifiedParameters)) { placeholder = std::min(placeholder, currentResult); } else { diff --git a/src/storm-pars/utility/ModelInstantiator.h b/src/storm-pars/utility/ModelInstantiator.h index cc4dff024..6e080f9dc 100644 --- a/src/storm-pars/utility/ModelInstantiator.h +++ b/src/storm-pars/utility/ModelInstantiator.h @@ -125,7 +125,7 @@ class ModelInstantiator { typename std::enable_if::value>::type instantiate_helper( storm::utility::parametric::Valuation const& valuation) { for (auto& functionResult : this->functions) { - functionResult.second = storm::utility::convertNumber(storm::utility::parametric::evaluate(functionResult.first, valuation)); + functionResult.second = storm::utility::parametric::evaluate(functionResult.first, valuation); } } diff --git a/src/storm-pars/utility/parametric.cpp b/src/storm-pars/utility/parametric.cpp index 5a83efc4b..60b805a20 100644 --- a/src/storm-pars/utility/parametric.cpp +++ b/src/storm-pars/utility/parametric.cpp @@ -4,20 +4,12 @@ #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/exceptions/IllegalArgumentException.h" #include "storm/exceptions/NotImplementedException.h" -#include "storm/utility/constants.h" #include "storm/utility/macros.h" namespace storm { namespace utility { namespace parametric { -#ifdef STORM_HAVE_CARL -template<> -typename CoefficientType::type evaluate(storm::RationalFunction const& function, - Valuation const& valuation) { - return function.evaluate(valuation); -} - template<> typename storm::RationalFunction substitute(storm::RationalFunction const& function, Valuation const& valuation) { @@ -48,7 +40,6 @@ bool isMultiLinearPolynomial(storm::RationalFunction co } return true; } -#endif } // namespace parametric } // namespace utility } // namespace storm diff --git a/src/storm-pars/utility/parametric.h b/src/storm-pars/utility/parametric.h index 7bcc57aec..9e43ef6ad 100644 --- a/src/storm-pars/utility/parametric.h +++ b/src/storm-pars/utility/parametric.h @@ -1,7 +1,7 @@ -#ifndef STORM_UTILITY_PARAMETRIC_H -#define STORM_UTILITY_PARAMETRIC_H +#pragma once #include "storm/adapters/RationalFunctionForward.h" +#include "storm/utility/constants.h" #include #include @@ -26,7 +26,6 @@ struct CoefficientType { typedef void type; }; -#ifdef STORM_HAVE_CARL template<> struct VariableType { typedef storm::RationalFunctionVariable type; @@ -35,16 +34,21 @@ template<> struct CoefficientType { typedef storm::RationalFunctionCoefficient type; }; -#endif template using Valuation = std::map::type, typename CoefficientType::type>; /*! - * Evaluates the given function wrt. the given valuation + * Evaluates the given function wrt. the given valuation and returns the required type. */ -template -typename CoefficientType::type evaluate(FunctionType const& function, Valuation const& valuation); +template +ReturnType evaluate(FunctionType const& function, Valuation const& valuation) { + if constexpr (std::is_same::type>::value) { + return function.evaluate(valuation); + } else { + return storm::utility::convertNumber(function.evaluate(valuation)); + } +} /*! * Evaluates the given function wrt. the given valuation @@ -71,8 +75,5 @@ template bool isMultiLinearPolynomial(FunctionType const& function); } // namespace parametric - } // namespace utility } // namespace storm - -#endif /* STORM_UTILITY_PARAMETRIC_H */ diff --git a/src/test/storm-pars/derivative/SparseDerivativeInstantiationModelCheckerTest.cpp b/src/test/storm-pars/derivative/SparseDerivativeInstantiationModelCheckerTest.cpp index 61ee90b77..32152da13 100644 --- a/src/test/storm-pars/derivative/SparseDerivativeInstantiationModelCheckerTest.cpp +++ b/src/test/storm-pars/derivative/SparseDerivativeInstantiationModelCheckerTest.cpp @@ -2,6 +2,11 @@ #include "storm-config.h" #include "test/storm_gtest.h" +#include "storm-pars/analysis/OrderExtender.h" +#include "storm-pars/api/storm-pars.h" +#include "storm-pars/derivative/SparseDerivativeInstantiationModelChecker.h" +#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h" +#include "storm-parsers/api/storm-parsers.h" #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/api/builder.h" #include "storm/api/storm.h" @@ -17,13 +22,6 @@ #include "storm/storage/expressions/BinaryRelationExpression.h" #include "storm/storage/expressions/ExpressionManager.h" -#include "storm-parsers/api/storm-parsers.h" - -#include "storm-pars/analysis/OrderExtender.h" -#include "storm-pars/api/storm-pars.h" -#include "storm-pars/derivative/SparseDerivativeInstantiationModelChecker.h" -#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h" - namespace { class RationalGmmxxEnvironment { public: @@ -143,9 +141,7 @@ void SparseDerivativeInstantiationModelCheckerTest::testModel(std::sha for (auto const& entry : instantiation) { auto parameter = entry.first; auto derivativeWrtParameter = derivatives[parameter]; - typename TestType::ConstantType evaluatedDerivative = - storm::utility::convertNumber(derivativeWrtParameter.evaluate(instantiation)); - resultMap[parameter] = evaluatedDerivative; + resultMap[parameter] = storm::utility::parametric::evaluate(derivativeWrtParameter, instantiation); } testCases[instantiation] = resultMap; } diff --git a/src/test/storm-pars/modelchecker/SymbolicParametricDtmcPrctlModelCheckerTest.cpp b/src/test/storm-pars/modelchecker/SymbolicParametricDtmcPrctlModelCheckerTest.cpp index 33a8973ab..128cfffea 100644 --- a/src/test/storm-pars/modelchecker/SymbolicParametricDtmcPrctlModelCheckerTest.cpp +++ b/src/test/storm-pars/modelchecker/SymbolicParametricDtmcPrctlModelCheckerTest.cpp @@ -1,9 +1,11 @@ #include "storm-config.h" #include "test/storm_gtest.h" +#include "storm-pars/utility/parametric.h" #include "storm-parsers/parser/FormulaParser.h" #include "storm-parsers/parser/PrismParser.h" #include "storm/builder/DdPrismModelBuilder.h" +#include "storm/environment/solver/SolverEnvironment.h" #include "storm/logic/Formulas.h" #include "storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h" #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" @@ -15,8 +17,6 @@ #include "storm/storage/SymbolicModelDescription.h" #include "storm/utility/solver.h" -#include "storm/environment/solver/SolverEnvironment.h" - TEST(SymbolicDtmcPrctlModelCheckerTest, Die_RationalFunction_Sylvan) { storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/pdtmc/parametric_die.pm"); storm::prism::Program program = modelDescription.preprocess().asPrismProgram(); @@ -51,7 +51,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_RationalFunction_Sylvan) { storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); - EXPECT_EQ(storm::utility::convertNumber(quantitativeResult1.sum().evaluate(instantiation)), + EXPECT_EQ(storm::utility::parametric::evaluate(quantitativeResult1.sum(), instantiation), storm::utility::convertNumber(std::string("1/6"))); formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]"); @@ -61,7 +61,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_RationalFunction_Sylvan) { storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); - EXPECT_EQ(storm::utility::convertNumber(quantitativeResult2.sum().evaluate(instantiation)), + EXPECT_EQ(storm::utility::parametric::evaluate(quantitativeResult2.sum(), instantiation), storm::utility::convertNumber(std::string("1/6"))); formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]"); @@ -71,7 +71,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_RationalFunction_Sylvan) { storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); - EXPECT_EQ(storm::utility::convertNumber(quantitativeResult3.sum().evaluate(instantiation)), + EXPECT_EQ(storm::utility::parametric::evaluate(quantitativeResult3.sum(), instantiation), storm::utility::convertNumber(std::string("1/6"))); formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]"); @@ -81,6 +81,6 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_RationalFunction_Sylvan) { storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult(); - EXPECT_EQ(storm::utility::convertNumber(quantitativeResult4.sum().evaluate(instantiation)), + EXPECT_EQ(storm::utility::parametric::evaluate(quantitativeResult4.sum(), instantiation), storm::utility::convertNumber(std::string("11/3"))); }