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

CLI: Provide the engine as a parameter in most of the CLI options.

main
Tim Quatmann 6 years ago
parent
17325419fb
commit
739151af8d
2 changed files with 26 additions and 36 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 37
      src/storm-cli-utilities/model-handling.h
  2. 25
      src/storm-pars-cli/storm-pars.cpp

37
src/storm-cli-utilities/model-handling.h
View File

@ -443,7 +443,7 @@ namespace storm {
}
template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType = ValueType>
std::pair<std::shared_ptr<storm::models::ModelBase>, bool> preprocessDdModel(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input) {
std::pair<std::shared_ptr<storm::models::ModelBase>, bool> preprocessDdModel(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input, storm::utility::Engine const& engine) {
auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
std::pair<std::shared_ptr<storm::models::Model<ValueType>>, bool> intermediateResult = std::make_pair(model, false);
@ -462,7 +462,7 @@ namespace storm {
result = std::make_unique<std::pair<std::shared_ptr<storm::models::Model<ExportValueType>>, bool>>(symbolicModel->template toValueType<ExportValueType>(), !std::is_same<ValueType, ExportValueType>::value);
}
if (result && result->first->isSymbolicModel() && storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::utility::Engine::DdSparse) {
if (result && result->first->isSymbolicModel() && engine == storm::utility::Engine::DdSparse) {
// Mark as changed.
result->second = true;
@ -479,7 +479,7 @@ namespace storm {
}
template <storm::dd::DdType DdType, typename BuildValueType, typename ExportValueType = BuildValueType>
std::pair<std::shared_ptr<storm::models::ModelBase>, bool> preprocessModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input) {
std::pair<std::shared_ptr<storm::models::ModelBase>, bool> preprocessModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input, storm::utility::Engine const& engine) {
storm::utility::Stopwatch preprocessingWatch(true);
std::pair<std::shared_ptr<storm::models::ModelBase>, bool> result = std::make_pair(model, false);
@ -487,7 +487,7 @@ namespace storm {
result = preprocessSparseModel<BuildValueType>(result.first->as<storm::models::sparse::Model<BuildValueType>>(), input);
} else {
STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type.");
result = preprocessDdModel<DdType, BuildValueType, ExportValueType>(result.first->as<storm::models::symbolic::Model<DdType, BuildValueType>>(), input);
result = preprocessDdModel<DdType, BuildValueType, ExportValueType>(result.first->as<storm::models::symbolic::Model<DdType, BuildValueType>>(), input, engine);
}
preprocessingWatch.stop();
@ -885,8 +885,7 @@ namespace storm {
}
template <storm::dd::DdType DdType, typename ValueType>
typename std::enable_if<DdType != storm::dd::DdType::CUDD || std::is_same<ValueType, double>::value, void>::type verifySymbolicModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input, storm::settings::modules::CoreSettings const& coreSettings) {
storm::utility::Engine engine = coreSettings.getEngine();;
typename std::enable_if<DdType != storm::dd::DdType::CUDD || std::is_same<ValueType, double>::value, void>::type verifySymbolicModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input, storm::utility::Engine const& engine) {
if (engine == storm::utility::Engine::Hybrid) {
verifyWithHybridEngine<DdType, ValueType>(model, input);
} else if (engine == storm::utility::Engine::Dd) {
@ -897,17 +896,17 @@ namespace storm {
}
template <storm::dd::DdType DdType, typename ValueType>
typename std::enable_if<DdType == storm::dd::DdType::CUDD && !std::is_same<ValueType, double>::value, void>::type verifySymbolicModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input, storm::settings::modules::CoreSettings const& coreSettings) {
typename std::enable_if<DdType == storm::dd::DdType::CUDD && !std::is_same<ValueType, double>::value, void>::type verifySymbolicModel(std::shared_ptr<storm::models::ModelBase> const&, SymbolicInput const& , storm::utility::Engine const&) {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "CUDD does not support the selected data-type.");
}
template <storm::dd::DdType DdType, typename ValueType>
void verifyModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input, storm::settings::modules::CoreSettings const& coreSettings) {
void verifyModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input, storm::utility::Engine const& engine) {
if (model->isSparseModel()) {
verifyWithSparseEngine<ValueType>(model, input);
} else {
STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type.");
verifySymbolicModel<DdType, ValueType>(model, input, coreSettings);
verifySymbolicModel<DdType, ValueType>(model, input, engine);
}
}
@ -927,7 +926,7 @@ namespace storm {
STORM_LOG_THROW(model || input.properties.empty(), storm::exceptions::InvalidSettingsException, "No input model.");
if (model) {
auto preprocessingResult = preprocessModel<DdType, BuildValueType, VerificationValueType>(model, input);
auto preprocessingResult = preprocessModel<DdType, BuildValueType, VerificationValueType>(model, input, engine);
if (preprocessingResult.second) {
model = preprocessingResult.first;
model->printModelInformationToStream(std::cout);
@ -938,48 +937,44 @@ namespace storm {
}
template <storm::dd::DdType DdType, typename BuildValueType, typename VerificationValueType = BuildValueType>
void processInputWithValueTypeAndDdlib(SymbolicInput const& input) {
auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
void processInputWithValueTypeAndDdlib(SymbolicInput const& input, storm::utility::Engine const& engine) {
auto abstractionSettings = storm::settings::getModule<storm::settings::modules::AbstractionSettings>();
auto counterexampleSettings = storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>();
// For several engines, no model building step is performed, but the verification is started right away.
storm::utility::Engine engine = coreSettings.getEngine();
if (engine == storm::utility::Engine::AbstractionRefinement && abstractionSettings.getAbstractionRefinementMethod() == storm::settings::modules::AbstractionSettings::Method::Games) {
verifyWithAbstractionRefinementEngine<DdType, VerificationValueType>(input);
} else if (engine == storm::utility::Engine::Exploration) {
verifyWithExplorationEngine<VerificationValueType>(input);
} else {
std::shared_ptr<storm::models::ModelBase> model = buildPreprocessExportModelWithValueTypeAndDdlib<DdType, BuildValueType, VerificationValueType>(input, engine);
if (model) {
if (counterexampleSettings.isCounterexampleSet()) {
generateCounterexamples<VerificationValueType>(model, input);
} else {
verifyModel<DdType, VerificationValueType>(model, input, coreSettings);
verifyModel<DdType, VerificationValueType>(model, input, engine);
}
}
}
}
template <typename ValueType>
void processInputWithValueType(SymbolicInput const& input) {
void processInputWithValueType(SymbolicInput const& input, storm::utility::Engine const& engine) {
auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
if (coreSettings.getDdLibraryType() == storm::dd::DdType::CUDD && coreSettings.isDdLibraryTypeSetFromDefaultValue() && generalSettings.isExactSet()) {
STORM_LOG_INFO("Switching to DD library sylvan to allow for rational arithmetic.");
processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, storm::RationalNumber>(input);
processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, storm::RationalNumber>(input, engine);
} else if (coreSettings.getDdLibraryType() == storm::dd::DdType::CUDD && coreSettings.isDdLibraryTypeSetFromDefaultValue() && std::is_same<ValueType, double>::value && generalSettings.isBisimulationSet() && bisimulationSettings.useExactArithmeticInDdBisimulation()) {
STORM_LOG_INFO("Switching to DD library sylvan to allow for rational arithmetic.");
processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, storm::RationalNumber, double>(input);
processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, storm::RationalNumber, double>(input, engine);
} else if (coreSettings.getDdLibraryType() == storm::dd::DdType::CUDD) {
processInputWithValueTypeAndDdlib<storm::dd::DdType::CUDD, double>(input);
processInputWithValueTypeAndDdlib<storm::dd::DdType::CUDD, double>(input, engine);
} else {
STORM_LOG_ASSERT(coreSettings.getDdLibraryType() == storm::dd::DdType::Sylvan, "Unknown DD library.");
processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, ValueType>(input);
processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, ValueType>(input, engine);
}
}

25
src/storm-pars-cli/storm-pars.cpp
View File

@ -200,14 +200,13 @@ 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) {
auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
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>();
auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
PreprocessResult result(model, false);
if (coreSettings.getEngine() == storm::utility::Engine::Hybrid) {
if (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);
@ -219,7 +218,7 @@ namespace storm {
result.formulas = sparsePreprocessingResult.formulas;
}
} else {
STORM_LOG_ASSERT(coreSettings.getEngine() == storm::utility::Engine::Dd, "Expected Dd engine.");
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);
result.changed = true;
@ -229,7 +228,7 @@ namespace storm {
}
template <storm::dd::DdType DdType, typename ValueType>
PreprocessResult preprocessModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input) {
PreprocessResult preprocessModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input, storm::utility::Engine const& engine) {
storm::utility::Stopwatch preprocessingWatch(true);
PreprocessResult result(model, false);
@ -237,7 +236,7 @@ namespace storm {
result = storm::pars::preprocessSparseModel<ValueType>(result.model->as<storm::models::sparse::Model<ValueType>>(), input);
} 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);
result = storm::pars::preprocessDdModel<DdType, ValueType>(result.model->as<storm::models::symbolic::Model<DdType, ValueType>>(), input, engine);
}
if (result.changed) {
@ -565,17 +564,13 @@ namespace storm {
}
}
template <storm::dd::DdType DdType, typename ValueType>
void processInputWithValueTypeAndDdlib(SymbolicInput& input) {
auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
void processInputWithValueTypeAndDdlib(SymbolicInput& input, storm::utility::Engine const& engine) {
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>();
auto engine = coreSettings.getEngine();
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.");
std::shared_ptr<storm::models::ModelBase> model;
@ -592,7 +587,7 @@ namespace storm {
if (model) {
auto preprocessingResult = storm::pars::preprocessModel<DdType, ValueType>(model, input);
auto preprocessingResult = storm::pars::preprocessModel<DdType, ValueType>(model, input, engine);
if (preprocessingResult.changed) {
model = preprocessingResult.model;
@ -646,7 +641,7 @@ namespace storm {
}
if (model) {
auto preprocessingResult = storm::pars::preprocessModel<DdType, ValueType>(model, input);
auto preprocessingResult = storm::pars::preprocessModel<DdType, ValueType>(model, input, engine);
if (preprocessingResult.changed) {
model = preprocessingResult.model;
@ -791,7 +786,7 @@ namespace storm {
// Parse and preprocess symbolic input (PRISM, JANI, properties, etc.)
SymbolicInput symbolicInput = storm::cli::parseAndPreprocessSymbolicInput(engine);
processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, storm::RationalFunction>(symbolicInput);
processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, storm::RationalFunction>(symbolicInput, engine);
}
}

Write Preview
Loading…
Cancel
Save