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

fixes and more settings for storm-pars

tempestpy_adaptions
TimQu 8 years ago
parent
9f82c34429
commit
c55a654c6c
11 changed files with 153 additions and 39 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. 2
      src/storm-pars/api/parametric.h
  2. 76
      src/storm-pars/api/region.h
  3. 53
      src/storm-pars/settings/ParsSettings.cpp
  4. 11
      src/storm-pars/settings/ParsSettings.h
  5. 14
      src/storm-pars/settings/modules/ParametricSettings.cpp
  6. 7
      src/storm-pars/settings/modules/ParametricSettings.h
  7. 15
      src/storm-pars/settings/modules/RegionSettings.cpp
  8. 1
      src/storm-pars/settings/modules/RegionSettings.h
  9. 8
      src/storm-pars/storage/ParameterRegion.cpp
  10. 4
      src/storm-pars/storage/ParameterRegion.h
  11. 1
      src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.h

2
src/storm-pars/api/parametric.h
View File

@ -13,7 +13,7 @@ namespace storm {
namespace api {
template <typename ValueType>
bool simplifyParametricModel(std::shared_ptr<storm::models::sparse::Model<ValueType> const& inputModel, std::shared_ptr<storm::logic::Formula const> const& inputFormula, std::shared_ptr<storm::models::sparse::Model<ValueType>& outputModel, std::shared_ptr<storm::logic::Formula const>& outputFormula) {
bool simplifyParametricModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& inputModel, std::shared_ptr<storm::logic::Formula const> const& inputFormula, std::shared_ptr<storm::models::sparse::Model<ValueType>>& outputModel, std::shared_ptr<storm::logic::Formula const>& outputFormula) {
if (inputModel->isOfType(storm::models::ModelType::Dtmc)) {
auto const& dtmc = *inputModel->template as<storm::models::sparse::Dtmc<ValueType>>();

76
src/storm-pars/api/region.h
View File

@ -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 <typename ValueType>
std::vector<storm::storage::ParameterRegion<ValueType>> parseRegions(std::string const& inputString, std::set<typename storm::storage::ParameterRegion<ValueType>::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 <typename ValueType>
std::vector<storm::storage::ParameterRegion<ValueType>> parseRegions(std::string const& inputString, storm::models::sparse::Model<ValueType> 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<storm::storage::ParameterRegion<ValueType>> parseRegions(std::string const& inputString, storm::models::ModelBase const& model) {
std::set<typename storm::storage::ParameterRegion<ValueType>::VariableType> modelParameters;
if (model.isSparseModel()) {
auto const& sparseModel = dynamic_cast<storm::models::sparse::Model<ValueType> 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<ValueType>(inputString, modelParameters);
}
template <typename ValueType>
storm::storage::ParameterRegion<ValueType> parseRegion(std::string const& inputString, std::set<typename storm::storage::ParameterRegion<ValueType>::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 <typename ValueType>
storm::storage::ParameterRegion<ValueType> 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 <typename ParametricType, typename ConstantType>
std::unique_ptr<storm::modelchecker::RegionModelChecker<ParametricType>> initializeParameterLiftingRegionModelChecker(std::shared_ptr<storm::models::sparse::Model<ParametricType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ParametricType> const& task) {
@ -57,17 +74,17 @@ namespace storm {
std::vector<std::shared_ptr<storm::logic::Formula const>> 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<ParametricType, ConstantType>(discreteTimeModel, task);
}
// Obtain the region model checker
std::unique_ptr<storm::modelchecker::RegionModelChecker<ParametricType>> result;
if (model->isOfType(storm::models::ModelType::Dtmc)) {
auto const& dtmc = *model->template as<storm::models::sparse::Dtmc<ParametricType>>();
result = std::make_unique<storm::modelchecker::SparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<ValueType>, ConstantType>>(dtmc);
result = std::make_unique<storm::modelchecker::SparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<ParametricType>, ConstantType>>(dtmc);
} else if (model->isOfType(storm::models::ModelType::Mdp)) {
auto const& mdp = *model->template as<storm::models::sparse::Mdp<ParametricType>>();
result = std::make_unique<storm::modelchecker::SparseMdpParameterLiftingModelChecker<storm::models::sparse::Mdp<ValueType>, ConstantType>>(mdp);
result = std::make_unique<storm::modelchecker::SparseMdpParameterLiftingModelChecker<storm::models::sparse::Mdp<ParametricType>, 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 <typename ParametricType, typename ImpreciseType, typename PreciseType>
std::unique_ptr<storm::modelchecker::RegionModelChecker<ValueType>> initializeValidatingRegionModelChecker(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ParametricType> const& task) {
std::unique_ptr<storm::modelchecker::RegionModelChecker<ParametricType>> initializeValidatingRegionModelChecker(std::shared_ptr<storm::models::sparse::Model<ParametricType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ParametricType> const& task) {
// todo
return nullptr;
}
template <typename ValueType>
std::unique_ptr<storm::modelchecker::RegionModelChecker<ValueType>> initializeRegionModelChecker(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task, RegionModelCheckerType checkerType) {
switch (checkerType) {
case RegionModelCheckerType::ParameterLifting:
std::unique_ptr<storm::modelchecker::RegionModelChecker<ValueType>> initializeRegionModelChecker(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task, storm::modelchecker::RegionCheckEngine engine) {
switch (engine) {
case storm::modelchecker::RegionCheckEngine::ParameterLifting:
return initializeParameterLiftingRegionModelChecker<ValueType, double>(model, task);
case RegionModelCheckerType::ExactParameterLifting:
case storm::modelchecker::RegionCheckEngine::ExactParameterLifting:
return initializeParameterLiftingRegionModelChecker<ValueType, storm::RationalNumber>(model, task);
case RegionModelCheckerType::ValidatingParameterLifting:
case storm::modelchecker::RegionCheckEngine::ValidatingParameterLifting:
return initializeValidatingRegionModelChecker<ValueType, double, storm::RationalNumber>(model, task);
default:
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected region model checker type.");
@ -99,25 +116,28 @@ namespace storm {
}
template <typename ValueType>
std::unique_ptr<storm::modelchecker::RegionCheckResult<ValueType>> checkRegionsWithSparseEngine(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task, std::vector<storm::storage::ParameterRegion<ValueType>> const& regions, RegionModelCheckerType checkerType) {
auto regionChecker = initializeRegionModelChecker(model, task, checkerType);
std::unique_ptr<storm::modelchecker::RegionCheckResult<ValueType>> checkRegionsWithSparseEngine(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task, std::vector<storm::storage::ParameterRegion<ValueType>> const& regions, storm::modelchecker::RegionCheckEngine engine) {
auto regionChecker = initializeRegionModelChecker(model, task, engine);
return regionChecker->analyzeRegions(regions, true);
}
template <typename ValueType>
td::unique_ptr<storm::modelchecker::RegionRefinementCheckResult<ValueType>> checkAndRefineRegionWithSparseEngine(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task, storm::storage::ParameterRegion<ValueType> const& region, ValueType const& refinementThreshold) {
auto regionChecker = initializeRegionModelChecker(model, task, checkerType);
std::unique_ptr<storm::modelchecker::RegionRefinementCheckResult<ValueType>> checkAndRefineRegionWithSparseEngine(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task, storm::storage::ParameterRegion<ValueType> const& region, ValueType const& refinementThreshold, storm::modelchecker::RegionCheckEngine engine) {
auto regionChecker = initializeRegionModelChecker(model, task, engine);
return regionChecker->performRegionRefinement(region, refinementThreshold);
}
template <typename ValueType>
void exportRegionCheckResultToFile(std::unique_ptr<storm::modelchecker::RegionCheckResult<ValueType>> const& checkResult, std::string const& filename) {
void exportRegionCheckResultToFile(std::unique_ptr<storm::modelchecker::CheckResult> const& checkResult, std::string const& filename) {
auto const* regionCheckResult = dynamic_cast<storm::modelchecker::RegionCheckResult<ValueType> 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;
}
}

53
src/storm-pars/settings/ParsSettings.cpp
View File

@ -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::modules::GeneralSettings>();
storm::settings::addModule<storm::settings::modules::IOSettings>();
storm::settings::addModule<storm::settings::modules::CoreSettings>();
storm::settings::addModule<storm::settings::modules::ParametricSettings>();
storm::settings::addModule<storm::settings::modules::RegionSettings>();
storm::settings::addModule<storm::settings::modules::DebugSettings>();
storm::settings::addModule<storm::settings::modules::SylvanSettings>();
storm::settings::addModule<storm::settings::modules::GmmxxEquationSolverSettings>();
storm::settings::addModule<storm::settings::modules::EigenEquationSolverSettings>();
storm::settings::addModule<storm::settings::modules::NativeEquationSolverSettings>();
storm::settings::addModule<storm::settings::modules::EliminationSettings>();
storm::settings::addModule<storm::settings::modules::MinMaxEquationSolverSettings>();
storm::settings::addModule<storm::settings::modules::GameSolverSettings>();
storm::settings::addModule<storm::settings::modules::BisimulationSettings>();
storm::settings::addModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>();
storm::settings::addModule<storm::settings::modules::ResourceSettings>();
storm::settings::addModule<storm::settings::modules::JaniExportSettings>();
storm::settings::addModule<storm::settings::modules::JitBuilderSettings>();
}
}
}

11
src/storm-pars/settings/ParsSettings.h
View File

@ -0,0 +1,11 @@
#pragma once
#include <string>
namespace storm {
namespace settings {
void initializeParsSettings(std::string const& name, std::string const& executableName);
}
}

14
src/storm-pars/settings/modules/ParametricSettings.cpp
View File

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

7
src/storm-pars/settings/modules/ParametricSettings.h
View File

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

15
src/storm-pars/settings/modules/RegionSettings.cpp
View File

@ -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<std::string> 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") {

1
src/storm-pars/settings/modules/RegionSettings.h
View File

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

8
src/storm-pars/storage/ParameterRegion.cpp
View File

@ -164,8 +164,16 @@ namespace storm {
return regionstring;
}
template <typename ParametricType>
std::ostream& operator<<(std::ostream& out, ParameterRegion<ParametricType> const& region) {
out << region.toString();
return out;
}
#ifdef STORM_HAVE_CARL
template class ParameterRegion<storm::RationalFunction>;
template std::ostream& operator<<(std::ostream& out, ParameterRegion<storm::RationalFunction> const& region);
#endif
}
}

4
src/storm-pars/storage/ParameterRegion.h
View File

@ -70,6 +70,10 @@ namespace storm {
Valuation upperBoundaries;
std::set<VariableType> variables;
};
template<typename ParametricType>
std::ostream& operator<<(std::ostream& out, ParameterRegion<ParametricType> const& region);
}
}

1
src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.h
View File

@ -14,6 +14,7 @@ namespace storm {
template <typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>>
class ContinuousToDiscreteTimeModelTransformer {
public:
// If this method returns true, the given formula is preserced by the transformation
static bool preservesFormula(storm::logic::Formula const& formula);

Write Preview
Loading…
Cancel
Save