sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

work on making jit-builder ready for exact arithmetic and parametric models 

Former-commit-id: 143a5d263f [formerly 37b5adfd08]
Former-commit-id: 219bd799c7
tempestpy_adaptions
dehnert 8 years ago
parent
7c56b43afc
commit
9f40400b56
13 changed files with 336 additions and 91 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 4
      resources/3rdparty/CMakeLists.txt
  2. 2
      src/adapters/CarlAdapter.h
  3. 4
      src/adapters/NumberAdapter.h
  4. 6
      src/builder/jit/Choice.cpp
  5. 4
      src/builder/jit/Choice.h
  6. 226
      src/builder/jit/ExplicitJitJaniModelBuilder.cpp
  7. 17
      src/builder/jit/ExplicitJitJaniModelBuilder.h
  8. 11
      src/settings/modules/JitBuilderSettings.cpp
  9. 6
      src/settings/modules/JitBuilderSettings.h
  10. 121
      src/storage/expressions/ToCppVisitor.cpp
  11. 17
      src/storage/expressions/ToCppVisitor.h
  12. 4
      src/utility/storm.h
  13. 5
      storm-config.h.in

4
resources/3rdparty/CMakeLists.txt
View File

@ -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}")
#############################################################
##

2
src/adapters/CarlAdapter.h
View File

@ -4,8 +4,6 @@
// Include config to know whether CARL is available or not.
#include "storm-config.h"
#include <boost/multiprecision/gmp.hpp>
#ifdef STORM_HAVE_CARL
#include <carl/numbers/numbers.h>

4
src/adapters/NumberAdapter.h
View File

@ -2,8 +2,6 @@
#include "storm-config.h"
#include <boost/multiprecision/gmp.hpp>
#ifdef STORM_HAVE_CARL
#include <carl/numbers/numbers.h>
@ -14,4 +12,4 @@ namespace storm {
typedef mpq_class RationalNumber;
#endif
}
#endif
#endif

6
src/builder/jit/Choice.cpp
View File

@ -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 <typename IndexType, typename ValueType>
void Choice<IndexType, ValueType>::resizeRewards(std::size_t numberOfRewards, ValueType const& fillValue) {
rewards.resize(numberOfRewards, fillValue);
void Choice<IndexType, ValueType>::resizeRewards(std::size_t numberOfRewards) {
rewards.resize(numberOfRewards, storm::utility::zero<ValueType>());
}
template <typename IndexType, typename ValueType>

4
src/builder/jit/Choice.h
View File

@ -59,9 +59,9 @@ namespace storm {
void setRewards(std::vector<ValueType>&& 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.

226
src/builder/jit/ExplicitJitJaniModelBuilder.cpp
View File

@ -4,8 +4,6 @@
#include <cstdio>
#include <chrono>
#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::shared_ptr<storm::logic::Formula const>>(), std::cout, false);
@ -347,7 +350,41 @@ namespace storm {
}
return result;
}
template <typename ValueType, typename RewardModelType>
bool ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::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<std::string> 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 <typename ValueType, typename RewardModelType>
bool ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::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<storm::RationalNumber, ValueType>::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<storm::models::sparse::Model<ValueType, storm::models::sparse::StandardRewardModel<ValueType>>> sparseModel(nullptr);
try {
sparseModel = std::shared_ptr<storm::models::sparse::Model<ValueType, storm::models::sparse::StandardRewardModel<ValueType>>>(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<storm::RationalNumber, ValueType>::value) {
list.push_back(cpptempl::data_map());
}
modelData["exact"] = cpptempl::make_data(list);
list = cpptempl::data_list();
if (std::is_same<storm::RationalFunction, ValueType>::value) {
list.push_back(cpptempl::data_map());
}
modelData["parametric"] = cpptempl::make_data(list);
list = cpptempl::data_list();
if (std::is_same<double, ValueType>::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<storm::RationalFunction, ValueType>::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<double, ValueType>::value) {
result["init"] = expressionTranslator.translate(variable.getInitExpression(), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastDouble));
} else if (std::is_same<storm::RationalNumber, ValueType>::value) {
result["init"] = expressionTranslator.translate(variable.getInitExpression(), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastRationalNumber));
} else if (std::is_same<storm::RationalFunction, ValueType>::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<IndexType, ValueType>& 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<double, ValueType>::value) {
destinationData["value"] = expressionTranslator.translate(expressionToTranslate, storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastDouble));
} else if (std::is_same<storm::RationalNumber, ValueType>::value) {
destinationData["value"] = expressionTranslator.translate(expressionToTranslate, storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastRationalNumber));
} else if (std::is_same<storm::RationalFunction, ValueType>::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<double, ValueType>::value) {
options = storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastDouble);
} else if (std::is_same<storm::RationalNumber, ValueType>::value) {
options = storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastRationalNumber);
} else if (std::is_same<storm::RationalFunction, ValueType>::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 <typename ValueType, typename RewardModelType>
void ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::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 <typename ValueType, typename RewardModelType>
std::string const& ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::getVariableName(storm::expressions::Variable const& variable) const {
@ -1470,7 +1575,7 @@ namespace storm {
std::string ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::asString(ValueTypePrime value) const {
return std::to_string(value);
}
template <typename ValueType, typename RewardModelType>
std::string ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::createSourceCodeFromSkeleton(cpptempl::data_map& modelData) {
std::string sourceTemplate = R"(
@ -1484,6 +1589,13 @@ namespace storm {
#include <unordered_map>
#include <boost/dll/alias.hpp>
{% 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<storm::RationalFunction> 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<IndexType, ValueType>& 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<std::string> error = execute(command);
if (error) {
@ -2214,10 +2362,48 @@ namespace storm {
return dynamicLibraryPath;
}
template<typename RationalFunctionType, typename TP = typename RationalFunctionType::PolyType, carl::EnableIf<carl::needs_cache<TP>> = carl::dummy>
RationalFunctionType convertVariableToPolynomial(carl::Variable const& variable, std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>> cache) {
return RationalFunctionType(typename RationalFunctionType::PolyType(typename RationalFunctionType::PolyType::PolyType(variable), cache));
}
template<typename RationalFunctionType, typename TP = typename RationalFunctionType::PolyType, carl::DisableIf<carl::needs_cache<TP>> = carl::dummy>
RationalFunctionType convertVariableToPolynomial(carl::Variable const& variable, std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>> cache) {
return RationalFunctionType(variable);
}
template<typename ValueType>
std::vector<storm::RationalFunction> getParameters(storm::jani::Model const& model, std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>> cache) {
STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "This function must not be called for this type.");
}
template<>
std::vector<storm::RationalFunction> getParameters<storm::RationalFunction>(storm::jani::Model const& model, std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>> cache) {
std::vector<storm::RationalFunction> parameters;
for (auto const& constant : model.getConstants()) {
if (!constant.isDefined() && constant.isRealConstant()) {
parameters.push_back(convertVariableToPolynomial<storm::RationalFunction>(carl::freshRealVariable(constant.getName()), cache));
}
}
return parameters;
}
template <typename ValueType, typename RewardModelType>
void ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::createBuilder(boost::filesystem::path const& dynamicLibraryPath) {
jitBuilderCreateFunction = boost::dll::import_alias<typename ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::CreateFunctionType>(dynamicLibraryPath, "create_builder");
builder = std::unique_ptr<JitModelBuilderInterface<IndexType, ValueType>>(jitBuilderCreateFunction(modelComponentsBuilder));
if (std::is_same<storm::RationalFunction, ValueType>::value) {
typedef void (InitializeParametersFunctionType)(std::vector<storm::RationalFunction> const&);
typedef boost::function<InitializeParametersFunctionType> ImportInitializeParametersFunctionType;
// Create the carl cache if we are building a parametric model.
cache = std::make_shared<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>>();
ImportInitializeParametersFunctionType initializeParametersFunction = boost::dll::import_alias<InitializeParametersFunctionType>(dynamicLibraryPath, "initialize_parameters");
std::vector<storm::RationalFunction> parameters = getParameters<ValueType>(this->model, cache);
initializeParametersFunction(parameters);
}
}
template class ExplicitJitJaniModelBuilder<double, storm::models::sparse::StandardRewardModel<double>>;

17
src/builder/jit/ExplicitJitJaniModelBuilder.h
View File

@ -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<IndexType, ValueType>* (CreateFunctionType)(ModelComponentsBuilder<IndexType, ValueType>& modelComponentsBuilder);
typedef boost::function<CreateFunctionType> ImportFunctionType;
typedef boost::function<CreateFunctionType> 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<ValueType, RewardModelType>::ImportFunctionType jitBuilderCreateFunction;
typename ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::ImportCreateFunctionType jitBuilderCreateFunction;
/// The pointer to the builder object created via the shared library.
std::unique_ptr<JitModelBuilderInterface<IndexType, ValueType>> builder;
@ -163,6 +167,7 @@ namespace storm {
std::map<storm::expressions::Variable, int_fast64_t> lowerBounds;
std::set<storm::expressions::Variable> transientVariables;
std::set<storm::expressions::Variable> nontransientVariables;
std::set<storm::expressions::Variable> realVariables;
std::unordered_map<storm::expressions::Variable, std::string> 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<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>> cache;
};
}

11
src/settings/modules/JitBuilderSettings.cpp
View File

@ -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();
}

6
src/settings/modules/JitBuilderSettings.h
View File

@ -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;
};

121
src/storage/expressions/ToCppVisitor.cpp
View File

@ -5,28 +5,20 @@
namespace storm {
namespace expressions {
ToCppTranslationOptions::ToCppTranslationOptions(std::unordered_map<storm::expressions::Variable, std::string> const& prefixes, std::unordered_map<storm::expressions::Variable, std::string> const& names, std::string const& valueTypeCast) : prefixes(prefixes), names(names), valueTypeCast(valueTypeCast) {
ToCppTranslationOptions::ToCppTranslationOptions(std::unordered_map<storm::expressions::Variable, std::string> const& prefixes, std::unordered_map<storm::expressions::Variable, std::string> const& names, ToCppTranslationMode mode) : prefixes(prefixes), names(names), mode(mode) {
// Intentionally left empty.
}
std::unordered_map<storm::expressions::Variable, std::string> const& ToCppTranslationOptions::getPrefixes() const {
return prefixes;
return prefixes.get();
}
std::unordered_map<storm::expressions::Variable, std::string> 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<ToCppTranslationOptions>(data);
conditionOptions.clearValueTypeCast();
ToCppTranslationOptions const& options = boost::any_cast<ToCppTranslationOptions>(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<ToCppTranslationOptions>(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<ToCppTranslationOptions>(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<ToCppTranslationOptions const&>(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<storm::expressions::Variable, std::string> const& prefixes, std::unordered_map<storm::expressions::Variable, std::string> 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<ToCppTranslationOptions const&>(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<double>(" << variableName << ")";
break;
case ToCppTranslationMode::CastRationalNumber:
stream << "carl::rationalize<storm::RationalNumber>(" << 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<ToCppTranslationOptions>(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<ToCppTranslationOptions const&>(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<double>(" << expression.getValue() << ")";
break;
case ToCppTranslationMode::CastRationalNumber:
stream << "carl::rationalize<storm::RationalNumber>(\"" << expression.getValue() << "\")";
break;
case ToCppTranslationMode::CastRationalFunction:
stream << "storm::RationalFunction(carl::rationalize<storm::RationalNumber>(\"" << 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<ToCppTranslationOptions const&>(data);
switch (options.getMode()) {
case ToCppTranslationMode::KeepType:
stream << expression.getValue();
break;
case ToCppTranslationMode::CastDouble:
stream << "static_cast<double>(" << expression.getValueAsDouble() << ")";
break;
case ToCppTranslationMode::CastRationalNumber:
stream << "carl::rationalize<storm::RationalNumber>(\"" << expression.getValue() << "\")";
break;
case ToCppTranslationMode::CastRationalFunction:
stream << "storm::RationalFunction(carl::rationalize<storm::RationalNumber>(\"" << expression.getValue() << "\"))";
break;
}
return boost::none;
}

17
src/storage/expressions/ToCppVisitor.h
View File

@ -10,21 +10,22 @@ namespace storm {
namespace expressions {
class Expression;
enum class ToCppTranslationMode {
KeepType, CastDouble, CastRationalNumber, CastRationalFunction
};
class ToCppTranslationOptions {
public:
ToCppTranslationOptions(std::unordered_map<storm::expressions::Variable, std::string> const& prefixes, std::unordered_map<storm::expressions::Variable, std::string> const& names, std::string const& valueTypeCast = "");
ToCppTranslationOptions(std::unordered_map<storm::expressions::Variable, std::string> const& prefixes, std::unordered_map<storm::expressions::Variable, std::string> const& names, ToCppTranslationMode mode = ToCppTranslationMode::KeepType);
std::unordered_map<storm::expressions::Variable, std::string> const& getPrefixes() const;
std::unordered_map<storm::expressions::Variable, std::string> const& getNames() const;
bool hasValueTypeCast() const;
std::string const& getValueTypeCast() const;
void clearValueTypeCast();
ToCppTranslationMode const& getMode() const;
private:
std::unordered_map<storm::expressions::Variable, std::string> const& prefixes;
std::unordered_map<storm::expressions::Variable, std::string> const& names;
std::string valueTypeCast;
std::reference_wrapper<std::unordered_map<storm::expressions::Variable, std::string> const> prefixes;
std::reference_wrapper<std::unordered_map<storm::expressions::Variable, std::string> const> names;
ToCppTranslationMode mode;
};
class ToCppVisitor : public ExpressionVisitor {

4
src/utility/storm.h
View File

@ -223,7 +223,7 @@ namespace storm {
template<typename ModelType>
std::shared_ptr<storm::models::ModelBase> preprocessModel(std::shared_ptr<storm::models::ModelBase> model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
if(model->getType() == storm::models::ModelType::MarkovAutomaton && model->isSparseModel()) {
if (model->getType() == storm::models::ModelType::MarkovAutomaton && model->isSparseModel()) {
std::shared_ptr<storm::models::sparse::MarkovAutomaton<typename ModelType::ValueType>> ma = model->template as<storm::models::sparse::MarkovAutomaton<typename ModelType::ValueType>>();
if (ma->hasOnlyTrivialNondeterminism()) {
// Markov automaton can be converted into CTMC
@ -459,7 +459,7 @@ namespace storm {
auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
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<storm::models::sparse::Dtmc<storm::RationalFunction>>(model,formulas);
regionModelChecker = std::make_shared<storm::modelchecker::region::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>>(model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(), settings);
} else if (model->isOfType(storm::models::ModelType::Mdp)){

5
storm-config.h.in
View File

@ -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

Write Preview
Loading…
Cancel
Save