From c55a654c6ca85e74f6c7730ab89adcb7946a2d15 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 26 Jun 2017 14:22:10 +0200 Subject: [PATCH] fixes and more settings for storm-pars --- src/storm-pars/api/parametric.h | 2 +- src/storm-pars/api/region.h | 76 ++++++++++++------- src/storm-pars/settings/ParsSettings.cpp | 53 +++++++++++++ src/storm-pars/settings/ParsSettings.h | 11 +++ .../settings/modules/ParametricSettings.cpp | 14 +++- .../settings/modules/ParametricSettings.h | 7 ++ .../settings/modules/RegionSettings.cpp | 15 ++-- .../settings/modules/RegionSettings.h | 1 + src/storm-pars/storage/ParameterRegion.cpp | 8 ++ src/storm-pars/storage/ParameterRegion.h | 4 + ...ContinuousToDiscreteTimeModelTransformer.h | 1 + 11 files changed, 153 insertions(+), 39 deletions(-) create mode 100644 src/storm-pars/settings/ParsSettings.cpp create mode 100644 src/storm-pars/settings/ParsSettings.h diff --git a/src/storm-pars/api/parametric.h b/src/storm-pars/api/parametric.h index 66f263a3f..aec977003 100644 --- a/src/storm-pars/api/parametric.h +++ b/src/storm-pars/api/parametric.h @@ -13,7 +13,7 @@ namespace storm { namespace api { template - bool simplifyParametricModel(std::shared_ptr const& inputModel, std::shared_ptr const& inputFormula, std::shared_ptr& outputModel, std::shared_ptr& outputFormula) { + bool simplifyParametricModel(std::shared_ptr> const& inputModel, std::shared_ptr const& inputFormula, std::shared_ptr>& outputModel, std::shared_ptr& outputFormula) { if (inputModel->isOfType(storm::models::ModelType::Dtmc)) { auto const& dtmc = *inputModel->template as>(); diff --git a/src/storm-pars/api/region.h b/src/storm-pars/api/region.h index 8dffe156b..2a5ff9fcd 100644 --- a/src/storm-pars/api/region.h +++ b/src/storm-pars/api/region.h @@ -11,25 +11,21 @@ #include "storm-pars/modelchecker/results/RegionCheckResult.h" #include "storm-pars/modelchecker/results/RegionRefinementCheckResult.h" #include "storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h" +#include "storm-pars/modelchecker/region/RegionCheckEngine.h" #include "storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h" #include "storm-pars/parser/ParameterRegionParser.h" #include "storm/api/transformation.h" +#include "storm/utility/file.h" #include "storm/models/sparse/Model.h" #include "storm/exceptions/UnexpectedException.h" #include "storm/exceptions/InvalidOperationException.h" +#include "storm/exceptions/NotSupportedException.h" namespace storm { namespace api { - - enum class RegionModelCheckerType { - ParameterLifting, - ExactParameterLifting, - ValidatingParameterLifting - }; - template std::vector> parseRegions(std::string const& inputString, std::set::VariableType> const& consideredVariables) { // If the given input string looks like a file (containing a dot and there exists a file with that name), @@ -42,12 +38,33 @@ namespace storm { } template - std::vector> parseRegions(std::string const& inputString, storm::models::sparse::Model const& model) { - auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); - auto rewParameters = storm::models::sparse::getRewardParameters(*model); - modelParameters.insert(rewParameters.begin(), rewParameters.end()); - return parseRegions(inputString, modelParameters); + std::vector> parseRegions(std::string const& inputString, storm::models::ModelBase const& model) { + std::set::VariableType> modelParameters; + if (model.isSparseModel()) { + auto const& sparseModel = dynamic_cast const&>(model); + modelParameters = storm::models::sparse::getProbabilityParameters(sparseModel); + auto rewParameters = storm::models::sparse::getRewardParameters(sparseModel); + modelParameters.insert(rewParameters.begin(), rewParameters.end()); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Retrieving model parameters is not supported for the given model type."); + } + return parseRegions(inputString, modelParameters); + } + + template + storm::storage::ParameterRegion parseRegion(std::string const& inputString, std::set::VariableType> const& consideredVariables) { + auto res = parseRegions(inputString, consideredVariables); + STORM_LOG_THROW(res.size() == 1, storm::exceptions::InvalidOperationException, "Parsed " << res.size() << " regions but exactly one was expected."); + return res.front(); + } + + template + storm::storage::ParameterRegion parseRegion(std::string const& inputString, storm::models::ModelBase const& model) { + auto res = parseRegions(inputString, model); + STORM_LOG_THROW(res.size() == 1, storm::exceptions::InvalidOperationException, "Parsed " << res.size() << " regions but exactly one was expected."); + return res.front(); } + template std::unique_ptr> initializeParameterLiftingRegionModelChecker(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { @@ -57,17 +74,17 @@ namespace storm { std::vector> taskFormulaAsVector { task.getFormula().asSharedPointer() }; auto discreteTimeModel = storm::api::transformContinuousToDiscreteTimeSparseModel(model, taskFormulaAsVector); STORM_LOG_THROW(discreteTimeModel->isOfType(storm::models::ModelType::Dtmc) || discreteTimeModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::UnexpectedException, "Transformation to discrete time model has failed."); - return initializeParameterLiftingRegionModelChecker(discreteTimeModel, task); + return initializeParameterLiftingRegionModelChecker(discreteTimeModel, task); } // Obtain the region model checker std::unique_ptr> result; if (model->isOfType(storm::models::ModelType::Dtmc)) { auto const& dtmc = *model->template as>(); - result = std::make_unique, ConstantType>>(dtmc); + result = std::make_unique, ConstantType>>(dtmc); } else if (model->isOfType(storm::models::ModelType::Mdp)) { auto const& mdp = *model->template as>(); - result = std::make_unique, ConstantType>>(mdp); + result = std::make_unique, ConstantType>>(mdp); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform parameterLifting on the provided model type."); } @@ -78,19 +95,19 @@ namespace storm { } template - std::unique_ptr> initializeValidatingRegionModelChecker(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { + std::unique_ptr> initializeValidatingRegionModelChecker(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { // todo return nullptr; } template - std::unique_ptr> initializeRegionModelChecker(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task, RegionModelCheckerType checkerType) { - switch (checkerType) { - case RegionModelCheckerType::ParameterLifting: + std::unique_ptr> initializeRegionModelChecker(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task, storm::modelchecker::RegionCheckEngine engine) { + switch (engine) { + case storm::modelchecker::RegionCheckEngine::ParameterLifting: return initializeParameterLiftingRegionModelChecker(model, task); - case RegionModelCheckerType::ExactParameterLifting: + case storm::modelchecker::RegionCheckEngine::ExactParameterLifting: return initializeParameterLiftingRegionModelChecker(model, task); - case RegionModelCheckerType::ValidatingParameterLifting: + case storm::modelchecker::RegionCheckEngine::ValidatingParameterLifting: return initializeValidatingRegionModelChecker(model, task); default: STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected region model checker type."); @@ -99,25 +116,28 @@ namespace storm { } template - std::unique_ptr> checkRegionsWithSparseEngine(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task, std::vector> const& regions, RegionModelCheckerType checkerType) { - auto regionChecker = initializeRegionModelChecker(model, task, checkerType); + std::unique_ptr> checkRegionsWithSparseEngine(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task, std::vector> const& regions, storm::modelchecker::RegionCheckEngine engine) { + auto regionChecker = initializeRegionModelChecker(model, task, engine); return regionChecker->analyzeRegions(regions, true); } template - td::unique_ptr> checkAndRefineRegionWithSparseEngine(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task, storm::storage::ParameterRegion const& region, ValueType const& refinementThreshold) { - auto regionChecker = initializeRegionModelChecker(model, task, checkerType); + std::unique_ptr> checkAndRefineRegionWithSparseEngine(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task, storm::storage::ParameterRegion const& region, ValueType const& refinementThreshold, storm::modelchecker::RegionCheckEngine engine) { + auto regionChecker = initializeRegionModelChecker(model, task, engine); return regionChecker->performRegionRefinement(region, refinementThreshold); } template - void exportRegionCheckResultToFile(std::unique_ptr> const& checkResult, std::string const& filename) { + void exportRegionCheckResultToFile(std::unique_ptr const& checkResult, std::string const& filename) { + auto const* regionCheckResult = dynamic_cast const*>(checkResult.get()); + STORM_LOG_THROW(regionCheckResult != nullptr, storm::exceptions::UnexpectedException, "Can not export region check result: The given checkresult does not have the expected type."); + std::ofstream filestream; - storm::utility::openFile(path, filestream); - for (auto const& res : checkResult->getRegionResults()) { + storm::utility::openFile(filename, filestream); + for (auto const& res : regionCheckResult->getRegionResults()) { filestream << res.second << ": " << res.first << std::endl; } } diff --git a/src/storm-pars/settings/ParsSettings.cpp b/src/storm-pars/settings/ParsSettings.cpp new file mode 100644 index 000000000..53907dc1c --- /dev/null +++ b/src/storm-pars/settings/ParsSettings.cpp @@ -0,0 +1,53 @@ +#include "storm-pars/settings/ParsSettings.h" + +#include "storm-pars/settings/modules/ParametricSettings.h" +#include "storm-pars/settings/modules/RegionSettings.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/GeneralSettings.h" +#include "storm/settings/modules/CoreSettings.h" +#include "storm/settings/modules/IOSettings.h" +#include "storm/settings/modules/DebugSettings.h" +#include "storm/settings/modules/SylvanSettings.h" +#include "storm/settings/modules/EigenEquationSolverSettings.h" +#include "storm/settings/modules/GmmxxEquationSolverSettings.h" +#include "storm/settings/modules/NativeEquationSolverSettings.h" +#include "storm/settings/modules/EliminationSettings.h" +#include "storm/settings/modules/MinMaxEquationSolverSettings.h" +#include "storm/settings/modules/GameSolverSettings.h" +#include "storm/settings/modules/BisimulationSettings.h" +#include "storm/settings/modules/TopologicalValueIterationEquationSolverSettings.h" +#include "storm/settings/modules/ResourceSettings.h" +#include "storm/settings/modules/JaniExportSettings.h" +#include "storm/settings/modules/JitBuilderSettings.h" + + +namespace storm { + namespace settings { + void initializeParsSettings(std::string const& name, std::string const& executableName) { + storm::settings::mutableManager().setName(name, executableName); + + // Register relevant settings modules. + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + } + + } +} \ No newline at end of file diff --git a/src/storm-pars/settings/ParsSettings.h b/src/storm-pars/settings/ParsSettings.h new file mode 100644 index 000000000..724fa2a44 --- /dev/null +++ b/src/storm-pars/settings/ParsSettings.h @@ -0,0 +1,11 @@ +#pragma once + +#include + +namespace storm { + namespace settings { + + void initializeParsSettings(std::string const& name, std::string const& executableName); + + } +} \ No newline at end of file diff --git a/src/storm-pars/settings/modules/ParametricSettings.cpp b/src/storm-pars/settings/modules/ParametricSettings.cpp index f57370683..5b7024af8 100644 --- a/src/storm-pars/settings/modules/ParametricSettings.cpp +++ b/src/storm-pars/settings/modules/ParametricSettings.cpp @@ -16,12 +16,15 @@ namespace storm { const std::string ParametricSettings::exportResultOptionName = "resultfile"; const std::string ParametricSettings::simplifyOptionName = "simplify"; const std::string ParametricSettings::derivativesOptionName = "derivatives"; + const std::string ParametricSettings::transformContinuousOptionName = "transformcontinuous"; + const std::string ParametricSettings::transformContinuousShortOptionName = "tc"; ParametricSettings::ParametricSettings() : ModuleSettings(moduleName) { - this->addOption(storm::settings::OptionBuilder(moduleName, exportResultOptionName, true, "A path to a file where the parametric result should be saved.") + this->addOption(storm::settings::OptionBuilder(moduleName, exportResultOptionName, false, "A path to a file where the parametric result should be saved.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "the location.").addValidatorString(ArgumentValidatorFactory::createWritableFileValidator()).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, simplifyOptionName, true, "Sets whether to perform simplification steps before model analysis.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, derivativesOptionName, true, "Sets whether to generate the derivatives of the resulting rational function.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, simplifyOptionName, false, "Sets whether to perform simplification steps before model analysis.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, derivativesOptionName, false, "Sets whether to generate the derivatives of the resulting rational function.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, transformContinuousOptionName, false, "Sets whether to transform a continuous time input model to a discrete time model.").setShortName(transformContinuousShortOptionName).build()); } bool ParametricSettings::exportResultToFile() const { @@ -39,6 +42,11 @@ namespace storm { bool ParametricSettings::isDerivativesSet() const { return this->getOption(derivativesOptionName).getHasOptionBeenSet(); } + + bool ParametricSettings::transformContinuousModel() const { + return this->getOption(transformContinuousOptionName).getHasOptionBeenSet(); + } + } // namespace modules } // namespace settings diff --git a/src/storm-pars/settings/modules/ParametricSettings.h b/src/storm-pars/settings/modules/ParametricSettings.h index 6ba91c80a..9bcfa9ea1 100644 --- a/src/storm-pars/settings/modules/ParametricSettings.h +++ b/src/storm-pars/settings/modules/ParametricSettings.h @@ -41,6 +41,11 @@ namespace storm { * @return True if the derivatives are to be generated. */ bool isDerivativesSet() const; + + /*! + * Retrieves whether Continuous time models should be transformed to discrete time models + */ + bool transformContinuousModel() const; const static std::string moduleName; @@ -48,6 +53,8 @@ namespace storm { const static std::string exportResultOptionName; const static std::string simplifyOptionName; const static std::string derivativesOptionName; + const static std::string transformContinuousOptionName; + const static std::string transformContinuousShortOptionName; }; } // namespace modules diff --git a/src/storm-pars/settings/modules/RegionSettings.cpp b/src/storm-pars/settings/modules/RegionSettings.cpp index daec46863..2dba3c300 100644 --- a/src/storm-pars/settings/modules/RegionSettings.cpp +++ b/src/storm-pars/settings/modules/RegionSettings.cpp @@ -14,25 +14,26 @@ namespace storm { const std::string RegionSettings::moduleName = "region"; const std::string RegionSettings::regionOptionName = "region"; + const std::string RegionSettings::regionShortOptionName = "reg"; const std::string RegionSettings::refineOptionName = "refine"; const std::string RegionSettings::checkEngineOptionName = "engine"; const std::string RegionSettings::printNoIllustrationOptionName = "noillustration"; const std::string RegionSettings::printFullResultOptionName = "printfullresult"; RegionSettings::RegionSettings() : ModuleSettings(moduleName) { - this->addOption(storm::settings::OptionBuilder(moduleName, regionOptionName, true, "Sets the region(s) considered for analysis.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("regioninput", "The region(s) given in format a<=x<=b,c<=y<=d seperated by ';'. Can also be point to a file.").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, regionOptionName, false, "Sets the region(s) considered for analysis.").setShortName(regionShortOptionName) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("regioninput", "The region(s) given in format a<=x<=b,c<=y<=d seperated by ';'. Can also be a file.").build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, refineOptionName, true, "Enables region refinement.") + this->addOption(storm::settings::OptionBuilder(moduleName, refineOptionName, false, "Enables region refinement.") .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("threshold", "Refinement converges if the fraction of unknown area falls below this threshold.").setDefaultValueDouble(0.05).addValidatorDouble(storm::settings::ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0,1.0)).build()).build()); std::vector engines = {"pl", "exactpl", "validatingpl"}; - this->addOption(storm::settings::OptionBuilder(moduleName, checkEngineOptionName, false, "Sets which engine is used for analyzing regions.") + this->addOption(storm::settings::OptionBuilder(moduleName, checkEngineOptionName, true, "Sets which engine is used for analyzing regions.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(engines)).setDefaultValueString("pl").build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, printNoIllustrationOptionName, true, "If set, no illustration of the result is printed.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, printNoIllustrationOptionName, false, "If set, no illustration of the result is printed.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, printFullResultOptionName, true, "If set, the full result for every region is printed.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, printFullResultOptionName, false, "If set, the full result for every region is printed.").build()); } bool RegionSettings::isRegionSet() const { @@ -52,7 +53,7 @@ namespace storm { } storm::modelchecker::RegionCheckEngine RegionSettings::getRegionCheckEngine() const { - std::string engineString = this->getOption(regionOptionName).getArgumentByName("regioninput").getValueAsString(); + std::string engineString = this->getOption(checkEngineOptionName).getArgumentByName("name").getValueAsString(); storm::modelchecker::RegionCheckEngine result; if (engineString == "pl") { diff --git a/src/storm-pars/settings/modules/RegionSettings.h b/src/storm-pars/settings/modules/RegionSettings.h index fc4160f83..e668a3146 100644 --- a/src/storm-pars/settings/modules/RegionSettings.h +++ b/src/storm-pars/settings/modules/RegionSettings.h @@ -59,6 +59,7 @@ namespace storm { private: const static std::string regionOptionName; + const static std::string regionShortOptionName; const static std::string refineOptionName; const static std::string checkEngineOptionName; const static std::string printNoIllustrationOptionName; diff --git a/src/storm-pars/storage/ParameterRegion.cpp b/src/storm-pars/storage/ParameterRegion.cpp index dceaa26ae..bc3e1d0d5 100644 --- a/src/storm-pars/storage/ParameterRegion.cpp +++ b/src/storm-pars/storage/ParameterRegion.cpp @@ -164,8 +164,16 @@ namespace storm { return regionstring; } + template + std::ostream& operator<<(std::ostream& out, ParameterRegion const& region) { + out << region.toString(); + return out; + } + + #ifdef STORM_HAVE_CARL template class ParameterRegion; + template std::ostream& operator<<(std::ostream& out, ParameterRegion const& region); #endif } } diff --git a/src/storm-pars/storage/ParameterRegion.h b/src/storm-pars/storage/ParameterRegion.h index 76e645683..c09c78733 100644 --- a/src/storm-pars/storage/ParameterRegion.h +++ b/src/storm-pars/storage/ParameterRegion.h @@ -70,6 +70,10 @@ namespace storm { Valuation upperBoundaries; std::set variables; }; + + template + std::ostream& operator<<(std::ostream& out, ParameterRegion const& region); + } } diff --git a/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.h b/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.h index a84f19faa..d26b96c1f 100644 --- a/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.h +++ b/src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.h @@ -14,6 +14,7 @@ namespace storm { template > class ContinuousToDiscreteTimeModelTransformer { + public: // If this method returns true, the given formula is preserced by the transformation static bool preservesFormula(storm::logic::Formula const& formula);