From 9f40400b5627c800c0dc5f85f9f28f5981447b23 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 13 Nov 2016 10:47:47 +0100 Subject: [PATCH] work on making jit-builder ready for exact arithmetic and parametric models Former-commit-id: 143a5d263fb973bbbde354d207a5b3da2ad39eaf [formerly 37b5adfd08f1f9e91ba6187b571e9a288c24e885] Former-commit-id: 219bd799c7c6d8059241e4f7520d179163956b8d --- resources/3rdparty/CMakeLists.txt | 4 +- src/adapters/CarlAdapter.h | 2 - src/adapters/NumberAdapter.h | 4 +- src/builder/jit/Choice.cpp | 6 +- src/builder/jit/Choice.h | 4 +- .../jit/ExplicitJitJaniModelBuilder.cpp | 226 ++++++++++++++++-- src/builder/jit/ExplicitJitJaniModelBuilder.h | 17 +- src/settings/modules/JitBuilderSettings.cpp | 11 + src/settings/modules/JitBuilderSettings.h | 6 +- src/storage/expressions/ToCppVisitor.cpp | 121 ++++++---- src/storage/expressions/ToCppVisitor.h | 17 +- src/utility/storm.h | 4 +- storm-config.h.in | 5 +- 13 files changed, 336 insertions(+), 91 deletions(-) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 115fbccdd..2b73ba22f 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -232,11 +232,13 @@ if(USE_CARL) ) add_dependencies(resources carl) - include_directories(${STORM_3RDPARTY_BINARY_DIR}/carl/include) + set(carl_INCLUDE_DIR "${STORM_3RDPARTY_BINARY_DIR}/carl/include") + include_directories("${carl_INCLUDE_DIR}") list(APPEND STORM_LINK_LIBRARIES ${STORM_3RDPARTY_BINARY_DIR}/carl/lib/libcarl${DYNAMIC_EXT}) set(STORM_HAVE_CARL ON) endif() endif() +set(STORM_CARL_INCLUDE_DIR "${carl_INCLUDE_DIR}") ############################################################# ## diff --git a/src/adapters/CarlAdapter.h b/src/adapters/CarlAdapter.h index 05656aea7..05e9e7a52 100644 --- a/src/adapters/CarlAdapter.h +++ b/src/adapters/CarlAdapter.h @@ -4,8 +4,6 @@ // Include config to know whether CARL is available or not. #include "storm-config.h" -#include - #ifdef STORM_HAVE_CARL #include diff --git a/src/adapters/NumberAdapter.h b/src/adapters/NumberAdapter.h index 73d567353..f300da9c7 100644 --- a/src/adapters/NumberAdapter.h +++ b/src/adapters/NumberAdapter.h @@ -2,8 +2,6 @@ #include "storm-config.h" -#include - #ifdef STORM_HAVE_CARL #include @@ -14,4 +12,4 @@ namespace storm { typedef mpq_class RationalNumber; #endif } -#endif \ No newline at end of file +#endif diff --git a/src/builder/jit/Choice.cpp b/src/builder/jit/Choice.cpp index 4b101cb0b..12c81eb8c 100644 --- a/src/builder/jit/Choice.cpp +++ b/src/builder/jit/Choice.cpp @@ -2,6 +2,8 @@ #include "src/adapters/CarlAdapter.h" +#include "src/utility/constants.h" + namespace storm { namespace builder { namespace jit { @@ -72,8 +74,8 @@ namespace storm { } template - void Choice::resizeRewards(std::size_t numberOfRewards, ValueType const& fillValue) { - rewards.resize(numberOfRewards, fillValue); + void Choice::resizeRewards(std::size_t numberOfRewards) { + rewards.resize(numberOfRewards, storm::utility::zero()); } template diff --git a/src/builder/jit/Choice.h b/src/builder/jit/Choice.h index 3bcc5b01d..d7600d141 100644 --- a/src/builder/jit/Choice.h +++ b/src/builder/jit/Choice.h @@ -59,9 +59,9 @@ namespace storm { void setRewards(std::vector&& rewards); /*! - * Resizes the rewards to the desired size and filles newly created values with the provided value. + * Resizes the rewards to the desired size and filles newly created values the zero value of the value type. */ - void resizeRewards(std::size_t numberOfRewards, ValueType const& fillValue); + void resizeRewards(std::size_t numberOfRewards); /*! * Retrieves the number of rewards of this choice. diff --git a/src/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/builder/jit/ExplicitJitJaniModelBuilder.cpp index 353879fdb..19bf14d90 100644 --- a/src/builder/jit/ExplicitJitJaniModelBuilder.cpp +++ b/src/builder/jit/ExplicitJitJaniModelBuilder.cpp @@ -4,8 +4,6 @@ #include #include -#include "src/adapters/CarlAdapter.h" - #include "src/solver/SmtSolver.h" #include "src/storage/jani/AutomatonComposition.h" #include "src/storage/jani/ParallelComposition.h" @@ -74,6 +72,11 @@ namespace storm { } else { stormRoot = STORM_CPP_BASE_PATH; } + if (settings.isCarlIncludeDirectorySet()) { + carlIncludeDir = settings.getCarlIncludeDirectory(); + } else { + carlIncludeDir = STORM_CARL_INCLUDE_DIR; + } // Register all transient variables as transient. for (auto const& variable : this->model.getGlobalVariables().getTransientVariables()) { @@ -125,7 +128,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The input model contains undefined constants that influence the graph structure of the underlying model, which is not allowed."); } #endif - + // Comment this in to print the JANI model for debugging purposes. // this->model.makeStandardJaniCompliant(); // storm::jani::JsonExporter::toStream(this->model, std::vector>(), std::cout, false); @@ -347,7 +350,41 @@ namespace storm { } return result; } - + + template + bool ExplicitJitJaniModelBuilder::checkCarlAvailable() const { + bool result = true; + std::string problem = "Unable to compile program using Carl data structures. Is Carls's include directory '" + carlIncludeDir + "' set correctly?"; + try { + std::string program = R"( +#include "src/adapters/NumberAdapter.h" + + int main() { + return 0; + } + )"; + boost::filesystem::path temporaryFile = writeToTemporaryFile(program); + std::string temporaryFilename = boost::filesystem::absolute(temporaryFile).string(); + boost::filesystem::path outputFile = temporaryFile; + outputFile += ".out"; + std::string outputFilename = boost::filesystem::absolute(outputFile).string(); + // FIXME: get right of build_xcode + boost::optional error = execute(compiler + " " + compilerFlags + " " + temporaryFilename + " -I" + stormRoot + " -I" + stormRoot + "/build_xcode/include -I" + carlIncludeDir + " -o " + outputFilename); + + if (error) { + result = false; + STORM_LOG_ERROR(problem); + STORM_LOG_TRACE(error.get()); + } else { + boost::filesystem::remove(outputFile); + } + } catch(std::exception const& e) { + result = false; + STORM_LOG_ERROR(problem); + } + return result; + } + template bool ExplicitJitJaniModelBuilder::doctor() const { bool result = true; @@ -389,9 +426,20 @@ namespace storm { STORM_LOG_DEBUG("Checking whether Storm's headers are available."); result = checkStormAvailable(); - if (result) { + if (!result) { + return result; + } + STORM_LOG_DEBUG("Success."); + + if (std::is_same::value) { + STORM_LOG_DEBUG("Checking whether Carl's headers are available."); + result = checkCarlAvailable(); + if (!result) { + return result; + } STORM_LOG_DEBUG("Success."); } + return result; } @@ -428,6 +476,8 @@ namespace storm { std::shared_ptr>> sparseModel(nullptr); try { sparseModel = std::shared_ptr>>(builder->build()); + STORM_LOG_THROW(sparseModel, storm::exceptions::UnexpectedException, "An unexpected error occurred."); + STORM_LOG_TRACE("Successfully got model from jit-builder."); } catch (std::exception const& e) { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Model building failed. Reason: " << e.what()); } @@ -448,13 +498,33 @@ namespace storm { modelData["deterministic_model"] = asString(model.isDeterministicModel()); modelData["discrete_time_model"] = asString(model.isDiscreteTimeModel()); - // Use a list here to enable if query in skeleton program. + // Use lists here to enable if query in skeleton program even if the property is just boolean. cpptempl::data_list list; if (options.isExplorationChecksSet()) { list.push_back(cpptempl::data_map()); } modelData["exploration_checks"] = cpptempl::make_data(list); + list = cpptempl::data_list(); + if (std::is_same::value) { + list.push_back(cpptempl::data_map()); + } + modelData["exact"] = cpptempl::make_data(list); + list = cpptempl::data_list(); + if (std::is_same::value) { + list.push_back(cpptempl::data_map()); + } + modelData["parametric"] = cpptempl::make_data(list); + list = cpptempl::data_list(); + if (std::is_same::value) { + list.push_back(cpptempl::data_map()); + } + modelData["double"] = cpptempl::make_data(list); + // If we are building a possibly parametric model, we need to create the parameters. + if (std::is_same::value) { + generateParameters(modelData); + } + // Generate non-trivial model-information. generateVariables(modelData); generateInitialStates(modelData); @@ -517,8 +587,15 @@ namespace storm { cpptempl::data_map result; result["name"] = registerVariable(variable.getExpressionVariable(), variable.isTransient()); + realVariables.insert(variable.getExpressionVariable()); if (variable.hasInitExpression()) { - result["init"] = asString(variable.getInitExpression().evaluateAsDouble()); + if (std::is_same::value) { + result["init"] = expressionTranslator.translate(variable.getInitExpression(), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastDouble)); + } else if (std::is_same::value) { + result["init"] = expressionTranslator.translate(variable.getInitExpression(), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastRationalNumber)); + } else if (std::is_same::value) { + result["init"] = expressionTranslator.translate(variable.getInitExpression(), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastRationalFunction)); + } } return result; @@ -1032,7 +1109,7 @@ namespace storm { indent(vectorSource, indentLevel + 2) << "Choice& choice = behaviour.addChoice();" << std::endl; std::stringstream tmp; - indent(tmp, indentLevel + 2) << "choice.resizeRewards({$edge_destination_rewards_count}, 0);" << std::endl; + indent(tmp, indentLevel + 2) << "choice.resizeRewards({$edge_destination_rewards_count});" << std::endl; indent(tmp, indentLevel + 2) << "{% for reward in edge_rewards %}choice.addReward({$reward.index}, transientOut.{$reward.variable});" << std::endl; indent(tmp, indentLevel + 2) << "{% endfor %}" << std::endl; @@ -1247,10 +1324,13 @@ namespace storm { cpptempl::data_list levels = generateLevels(destination.getOrderedAssignments()); destinationData["name"] = asString(destinationIndex); destinationData["levels"] = cpptempl::make_data(levels); - if (rate) { - destinationData["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(rate.get() * destination.getProbability()), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, "double")); - } else { - destinationData["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(destination.getProbability()), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, "double")); + storm::expressions::Expression expressionToTranslate = rate ? shiftVariablesWrtLowerBound(rate.get() * destination.getProbability()) : shiftVariablesWrtLowerBound(destination.getProbability()); + if (std::is_same::value) { + destinationData["value"] = expressionTranslator.translate(expressionToTranslate, storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastDouble)); + } else if (std::is_same::value) { + destinationData["value"] = expressionTranslator.translate(expressionToTranslate, storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastRationalNumber)); + } else if (std::is_same::value) { + destinationData["value"] = expressionTranslator.translate(expressionToTranslate, storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastRationalFunction)); } if (destination.getOrderedAssignments().empty()) { destinationData["lowestLevel"] = "0"; @@ -1333,16 +1413,28 @@ namespace storm { cpptempl::data_map result; result["variable"] = getVariableName(assignment.getExpressionVariable()); auto lowerBoundIt = lowerBounds.find(assignment.getExpressionVariable()); + + storm::expressions::ToCppTranslationOptions options(variablePrefixes, variableToName); + if (realVariables.find(assignment.getExpressionVariable()) != realVariables.end()) { + if (std::is_same::value) { + options = storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastDouble); + } else if (std::is_same::value) { + options = storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastRationalNumber); + } else if (std::is_same::value) { + options = storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastRationalFunction); + } + } + if (lowerBoundIt != lowerBounds.end()) { if (lowerBoundIt->second < 0) { - result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()) + model.getManager().integer(lowerBoundIt->second), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)); + result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()) + model.getManager().integer(lowerBoundIt->second), options); } else if (lowerBoundIt->second == 0) { - result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)); + result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()), options); } else { - result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()) - model.getManager().integer(lowerBoundIt->second), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)); + result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()) - model.getManager().integer(lowerBoundIt->second), options); } } else { - result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)); + result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()), options); } return result; } @@ -1428,6 +1520,19 @@ namespace storm { modelData["terminalExpressions"] = cpptempl::make_data(terminalExpressions); } + + template + void ExplicitJitJaniModelBuilder::generateParameters(cpptempl::data_map& modelData) { + cpptempl::data_list parameters; + for (auto const& constant : model.getConstants()) { + if (!constant.isDefined() && constant.isRealConstant()) { + cpptempl::data_map parameter; + parameter["name"] = constant.getName(); + parameters.push_back(parameter); + } + } + modelData["parameters"] = cpptempl::make_data(parameters); + } template std::string const& ExplicitJitJaniModelBuilder::getVariableName(storm::expressions::Variable const& variable) const { @@ -1470,7 +1575,7 @@ namespace storm { std::string ExplicitJitJaniModelBuilder::asString(ValueTypePrime value) const { return std::to_string(value); } - + template std::string ExplicitJitJaniModelBuilder::createSourceCodeFromSkeleton(cpptempl::data_map& modelData) { std::string sourceTemplate = R"( @@ -1484,6 +1589,13 @@ namespace storm { #include #include +{% if exact %} +#include "src/adapters/NumberAdapter.h" +{% endif %} +{% if parametric %} +#include "src/adapters/CarlAdapter.h" +{% endif %} + #include "resources/3rdparty/sparsepp/sparsepp.h" #include "src/builder/jit/StateSet.h" @@ -1492,6 +1604,8 @@ namespace storm { #include "src/builder/jit/ModelComponentsBuilder.h" #include "src/builder/RewardModelInformation.h" +#include "src/utility/constants.h" + #include "src/exceptions/WrongFormatException.h" namespace storm { @@ -1499,7 +1613,16 @@ namespace storm { namespace jit { typedef uint32_t IndexType; + + {% if double %} typedef double ValueType; + {% endif %} + {% if exact %} + typedef storm::RationalNumber ValueType; + {% endif %} + {% if parametric %} + typedef storm::RationalFunction ValueType; + {% endif %} struct StateType { // Boolean variables. @@ -1576,8 +1699,18 @@ namespace storm { {% for variable in transient_variables.unboundedInteger %}int64_t {$variable.name}; {% endfor %} // Real variables. + {% if double %} {% for variable in transient_variables.real %}double {$variable.name}; {% endfor %} + {% endif %} + {% if exact %} + {% for variable in transient_variables.real %}storm::RationalNumber {$variable.name}; + {% endfor %} + {% endif %} + {% if parametric %} + {% for variable in transient_variables.real %}storm::RationalFunction {$variable.name}; + {% endfor %} + {% endif %} }; std::ostream& operator<<(std::ostream& out, TransientVariables const& in) { @@ -1694,6 +1827,19 @@ namespace storm { {% endif %} } + {% if parametric %} + {% for parameter in parameters %}static storm::RationalFunction {$parameter.name}; + {% endfor %} + + void initialize_parameters(std::vector const& parameters) { +#ifndef NDEBUG + std::cout << "initializing parameters" << std::endl; +#endif + {% for parameter in parameters %}{$parameter.name} = parameters[{$loop.index} - 1]; + {% endfor %} + } + {% endif %} + // Non-synchronizing edges. {% for edge in nonsynch_edges %}static bool edge_enabled_{$edge.name}(StateType const& in) { if ({$edge.guard}) { @@ -2085,7 +2231,7 @@ namespace storm { } } - bool isTerminalState(StateType const& state) const { + bool isTerminalState(StateType const& in) const { {% for expression in terminalExpressions %}if ({$expression}) { return true; } @@ -2097,7 +2243,7 @@ namespace storm { {% for edge in nonsynch_edges %}{ if ({$edge.guard}) { Choice& choice = behaviour.addChoice(!model_is_deterministic() && !model_is_discrete_time() && {$edge.markovian}); - choice.resizeRewards({$edge_destination_rewards_count}, 0); + choice.resizeRewards({$edge_destination_rewards_count}); { {% if exploration_checks %}VariableWrites variableWrites; {% endif %} @@ -2188,6 +2334,7 @@ namespace storm { }; BOOST_DLL_ALIAS(storm::builder::jit::JitBuilder::create, create_builder) + BOOST_DLL_ALIAS(storm::builder::jit::initialize_parameters, initialize_parameters) } } } @@ -2203,7 +2350,8 @@ namespace storm { dynamicLibraryPath += DYLIB_EXTENSION; std::string dynamicLibraryFilename = boost::filesystem::absolute(dynamicLibraryPath).string(); - std::string command = compiler + " " + sourceFilename + " " + compilerFlags + " -I" + stormRoot + " -I" + stormRoot + "/build_xcode/include -I" + boostIncludeDirectory + " -o " + dynamicLibraryFilename; + // FIXME: get right of build_xcode/include + std::string command = compiler + " " + sourceFilename + " " + compilerFlags + " -I" + stormRoot + " -I" + stormRoot + "/build_xcode/include -I" + boostIncludeDirectory + " -I" + carlIncludeDir + " -o " + dynamicLibraryFilename; boost::optional error = execute(command); if (error) { @@ -2214,10 +2362,48 @@ namespace storm { return dynamicLibraryPath; } + template> = carl::dummy> + RationalFunctionType convertVariableToPolynomial(carl::Variable const& variable, std::shared_ptr>> cache) { + return RationalFunctionType(typename RationalFunctionType::PolyType(typename RationalFunctionType::PolyType::PolyType(variable), cache)); + } + + template> = carl::dummy> + RationalFunctionType convertVariableToPolynomial(carl::Variable const& variable, std::shared_ptr>> cache) { + return RationalFunctionType(variable); + } + + template + std::vector getParameters(storm::jani::Model const& model, std::shared_ptr>> cache) { + STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "This function must not be called for this type."); + } + + template<> + std::vector getParameters(storm::jani::Model const& model, std::shared_ptr>> cache) { + std::vector parameters; + for (auto const& constant : model.getConstants()) { + if (!constant.isDefined() && constant.isRealConstant()) { + parameters.push_back(convertVariableToPolynomial(carl::freshRealVariable(constant.getName()), cache)); + } + } + return parameters; + } + template void ExplicitJitJaniModelBuilder::createBuilder(boost::filesystem::path const& dynamicLibraryPath) { jitBuilderCreateFunction = boost::dll::import_alias::CreateFunctionType>(dynamicLibraryPath, "create_builder"); builder = std::unique_ptr>(jitBuilderCreateFunction(modelComponentsBuilder)); + + if (std::is_same::value) { + typedef void (InitializeParametersFunctionType)(std::vector const&); + typedef boost::function ImportInitializeParametersFunctionType; + + // Create the carl cache if we are building a parametric model. + cache = std::make_shared>>(); + + ImportInitializeParametersFunctionType initializeParametersFunction = boost::dll::import_alias(dynamicLibraryPath, "initialize_parameters"); + std::vector parameters = getParameters(this->model, cache); + initializeParametersFunction(parameters); + } } template class ExplicitJitJaniModelBuilder>; diff --git a/src/builder/jit/ExplicitJitJaniModelBuilder.h b/src/builder/jit/ExplicitJitJaniModelBuilder.h index 2a652befe..e8b8a5ee5 100644 --- a/src/builder/jit/ExplicitJitJaniModelBuilder.h +++ b/src/builder/jit/ExplicitJitJaniModelBuilder.h @@ -8,6 +8,8 @@ #include "cpptempl.h" +#include "src/adapters/CarlAdapter.h" + #include "src/storage/jani/Model.h" #include "src/storage/jani/ParallelComposition.h" #include "src/storage/expressions/ToCppVisitor.h" @@ -36,7 +38,7 @@ namespace storm { class ExplicitJitJaniModelBuilder { public: typedef JitModelBuilderInterface* (CreateFunctionType)(ModelComponentsBuilder& modelComponentsBuilder); - typedef boost::function ImportFunctionType; + typedef boost::function ImportCreateFunctionType; /*! * Creates a model builder for the given model. The provided options are used to determine which part of @@ -63,6 +65,7 @@ namespace storm { bool checkBoostAvailable() const; bool checkBoostDllAvailable() const; bool checkStormAvailable() const; + bool checkCarlAvailable() const; /*! * Executes the given command. If the command fails with a non-zero error code, the error stream content @@ -92,7 +95,8 @@ namespace storm { void generateLocations(cpptempl::data_map& modelData); void generateLabels(cpptempl::data_map& modelData); void generateTerminalExpressions(cpptempl::data_map& modelData); - + void generateParameters(cpptempl::data_map& modelData); + // Functions related to the generation of edge data. void generateEdges(cpptempl::data_map& modelData); cpptempl::data_map generateSynchronizationVector(cpptempl::data_map& modelData, storm::jani::ParallelComposition const& parallelComposition, storm::jani::SynchronizationVector const& synchronizationVector, uint64_t synchronizationVectorIndex); @@ -149,7 +153,7 @@ namespace storm { /// The function that was loaded from the shared library. We have to keep this function around, because /// otherwise the shared library gets unloaded. - typename ExplicitJitJaniModelBuilder::ImportFunctionType jitBuilderCreateFunction; + typename ExplicitJitJaniModelBuilder::ImportCreateFunctionType jitBuilderCreateFunction; /// The pointer to the builder object created via the shared library. std::unique_ptr> builder; @@ -163,6 +167,7 @@ namespace storm { std::map lowerBounds; std::set transientVariables; std::set nontransientVariables; + std::set realVariables; std::unordered_map variablePrefixes; /// The compiler binary. @@ -176,6 +181,12 @@ namespace storm { /// The root directory of storm. std::string stormRoot; + + /// The include directory of carl. + std::string carlIncludeDir; + + /// A cache that is used by carl. + std::shared_ptr>> cache; }; } diff --git a/src/settings/modules/JitBuilderSettings.cpp b/src/settings/modules/JitBuilderSettings.cpp index fa44ac4b3..4aa53d925 100644 --- a/src/settings/modules/JitBuilderSettings.cpp +++ b/src/settings/modules/JitBuilderSettings.cpp @@ -18,6 +18,7 @@ namespace storm { const std::string JitBuilderSettings::compilerOptionName = "compiler"; const std::string JitBuilderSettings::stormRootOptionName = "storm"; const std::string JitBuilderSettings::boostIncludeDirectoryOptionName = "boost"; + const std::string JitBuilderSettings::carlIncludeDirectoryOptionName = "carl"; const std::string JitBuilderSettings::compilerFlagsOptionName = "cxxflags"; JitBuilderSettings::JitBuilderSettings() : ModuleSettings(moduleName) { @@ -28,6 +29,8 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("dir", "The directory that contains the src/ subtree of Storm.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, boostIncludeDirectoryOptionName, false, "The include directory of boost.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("dir", "The directory containing the boost headers version >= 1.61.").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, carlIncludeDirectoryOptionName, false, "The include directory of carl.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("dir", "The directory containing the carl headers.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, compilerFlagsOptionName, false, "The flags passed to the compiler.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("flags", "The compiler flags.").build()).build()); } @@ -56,6 +59,14 @@ namespace storm { return this->getOption(boostIncludeDirectoryOptionName).getArgumentByName("dir").getValueAsString(); } + bool JitBuilderSettings::isCarlIncludeDirectorySet() const { + return this->getOption(carlIncludeDirectoryOptionName).getHasOptionBeenSet(); + } + + std::string JitBuilderSettings::getCarlIncludeDirectory() const { + return this->getOption(carlIncludeDirectoryOptionName).getArgumentByName("dir").getValueAsString(); + } + bool JitBuilderSettings::isDoctorSet() const { return this->getOption(doctorOptionName).getHasOptionBeenSet(); } diff --git a/src/settings/modules/JitBuilderSettings.h b/src/settings/modules/JitBuilderSettings.h index abb916170..948620900 100644 --- a/src/settings/modules/JitBuilderSettings.h +++ b/src/settings/modules/JitBuilderSettings.h @@ -23,7 +23,10 @@ namespace storm { bool isBoostIncludeDirectorySet() const; std::string getBoostIncludeDirectory() const; - + + bool isCarlIncludeDirectorySet() const; + std::string getCarlIncludeDirectory() const; + bool isCompilerFlagsSet() const; std::string getCompilerFlags() const; @@ -36,6 +39,7 @@ namespace storm { static const std::string compilerOptionName; static const std::string stormRootOptionName; static const std::string boostIncludeDirectoryOptionName; + static const std::string carlIncludeDirectoryOptionName; static const std::string compilerFlagsOptionName; static const std::string doctorOptionName; }; diff --git a/src/storage/expressions/ToCppVisitor.cpp b/src/storage/expressions/ToCppVisitor.cpp index 108d95fe8..f705e7b6b 100644 --- a/src/storage/expressions/ToCppVisitor.cpp +++ b/src/storage/expressions/ToCppVisitor.cpp @@ -5,28 +5,20 @@ namespace storm { namespace expressions { - ToCppTranslationOptions::ToCppTranslationOptions(std::unordered_map const& prefixes, std::unordered_map const& names, std::string const& valueTypeCast) : prefixes(prefixes), names(names), valueTypeCast(valueTypeCast) { + ToCppTranslationOptions::ToCppTranslationOptions(std::unordered_map const& prefixes, std::unordered_map const& names, ToCppTranslationMode mode) : prefixes(prefixes), names(names), mode(mode) { // Intentionally left empty. } std::unordered_map const& ToCppTranslationOptions::getPrefixes() const { - return prefixes; + return prefixes.get(); } std::unordered_map const& ToCppTranslationOptions::getNames() const { - return names; + return names.get(); } - bool ToCppTranslationOptions::hasValueTypeCast() const { - return !valueTypeCast.empty(); - } - - std::string const& ToCppTranslationOptions::getValueTypeCast() const { - return valueTypeCast; - } - - void ToCppTranslationOptions::clearValueTypeCast() { - valueTypeCast = ""; + ToCppTranslationMode const& ToCppTranslationOptions::getMode() const { + return mode; } std::string ToCppVisitor::translate(storm::expressions::Expression const& expression, ToCppTranslationOptions const& options) { @@ -37,8 +29,10 @@ namespace storm { } boost::any ToCppVisitor::visit(IfThenElseExpression const& expression, boost::any const& data) { - ToCppTranslationOptions conditionOptions = boost::any_cast(data); - conditionOptions.clearValueTypeCast(); + ToCppTranslationOptions const& options = boost::any_cast(data); + + // Clear the type cast for the condition. + ToCppTranslationOptions conditionOptions(options.getPrefixes(), options.getNames()); stream << "("; expression.getCondition()->accept(*this, conditionOptions); stream << " ? "; @@ -51,7 +45,6 @@ namespace storm { boost::any ToCppVisitor::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) { ToCppTranslationOptions newOptions = boost::any_cast(data); - newOptions.clearValueTypeCast(); switch (expression.getOperatorType()) { case BinaryBooleanFunctionExpression::OperatorType::And: @@ -150,7 +143,6 @@ namespace storm { boost::any ToCppVisitor::visit(BinaryRelationExpression const& expression, boost::any const& data) { ToCppTranslationOptions newOptions = boost::any_cast(data); - newOptions.clearValueTypeCast(); switch (expression.getRelationType()) { case BinaryRelationExpression::RelationType::Equal: @@ -198,39 +190,55 @@ namespace storm { } return boost::none; } - - boost::any ToCppVisitor::visit(VariableExpression const& expression, boost::any const& data) { - ToCppTranslationOptions const& options = boost::any_cast(data); - if (options.hasValueTypeCast()) { - stream << "static_cast<" << options.getValueTypeCast() << ">("; - } - - auto prefixIt = options.getPrefixes().find(expression.getVariable()); - if (prefixIt != options.getPrefixes().end()) { - auto nameIt = options.getNames().find(expression.getVariable()); - if (nameIt != options.getNames().end()) { - stream << prefixIt->second << nameIt->second; + + std::string getVariableName(storm::expressions::Variable const& variable, std::unordered_map const& prefixes, std::unordered_map const& names) { + auto prefixIt = prefixes.find(variable); + if (prefixIt != prefixes.end()) { + auto nameIt = names.find(variable); + if (nameIt != names.end()) { + return prefixIt->second + nameIt->second; } else { - stream << prefixIt->second << expression.getVariableName(); + return prefixIt->second + variable.getName(); } } else { - auto nameIt = options.getNames().find(expression.getVariable()); - if (nameIt != options.getNames().end()) { - stream << nameIt->second; + auto nameIt = names.find(variable); + if (nameIt != names.end()) { + return nameIt->second; } else { - stream << expression.getVariableName(); + return variable.getName(); } } + } + + boost::any ToCppVisitor::visit(VariableExpression const& expression, boost::any const& data) { + ToCppTranslationOptions const& options = boost::any_cast(data); + storm::expressions::Variable const& variable = expression.getVariable(); + std::string variableName = getVariableName(variable, options.getPrefixes(), options.getNames()); - if (options.hasValueTypeCast()) { - stream << ")"; + if (variable.hasBooleanType()) { + stream << variableName; + } else { + switch (options.getMode()) { + case ToCppTranslationMode::KeepType: + stream << variableName; + break; + case ToCppTranslationMode::CastDouble: + stream << "static_cast(" << variableName << ")"; + break; + case ToCppTranslationMode::CastRationalNumber: + stream << "carl::rationalize(" << variableName << ")"; + break; + case ToCppTranslationMode::CastRationalFunction: + // Here, we rely on the variable name mapping to a rational function representing the variable being available. + stream << variableName; + break; + } } return boost::none; } - + boost::any ToCppVisitor::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) { ToCppTranslationOptions newOptions = boost::any_cast(data); - newOptions.clearValueTypeCast(); switch (expression.getOperatorType()) { case UnaryBooleanFunctionExpression::OperatorType::Not: @@ -270,18 +278,39 @@ namespace storm { boost::any ToCppVisitor::visit(IntegerLiteralExpression const& expression, boost::any const& data) { ToCppTranslationOptions const& options = boost::any_cast(data); - if (options.hasValueTypeCast()) { - stream << "static_cast<" << options.getValueTypeCast() << ">("; - } - stream << expression.getValue(); - if (options.hasValueTypeCast()) { - stream << ")"; + switch (options.getMode()) { + case ToCppTranslationMode::KeepType: + stream << expression.getValue(); + break; + case ToCppTranslationMode::CastDouble: + stream << "static_cast(" << expression.getValue() << ")"; + break; + case ToCppTranslationMode::CastRationalNumber: + stream << "carl::rationalize(\"" << expression.getValue() << "\")"; + break; + case ToCppTranslationMode::CastRationalFunction: + stream << "storm::RationalFunction(carl::rationalize(\"" << expression.getValue() << "\"))"; + break; } return boost::none; } - + boost::any ToCppVisitor::visit(RationalLiteralExpression const& expression, boost::any const& data) { - stream << expression.getValueAsDouble(); + ToCppTranslationOptions const& options = boost::any_cast(data); + switch (options.getMode()) { + case ToCppTranslationMode::KeepType: + stream << expression.getValue(); + break; + case ToCppTranslationMode::CastDouble: + stream << "static_cast(" << expression.getValueAsDouble() << ")"; + break; + case ToCppTranslationMode::CastRationalNumber: + stream << "carl::rationalize(\"" << expression.getValue() << "\")"; + break; + case ToCppTranslationMode::CastRationalFunction: + stream << "storm::RationalFunction(carl::rationalize(\"" << expression.getValue() << "\"))"; + break; + } return boost::none; } diff --git a/src/storage/expressions/ToCppVisitor.h b/src/storage/expressions/ToCppVisitor.h index a94af32de..3eb1a3120 100644 --- a/src/storage/expressions/ToCppVisitor.h +++ b/src/storage/expressions/ToCppVisitor.h @@ -10,21 +10,22 @@ namespace storm { namespace expressions { class Expression; + enum class ToCppTranslationMode { + KeepType, CastDouble, CastRationalNumber, CastRationalFunction + }; + class ToCppTranslationOptions { public: - ToCppTranslationOptions(std::unordered_map const& prefixes, std::unordered_map const& names, std::string const& valueTypeCast = ""); + ToCppTranslationOptions(std::unordered_map const& prefixes, std::unordered_map const& names, ToCppTranslationMode mode = ToCppTranslationMode::KeepType); std::unordered_map const& getPrefixes() const; std::unordered_map const& getNames() const; - - bool hasValueTypeCast() const; - std::string const& getValueTypeCast() const; - void clearValueTypeCast(); + ToCppTranslationMode const& getMode() const; private: - std::unordered_map const& prefixes; - std::unordered_map const& names; - std::string valueTypeCast; + std::reference_wrapper const> prefixes; + std::reference_wrapper const> names; + ToCppTranslationMode mode; }; class ToCppVisitor : public ExpressionVisitor { diff --git a/src/utility/storm.h b/src/utility/storm.h index 06089b763..7d8ac5526 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -223,7 +223,7 @@ namespace storm { template std::shared_ptr preprocessModel(std::shared_ptr model, std::vector> const& formulas) { - if(model->getType() == storm::models::ModelType::MarkovAutomaton && model->isSparseModel()) { + if (model->getType() == storm::models::ModelType::MarkovAutomaton && model->isSparseModel()) { std::shared_ptr> ma = model->template as>(); if (ma->hasOnlyTrivialNondeterminism()) { // Markov automaton can be converted into CTMC @@ -459,7 +459,7 @@ namespace storm { auto const& regionSettings = storm::settings::getModule(); storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode()); // Preprocessing and ModelChecker - if(model->isOfType(storm::models::ModelType::Dtmc)){ + if (model->isOfType(storm::models::ModelType::Dtmc)){ preprocessModel>(model,formulas); regionModelChecker = std::make_shared, double>>(model->as>(), settings); } else if (model->isOfType(storm::models::ModelType::Mdp)){ diff --git a/storm-config.h.in b/storm-config.h.in index fa69055be..a3887b691 100644 --- a/storm-config.h.in +++ b/storm-config.h.in @@ -14,9 +14,12 @@ // The path used in the functional and performance tests to load the supplied example files #define STORM_CPP_TESTS_BASE_PATH "@STORM_CPP_TESTS_BASE_PATH@" -// The path to boost used during compilation. +// Boost include directory used during compilation. #define STORM_BOOST_INCLUDE_DIR "@STORM_BOOST_INCLUDE_DIR@" +// Carl include directory used during compilation. +#define STORM_CARL_INCLUDE_DIR "@STORM_CARL_INCLUDE_DIR@" + // Whether Gurobi is available and to be used (define/undef) #cmakedefine STORM_HAVE_GUROBI