From c6c6f45483bf01787de9b2619846ca989e69bf3a Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 18 Feb 2020 13:48:25 +0100
Subject: [PATCH] Fixed compilation for storm-pars and storm-pomdp
---
src/storm-pars-cli/storm-pars.cpp | 41 ++++++++++++++---------------
src/storm-pomdp-cli/storm-pomdp.cpp | 10 +++----
2 files changed, 25 insertions(+), 26 deletions(-)
diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp
index a8f98fbdc..0b7ff3bbd 100644
--- a/src/storm-pars-cli/storm-pars.cpp
+++ b/src/storm-pars-cli/storm-pars.cpp
@@ -158,8 +158,7 @@ namespace storm {
}
template <typename ValueType>
- PreprocessResult preprocessSparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input) {
- auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
+ PreprocessResult preprocessSparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input, storm::cli::ModelProcessingInformation const& mpi) {
auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
auto parametricSettings = storm::settings::getModule<storm::settings::modules::ParametricSettings>();
auto transformationSettings = storm::settings::getModule<storm::settings::modules::TransformationSettings>();
@@ -171,7 +170,7 @@ namespace storm {
result.changed = true;
}
- if (generalSettings.isBisimulationSet()) {
+ if (mpi.applyBisimulation) {
result.model = storm::cli::preprocessSparseModelBisimulation(result.model->template as<storm::models::sparse::Model<ValueType>>(), input, bisimulationSettings);
result.changed = true;
}
@@ -200,27 +199,26 @@ namespace storm {
}
template <storm::dd::DdType DdType, typename ValueType>
- PreprocessResult preprocessDdModel(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input, storm::utility::Engine const& engine) {
- auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
+ PreprocessResult preprocessDdModel(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input, storm::cli::ModelProcessingInformation const& mpi) {
auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
PreprocessResult result(model, false);
- if (engine == storm::utility::Engine::Hybrid) {
+ if (mpi.engine == storm::utility::Engine::Hybrid) {
// Currently, hybrid engine for parametric models just refers to building the model symbolically.
STORM_LOG_INFO("Translating symbolic model to sparse model...");
result.model = storm::api::transformSymbolicToSparseModel(model);
result.changed = true;
// Invoke preprocessing on the sparse model
- PreprocessResult sparsePreprocessingResult = storm::pars::preprocessSparseModel<ValueType>(result.model->as<storm::models::sparse::Model<ValueType>>(), input);
+ PreprocessResult sparsePreprocessingResult = storm::pars::preprocessSparseModel<ValueType>(result.model->as<storm::models::sparse::Model<ValueType>>(), input, mpi);
if (sparsePreprocessingResult.changed) {
result.model = sparsePreprocessingResult.model;
result.formulas = sparsePreprocessingResult.formulas;
}
} else {
- STORM_LOG_ASSERT(engine == storm::utility::Engine::Dd, "Expected Dd engine.");
- if (generalSettings.isBisimulationSet()) {
- result.model = storm::cli::preprocessDdModelBisimulation(result.model->template as<storm::models::symbolic::Model<DdType, ValueType>>(), input, bisimulationSettings);
+ STORM_LOG_ASSERT(mpi.engine == storm::utility::Engine::Dd, "Expected Dd engine.");
+ if (mpi.applyBisimulation) {
+ result.model = storm::cli::preprocessDdModelBisimulation(result.model->template as<storm::models::symbolic::Model<DdType, ValueType>>(), input, bisimulationSettings, mpi);
result.changed = true;
}
}
@@ -228,15 +226,15 @@ namespace storm {
}
template <storm::dd::DdType DdType, typename ValueType>
- PreprocessResult preprocessModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input, storm::utility::Engine const& engine) {
+ PreprocessResult preprocessModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input, storm::cli::ModelProcessingInformation const& mpi) {
storm::utility::Stopwatch preprocessingWatch(true);
PreprocessResult result(model, false);
if (model->isSparseModel()) {
- result = storm::pars::preprocessSparseModel<ValueType>(result.model->as<storm::models::sparse::Model<ValueType>>(), input);
+ result = storm::pars::preprocessSparseModel<ValueType>(result.model->as<storm::models::sparse::Model<ValueType>>(), input, mpi);
} else {
STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type.");
- result = storm::pars::preprocessDdModel<DdType, ValueType>(result.model->as<storm::models::symbolic::Model<DdType, ValueType>>(), input, engine);
+ result = storm::pars::preprocessDdModel<DdType, ValueType>(result.model->as<storm::models::symbolic::Model<DdType, ValueType>>(), input, mpi);
}
if (result.changed) {
@@ -565,17 +563,17 @@ namespace storm {
}
template <storm::dd::DdType DdType, typename ValueType>
- void processInputWithValueTypeAndDdlib(SymbolicInput& input, storm::utility::Engine const& engine) {
+ void processInputWithValueTypeAndDdlib(SymbolicInput& input, storm::cli::ModelProcessingInformation const& mpi) {
auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
auto parSettings = storm::settings::getModule<storm::settings::modules::ParametricSettings>();
auto monSettings = storm::settings::getModule<storm::settings::modules::MonotonicitySettings>();
- STORM_LOG_THROW(engine == storm::utility::Engine::Sparse || engine == storm::utility::Engine::Hybrid || engine == storm::utility::Engine::Dd, storm::exceptions::InvalidSettingsException, "The selected engine is not supported for parametric models.");
+ STORM_LOG_THROW(mpi.engine == storm::utility::Engine::Sparse || mpi.engine == storm::utility::Engine::Hybrid || mpi.engine == storm::utility::Engine::Dd, storm::exceptions::InvalidSettingsException, "The selected engine is not supported for parametric models.");
std::shared_ptr<storm::models::ModelBase> model;
if (!buildSettings.isNoBuildModelSet()) {
- model = storm::cli::buildModel<DdType, ValueType>(engine, input, ioSettings);
+ model = storm::cli::buildModel<DdType, ValueType>(input, ioSettings, mpi);
}
if (model) {
@@ -587,7 +585,7 @@ namespace storm {
if (model) {
- auto preprocessingResult = storm::pars::preprocessModel<DdType, ValueType>(model, input, engine);
+ auto preprocessingResult = storm::pars::preprocessModel<DdType, ValueType>(model, input, mpi);
if (preprocessingResult.changed) {
model = preprocessingResult.model;
@@ -641,7 +639,7 @@ namespace storm {
}
if (model) {
- auto preprocessingResult = storm::pars::preprocessModel<DdType, ValueType>(model, input, engine);
+ auto preprocessingResult = storm::pars::preprocessModel<DdType, ValueType>(model, input, mpi);
if (preprocessingResult.changed) {
model = preprocessingResult.model;
@@ -784,9 +782,10 @@ namespace storm {
STORM_LOG_WARN_COND(engine != storm::utility::Engine::Dd || engine != storm::utility::Engine::Hybrid || coreSettings.getDdLibraryType() == storm::dd::DdType::Sylvan, "The selected DD library does not support parametric models. Switching to Sylvan...");
// Parse and preprocess symbolic input (PRISM, JANI, properties, etc.)
- SymbolicInput symbolicInput = storm::cli::parseAndPreprocessSymbolicInput(engine);
-
- processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, storm::RationalFunction>(symbolicInput, engine);
+ auto symbolicInput = storm::cli::parseSymbolicInput();
+ auto mpi = storm::cli::getModelProcessingInformation(symbolicInput);
+ symbolicInput = storm::cli::preprocessSymbolicInput(symbolicInput, mpi.engine);
+ processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, storm::RationalFunction>(symbolicInput, mpi);
}
}
diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp
index 25c0ac954..3da5f6662 100644
--- a/src/storm-pomdp-cli/storm-pomdp.cpp
+++ b/src/storm-pomdp-cli/storm-pomdp.cpp
@@ -98,12 +98,12 @@ int main(const int argc, const char** argv) {
auto const& coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
auto const& pomdpSettings = storm::settings::getModule<storm::settings::modules::POMDPSettings>();
- // For several engines, no model building step is performed, but the verification is started right away.
- storm::utility::Engine engine = coreSettings.getEngine();
-
- storm::cli::SymbolicInput symbolicInput = storm::cli::parseAndPreprocessSymbolicInput(engine);
+ auto symbolicInput = storm::cli::parseSymbolicInput();
+ auto mpi = storm::cli::getModelProcessingInformation(symbolicInput);
+ symbolicInput = storm::cli::preprocessSymbolicInput(symbolicInput, mpi.engine);
+
// We should not export here if we are going to do some processing first.
- auto model = storm::cli::buildPreprocessExportModelWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, storm::RationalNumber>(symbolicInput, engine);
+ auto model = storm::cli::buildPreprocessExportModelWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, storm::RationalNumber>(symbolicInput, mpi);
STORM_LOG_THROW(model && model->getType() == storm::models::ModelType::Pomdp, storm::exceptions::WrongFormatException, "Expected a POMDP.");
std::shared_ptr<storm::models::sparse::Pomdp<storm::RationalNumber>> pomdp = model->template as<storm::models::sparse::Pomdp<storm::RationalNumber>>();
storm::transformer::MakePOMDPCanonic<storm::RationalNumber> makeCanonic(*pomdp);