diff --git a/CMakeLists.txt b/CMakeLists.txt index b6c56e03c..c0d958476 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -14,7 +14,8 @@ set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${PROJECT_SOURCE_DIR}/resources/cmak include(ExternalProject) include(RegisterSourceGroup) include(imported) - +include(CheckCXXSourceCompiles) +include(CheckCSourceCompiles) ############################################################# ## @@ -292,6 +293,31 @@ else() set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -fomit-frame-pointer") endif() +# Test compiler by compiling small program. +CHECK_C_SOURCE_COMPILES(" + #include + int main() { + const char* text = \"A Storm is coming.\"; + return 0; + }" + COMPILER_C_WORKS +) +CHECK_CXX_SOURCE_COMPILES(" + #include + int main() { + const std::string text = \"A Storm is coming.\"; + return 0; + }" + COMPILER_CXX_WORKS +) +if ((NOT COMPILER_CXX_WORKS) OR (NOT COMPILER_C_WORKS)) + if (MACOSX) + message(FATAL_ERROR "The C/C++ compiler is not configured correctly.\nTry running 'xcode-select --install'.") + else() + message(FATAL_ERROR "The C/C++ compiler is not configured correctly.") + endif() +endif() + ############################################################# ## ## RPATH settings diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index d91d84479..35a8a0196 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -27,6 +27,7 @@ #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/ResourceSettings.h" #include "storm/settings/modules/JitBuilderSettings.h" +#include "storm/settings/modules/BuildSettings.h" #include "storm/settings/modules/DebugSettings.h" #include "storm/settings/modules/IOSettings.h" #include "storm/settings/modules/CoreSettings.h" @@ -50,7 +51,7 @@ namespace storm { void parseSymbolicModelDescription(storm::settings::modules::IOSettings const& ioSettings, SymbolicInput& input) { if (ioSettings.isPrismOrJaniInputSet()) { if (ioSettings.isPrismInputSet()) { - input.model = storm::api::parseProgram(ioSettings.getPrismInputFilename()); + input.model = storm::api::parseProgram(ioSettings.getPrismInputFilename(), storm::settings::getModule().isPrismCompatibilityEnabled()); } else { auto janiInput = storm::api::parseJaniModel(ioSettings.getJaniInputFilename()); input.model = janiInput.first; @@ -95,6 +96,7 @@ namespace storm { SymbolicInput preprocessSymbolicInput(SymbolicInput const& input) { auto ioSettings = storm::settings::getModule(); + auto buildSettings = storm::settings::getModule(); auto coreSettings = storm::settings::getModule(); SymbolicInput output = input; @@ -113,7 +115,7 @@ namespace storm { // Check whether conversion for PRISM to JANI is requested or necessary. if (input.model && input.model.get().isPrismProgram()) { bool transformToJani = ioSettings.isPrismToJaniSet(); - bool transformToJaniForJit = coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse && ioSettings.isJitSet(); + bool transformToJaniForJit = coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse && buildSettings.isJitSet(); STORM_LOG_WARN_COND(transformToJani || !transformToJaniForJit, "The JIT-based model builder is only available for JANI models, automatically converting the PRISM input model."); transformToJani |= transformToJaniForJit; @@ -171,22 +173,22 @@ namespace storm { template std::shared_ptr buildModelDd(SymbolicInput const& input) { - return storm::api::buildSymbolicModel(input.model.get(), createFormulasToRespect(input.properties), storm::settings::getModule().isBuildFullModelSet()); + return storm::api::buildSymbolicModel(input.model.get(), createFormulasToRespect(input.properties), storm::settings::getModule().isBuildFullModelSet()); } template - std::shared_ptr buildModelSparse(SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) { + std::shared_ptr buildModelSparse(SymbolicInput const& input, storm::settings::modules::BuildSettings const& buildSettings) { auto counterexampleGeneratorSettings = storm::settings::getModule(); storm::builder::BuilderOptions options(createFormulasToRespect(input.properties)); - options.setBuildChoiceLabels(ioSettings.isBuildChoiceLabelsSet()); - options.setBuildStateValuations(ioSettings.isBuildStateValuationsSet()); + options.setBuildChoiceLabels(buildSettings.isBuildChoiceLabelsSet()); + options.setBuildStateValuations(buildSettings.isBuildStateValuationsSet()); options.setBuildChoiceOrigins(counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet()); - options.setBuildAllLabels(ioSettings.isBuildFullModelSet()); - options.setBuildAllRewardModels(ioSettings.isBuildFullModelSet()); - if (ioSettings.isBuildFullModelSet()) { + options.setBuildAllLabels(buildSettings.isBuildFullModelSet()); + options.setBuildAllRewardModels(buildSettings.isBuildFullModelSet()); + if (buildSettings.isBuildFullModelSet()) { options.clearTerminalStates(); } - return storm::api::buildSparseModel(input.model.get(), options, ioSettings.isJitSet(), storm::settings::getModule().isDoctorSet()); + return storm::api::buildSparseModel(input.model.get(), options, buildSettings.isJitSet(), storm::settings::getModule().isDoctorSet()); } template @@ -206,13 +208,14 @@ namespace storm { template std::shared_ptr buildModel(storm::settings::modules::CoreSettings::Engine const& engine, SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) { storm::utility::Stopwatch modelBuildingWatch(true); + auto buildSettings = storm::settings::getModule(); std::shared_ptr result; if (input.model) { if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid) { result = buildModelDd(input); } else if (engine == storm::settings::modules::CoreSettings::Engine::Sparse) { - result = buildModelSparse(input, ioSettings); + result = buildModelSparse(input, buildSettings); } } else if (ioSettings.isExplicitSet() || ioSettings.isExplicitDRNSet() || ioSettings.isExplicitIMCASet()) { STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Can only use sparse engine with explicit input."); @@ -254,18 +257,17 @@ namespace storm { std::pair>, bool> preprocessSparseModel(std::shared_ptr> const& model, SymbolicInput const& input) { auto generalSettings = storm::settings::getModule(); auto bisimulationSettings = storm::settings::getModule(); - auto ioSettings = storm::settings::getModule(); std::pair>, bool> result = std::make_pair(model, false); if (result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) { - result.first = preprocessSparseMarkovAutomaton(result.first->template as>()); - result.second = true; + result.first = preprocessSparseMarkovAutomaton(result.first->template as>()); + result.second = true; } if (generalSettings.isBisimulationSet()) { - result.first = preprocessSparseModelBisimulation(result.first, input, bisimulationSettings); - result.second = true; + result.first = preprocessSparseModelBisimulation(result.first, input, bisimulationSettings); + result.second = true; } return result; @@ -597,8 +599,9 @@ namespace storm { template std::shared_ptr buildPreprocessExportModelWithValueTypeAndDdlib(SymbolicInput const& input, storm::settings::modules::CoreSettings::Engine engine) { auto ioSettings = storm::settings::getModule(); + auto buildSettings = storm::settings::getModule(); std::shared_ptr model; - if (!ioSettings.isNoBuildModelSet()) { + if (!buildSettings.isNoBuildModelSet()) { model = buildModel(engine, input, ioSettings); } diff --git a/src/storm-dft/settings/DftSettings.cpp b/src/storm-dft/settings/DftSettings.cpp index ce48c6fd9..b80afa2ce 100644 --- a/src/storm-dft/settings/DftSettings.cpp +++ b/src/storm-dft/settings/DftSettings.cpp @@ -16,8 +16,8 @@ #include "storm/settings/modules/BisimulationSettings.h" #include "storm/settings/modules/ResourceSettings.h" #include "storm/settings/modules/JaniExportSettings.h" -#include "storm/settings/modules/GSPNSettings.h" -#include "storm/settings/modules/GSPNExportSettings.h" +#include "storm-gspn/settings/modules/GSPNSettings.h" +#include "storm-gspn/settings/modules/GSPNExportSettings.h" namespace storm { diff --git a/src/storm-gspn-cli/storm-gspn.cpp b/src/storm-gspn-cli/storm-gspn.cpp index fc493391a..d6a493981 100644 --- a/src/storm-gspn-cli/storm-gspn.cpp +++ b/src/storm-gspn-cli/storm-gspn.cpp @@ -28,8 +28,8 @@ #include "storm/exceptions/FileIoException.h" #include "storm/settings/modules/IOSettings.h" -#include "storm/settings/modules/GSPNSettings.h" -#include "storm/settings/modules/GSPNExportSettings.h" +#include "storm-gspn/settings/modules/GSPNSettings.h" +#include "storm-gspn/settings/modules/GSPNExportSettings.h" #include "storm/settings/modules/CoreSettings.h" #include "storm/settings/modules/DebugSettings.h" #include "storm/settings/modules/JaniExportSettings.h" diff --git a/src/storm/settings/modules/GSPNExportSettings.cpp b/src/storm-gspn/settings/modules/GSPNExportSettings.cpp similarity index 97% rename from src/storm/settings/modules/GSPNExportSettings.cpp rename to src/storm-gspn/settings/modules/GSPNExportSettings.cpp index 8a5c315dc..a3c46f250 100644 --- a/src/storm/settings/modules/GSPNExportSettings.cpp +++ b/src/storm-gspn/settings/modules/GSPNExportSettings.cpp @@ -1,5 +1,5 @@ -#include "GSPNExportSettings.h" -#include "JaniExportSettings.h" +#include "storm-gspn/settings/modules/GSPNExportSettings.h" +#include "storm/settings/modules/JaniExportSettings.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/SettingMemento.h" diff --git a/src/storm/settings/modules/GSPNExportSettings.h b/src/storm-gspn/settings/modules/GSPNExportSettings.h similarity index 100% rename from src/storm/settings/modules/GSPNExportSettings.h rename to src/storm-gspn/settings/modules/GSPNExportSettings.h diff --git a/src/storm/settings/modules/GSPNSettings.cpp b/src/storm-gspn/settings/modules/GSPNSettings.cpp similarity index 98% rename from src/storm/settings/modules/GSPNSettings.cpp rename to src/storm-gspn/settings/modules/GSPNSettings.cpp index 9184f9137..2a0588b3d 100644 --- a/src/storm/settings/modules/GSPNSettings.cpp +++ b/src/storm-gspn/settings/modules/GSPNSettings.cpp @@ -1,4 +1,4 @@ -#include "GSPNSettings.h" +#include "storm-gspn/settings/modules/GSPNSettings.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/SettingMemento.h" diff --git a/src/storm/settings/modules/GSPNSettings.h b/src/storm-gspn/settings/modules/GSPNSettings.h similarity index 100% rename from src/storm/settings/modules/GSPNSettings.h rename to src/storm-gspn/settings/modules/GSPNSettings.h diff --git a/src/storm-gspn/storm-gspn.h b/src/storm-gspn/storm-gspn.h index d043ce53d..e0d6dd3a6 100644 --- a/src/storm-gspn/storm-gspn.h +++ b/src/storm-gspn/storm-gspn.h @@ -6,7 +6,7 @@ #include "storm-gspn/storage/gspn/GSPN.h" #include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/GSPNExportSettings.h" +#include "storm-gspn/settings/modules/GSPNExportSettings.h" #include "storm/utility/file.h" diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 907688ef4..8a8c9fa6a 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -29,34 +29,6 @@ namespace storm { typedef typename storm::cli::SymbolicInput SymbolicInput; - template - std::shared_ptr buildModelSparse(SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) { - return storm::api::buildSparseModel(input.model.get(), storm::api::extractFormulasFromProperties(input.properties), ioSettings.isBuildChoiceLabelsSet()); - } - - template - std::shared_ptr buildModel(storm::settings::modules::CoreSettings::Engine const& engine, SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) { - storm::utility::Stopwatch modelBuildingWatch(true); - - std::shared_ptr result; - if (input.model) { - if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid) { - result = storm::cli::buildModelDd(input); - } else if (engine == storm::settings::modules::CoreSettings::Engine::Sparse) { - result = storm::pars::buildModelSparse(input, ioSettings); - } - } else if (ioSettings.isExplicitSet() || ioSettings.isExplicitDRNSet()) { - STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Can only use sparse engine with explicit input."); - result = storm::cli::buildModelExplicit(ioSettings); - } - - modelBuildingWatch.stop(); - if (result) { - STORM_PRINT_AND_LOG("Time for model construction: " << modelBuildingWatch << "." << std::endl << std::endl); - } - - return result; - } template @@ -271,14 +243,16 @@ namespace storm { void processInputWithValueTypeAndDdlib(SymbolicInput& input) { auto coreSettings = storm::settings::getModule(); auto ioSettings = storm::settings::getModule(); + + auto buildSettings = storm::settings::getModule(); auto parSettings = storm::settings::getModule(); auto engine = coreSettings.getEngine(); STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse || engine == storm::settings::modules::CoreSettings::Engine::Hybrid || engine == storm::settings::modules::CoreSettings::Engine::Dd, storm::exceptions::InvalidSettingsException, "The selected engine is not supported for parametric models."); std::shared_ptr model; - if (!ioSettings.isNoBuildModelSet()) { - model = storm::pars::buildModel(engine, input, ioSettings); + if (!buildSettings.isNoBuildModelSet()) { + model = storm::cli::buildModel(engine, input, ioSettings); } if (model) { diff --git a/src/storm-pars/settings/ParsSettings.cpp b/src/storm-pars/settings/ParsSettings.cpp index 53907dc1c..e36793b04 100644 --- a/src/storm-pars/settings/ParsSettings.cpp +++ b/src/storm-pars/settings/ParsSettings.cpp @@ -1,3 +1,4 @@ +#include #include "storm-pars/settings/ParsSettings.h" #include "storm-pars/settings/modules/ParametricSettings.h" @@ -7,6 +8,7 @@ #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/modules/CoreSettings.h" #include "storm/settings/modules/IOSettings.h" +#include "storm/settings/modules/BuildSettings.h" #include "storm/settings/modules/DebugSettings.h" #include "storm/settings/modules/SylvanSettings.h" #include "storm/settings/modules/EigenEquationSolverSettings.h" @@ -33,7 +35,10 @@ namespace storm { storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); - + storm::settings::addModule(); + storm::settings::addModule(); + + storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); diff --git a/src/storm-pgcl-cli/storm-pgcl.cpp b/src/storm-pgcl-cli/storm-pgcl.cpp index ce579938f..bfbb6cad4 100644 --- a/src/storm-pgcl-cli/storm-pgcl.cpp +++ b/src/storm-pgcl-cli/storm-pgcl.cpp @@ -15,7 +15,7 @@ #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/modules/ResourceSettings.h" -#include "storm/settings/modules/PGCLSettings.h" +#include "storm-pgcl/settings/modules/PGCLSettings.h" #include "storm/settings/modules/CoreSettings.h" #include "storm/settings/modules/DebugSettings.h" #include "storm/settings/modules/JaniExportSettings.h" diff --git a/src/storm/settings/modules/PGCLSettings.cpp b/src/storm-pgcl/settings/modules/PGCLSettings.cpp similarity index 98% rename from src/storm/settings/modules/PGCLSettings.cpp rename to src/storm-pgcl/settings/modules/PGCLSettings.cpp index 5035f3632..a70b87f6f 100644 --- a/src/storm/settings/modules/PGCLSettings.cpp +++ b/src/storm-pgcl/settings/modules/PGCLSettings.cpp @@ -1,4 +1,4 @@ -#include "storm/settings/modules/PGCLSettings.h" +#include "PGCLSettings.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/SettingMemento.h" diff --git a/src/storm/settings/modules/PGCLSettings.h b/src/storm-pgcl/settings/modules/PGCLSettings.h similarity index 100% rename from src/storm/settings/modules/PGCLSettings.h rename to src/storm-pgcl/settings/modules/PGCLSettings.h diff --git a/src/storm/adapters/Z3ExpressionAdapter.cpp b/src/storm/adapters/Z3ExpressionAdapter.cpp index d715f4599..e55f5fe3c 100644 --- a/src/storm/adapters/Z3ExpressionAdapter.cpp +++ b/src/storm/adapters/Z3ExpressionAdapter.cpp @@ -237,7 +237,7 @@ namespace storm { } boost::any Z3ExpressionAdapter::visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const&) { - return context.int_val(static_cast(expression.getValue())); + return context.int_val(static_cast(expression.getValue())); } boost::any Z3ExpressionAdapter::visit(storm::expressions::UnaryBooleanFunctionExpression const& expression, boost::any const& data) { diff --git a/src/storm/api/model_descriptions.cpp b/src/storm/api/model_descriptions.cpp index bd1e399f3..76ce24116 100644 --- a/src/storm/api/model_descriptions.cpp +++ b/src/storm/api/model_descriptions.cpp @@ -6,11 +6,15 @@ #include "storm/storage/jani/Model.h" #include "storm/storage/jani/Property.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/BuildSettings.h" + namespace storm { namespace api { - storm::prism::Program parseProgram(std::string const& filename) { - storm::prism::Program program = storm::parser::PrismParser::parse(filename).simplify().simplify(); + storm::prism::Program parseProgram(std::string const& filename, bool prismCompatibility) { + storm::prism::Program program = storm::parser::PrismParser::parse(filename, prismCompatibility).simplify().simplify(); program.checkValidity(); return program; } diff --git a/src/storm/api/model_descriptions.h b/src/storm/api/model_descriptions.h index 99ab5d24d..533c5e8d1 100644 --- a/src/storm/api/model_descriptions.h +++ b/src/storm/api/model_descriptions.h @@ -14,7 +14,7 @@ namespace storm { namespace api { - storm::prism::Program parseProgram(std::string const& filename); + storm::prism::Program parseProgram(std::string const& filename, bool prismCompatibility = false); std::pair> parseJaniModel(std::string const& filename); diff --git a/src/storm/builder/BuilderOptions.cpp b/src/storm/builder/BuilderOptions.cpp index 2ee5bf37c..00718e3f1 100644 --- a/src/storm/builder/BuilderOptions.cpp +++ b/src/storm/builder/BuilderOptions.cpp @@ -3,7 +3,7 @@ #include "storm/logic/Formulas.h" #include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/IOSettings.h" +#include "storm/settings/modules/BuildSettings.h" #include "storm/settings/modules/GeneralSettings.h" #include "storm/utility/macros.h" @@ -55,9 +55,9 @@ namespace storm { } } - auto const& ioSettings = storm::settings::getModule(); + auto const& buildSettings = storm::settings::getModule(); auto const& generalSettings = storm::settings::getModule(); - explorationChecks = ioSettings.isExplorationChecksSet(); + explorationChecks = buildSettings.isExplorationChecksSet(); showProgress = generalSettings.isVerboseSet(); showProgressDelay = generalSettings.getShowProgressDelay(); } diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp index 7a552e9bd..ac4b554d5 100644 --- a/src/storm/builder/ExplicitModelBuilder.cpp +++ b/src/storm/builder/ExplicitModelBuilder.cpp @@ -11,7 +11,7 @@ #include "storm/storage/expressions/ExpressionManager.h" #include "storm/settings/modules/CoreSettings.h" -#include "storm/settings/modules/IOSettings.h" +#include "storm/settings/modules/BuildSettings.h" #include "storm/builder/RewardModelBuilder.h" #include "storm/builder/ChoiceInformationBuilder.h" @@ -43,7 +43,7 @@ namespace storm { namespace builder { template - ExplicitModelBuilder::Options::Options() : explorationOrder(storm::settings::getModule().getExplorationOrder()) { + ExplicitModelBuilder::Options::Options() : explorationOrder(storm::settings::getModule().getExplorationOrder()) { // Intentionally left empty. } @@ -89,20 +89,22 @@ namespace storm { // Check, if the state was already registered. std::pair actualIndexBucketPair = stateStorage.stateToId.findOrAddAndGetBucket(state, newIndex); - if (actualIndexBucketPair.first == newIndex) { + StateType actualIndex = actualIndexBucketPair.first; + + if (actualIndex == newIndex) { if (options.explorationOrder == ExplorationOrder::Dfs) { - statesToExplore.push_front(state); + statesToExplore.emplace_front(state, actualIndex); // Reserve one slot for the new state in the remapping. stateRemapping.get().push_back(storm::utility::zero()); } else if (options.explorationOrder == ExplorationOrder::Bfs) { - statesToExplore.push_back(state); + statesToExplore.emplace_back(state, actualIndex); } else { STORM_LOG_ASSERT(false, "Invalid exploration order."); } } - return actualIndexBucketPair.first; + return actualIndex; } template @@ -139,8 +141,8 @@ namespace storm { // Perform a search through the model. while (!statesToExplore.empty()) { // Get the first state in the queue. - CompressedState currentState = statesToExplore.front(); - StateType currentIndex = stateStorage.stateToId.getValue(currentState); + CompressedState currentState = statesToExplore.front().first; + StateType currentIndex = statesToExplore.front().second; statesToExplore.pop_front(); // If the exploration order differs from breadth-first, we remember that this row group was actually @@ -149,7 +151,9 @@ namespace storm { stateRemapping.get()[currentIndex] = currentRowGroup; } - STORM_LOG_TRACE("Exploring state with id " << currentIndex << "."); + if (currentIndex % 100000 == 0) { + STORM_LOG_TRACE("Exploring state with id " << currentIndex << "."); + } generator->load(currentState); storm::generator::StateBehavior behavior = generator->expand(stateToIdCallback); @@ -304,7 +308,7 @@ namespace storm { buildMatrices(transitionMatrixBuilder, rewardModelBuilders, choiceInformationBuilder, markovianStates); - // initialize the model components with the obtained information. + // Initialize the model components with the obtained information. storm::storage::sparse::ModelComponents modelComponents(transitionMatrixBuilder.build(), buildStateLabeling(), std::unordered_map(), !generator->isDiscreteTimeModel(), std::move(markovianStates)); // Now finalize all reward models. @@ -314,7 +318,7 @@ namespace storm { // Build the choice labeling modelComponents.choiceLabeling = choiceInformationBuilder.buildChoiceLabeling(modelComponents.transitionMatrix.getRowCount()); - // if requested, build the state valuations and choice origins + // If requested, build the state valuations and choice origins if (generator->getOptions().isBuildStateValuationsSet()) { std::vector valuations(modelComponents.transitionMatrix.getRowGroupCount()); for (auto const& bitVectorIndexPair : stateStorage.stateToId) { @@ -332,7 +336,7 @@ namespace storm { template storm::models::sparse::StateLabeling ExplicitModelBuilder::buildStateLabeling() { - return generator->label(stateStorage.stateToId, stateStorage.initialStateIndices, stateStorage.deadlockStateIndices); + return generator->label(stateStorage, stateStorage.initialStateIndices, stateStorage.deadlockStateIndices); } // Explicitly instantiate the class. diff --git a/src/storm/builder/ExplicitModelBuilder.h b/src/storm/builder/ExplicitModelBuilder.h index ef5da691b..9440b7e08 100644 --- a/src/storm/builder/ExplicitModelBuilder.h +++ b/src/storm/builder/ExplicitModelBuilder.h @@ -136,7 +136,7 @@ namespace storm { storm::storage::sparse::StateStorage stateStorage; /// A set of states that still need to be explored. - std::deque statesToExplore; + std::deque> statesToExplore; /// An optional mapping from state indices to the row groups in which they actually reside. This needs to be /// built in case the exploration order is not BFS. diff --git a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h index e2373b567..fe313ab51 100644 --- a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h +++ b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h @@ -451,7 +451,7 @@ namespace storm { // This is because it could be that the commands are taken to enable other synchronizations. Therefore, we need // to add an additional clause that says that the right-hand side of the implication is also true if all commands // of the current choice have enabled synchronization options. - storm::expressions::Expression finalDisjunct = variableInformation.manager->boolean(false); + storm::expressions::Expression finalDisjunct = variableInformation.manager->boolean(true); for (auto label : labelSetFollowingSetsPair.first) { storm::expressions::Expression alternativeExpressionForLabel = variableInformation.manager->boolean(false); std::set> const& synchsForCommand = synchronizingLabels.at(label); diff --git a/src/storm/exceptions/InternalException.h b/src/storm/exceptions/InternalException.h new file mode 100644 index 000000000..e28f8f4fd --- /dev/null +++ b/src/storm/exceptions/InternalException.h @@ -0,0 +1,12 @@ +#pragma once + +#include "storm/exceptions/BaseException.h" +#include "storm/exceptions/ExceptionMacros.h" + +namespace storm { + namespace exceptions { + + STORM_NEW_EXCEPTION(InternalException) + + } +} diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index f7d86e914..40481fd83 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -608,7 +608,7 @@ namespace storm { } template - storm::models::sparse::StateLabeling JaniNextStateGenerator::label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices, std::vector const& deadlockStateIndices) { + storm::models::sparse::StateLabeling JaniNextStateGenerator::label(storm::storage::sparse::StateStorage const& stateStorage, std::vector const& initialStateIndices, std::vector const& deadlockStateIndices) { // As in JANI we can use transient boolean variable assignments in locations to identify states, we need to // create a list of boolean transient variables and the expressions that define them. std::unordered_map transientVariableToExpressionMap; @@ -625,7 +625,7 @@ namespace storm { transientVariableExpressions.push_back(std::make_pair(element.first.getName(), element.second)); } - return NextStateGenerator::label(states, initialStateIndices, deadlockStateIndices, transientVariableExpressions); + return NextStateGenerator::label(stateStorage, initialStateIndices, deadlockStateIndices, transientVariableExpressions); } template diff --git a/src/storm/generator/JaniNextStateGenerator.h b/src/storm/generator/JaniNextStateGenerator.h index 3fcfc2777..594efc91c 100644 --- a/src/storm/generator/JaniNextStateGenerator.h +++ b/src/storm/generator/JaniNextStateGenerator.h @@ -30,7 +30,7 @@ namespace storm { virtual std::size_t getNumberOfRewardModels() const override; virtual storm::builder::RewardModelInformation getRewardModelInformation(uint64_t const& index) const override; - virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices = {}, std::vector const& deadlockStateIndices = {}) override; + virtual storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage const& stateStorage, std::vector const& initialStateIndices = {}, std::vector const& deadlockStateIndices = {}) override; private: /*! diff --git a/src/storm/generator/NextStateGenerator.cpp b/src/storm/generator/NextStateGenerator.cpp index 15c6048c3..f69014364 100644 --- a/src/storm/generator/NextStateGenerator.cpp +++ b/src/storm/generator/NextStateGenerator.cpp @@ -53,7 +53,7 @@ namespace storm { } template - storm::models::sparse::StateLabeling NextStateGenerator::label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices, std::vector const& deadlockStateIndices, std::vector> labelsAndExpressions) { + storm::models::sparse::StateLabeling NextStateGenerator::label(storm::storage::sparse::StateStorage const& stateStorage, std::vector const& initialStateIndices, std::vector const& deadlockStateIndices, std::vector> labelsAndExpressions) { for (auto const& expression : this->options.getExpressionLabels()) { std::stringstream stream; @@ -67,12 +67,14 @@ namespace storm { labelsAndExpressions.resize(std::distance(labelsAndExpressions.begin(), it)); // Prepare result. - storm::models::sparse::StateLabeling result(states.size()); + storm::models::sparse::StateLabeling result(stateStorage.getNumberOfStates()); // Initialize labeling. for (auto const& label : labelsAndExpressions) { result.addLabel(label.first); } + + storm::storage::BitVectorHashMap const& states = stateStorage.stateToId; for (auto const& stateIndexPair : states) { unpackStateIntoEvaluator(stateIndexPair.first, variableInformation, *this->evaluator); diff --git a/src/storm/generator/NextStateGenerator.h b/src/storm/generator/NextStateGenerator.h index 25335dbfc..54f7f1024 100644 --- a/src/storm/generator/NextStateGenerator.h +++ b/src/storm/generator/NextStateGenerator.h @@ -7,7 +7,7 @@ #include #include "storm/storage/expressions/Expression.h" -#include "storm/storage/BitVectorHashMap.h" +#include "storm/storage/sparse/StateStorage.h" #include "storm/storage/expressions/ExpressionEvaluator.h" #include "storm/storage/sparse/ChoiceOrigins.h" @@ -61,7 +61,7 @@ namespace storm { storm::expressions::SimpleValuation toValuation(CompressedState const& state) const; - virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices = {}, std::vector const& deadlockStateIndices = {}) = 0; + virtual storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage const& stateStorage, std::vector const& initialStateIndices = {}, std::vector const& deadlockStateIndices = {}) = 0; NextStateGeneratorOptions const& getOptions() const; @@ -71,7 +71,7 @@ namespace storm { /*! * Creates the state labeling for the given states using the provided labels and expressions. */ - storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices, std::vector const& deadlockStateIndices, std::vector> labelsAndExpressions); + storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage const& stateStorage, std::vector const& initialStateIndices, std::vector const& deadlockStateIndices, std::vector> labelsAndExpressions); void postprocess(StateBehavior& result); diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp index bf9d73876..db74175c0 100644 --- a/src/storm/generator/PrismNextStateGenerator.cpp +++ b/src/storm/generator/PrismNextStateGenerator.cpp @@ -575,7 +575,7 @@ namespace storm { } template - storm::models::sparse::StateLabeling PrismNextStateGenerator::label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices, std::vector const& deadlockStateIndices) { + storm::models::sparse::StateLabeling PrismNextStateGenerator::label(storm::storage::sparse::StateStorage const& stateStorage, std::vector const& initialStateIndices, std::vector const& deadlockStateIndices) { // Gather a vector of labels and their expressions. std::vector> labels; if (this->options.isBuildAllLabelsSet()) { @@ -592,7 +592,7 @@ namespace storm { } } - return NextStateGenerator::label(states, initialStateIndices, deadlockStateIndices, labels); + return NextStateGenerator::label(stateStorage, initialStateIndices, deadlockStateIndices, labels); } template diff --git a/src/storm/generator/PrismNextStateGenerator.h b/src/storm/generator/PrismNextStateGenerator.h index 0097e7055..5cc8ce9ba 100644 --- a/src/storm/generator/PrismNextStateGenerator.h +++ b/src/storm/generator/PrismNextStateGenerator.h @@ -28,7 +28,7 @@ namespace storm { virtual std::size_t getNumberOfRewardModels() const override; virtual storm::builder::RewardModelInformation getRewardModelInformation(uint64_t const& index) const override; - virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices = {}, std::vector const& deadlockStateIndices = {}) override; + virtual storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage const& stateStorage, std::vector const& initialStateIndices = {}, std::vector const& deadlockStateIndices = {}) override; virtual std::shared_ptr generateChoiceOrigins(std::vector& dataForChoiceOrigins) const override; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp index 1887e86ce..f82fef6ac 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp @@ -104,7 +104,7 @@ namespace storm { for (uint64_t i = 0; i < this->objectives.size(); ++i) { headers.push_back("obj" + std::to_string(i)); } - storm::utility::exportDataToCSVFile("cdf" + std::to_string(numChecks) + ".csv", cdfData, weightVector, headers); + storm::utility::exportDataToCSVFile(storm::settings::getModule().getExportCdfDirectory() + "cdf" + std::to_string(numChecks) + ".csv", cdfData, weightVector, headers); } auto solution = rewardUnfolding.getInitialStateResult(initEpoch); auto solutionIt = solution.begin(); diff --git a/src/storm/parser/ImcaMarkovAutomatonParser.cpp b/src/storm/parser/ImcaMarkovAutomatonParser.cpp index c00b44497..01cb93671 100644 --- a/src/storm/parser/ImcaMarkovAutomatonParser.cpp +++ b/src/storm/parser/ImcaMarkovAutomatonParser.cpp @@ -1,7 +1,7 @@ #include "storm/parser/ImcaMarkovAutomatonParser.h" #include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/IOSettings.h" +#include "storm/settings/modules/BuildSettings.h" #include "storm/settings/modules/CoreSettings.h" #include "storm/utility/file.h" #include "storm/utility/builder.h" @@ -11,7 +11,7 @@ namespace storm { template ImcaParserGrammar::ImcaParserGrammar() : ImcaParserGrammar::base_type(start), numStates(0), numChoices(0), numTransitions(0), hasStateReward(false), hasActionReward(false) { - buildChoiceLabels = storm::settings::getModule().isBuildChoiceLabelsSet(); + buildChoiceLabels = storm::settings::getModule().isBuildChoiceLabelsSet(); initialize(); } diff --git a/src/storm/parser/PrismParser.cpp b/src/storm/parser/PrismParser.cpp index 38ed0cb12..18f42d39c 100644 --- a/src/storm/parser/PrismParser.cpp +++ b/src/storm/parser/PrismParser.cpp @@ -2,7 +2,6 @@ #include "storm/storage/prism/Compositions.h" -#include "storm/settings/SettingsManager.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/InvalidTypeException.h" @@ -16,7 +15,7 @@ namespace storm { namespace parser { - storm::prism::Program PrismParser::parse(std::string const& filename) { + storm::prism::Program PrismParser::parse(std::string const& filename, bool prismCompatibility) { // Open file and initialize result. std::ifstream inputFileStream; storm::utility::openFile(filename, inputFileStream); @@ -25,7 +24,7 @@ namespace storm { // Now try to parse the contents of the file. try { std::string fileContent((std::istreambuf_iterator(inputFileStream)), (std::istreambuf_iterator())); - result = parseFromString(fileContent, filename); + result = parseFromString(fileContent, filename, prismCompatibility); } catch(std::exception& e) { // In case of an exception properly close the file before passing exception. storm::utility::closeFile(inputFileStream); @@ -37,7 +36,7 @@ namespace storm { return result; } - storm::prism::Program PrismParser::parseFromString(std::string const& input, std::string const& filename) { + storm::prism::Program PrismParser::parseFromString(std::string const& input, std::string const& filename, bool prismCompatibility) { PositionIteratorType first(input.begin()); PositionIteratorType iter = first; PositionIteratorType last(input.end()); @@ -47,7 +46,7 @@ namespace storm { storm::prism::Program result; // Create grammar. - storm::parser::PrismParser grammar(filename, first); + storm::parser::PrismParser grammar(filename, first, prismCompatibility); try { // Start first run. bool succeeded = qi::phrase_parse(iter, last, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), result); @@ -74,7 +73,7 @@ namespace storm { return result; } - PrismParser::PrismParser(std::string const& filename, Iterator first) : PrismParser::base_type(start), secondRun(false), filename(filename), annotate(first), manager(new storm::expressions::ExpressionManager()), expressionParser(new ExpressionParser(*manager, keywords_, false, false)) { + PrismParser::PrismParser(std::string const& filename, Iterator first, bool prismCompatibility) : PrismParser::base_type(start), secondRun(false), prismCompatibility(prismCompatibility), filename(filename), annotate(first), manager(new storm::expressions::ExpressionManager()), expressionParser(new ExpressionParser(*manager, keywords_, false, false)) { ExpressionParser& expression_ = *expressionParser; // Parse simple identifier. @@ -671,8 +670,9 @@ namespace storm { STORM_LOG_WARN("Program does not specify model type. Implicitly assuming 'mdp'."); finalModelType = storm::prism::Program::ModelType::MDP; } + - return storm::prism::Program(manager, finalModelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, globalProgramInformation.formulas, globalProgramInformation.modules, globalProgramInformation.actionIndices, globalProgramInformation.rewardModels, globalProgramInformation.labels, secondRun && !globalProgramInformation.hasInitialConstruct ? boost::none : boost::make_optional(globalProgramInformation.initialConstruct), globalProgramInformation.systemCompositionConstruct, this->getFilename(), 1, this->secondRun); + return storm::prism::Program(manager, finalModelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, globalProgramInformation.formulas, globalProgramInformation.modules, globalProgramInformation.actionIndices, globalProgramInformation.rewardModels, globalProgramInformation.labels, secondRun && !globalProgramInformation.hasInitialConstruct ? boost::none : boost::make_optional(globalProgramInformation.initialConstruct), globalProgramInformation.systemCompositionConstruct, prismCompatibility, this->getFilename(), 1, this->secondRun); } void PrismParser::removeInitialConstruct(GlobalProgramInformation& globalProgramInformation) const { diff --git a/src/storm/parser/PrismParser.h b/src/storm/parser/PrismParser.h index 129cd7b43..fe7f0bc83 100644 --- a/src/storm/parser/PrismParser.h +++ b/src/storm/parser/PrismParser.h @@ -77,7 +77,7 @@ namespace storm { * @param filename the name of the file to parse. * @return The resulting PRISM program. */ - static storm::prism::Program parse(std::string const& filename); + static storm::prism::Program parse(std::string const& filename, bool prismCompatability = false); /*! * Parses the given input stream into the PRISM storage classes assuming it complies with the PRISM syntax. @@ -86,7 +86,7 @@ namespace storm { * @param filename The name of the file from which the input was read. * @return The resulting PRISM program. */ - static storm::prism::Program parseFromString(std::string const& input, std::string const& filename); + static storm::prism::Program parseFromString(std::string const& input, std::string const& filename, bool prismCompatability = false); private: struct modelTypeStruct : qi::symbols { @@ -150,7 +150,7 @@ namespace storm { * @param filename The filename that is to be read. This is used for proper error reporting. * @param first The iterator to the beginning of the input. */ - PrismParser(std::string const& filename, Iterator first); + PrismParser(std::string const& filename, Iterator first, bool prismCompatibility); /*! * Sets an internal flag that indicates the second run is now taking place. @@ -159,6 +159,8 @@ namespace storm { // A flag that stores whether the grammar is currently doing the second run. bool secondRun; + + bool prismCompatibility; /*! * Sets whether doubles literals are allowed in the parsed expression. diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp index b271ca581..188d1cba2 100644 --- a/src/storm/settings/SettingsManager.cpp +++ b/src/storm/settings/SettingsManager.cpp @@ -1,7 +1,6 @@ #include "storm/settings/SettingsManager.h" #include -#include #include #include #include @@ -19,6 +18,7 @@ #include "storm/settings/modules/DebugSettings.h" #include "storm/settings/modules/CounterexampleGeneratorSettings.h" #include "storm/settings/modules/CuddSettings.h" +#include "storm/settings/modules/BuildSettings.h" #include "storm/settings/modules/SylvanSettings.h" #include "storm/settings/modules/EigenEquationSolverSettings.h" #include "storm/settings/modules/GmmxxEquationSolverSettings.h" @@ -511,6 +511,7 @@ namespace storm { // Register all known settings modules. storm::settings::addModule(); storm::settings::addModule(); + storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); diff --git a/src/storm/settings/modules/BuildSettings.cpp b/src/storm/settings/modules/BuildSettings.cpp new file mode 100644 index 000000000..a813b08fa --- /dev/null +++ b/src/storm/settings/modules/BuildSettings.cpp @@ -0,0 +1,95 @@ +#include "storm/settings/modules/BuildSettings.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/SettingMemento.h" +#include "storm/settings/Option.h" +#include "storm/settings/OptionBuilder.h" +#include "storm/settings/ArgumentBuilder.h" +#include "storm/settings/Argument.h" +#include "storm/exceptions/InvalidSettingsException.h" +#include "storm/parser/CSVParser.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/IllegalArgumentValueException.h" + +namespace storm { + namespace settings { + namespace modules { + + const std::string BuildSettings::moduleName = "build"; + + const std::string jitOptionName = "jit"; + const std::string explorationOrderOptionName = "explorder"; + const std::string explorationOrderOptionShortName = "eo"; + const std::string explorationChecksOptionName = "explchecks"; + const std::string explorationChecksOptionShortName = "ec"; + const std::string prismCompatibilityOptionName = "prismcompat"; + const std::string prismCompatibilityOptionShortName = "pc"; + const std::string noBuildOptionName = "nobuild"; + const std::string fullModelBuildOptionName = "buildfull"; + const std::string buildChoiceLabelOptionName = "buildchoicelab"; + const std::string buildStateValuationsOptionName = "buildstateval"; + BuildSettings::BuildSettings() : ModuleSettings(moduleName) { + + std::vector explorationOrders = {"dfs", "bfs"}; + this->addOption(storm::settings::OptionBuilder(moduleName, prismCompatibilityOptionName, false, "Enables PRISM compatibility. This may be necessary to process some PRISM models.").setShortName(prismCompatibilityOptionShortName).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, jitOptionName, false, "If set, the model is built using the JIT model builder.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, fullModelBuildOptionName, false, "If set, include all rewards and labels.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, buildChoiceLabelOptionName, false, "If set, also build the choice labels").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, buildStateValuationsOptionName, false, "If set, also build the state valuations").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, noBuildOptionName, false, "If set, do not build the model.").build()); + + this->addOption(storm::settings::OptionBuilder(moduleName, explorationOrderOptionName, false, "Sets which exploration order to use.").setShortName(explorationOrderOptionShortName) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the exploration order to choose.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(explorationOrders)).setDefaultValueString("bfs").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, explorationChecksOptionName, false, "If set, additional checks (if available) are performed during model exploration to debug the model.").setShortName(explorationChecksOptionShortName).build()); + + } + + + bool BuildSettings::isJitSet() const { + return this->getOption(jitOptionName).getHasOptionBeenSet(); + } + + bool BuildSettings::isExplorationOrderSet() const { + return this->getOption(explorationOrderOptionName).getHasOptionBeenSet(); + } + + bool BuildSettings::isPrismCompatibilityEnabled() const { + return this->getOption(prismCompatibilityOptionName).getHasOptionBeenSet(); + } + + bool BuildSettings::isBuildFullModelSet() const { + return this->getOption(fullModelBuildOptionName).getHasOptionBeenSet(); + } + + bool BuildSettings::isNoBuildModelSet() const { + return this->getOption(noBuildOptionName).getHasOptionBeenSet(); + } + + bool BuildSettings::isBuildChoiceLabelsSet() const { + return this->getOption(buildChoiceLabelOptionName).getHasOptionBeenSet(); + } + + bool BuildSettings::isBuildStateValuationsSet() const { + return this->getOption(buildStateValuationsOptionName).getHasOptionBeenSet(); + } + + + storm::builder::ExplorationOrder BuildSettings::getExplorationOrder() const { + std::string explorationOrderAsString = this->getOption(explorationOrderOptionName).getArgumentByName("name").getValueAsString(); + if (explorationOrderAsString == "dfs") { + return storm::builder::ExplorationOrder::Dfs; + } else if (explorationOrderAsString == "bfs") { + return storm::builder::ExplorationOrder::Bfs; + } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown exploration order '" << explorationOrderAsString << "'."); + } + + bool BuildSettings::isExplorationChecksSet() const { + return this->getOption(explorationChecksOptionName).getHasOptionBeenSet(); + } + } + + + } +} diff --git a/src/storm/settings/modules/BuildSettings.h b/src/storm/settings/modules/BuildSettings.h new file mode 100644 index 000000000..4ef0f5193 --- /dev/null +++ b/src/storm/settings/modules/BuildSettings.h @@ -0,0 +1,84 @@ +#pragma once + + +#include "storm-config.h" +#include "storm/settings/modules/ModuleSettings.h" +#include "storm/builder/ExplorationOrder.h" + +namespace storm { + namespace settings { + namespace modules { + class BuildSettings : public ModuleSettings { + + public: + + /*! + * Creates a new set of core settings. + */ + BuildSettings(); + /*! + * Retrieves whether the option to use the JIT builder is set. + * + * @return True iff the JIT builder is to be used. + */ + bool isJitSet() const; + + /*! + * Retrieves whether the model exploration order was set. + * + * @return True if the model exploration option was set. + */ + bool isExplorationOrderSet() const; + + /*! + * Retrieves whether to perform additional checks during model exploration (e.g. out-of-bounds, etc.). + * + * @return True if additional checks are to be performed. + */ + bool isExplorationChecksSet() const; + + /*! + * Retrieves the exploration order if it was set. + * + * @return The chosen exploration order. + */ + storm::builder::ExplorationOrder getExplorationOrder() const; + + /*! + * Retrieves whether the PRISM compatibility mode was enabled. + * + * @return True iff the PRISM compatibility mode was enabled. + */ + bool isPrismCompatibilityEnabled() const; + + /** + * Retrieves whether no model should be build at all, in case one just want to translate models or parse a file. + */ + bool isNoBuildModelSet() const; + + /*! + * Retrieves whether the full model should be build, that is, the model including all labels and rewards. + * + * @return true iff the full model should be build. + */ + bool isBuildFullModelSet() const; + + /*! + * Retrieves whether the choice labels should be build + * @return + */ + bool isBuildChoiceLabelsSet() const; + + /*! + * Retrieves whether the choice labels should be build + * @return + */ + bool isBuildStateValuationsSet() const; + + + // The name of the module. + static const std::string moduleName; + }; + } + } +} \ No newline at end of file diff --git a/src/storm/settings/modules/CoreSettings.h b/src/storm/settings/modules/CoreSettings.h index e0359bf62..afd16cd78 100644 --- a/src/storm/settings/modules/CoreSettings.h +++ b/src/storm/settings/modules/CoreSettings.h @@ -117,9 +117,9 @@ namespace storm { bool isDdLibraryTypeSetFromDefaultValue() const; /*! - * Retrieves whether statistics are to be shown for counterexample generation. + * Retrieves whether statistics are to be shown * - * @return True iff statistics are to be shown for counterexample generation. + * @return True iff statistics are to be shown */ bool isShowStatisticsSet() const; diff --git a/src/storm/settings/modules/CounterexampleGeneratorSettings.cpp b/src/storm/settings/modules/CounterexampleGeneratorSettings.cpp index f2c4a483d..b33a332df 100644 --- a/src/storm/settings/modules/CounterexampleGeneratorSettings.cpp +++ b/src/storm/settings/modules/CounterexampleGeneratorSettings.cpp @@ -29,7 +29,6 @@ namespace storm { return this->getOption(minimalCommandSetOptionName).getHasOptionBeenSet(); } - bool CounterexampleGeneratorSettings::isUseMilpBasedMinimalCommandSetGenerationSet() const { return this->getOption(minimalCommandSetOptionName).getArgumentByName("method").getValueAsString() == "milp"; } diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp index 7b26d43d6..658b59cbe 100644 --- a/src/storm/settings/modules/IOSettings.cpp +++ b/src/storm/settings/modules/IOSettings.cpp @@ -31,22 +31,13 @@ namespace storm { const std::string IOSettings::prismInputOptionName = "prism"; const std::string IOSettings::janiInputOptionName = "jani"; const std::string IOSettings::prismToJaniOptionName = "prism2jani"; - const std::string IOSettings::jitOptionName = "jit"; - const std::string IOSettings::explorationOrderOptionName = "explorder"; - const std::string IOSettings::explorationOrderOptionShortName = "eo"; - const std::string IOSettings::explorationChecksOptionName = "explchecks"; - const std::string IOSettings::explorationChecksOptionShortName = "ec"; + const std::string IOSettings::transitionRewardsOptionName = "transrew"; const std::string IOSettings::stateRewardsOptionName = "staterew"; const std::string IOSettings::choiceLabelingOptionName = "choicelab"; const std::string IOSettings::constantsOptionName = "constants"; const std::string IOSettings::constantsOptionShortName = "const"; - const std::string IOSettings::prismCompatibilityOptionName = "prismcompat"; - const std::string IOSettings::prismCompatibilityOptionShortName = "pc"; - const std::string IOSettings::noBuildOptionName = "nobuild"; - const std::string IOSettings::fullModelBuildOptionName = "buildfull"; - const std::string IOSettings::buildChoiceLabelOptionName = "buildchoicelab"; - const std::string IOSettings::buildStateValuationsOptionName = "buildstateval"; + const std::string IOSettings::janiPropertyOptionName = "janiproperty"; const std::string IOSettings::janiPropertyOptionShortName = "jprop"; const std::string IOSettings::propertyOptionName = "prop"; @@ -54,12 +45,11 @@ namespace storm { IOSettings::IOSettings() : ModuleSettings(moduleName) { - this->addOption(storm::settings::OptionBuilder(moduleName, prismCompatibilityOptionName, false, "Enables PRISM compatibility. This may be necessary to process some PRISM models.").setShortName(prismCompatibilityOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportDotOptionName, "", "If given, the loaded model will be written to the specified file in the dot format.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportJaniDotOptionName, "", "If given, the loaded jani model will be written to the specified file in the dot format.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, exportCdfOptionName, false, "Exports the cumulative density function for reward bounded properties into a .csv file.").setShortName(exportCdfOptionShortName).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, exportCdfOptionName, false, "Exports the cumulative density function for reward bounded properties into a .csv file.").setShortName(exportCdfOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("directory", "A path to an existing directory where the cdf files will be stored.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportExplicitOptionName, "", "If given, the loaded model will be written to the specified file in the drn format.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "the name of the file to which the model is to be writen.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, explicitOptionName, false, "Parses the model given in an explicit (sparse) representation.").setShortName(explicitOptionShortName) @@ -76,19 +66,10 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, janiInputOptionName, false, "Parses the model given in the JANI format.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the JANI input.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, prismToJaniOptionName, false, "If set, the input PRISM model is transformed to JANI.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, jitOptionName, false, "If set, the model is built using the JIT model builder.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, fullModelBuildOptionName, false, "If set, include all rewards and labels.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, buildChoiceLabelOptionName, false, "If set, also build the choice labels").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, buildStateValuationsOptionName, false, "If set, also build the state valuations").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, noBuildOptionName, false, "If set, do not build the model.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, propertyOptionName, false, "Specifies the properties to be checked on the model.").setShortName(propertyOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("property or filename", "The formula or the file containing the formulas.").build()) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filter", "The names of the properties to check.").setDefaultValueString("all").build()) .build()); - std::vector explorationOrders = {"dfs", "bfs"}; - this->addOption(storm::settings::OptionBuilder(moduleName, explorationOrderOptionName, false, "Sets which exploration order to use.").setShortName(explorationOrderOptionShortName) - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the exploration order to choose.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(explorationOrders)).setDefaultValueString("bfs").build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, explorationChecksOptionName, false, "If set, additional checks (if available) are performed during model exploration to debug the model.").setShortName(explorationChecksOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, transitionRewardsOptionName, false, "If given, the transition rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the transition rewards.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); @@ -105,7 +86,7 @@ namespace storm { bool IOSettings::isExportDotSet() const { return this->getOption(exportDotOptionName).getHasOptionBeenSet(); } - + std::string IOSettings::getExportDotFilename() const { return this->getOption(exportDotOptionName).getArgumentByName("filename").getValueAsString(); } @@ -117,23 +98,35 @@ namespace storm { std::string IOSettings::getExportJaniDotFilename() const { return this->getOption(exportJaniDotOptionName).getArgumentByName("filename").getValueAsString(); } - + bool IOSettings::isExportExplicitSet() const { return this->getOption(exportExplicitOptionName).getHasOptionBeenSet(); } - + std::string IOSettings::getExportExplicitFilename() const { return this->getOption(exportExplicitOptionName).getArgumentByName("filename").getValueAsString(); } - + + bool IOSettings::isExportCdfSet() const { + return this->getOption(exportCdfOptionName).getHasOptionBeenSet(); + } + + std::string IOSettings::getExportCdfDirectory() const { + std::string result = this->getOption(exportCdfOptionName).getArgumentByName("directory").getValueAsString(); + if (result.back() != '/') { + result.push_back('/'); + } + return result; + } + bool IOSettings::isExplicitSet() const { return this->getOption(explicitOptionName).getHasOptionBeenSet(); } - + std::string IOSettings::getTransitionFilename() const { return this->getOption(explicitOptionName).getArgumentByName("transition filename").getValueAsString(); } - + std::string IOSettings::getLabelingFilename() const { return this->getOption(explicitOptionName).getArgumentByName("labeling filename").getValueAsString(); } @@ -157,15 +150,15 @@ namespace storm { bool IOSettings::isPrismInputSet() const { return this->getOption(prismInputOptionName).getHasOptionBeenSet(); } - + bool IOSettings::isPrismOrJaniInputSet() const { return isJaniInputSet() || isPrismInputSet(); } - + bool IOSettings::isPrismToJaniSet() const { return this->getOption(prismToJaniOptionName).getHasOptionBeenSet(); } - + std::string IOSettings::getPrismInputFilename() const { return this->getOption(prismInputOptionName).getArgumentByName("filename").getValueAsString(); } @@ -177,97 +170,47 @@ namespace storm { std::string IOSettings::getJaniInputFilename() const { return this->getOption(janiInputOptionName).getArgumentByName("filename").getValueAsString(); } - - bool IOSettings::isJitSet() const { - return this->getOption(jitOptionName).getHasOptionBeenSet(); - } - bool IOSettings::isExplorationOrderSet() const { - return this->getOption(explorationOrderOptionName).getHasOptionBeenSet(); - } - - storm::builder::ExplorationOrder IOSettings::getExplorationOrder() const { - std::string explorationOrderAsString = this->getOption(explorationOrderOptionName).getArgumentByName("name").getValueAsString(); - if (explorationOrderAsString == "dfs") { - return storm::builder::ExplorationOrder::Dfs; - } else if (explorationOrderAsString == "bfs") { - return storm::builder::ExplorationOrder::Bfs; - } - STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown exploration order '" << explorationOrderAsString << "'."); - } - - bool IOSettings::isExplorationChecksSet() const { - return this->getOption(explorationChecksOptionName).getHasOptionBeenSet(); - } - bool IOSettings::isTransitionRewardsSet() const { return this->getOption(transitionRewardsOptionName).getHasOptionBeenSet(); } - + std::string IOSettings::getTransitionRewardsFilename() const { return this->getOption(transitionRewardsOptionName).getArgumentByName("filename").getValueAsString(); } - + bool IOSettings::isStateRewardsSet() const { return this->getOption(stateRewardsOptionName).getHasOptionBeenSet(); } - + std::string IOSettings::getStateRewardsFilename() const { return this->getOption(stateRewardsOptionName).getArgumentByName("filename").getValueAsString(); } - + bool IOSettings::isChoiceLabelingSet() const { return this->getOption(choiceLabelingOptionName).getHasOptionBeenSet(); } - + std::string IOSettings::getChoiceLabelingFilename() const { return this->getOption(choiceLabelingOptionName).getArgumentByName("filename").getValueAsString(); } - - std::unique_ptr IOSettings::overridePrismCompatibilityMode(bool stateToSet) { - return this->overrideOption(prismCompatibilityOptionName, stateToSet); - } - + bool IOSettings::isConstantsSet() const { return this->getOption(constantsOptionName).getHasOptionBeenSet(); } - + std::string IOSettings::getConstantDefinitionString() const { return this->getOption(constantsOptionName).getArgumentByName("values").getValueAsString(); } - + bool IOSettings::isJaniPropertiesSet() const { return this->getOption(janiPropertyOptionName).getHasOptionBeenSet(); } - + std::vector IOSettings::getJaniProperties() const { return storm::parser::parseCommaSeperatedValues(this->getOption(janiPropertyOptionName).getArgumentByName("values").getValueAsString()); } - bool IOSettings::isPrismCompatibilityEnabled() const { - return this->getOption(prismCompatibilityOptionName).getHasOptionBeenSet(); - } - - bool IOSettings::isBuildFullModelSet() const { - return this->getOption(fullModelBuildOptionName).getHasOptionBeenSet(); - } - - bool IOSettings::isNoBuildModelSet() const { - return this->getOption(noBuildOptionName).getHasOptionBeenSet(); - } - - bool IOSettings::isBuildChoiceLabelsSet() const { - return this->getOption(buildChoiceLabelOptionName).getHasOptionBeenSet(); - } - - bool IOSettings::isBuildStateValuationsSet() const { - return this->getOption(buildStateValuationsOptionName).getHasOptionBeenSet(); - } - - bool IOSettings::isExportCdfSet() const { - return this->getOption(exportCdfOptionName).getHasOptionBeenSet(); - } - bool IOSettings::isPropertySet() const { return this->getOption(propertyOptionName).getHasOptionBeenSet(); } diff --git a/src/storm/settings/modules/IOSettings.h b/src/storm/settings/modules/IOSettings.h index 053b144e3..cc41176bf 100644 --- a/src/storm/settings/modules/IOSettings.h +++ b/src/storm/settings/modules/IOSettings.h @@ -63,6 +63,16 @@ namespace storm { */ std::string getExportExplicitFilename() const; + /*! + * Retrieves whether the cumulative density function for reward bounded properties should be exported + */ + bool isExportCdfSet() const; + + /*! + * Retrieves a path to a directory in which the cdf files will be stored + */ + std::string getExportCdfDirectory() const; + /*! * Retrieves whether the explicit option was set. * @@ -158,34 +168,6 @@ namespace storm { */ std::string getJaniInputFilename() const; - /*! - * Retrieves whether the option to use the JIT builder is set. - * - * @return True iff the JIT builder is to be used. - */ - bool isJitSet() const; - - /*! - * Retrieves whether the model exploration order was set. - * - * @return True if the model exploration option was set. - */ - bool isExplorationOrderSet() const; - - /*! - * Retrieves whether to perform additional checks during model exploration (e.g. out-of-bounds, etc.). - * - * @return True if additional checks are to be performed. - */ - bool isExplorationChecksSet() const; - - /*! - * Retrieves the exploration order if it was set. - * - * @return The chosen exploration order. - */ - storm::builder::ExplorationOrder getExplorationOrder() const; - /*! * Retrieves whether the transition reward option was set. * @@ -218,7 +200,7 @@ namespace storm { /*! * Retrieves whether the choice labeling option was set. - * + * * @return True iff the choice labeling option was set. */ bool isChoiceLabelingSet() const; @@ -231,15 +213,6 @@ namespace storm { */ std::string getChoiceLabelingFilename() const; - /*! - * Overrides the option to enable the PRISM compatibility mode by setting it to the specified value. As - * soon as the returned memento goes out of scope, the original value is restored. - * - * @param stateToSet The value that is to be set for the option. - * @return The memento that will eventually restore the original value. - */ - std::unique_ptr overridePrismCompatibilityMode(bool stateToSet); - /*! * Retrieves whether the export-to-dot option was set. * @@ -286,39 +259,6 @@ namespace storm { */ std::string getPropertyFilter() const; - /*! - * Retrieves whether the PRISM compatibility mode was enabled. - * - * @return True iff the PRISM compatibility mode was enabled. - */ - bool isPrismCompatibilityEnabled() const; - - /** - * Retrieves whether no model should be build at all, in case one just want to translate models or parse a file. - */ - bool isNoBuildModelSet() const; - - /*! - * Retrieves whether the full model should be build, that is, the model including all labels and rewards. - * - * @return true iff the full model should be build. - */ - bool isBuildFullModelSet() const; - - /*! - * Retrieves whether the choice labels should be build - * @return - */ - bool isBuildChoiceLabelsSet() const; - - /*! - * Retrieves whether the choice labels should be build - * @return - */ - bool isBuildStateValuationsSet() const; - - bool isExportCdfSet() const; - bool check() const override; void finalize() override; @@ -341,22 +281,11 @@ namespace storm { static const std::string prismInputOptionName; static const std::string janiInputOptionName; static const std::string prismToJaniOptionName; - static const std::string jitOptionName; - static const std::string explorationChecksOptionName; - static const std::string explorationChecksOptionShortName; - static const std::string explorationOrderOptionName; - static const std::string explorationOrderOptionShortName; static const std::string transitionRewardsOptionName; static const std::string stateRewardsOptionName; static const std::string choiceLabelingOptionName; static const std::string constantsOptionName; static const std::string constantsOptionShortName; - static const std::string prismCompatibilityOptionName; - static const std::string prismCompatibilityOptionShortName; - static const std::string fullModelBuildOptionName; - static const std::string noBuildOptionName; - static const std::string buildChoiceLabelOptionName; - static const std::string buildStateValuationsOptionName; static const std::string janiPropertyOptionName; static const std::string janiPropertyOptionShortName; static const std::string propertyOptionName; diff --git a/src/storm/settings/modules/MultiObjectiveSettings.cpp b/src/storm/settings/modules/MultiObjectiveSettings.cpp index 1ebc3464b..9d0cc8863 100644 --- a/src/storm/settings/modules/MultiObjectiveSettings.cpp +++ b/src/storm/settings/modules/MultiObjectiveSettings.cpp @@ -21,7 +21,7 @@ namespace storm { std::vector methods = {"pcaa", "constraintbased"}; this->addOption(storm::settings::OptionBuilder(moduleName, methodOptionName, true, "The method to be used for multi objective model checking.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(methods)).setDefaultValueString("pcaa").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportPlotOptionName, true, "Saves data for plotting of pareto curves and achievable values.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("directory", "A path to a directory in which the results will be saved.").build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("directory", "A path to an existing directory in which the results will be saved.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "The precision used for the approximation of numerical- and pareto queries.") .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision.").setDefaultValueDouble(1e-04).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, maxStepsOptionName, true, "Aborts the computation after the given number of refinement steps (= computed pareto optimal points).") diff --git a/src/storm/solver/AbstractEquationSolver.cpp b/src/storm/solver/AbstractEquationSolver.cpp index 86dbf0bd1..a3c5a682b 100644 --- a/src/storm/solver/AbstractEquationSolver.cpp +++ b/src/storm/solver/AbstractEquationSolver.cpp @@ -4,7 +4,6 @@ #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/IOSettings.h" #include "storm/settings/modules/GeneralSettings.h" #include "storm/utility/constants.h" diff --git a/src/storm/storage/BitVector.cpp b/src/storm/storage/BitVector.cpp index f87e80853..f558afc18 100644 --- a/src/storm/storage/BitVector.cpp +++ b/src/storm/storage/BitVector.cpp @@ -1031,22 +1031,6 @@ namespace storm { out << std::endl; } - std::size_t NonZeroBitVectorHash::operator()(storm::storage::BitVector const& bitvector) const { - STORM_LOG_ASSERT(bitvector.size() > 0, "Cannot hash bit vector of zero size."); - std::size_t result = 0; - - for (uint_fast64_t index = 0; index < bitvector.bucketCount(); ++index) { - result ^= result << 3; - result ^= result >> bitvector.getAsInt(index << 6, 5); - } - - // Erase the last bit and add one to definitely make this hash value non-zero. - result &= ~1ull; - result += 1; - - return result; - } - // All necessary explicit template instantiations. template BitVector::BitVector(uint_fast64_t length, std::vector::iterator begin, std::vector::iterator end); template BitVector::BitVector(uint_fast64_t length, std::vector::const_iterator begin, std::vector::const_iterator end); @@ -1060,7 +1044,6 @@ namespace storm { } namespace std { - std::size_t hash::operator()(storm::storage::BitVector const& bitvector) const { return boost::hash_range(bitvector.buckets, bitvector.buckets + bitvector.bucketCount()); } diff --git a/src/storm/storage/BitVector.h b/src/storm/storage/BitVector.h index 6a7aab7eb..9fa29c8ae 100644 --- a/src/storm/storage/BitVector.h +++ b/src/storm/storage/BitVector.h @@ -513,7 +513,6 @@ namespace storm { friend std::ostream& operator<<(std::ostream& out, BitVector const& bitVector); friend struct std::hash; - friend struct NonZeroBitVectorHash; private: /*! @@ -583,11 +582,6 @@ namespace storm { static const uint_fast64_t mod64mask = (1 << 6) - 1; }; - // A hashing functor that guarantees that the result of the hash is never going to be -1. - struct NonZeroBitVectorHash { - std::size_t operator()(storm::storage::BitVector const& bv) const; - }; - } // namespace storage } // namespace storm diff --git a/src/storm/storage/BitVectorHashMap.cpp b/src/storm/storage/BitVectorHashMap.cpp index dd3e3dbb0..434ab6906 100644 --- a/src/storm/storage/BitVectorHashMap.cpp +++ b/src/storm/storage/BitVectorHashMap.cpp @@ -5,46 +5,47 @@ #include #include "storm/utility/macros.h" +#include "storm/exceptions/InternalException.h" namespace storm { namespace storage { - template - const std::vector BitVectorHashMap::sizes = {5, 13, 31, 79, 163, 277, 499, 1021, 2029, 3989, 8059, 16001, 32099, 64301, 127921, 256499, 511111, 1024901, 2048003, 4096891, 8192411, 15485863, 32142191, 64285127, 128572517, 257148523, 514299959, 102863003}; + template + const std::vector BitVectorHashMap::sizes = {5, 13, 31, 79, 163, 277, 499, 1021, 2029, 3989, 8059, 16001, 32099, 64301, 127921, 256499, 511111, 1024901, 2048003, 4096891, 8192411, 15485863, 32142191, 64285127, 128572517, 257148523, 514299959, 1028599919, 2057199839, 4114399697, 8228799419, 16457598791, 32915197603, 65830395223}; - template - BitVectorHashMap::BitVectorHashMapIterator::BitVectorHashMapIterator(BitVectorHashMap const& map, BitVector::const_iterator indexIt) : map(map), indexIt(indexIt) { + template + BitVectorHashMap::BitVectorHashMapIterator::BitVectorHashMapIterator(BitVectorHashMap const& map, BitVector::const_iterator indexIt) : map(map), indexIt(indexIt) { // Intentionally left empty. } - template - bool BitVectorHashMap::BitVectorHashMapIterator::operator==(BitVectorHashMapIterator const& other) { + template + bool BitVectorHashMap::BitVectorHashMapIterator::operator==(BitVectorHashMapIterator const& other) { return &map == &other.map && *indexIt == *other.indexIt; } - template - bool BitVectorHashMap::BitVectorHashMapIterator::operator!=(BitVectorHashMapIterator const& other) { + template + bool BitVectorHashMap::BitVectorHashMapIterator::operator!=(BitVectorHashMapIterator const& other) { return !(*this == other); } - template - typename BitVectorHashMap::BitVectorHashMapIterator& BitVectorHashMap::BitVectorHashMapIterator::operator++(int) { + template + typename BitVectorHashMap::BitVectorHashMapIterator& BitVectorHashMap::BitVectorHashMapIterator::operator++(int) { ++indexIt; return *this; } - template - typename BitVectorHashMap::BitVectorHashMapIterator& BitVectorHashMap::BitVectorHashMapIterator::operator++() { + template + typename BitVectorHashMap::BitVectorHashMapIterator& BitVectorHashMap::BitVectorHashMapIterator::operator++() { ++indexIt; return *this; } - template - std::pair BitVectorHashMap::BitVectorHashMapIterator::operator*() const { + template + std::pair BitVectorHashMap::BitVectorHashMapIterator::operator*() const { return map.getBucketAndValue(*indexIt); } - template - BitVectorHashMap::BitVectorHashMap(uint64_t bucketSize, uint64_t initialSize, double loadFactor) : loadFactor(loadFactor), bucketSize(bucketSize), numberOfElements(0) { + template + BitVectorHashMap::BitVectorHashMap(uint64_t bucketSize, uint64_t initialSize, double loadFactor) : loadFactor(loadFactor), bucketSize(bucketSize), numberOfElements(0) { STORM_LOG_ASSERT(bucketSize % 64 == 0, "Bucket size must be a multiple of 64."); currentSizeIterator = std::find_if(sizes.begin(), sizes.end(), [=] (uint64_t value) { return value > initialSize; } ); @@ -52,27 +53,42 @@ namespace storm { buckets = storm::storage::BitVector(bucketSize * *currentSizeIterator); occupied = storm::storage::BitVector(*currentSizeIterator); values = std::vector(*currentSizeIterator); + +#ifndef NDEBUG + for (uint64_t i = 0; i < sizes.size() - 1; ++i) { + STORM_LOG_ASSERT(sizes[i] < sizes[i + 1], "Expected stricly increasing sizes."); + } + numberOfInsertions = 0; + numberOfInsertionProbingSteps = 0; + numberOfFinds = 0; + numberOfFindProbingSteps = 0; +#endif } - template - bool BitVectorHashMap::isBucketOccupied(uint_fast64_t bucket) const { + template + bool BitVectorHashMap::isBucketOccupied(uint_fast64_t bucket) const { return occupied.get(bucket); } - template - std::size_t BitVectorHashMap::size() const { + template + std::size_t BitVectorHashMap::size() const { return numberOfElements; } - template - std::size_t BitVectorHashMap::capacity() const { + template + std::size_t BitVectorHashMap::capacity() const { return *currentSizeIterator; } - template - void BitVectorHashMap::increaseSize() { + template + void BitVectorHashMap::increaseSize() { ++currentSizeIterator; STORM_LOG_ASSERT(currentSizeIterator != sizes.end(), "Hash map became to big."); +#ifndef NDEBUG + STORM_LOG_TRACE("Increasing size of hash map from " << *(currentSizeIterator - 1) << " to " << *currentSizeIterator << ". Stats: " << numberOfFinds << " finds (avg. " << (numberOfFindProbingSteps / static_cast(numberOfFinds)) << " probing steps), " << numberOfInsertions << " insertions (avg. " << (numberOfInsertionProbingSteps / static_cast(numberOfInsertions)) << " probing steps)."); +#else + STORM_LOG_TRACE("Increasing size of hash map from " << *(currentSizeIterator - 1) << " to " << *currentSizeIterator << "."); +#endif // Create new containers and swap them with the old ones. numberOfElements = 0; @@ -97,10 +113,10 @@ namespace storm { uint_fast64_t failCount = 0; while (fail) { ++failCount; - STORM_LOG_ASSERT(failCount < 2, "Increasing size failed too often."); + STORM_LOG_THROW(failCount < 2, storm::exceptions::InternalException, "Increasing size failed too often."); ++currentSizeIterator; - STORM_LOG_ASSERT(currentSizeIterator != sizes.end(), "Hash map became to big."); + STORM_LOG_THROW(currentSizeIterator != sizes.end(), storm::exceptions::InternalException, "Hash map became to big."); numberOfElements = 0; buckets = storm::storage::BitVector(bucketSize * *currentSizeIterator); @@ -112,14 +128,14 @@ namespace storm { // If we failed to insert just one element, we have to redo the procedure with a larger container size. if (fail) { - continue; + break; } } } } - template - bool BitVectorHashMap::insertWithoutIncreasingSize(storm::storage::BitVector const& key, ValueType const& value) { + template + bool BitVectorHashMap::insertWithoutIncreasingSize(storm::storage::BitVector const& key, ValueType const& value) { std::tuple flagBucketTuple = this->findBucketToInsert(key); if (std::get<2>(flagBucketTuple)) { return false; @@ -137,18 +153,18 @@ namespace storm { } } - template - ValueType BitVectorHashMap::findOrAdd(storm::storage::BitVector const& key, ValueType const& value) { + template + ValueType BitVectorHashMap::findOrAdd(storm::storage::BitVector const& key, ValueType const& value) { return findOrAddAndGetBucket(key, value).first; } - template - void BitVectorHashMap::setOrAdd(storm::storage::BitVector const& key, ValueType const& value) { + template + void BitVectorHashMap::setOrAdd(storm::storage::BitVector const& key, ValueType const& value) { setOrAddAndGetBucket(key, value); } - template - std::pair BitVectorHashMap::findOrAddAndGetBucket(storm::storage::BitVector const& key, ValueType const& value) { + template + std::pair BitVectorHashMap::findOrAddAndGetBucket(storm::storage::BitVector const& key, ValueType const& value) { // If the load of the map is too high, we increase the size. if (numberOfElements >= loadFactor * *currentSizeIterator) { this->increaseSize(); @@ -168,8 +184,8 @@ namespace storm { } } - template - std::size_t BitVectorHashMap::setOrAddAndGetBucket(storm::storage::BitVector const& key, ValueType const& value) { + template + std::size_t BitVectorHashMap::setOrAddAndGetBucket(storm::storage::BitVector const& key, ValueType const& value) { // If the load of the map is too high, we increase the size. if (numberOfElements >= loadFactor * *currentSizeIterator) { this->increaseSize(); @@ -187,41 +203,56 @@ namespace storm { return std::get<1>(flagBucketTuple); } - template - ValueType BitVectorHashMap::getValue(storm::storage::BitVector const& key) const { + template + ValueType BitVectorHashMap::getValue(storm::storage::BitVector const& key) const { std::pair flagBucketPair = this->findBucket(key); STORM_LOG_ASSERT(flagBucketPair.first, "Unknown key."); return values[flagBucketPair.second]; } - template - bool BitVectorHashMap::contains(storm::storage::BitVector const& key) const { + template + ValueType BitVectorHashMap::getValue(std::size_t bucket) const { + return values[bucket]; + } + + template + bool BitVectorHashMap::contains(storm::storage::BitVector const& key) const { return findBucket(key).first; } - template - typename BitVectorHashMap::const_iterator BitVectorHashMap::begin() const { + template + typename BitVectorHashMap::const_iterator BitVectorHashMap::begin() const { return const_iterator(*this, occupied.begin()); } - template - typename BitVectorHashMap::const_iterator BitVectorHashMap::end() const { + template + typename BitVectorHashMap::const_iterator BitVectorHashMap::end() const { return const_iterator(*this, occupied.end()); } - template - std::pair BitVectorHashMap::findBucket(storm::storage::BitVector const& key) const { - uint_fast64_t initialHash = hasher1(key) % *currentSizeIterator; + template + uint_fast64_t BitVectorHashMap::getNextBucketInProbingSequence(uint_fast64_t, uint_fast64_t currentValue, uint_fast64_t step) const { + return (currentValue + step + step*step) % *currentSizeIterator; + } + + template + std::pair BitVectorHashMap::findBucket(storm::storage::BitVector const& key) const { +#ifndef NDEBUG + ++numberOfFinds; +#endif + uint_fast64_t initialHash = hasher(key) % *currentSizeIterator; uint_fast64_t bucket = initialHash; - - uint_fast64_t counter = 0; + + uint_fast64_t i = 0; while (isBucketOccupied(bucket)) { - ++counter; + ++i; +#ifndef NDEBUG + ++numberOfFindProbingSteps; +#endif if (buckets.matches(bucket * bucketSize, key)) { return std::make_pair(true, bucket); } - bucket += hasher2(key); - bucket %= *currentSizeIterator; + bucket = getNextBucketInProbingSequence(initialHash, bucket, i); if (bucket == initialHash) { return std::make_pair(false, bucket); @@ -231,41 +262,46 @@ namespace storm { return std::make_pair(false, bucket); } - template + template template - std::tuple BitVectorHashMap::findBucketToInsert(storm::storage::BitVector const& key) { - uint_fast64_t initialHash = hasher1(key) % *currentSizeIterator; + std::tuple BitVectorHashMap::findBucketToInsert(storm::storage::BitVector const& key) { +#ifndef NDEBUG + ++numberOfInsertions; +#endif + uint_fast64_t initialHash = hasher(key) % *currentSizeIterator; uint_fast64_t bucket = initialHash; - - uint_fast64_t counter = 0; + + uint64_t i = 0; while (isBucketOccupied(bucket)) { - ++counter; + ++i; +#ifndef NDEBUG + ++numberOfInsertionProbingSteps; +#endif if (buckets.matches(bucket * bucketSize, key)) { return std::make_tuple(true, bucket, false); } - bucket += hasher2(key); - bucket %= *currentSizeIterator; + bucket = getNextBucketInProbingSequence(initialHash, bucket, i); if (bucket == initialHash) { if (increaseStorage) { this->increaseSize(); - bucket = initialHash = hasher1(key) % *currentSizeIterator; + bucket = initialHash = hasher(key) % *currentSizeIterator; } else { return std::make_tuple(false, bucket, true); } } } - + return std::make_tuple(false, bucket, false); } - template - std::pair BitVectorHashMap::getBucketAndValue(std::size_t bucket) const { + template + std::pair BitVectorHashMap::getBucketAndValue(std::size_t bucket) const { return std::make_pair(buckets.get(bucket * bucketSize, bucketSize), values[bucket]); } - template - void BitVectorHashMap::remap(std::function const& remapping) { + template + void BitVectorHashMap::remap(std::function const& remapping) { for (auto pos : occupied) { values[pos] = remapping(values[pos]); } diff --git a/src/storm/storage/BitVectorHashMap.h b/src/storm/storage/BitVectorHashMap.h index a5941e2f8..7c400c1cd 100644 --- a/src/storm/storage/BitVectorHashMap.h +++ b/src/storm/storage/BitVectorHashMap.h @@ -14,7 +14,7 @@ namespace storm { * queries and insertions are supported. Also, the keys must be bit vectors with a length that is a multiple of * 64. */ - template, class Hash2 = storm::storage::NonZeroBitVectorHash> + template> class BitVectorHashMap { public: class BitVectorHashMapIterator { @@ -113,6 +113,13 @@ namespace storm { * @return The value associated with the given key (if any). */ ValueType getValue(storm::storage::BitVector const& key) const; + + /*! + * Retrieves the value associated with the given bucket. + * + * @return The value associated with the given bucket (if any). + */ + ValueType getValue(std::size_t bucket) const; /*! * Checks if the given key is already contained in the map. @@ -204,6 +211,11 @@ namespace storm { */ void increaseSize(); + /*! + * Computes the next bucket in the probing sequence. + */ + uint_fast64_t getNextBucketInProbingSequence(uint_fast64_t initialValue, uint_fast64_t currentValue, uint_fast64_t step) const; + // The load factor determining when the size of the map is increased. double loadFactor; @@ -229,11 +241,18 @@ namespace storm { std::vector::const_iterator currentSizeIterator; // Functor object that are used to perform the actual hashing. - Hash1 hasher1; - Hash2 hasher2; + Hash hasher; // A static table that produces the next possible size of the hash table. static const std::vector sizes; + +#ifndef NDEBUG + // Some performance metrics. + mutable uint64_t numberOfInsertions; + mutable uint64_t numberOfInsertionProbingSteps; + mutable uint64_t numberOfFinds; + mutable uint64_t numberOfFindProbingSteps; +#endif }; } diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index bf1b15d14..d4c9ba5ad 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -897,12 +897,11 @@ namespace storm { // Start by creating a temporary vector that stores for each index whose bit is set to true the number of // bits that were set before that particular index. std::vector columnBitsSetBeforeIndex = columnConstraint.getNumberOfSetBitsBeforeIndices(); - std::vector* rowBitsSetBeforeIndex; - if (&rowGroupConstraint == &columnConstraint) { - rowBitsSetBeforeIndex = &columnBitsSetBeforeIndex; - } else { - rowBitsSetBeforeIndex = new std::vector(rowGroupConstraint.getNumberOfSetBitsBeforeIndices()); + std::unique_ptr> tmp; + if (rowGroupConstraint != columnConstraint) { + tmp = std::make_unique>(rowGroupConstraint.getNumberOfSetBitsBeforeIndices()); } + std::vector const& rowBitsSetBeforeIndex = tmp ? *tmp : columnBitsSetBeforeIndex; // Then, we need to determine the number of entries and the number of rows of the submatrix. index_type subEntries = 0; @@ -917,7 +916,7 @@ namespace storm { if (columnConstraint.get(it->getColumn())) { ++subEntries; - if (columnBitsSetBeforeIndex[it->getColumn()] == (*rowBitsSetBeforeIndex)[index]) { + if (columnBitsSetBeforeIndex[it->getColumn()] == rowBitsSetBeforeIndex[index]) { foundDiagonalElement = true; } } @@ -946,9 +945,9 @@ namespace storm { for (const_iterator it = this->begin(i), ite = this->end(i); it != ite; ++it) { if (columnConstraint.get(it->getColumn())) { - if (columnBitsSetBeforeIndex[it->getColumn()] == (*rowBitsSetBeforeIndex)[index]) { + if (columnBitsSetBeforeIndex[it->getColumn()] == rowBitsSetBeforeIndex[index]) { insertedDiagonalElement = true; - } else if (insertDiagonalEntries && !insertedDiagonalElement && columnBitsSetBeforeIndex[it->getColumn()] > (*rowBitsSetBeforeIndex)[index]) { + } else if (insertDiagonalEntries && !insertedDiagonalElement && columnBitsSetBeforeIndex[it->getColumn()] > rowBitsSetBeforeIndex[index]) { matrixBuilder.addNextValue(rowCount, rowGroupCount, storm::utility::zero()); insertedDiagonalElement = true; } @@ -956,18 +955,13 @@ namespace storm { } } if (insertDiagonalEntries && !insertedDiagonalElement && rowGroupCount < submatrixColumnCount) { - matrixBuilder.addNextValue(rowGroupCount, rowGroupCount, storm::utility::zero()); + matrixBuilder.addNextValue(rowCount, rowGroupCount, storm::utility::zero()); } ++rowCount; } ++rowGroupCount; } - // If the constraints were not the same, we have allocated some additional memory we need to free now. - if (&rowGroupConstraint != &columnConstraint) { - delete rowBitsSetBeforeIndex; - } - return matrixBuilder.build(); } diff --git a/src/storm/storage/expressions/CompiledExpression.cpp b/src/storm/storage/expressions/CompiledExpression.cpp new file mode 100644 index 000000000..759ea899c --- /dev/null +++ b/src/storm/storage/expressions/CompiledExpression.cpp @@ -0,0 +1,21 @@ +#include "storm/storage/expressions/CompiledExpression.h" + +#include "storm/storage/expressions/ExprtkCompiledExpression.h" + +namespace storm { + namespace expressions { + + bool CompiledExpression::isExprtkCompiledExpression() const { + return false; + } + + ExprtkCompiledExpression& CompiledExpression::asExprtkCompiledExpression() { + return static_cast(*this); + } + + ExprtkCompiledExpression const& CompiledExpression::asExprtkCompiledExpression() const { + return static_cast(*this); + } + + } +} diff --git a/src/storm/storage/expressions/CompiledExpression.h b/src/storm/storage/expressions/CompiledExpression.h new file mode 100644 index 000000000..786408c94 --- /dev/null +++ b/src/storm/storage/expressions/CompiledExpression.h @@ -0,0 +1,20 @@ +#pragma once + +namespace storm { + namespace expressions { + + class ExprtkCompiledExpression; + + class CompiledExpression { + public: + + virtual bool isExprtkCompiledExpression() const; + ExprtkCompiledExpression& asExprtkCompiledExpression(); + ExprtkCompiledExpression const& asExprtkCompiledExpression() const; + + private: + // Currently empty. + }; + + } +} diff --git a/src/storm/storage/expressions/Expression.cpp b/src/storm/storage/expressions/Expression.cpp index 95c4f69e0..ed00728f0 100644 --- a/src/storm/storage/expressions/Expression.cpp +++ b/src/storm/storage/expressions/Expression.cpp @@ -9,6 +9,7 @@ #include "storm/storage/expressions/ChangeManagerVisitor.h" #include "storm/storage/expressions/CheckIfThenElseGuardVisitor.h" #include "storm/storage/expressions/Expressions.h" +#include "storm/storage/expressions/CompiledExpression.h" #include "storm/exceptions/InvalidTypeException.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/utility/macros.h" @@ -26,6 +27,11 @@ namespace storm { STORM_LOG_THROW(a.getManager() == b.getManager(), storm::exceptions::InvalidArgumentException, "Expressions are managed by different manager."); } + // Spell out destructor explicitly so we can use forward declarations in the header. + Expression::~Expression() { + // Intentionally left empty. + } + Expression::Expression(std::shared_ptr const& expressionPtr) : expressionPtr(expressionPtr) { // Intentionally left empty. } @@ -196,7 +202,19 @@ namespace storm { return true; } SyntacticalEqualityCheckVisitor checker; - return checker.isSyntaticallyEqual(*this, other); + return checker.isSyntacticallyEqual(*this, other); + } + + bool Expression::hasCompiledExpression() const { + return static_cast(compiledExpression); + } + + void Expression::setCompiledExpression(std::shared_ptr const& compiledExpression) const { + this->compiledExpression = compiledExpression; + } + + CompiledExpression const& Expression::getCompiledExpression() const { + return *compiledExpression; } std::string Expression::toString() const { diff --git a/src/storm/storage/expressions/Expression.h b/src/storm/storage/expressions/Expression.h index 26d6033c6..98a2e6417 100644 --- a/src/storm/storage/expressions/Expression.h +++ b/src/storm/storage/expressions/Expression.h @@ -15,6 +15,7 @@ namespace storm { class ExpressionManager; class Variable; class ExpressionVisitor; + class CompiledExpression; class Expression { public: @@ -58,6 +59,7 @@ namespace storm { friend Expression maximum(Expression const& first, Expression const& second); Expression() = default; + ~Expression(); /*! * Creates an expression representing the given variable. @@ -358,11 +360,29 @@ namespace storm { */ bool isSyntacticallyEqual(storm::expressions::Expression const& other) const; + /*! + * Retrieves whether this expression object has an associated compiled expression. + */ + bool hasCompiledExpression() const; + + /*! + * Associates the given compiled expression with this expression object. + */ + void setCompiledExpression(std::shared_ptr const& compiledExpression) const; + + /*! + * Retrieves the associated compiled expression object (if there is any). + */ + CompiledExpression const& getCompiledExpression() const; + friend std::ostream& operator<<(std::ostream& stream, Expression const& expression); private: // A pointer to the underlying base expression. std::shared_ptr expressionPtr; + + // A pointer to an associated compiled expression object (if any). + mutable std::shared_ptr compiledExpression; }; // Provide operator overloads to conveniently construct new expressions from other expressions. diff --git a/src/storm/storage/expressions/ExprtkCompiledExpression.cpp b/src/storm/storage/expressions/ExprtkCompiledExpression.cpp new file mode 100644 index 000000000..2dda7945d --- /dev/null +++ b/src/storm/storage/expressions/ExprtkCompiledExpression.cpp @@ -0,0 +1,19 @@ +#include "storm/storage/expressions/ExprtkCompiledExpression.h" + +namespace storm { + namespace expressions { + + ExprtkCompiledExpression::ExprtkCompiledExpression(CompiledExpressionType const& exprtkCompiledExpression) : exprtkCompiledExpression(exprtkCompiledExpression) { + // Intentionally left empty. + } + + ExprtkCompiledExpression::CompiledExpressionType const& ExprtkCompiledExpression::getCompiledExpression() const { + return exprtkCompiledExpression; + } + + bool ExprtkCompiledExpression::isExprtkCompiledExpression() const { + return true; + } + + } +} diff --git a/src/storm/storage/expressions/ExprtkCompiledExpression.h b/src/storm/storage/expressions/ExprtkCompiledExpression.h new file mode 100644 index 000000000..b2c98fc2b --- /dev/null +++ b/src/storm/storage/expressions/ExprtkCompiledExpression.h @@ -0,0 +1,25 @@ +#pragma once + +#include "storm/storage/expressions/CompiledExpression.h" + +#include "storm/utility/exprtk.h" + +namespace storm { + namespace expressions { + + class ExprtkCompiledExpression : public CompiledExpression { + public: + typedef exprtk::expression CompiledExpressionType; + + ExprtkCompiledExpression(CompiledExpressionType const& exprtkCompiledExpression); + + CompiledExpressionType const& getCompiledExpression() const; + + virtual bool isExprtkCompiledExpression() const override; + + private: + CompiledExpressionType exprtkCompiledExpression; + }; + + } +} diff --git a/src/storm/storage/expressions/ExprtkExpressionEvaluator.cpp b/src/storm/storage/expressions/ExprtkExpressionEvaluator.cpp index 70cd6e162..3b8b3ea70 100755 --- a/src/storm/storage/expressions/ExprtkExpressionEvaluator.cpp +++ b/src/storm/storage/expressions/ExprtkExpressionEvaluator.cpp @@ -26,34 +26,26 @@ namespace storm { template bool ExprtkExpressionEvaluatorBase::asBool(Expression const& expression) const { - std::shared_ptr expressionPtr = expression.getBaseExpressionPointer(); - auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer()); - if (expressionPair == this->compiledExpressions.end()) { - CompiledExpressionType const& compiledExpression = this->getCompiledExpression(expression); - return compiledExpression.value() == ValueType(1); - } - return expressionPair->second.value() == ValueType(1); + auto const& compiledExpression = getCompiledExpression(expression); + return compiledExpression.value() == ValueType(1); } template int_fast64_t ExprtkExpressionEvaluatorBase::asInt(Expression const& expression) const { - std::shared_ptr expressionPtr = expression.getBaseExpressionPointer(); - auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer()); - if (expressionPair == this->compiledExpressions.end()) { - CompiledExpressionType const& compiledExpression = this->getCompiledExpression(expression); - return static_cast(compiledExpression.value()); - } - return static_cast(expressionPair->second.value()); + auto const& compiledExpression = getCompiledExpression(expression); + return static_cast(compiledExpression.value()); } template - typename ExprtkExpressionEvaluatorBase::CompiledExpressionType& ExprtkExpressionEvaluatorBase::getCompiledExpression(storm::expressions::Expression const& expression) const { - std::pair result = this->compiledExpressions.emplace(expression.getBaseExpressionPointer(), CompiledExpressionType()); - CompiledExpressionType& compiledExpression = result.first->second; - compiledExpression.register_symbol_table(*symbolTable); - bool parsingOk = parser->compile(ToExprtkStringVisitor().toString(expression), compiledExpression); - STORM_LOG_THROW(parsingOk, storm::exceptions::UnexpectedException, "Expression was not properly parsed by ExprTk: " << expression << ". (Returned error: " << parser->error() << ")"); - return compiledExpression; + typename ExprtkExpressionEvaluatorBase::CompiledExpressionType const& ExprtkExpressionEvaluatorBase::getCompiledExpression(storm::expressions::Expression const& expression) const { + if (!expression.hasCompiledExpression() || !expression.getCompiledExpression().isExprtkCompiledExpression()) { + CompiledExpressionType compiledExpression; + compiledExpression.register_symbol_table(*symbolTable); + bool parsingOk = parser->compile(ToExprtkStringVisitor().toString(expression), compiledExpression); + STORM_LOG_THROW(parsingOk, storm::exceptions::UnexpectedException, "Expression was not properly parsed by ExprTk: " << expression << ". (Returned error: " << parser->error() << ")"); + expression.setCompiledExpression(std::make_shared(compiledExpression)); + } + return expression.getCompiledExpression().asExprtkCompiledExpression().getCompiledExpression(); } template @@ -76,13 +68,8 @@ namespace storm { } double ExprtkExpressionEvaluator::asRational(Expression const& expression) const { - std::shared_ptr expressionPtr = expression.getBaseExpressionPointer(); - auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer()); - if (expressionPair == this->compiledExpressions.end()) { - CompiledExpressionType const& compiledExpression = this->getCompiledExpression(expression); - return static_cast(compiledExpression.value()); - } - return static_cast(expressionPair->second.value()); + auto const& compiledExpression = getCompiledExpression(expression); + return static_cast(compiledExpression.value()); } template class ExprtkExpressionEvaluatorBase; diff --git a/src/storm/storage/expressions/ExprtkExpressionEvaluator.h b/src/storm/storage/expressions/ExprtkExpressionEvaluator.h index 1eefe163b..e6a7c6fb4 100755 --- a/src/storm/storage/expressions/ExprtkExpressionEvaluator.h +++ b/src/storm/storage/expressions/ExprtkExpressionEvaluator.h @@ -6,18 +6,12 @@ #include "storm/storage/expressions/ExpressionEvaluatorBase.h" -#pragma clang diagnostic push -#pragma clang diagnostic ignored "-Wunused-variable" - -#pragma GCC diagnostic push - -#include "exprtk.hpp" - -#pragma GCC diagnostic pop -#pragma clang diagnostic pop +#include "storm/utility/exprtk.h" #include "storm/storage/expressions/ToExprtkStringVisitor.h" +#include "storm/storage/expressions/ExprtkCompiledExpression.h" + namespace storm { namespace expressions { template @@ -34,15 +28,14 @@ namespace storm { protected: typedef double ValueType; - typedef exprtk::expression CompiledExpressionType; - typedef std::unordered_map, CompiledExpressionType> CacheType; + typedef ExprtkCompiledExpression::CompiledExpressionType CompiledExpressionType; /*! - * Adds a compiled version of the given expression to the internal storage. + * Retrieves a compiled version of the given expression. * * @param expression The expression that is to be compiled. */ - CompiledExpressionType& getCompiledExpression(storm::expressions::Expression const& expression) const; + CompiledExpressionType const& getCompiledExpression(storm::expressions::Expression const& expression) const; // The parser used. mutable std::unique_ptr> parser; @@ -54,9 +47,6 @@ namespace storm { std::vector booleanValues; std::vector integerValues; std::vector rationalValues; - - // A mapping of expressions to their compiled counterpart. - mutable CacheType compiledExpressions; }; class ExprtkExpressionEvaluator : public ExprtkExpressionEvaluatorBase { diff --git a/src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.cpp b/src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.cpp index c1133c9db..7f45240d7 100644 --- a/src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.cpp +++ b/src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.cpp @@ -5,7 +5,7 @@ namespace storm { namespace expressions { - bool SyntacticalEqualityCheckVisitor::isSyntaticallyEqual(storm::expressions::Expression const& expression1, storm::expressions::Expression const& expression2) { + bool SyntacticalEqualityCheckVisitor::isSyntacticallyEqual(storm::expressions::Expression const& expression1, storm::expressions::Expression const& expression2) { return boost::any_cast(expression1.accept(*this, std::ref(expression2.getBaseExpression()))); } diff --git a/src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.h b/src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.h index ef556d827..2c255b5c2 100644 --- a/src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.h +++ b/src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.h @@ -9,7 +9,7 @@ namespace storm { class SyntacticalEqualityCheckVisitor : public ExpressionVisitor { public: - bool isSyntaticallyEqual(storm::expressions::Expression const& expression1, storm::expressions::Expression const& expression2); + bool isSyntacticallyEqual(storm::expressions::Expression const& expression1, storm::expressions::Expression const& expression2); virtual boost::any visit(IfThenElseExpression const& expression, boost::any const& data) override; virtual boost::any visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) override; diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp index 387423066..9a4132420 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/src/storm/storage/prism/Program.cpp @@ -8,8 +8,6 @@ #include "storm/storage/jani/Property.h" #include "storm/storage/expressions/ExpressionManager.h" -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/IOSettings.h" #include "storm/utility/macros.h" #include "storm/utility/solver.h" #include "storm/utility/vector.h" @@ -138,7 +136,7 @@ namespace storm { std::set appearingModules; }; - Program::Program(std::shared_ptr manager, ModelType modelType, std::vector const& constants, std::vector const& globalBooleanVariables, std::vector const& globalIntegerVariables, std::vector const& formulas, std::vector const& modules, std::map const& actionToIndexMap, std::vector const& rewardModels, std::vector