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

started on enabling sampling of parametric models from command line

main
dehnert 7 years ago
parent
601b73608a
commit
10da10a7d1
3 changed files with 145 additions and 26 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 152
      src/storm-pars-cli/storm-pars.cpp
  2. 7
      src/storm-pars/settings/modules/ParametricSettings.cpp
  3. 8
      src/storm-pars/settings/modules/ParametricSettings.h

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

@ -41,6 +41,69 @@ namespace storm {
return result; return result;
} }
template <typename ValueType>
std::map<typename utility::parametric::VariableType<ValueType>::type, std::vector<typename utility::parametric::CoefficientType<ValueType>::type>> parseSamples(std::shared_ptr<storm::models::ModelBase> const& model, std::string const& sampleString) {
STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::NotSupportedException, "Sampling is only supported for sparse models.");
std::map<typename utility::parametric::VariableType<ValueType>::type, std::vector<typename utility::parametric::CoefficientType<ValueType>::type>> samplesForVariables;
if (sampleString.empty()) {
return samplesForVariables;
}
// Get all parameters from the model.
std::set<typename utility::parametric::VariableType<ValueType>::type> modelParameters;
auto const& sparseModel = *model->as<storm::models::sparse::Model<ValueType>>();
modelParameters = storm::models::sparse::getProbabilityParameters(sparseModel);
auto rewParameters = storm::models::sparse::getRewardParameters(sparseModel);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
// Get the values string for each variable.
std::vector<std::string> valuesForVariables;
boost::split(valuesForVariables, sampleString, boost::is_any_of(","));
for (auto& values : valuesForVariables) {
boost::trim(values);
}
std::set<typename utility::parametric::VariableType<ValueType>::type> encounteredParameters;
for (auto const& varValues : valuesForVariables) {
auto equalsPosition = varValues.find("=");
STORM_LOG_THROW(equalsPosition != varValues.npos, storm::exceptions::WrongFormatException, "Incorrect format of samples.");
std::string variableName = varValues.substr(0, equalsPosition);
boost::trim(variableName);
std::string values = varValues.substr(equalsPosition + 1);
boost::trim(values);
bool foundParameter = false;
typename utility::parametric::VariableType<ValueType>::type theParameter;
for (auto const& parameter : modelParameters) {
std::stringstream parameterStream;
parameterStream << parameter;
std::cout << parameterStream.str() << " vs " << variableName << std::endl;
if (parameterStream.str() == variableName) {
foundParameter = true;
theParameter = parameter;
encounteredParameters.insert(parameter);
}
}
STORM_LOG_THROW(foundParameter, storm::exceptions::WrongFormatException, "Unknown parameter '" << variableName << "'.");
std::vector<std::string> splitValues;
boost::split(splitValues, values, boost::is_any_of(":"));
STORM_LOG_THROW(!splitValues.empty(), storm::exceptions::WrongFormatException, "Expecting at least one value per parameter.");
auto& list = samplesForVariables[theParameter];
for (auto& value : splitValues) {
boost::trim(value);
list.push_back(storm::utility::convertNumber<typename utility::parametric::CoefficientType<ValueType>::type>(value));
}
}
STORM_LOG_THROW(encounteredParameters == modelParameters, storm::exceptions::WrongFormatException, "Variables for all parameters are required when providing samples.")
return samplesForVariables;
}
template <typename ValueType> template <typename ValueType>
std::pair<std::shared_ptr<storm::models::ModelBase>, bool> preprocessSparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input) { std::pair<std::shared_ptr<storm::models::ModelBase>, bool> preprocessSparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input) {
auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>(); auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
@ -152,23 +215,65 @@ namespace storm {
} }
template <typename ValueType> template <typename ValueType>
void verifyPropertiesWithSparseEngine(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input) {
verifyProperties<ValueType>(input.properties,
[&model] (std::shared_ptr<storm::logic::Formula const> const& formula) {
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithSparseEngine<ValueType>(model, storm::api::createTask<ValueType>(formula, true));
if (result) {
result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
}
return result;
},
[&model] (std::unique_ptr<storm::modelchecker::CheckResult> const& result) {
auto parametricSettings = storm::settings::getModule<storm::settings::modules::ParametricSettings>();
if (parametricSettings.exportResultToFile() && model->isOfType(storm::models::ModelType::Dtmc)) {
auto dtmc = model->template as<storm::models::sparse::Dtmc<ValueType>>();
boost::optional<ValueType> rationalFunction = result->asExplicitQuantitativeCheckResult<ValueType>()[*model->getInitialStates().begin()];
storm::api::exportParametricResultToFile(rationalFunction, storm::analysis::ConstraintCollector<ValueType>(*dtmc), parametricSettings.exportResultPath());
}
});
void verifyPropertiesWithSparseEngine(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input, std::map<typename utility::parametric::VariableType<ValueType>::type, std::vector<typename utility::parametric::CoefficientType<ValueType>::type>> const& samples) {
if (samples.empty()) {
verifyProperties<ValueType>(input.properties,
[&model] (std::shared_ptr<storm::logic::Formula const> const& formula) {
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithSparseEngine<ValueType>(model, storm::api::createTask<ValueType>(formula, true));
if (result) {
result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
}
return result;
},
[&model] (std::unique_ptr<storm::modelchecker::CheckResult> const& result) {
auto parametricSettings = storm::settings::getModule<storm::settings::modules::ParametricSettings>();
if (parametricSettings.exportResultToFile() && model->isOfType(storm::models::ModelType::Dtmc)) {
auto dtmc = model->template as<storm::models::sparse::Dtmc<ValueType>>();
boost::optional<ValueType> rationalFunction = result->asExplicitQuantitativeCheckResult<ValueType>()[*model->getInitialStates().begin()];
storm::api::exportParametricResultToFile(rationalFunction, storm::analysis::ConstraintCollector<ValueType>(*dtmc), parametricSettings.exportResultPath());
}
});
} else {
STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Dtmc), storm::exceptions::NotSupportedException, "Sampling is currently only supported for DTMCs.");
// When samples are provided, we create an instantiation model checker.
std::unique_ptr<storm::modelchecker::SparseDtmcInstantiationModelChecker<storm::models::sparse::Dtmc<ValueType>, double>> modelchecker(*model->template as<storm::models::sparse::Dtmc<ValueType>>());
for (auto const& property : input.properties) {
storm::cli::printModelCheckingProperty(property);
modelchecker->specifyFormula(property.getRawFormula(storm::api::createTask<ValueType>(property.getRawFormula(), true)));
// TODO: check.
modelchecker->setInstantiationsAreGraphPreserving(true);
storm::utility::parametric::Valuation<ValueType> valuation;
// Enumerate all sample points.
for () {
bool first = true;
std::stringstream ss;
ss << "Treating instance [";
for (auto const& entry : valuation) {
if (!first) {
ss << ", ";
} else {
first = false;
}
ss << entry.first << ": " << entry.second;
}
ss << "]...";
STORM_PRINT_AND_LOG(ss.str());
storm::utility::Stopwatch watch(true);
std::unique_ptr<storm::modelchecker::CheckResult> result = modelchecker->check(Environment(), valuation);
watch.stop();
printInitialStatesResult<ValueType>(result, property, &watch);
}
}
}
} }
template <typename ValueType> template <typename ValueType>
@ -226,18 +331,18 @@ namespace storm {
} }
template <typename ValueType> template <typename ValueType>
void verifyWithSparseEngine(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input, std::vector<storm::storage::ParameterRegion<ValueType>> const& regions) {
void verifyWithSparseEngine(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input, std::vector<storm::storage::ParameterRegion<ValueType>> const& regions, std::map<typename utility::parametric::VariableType<ValueType>::type, std::vector<typename utility::parametric::CoefficientType<ValueType>::type>> const& samples) {
if (regions.empty()) { if (regions.empty()) {
storm::pars::verifyPropertiesWithSparseEngine(model, input);
storm::pars::verifyPropertiesWithSparseEngine(model, input, samples);
} else { } else {
storm::pars::verifyRegionsWithSparseEngine(model, input, regions); storm::pars::verifyRegionsWithSparseEngine(model, input, regions);
} }
} }
template <storm::dd::DdType DdType, typename ValueType> template <storm::dd::DdType DdType, typename ValueType>
void verifyParametricModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input, std::vector<storm::storage::ParameterRegion<ValueType>> const& regions) {
void verifyParametricModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input, std::vector<storm::storage::ParameterRegion<ValueType>> const& regions, std::map<typename utility::parametric::VariableType<ValueType>::type, std::vector<typename utility::parametric::CoefficientType<ValueType>::type>> const& samples) {
STORM_LOG_ASSERT(model->isSparseModel(), "Unexpected model type."); STORM_LOG_ASSERT(model->isSparseModel(), "Unexpected model type.");
storm::pars::verifyWithSparseEngine<ValueType>(model->as<storm::models::sparse::Model<ValueType>>(), input, regions);
storm::pars::verifyWithSparseEngine<ValueType>(model->as<storm::models::sparse::Model<ValueType>>(), input, regions, samples);
} }
template <storm::dd::DdType DdType, typename ValueType> template <storm::dd::DdType DdType, typename ValueType>
@ -271,8 +376,7 @@ namespace storm {
} }
std::vector<storm::storage::ParameterRegion<ValueType>> regions = parseRegions<ValueType>(model); std::vector<storm::storage::ParameterRegion<ValueType>> regions = parseRegions<ValueType>(model);
std::map<typename utility::parametric::VariableType<ValueType>::type, std::vector<typename utility::parametric::CoefficientType<ValueType>::type>> samples = parseSamples<ValueType>(model, parSettings.getSamples());
if (model) { if (model) {
storm::cli::exportModel<DdType, ValueType>(model, input); storm::cli::exportModel<DdType, ValueType>(model, input);
@ -285,7 +389,7 @@ namespace storm {
} }
if (model) { if (model) {
verifyParametricModel<DdType, ValueType>(model, input, regions);
verifyParametricModel<DdType, ValueType>(model, input, regions, samples);
} }
} }

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

@ -18,6 +18,7 @@ namespace storm {
const std::string ParametricSettings::transformContinuousOptionName = "transformcontinuous"; const std::string ParametricSettings::transformContinuousOptionName = "transformcontinuous";
const std::string ParametricSettings::transformContinuousShortOptionName = "tc"; const std::string ParametricSettings::transformContinuousShortOptionName = "tc";
const std::string ParametricSettings::onlyWellformednessConstraintsOptionName = "onlyconstraints"; const std::string ParametricSettings::onlyWellformednessConstraintsOptionName = "onlyconstraints";
const std::string ParametricSettings::samplesOptionName = "samples";
ParametricSettings::ParametricSettings() : ModuleSettings(moduleName) { ParametricSettings::ParametricSettings() : ModuleSettings(moduleName) {
this->addOption(storm::settings::OptionBuilder(moduleName, exportResultOptionName, false, "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.")
@ -25,6 +26,8 @@ namespace storm {
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, 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()); 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());
this->addOption(storm::settings::OptionBuilder(moduleName, onlyWellformednessConstraintsOptionName, false, "Sets whether you only want to obtain the wellformedness constraints").build()); this->addOption(storm::settings::OptionBuilder(moduleName, onlyWellformednessConstraintsOptionName, false, "Sets whether you only want to obtain the wellformedness constraints").build());
this->addOption(storm::settings::OptionBuilder(moduleName, samplesOptionName, false, "The points at which to sample the model.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("samples", "The samples given in the form 'Var1=Val1:Val2:...:Valk,Var2=...").setDefaultValueString("").build()).build());
} }
bool ParametricSettings::exportResultToFile() const { bool ParametricSettings::exportResultToFile() const {
@ -47,6 +50,10 @@ namespace storm {
return this->getOption(onlyWellformednessConstraintsOptionName).getHasOptionBeenSet(); return this->getOption(onlyWellformednessConstraintsOptionName).getHasOptionBeenSet();
} }
std::string ParametricSettings::getSamples() const {
return this->getOption(samplesOptionName).getArgumentByName("samples").getValueAsString();
}
} // namespace modules } // namespace modules
} // namespace settings } // namespace settings
} // namespace storm } // namespace storm

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

@ -47,6 +47,13 @@ namespace storm {
*/ */
bool onlyObtainConstraints() const; bool onlyObtainConstraints() const;
/*!
* Retrieves the samples as a comma-separated list of samples for each (relevant) variable, where the
* samples are colon-separated values. For example, 'N=1:2:3,K=2:4' means that N takes the values 1 to
* 3 and K either 2 or 4.
*/
std::string getSamples() const;
const static std::string moduleName; const static std::string moduleName;
private: private:
@ -55,6 +62,7 @@ namespace storm {
const static std::string transformContinuousOptionName; const static std::string transformContinuousOptionName;
const static std::string transformContinuousShortOptionName; const static std::string transformContinuousShortOptionName;
const static std::string onlyWellformednessConstraintsOptionName; const static std::string onlyWellformednessConstraintsOptionName;
const static std::string samplesOptionName;
}; };
} // namespace modules } // namespace modules

Write Preview
Loading…
Cancel
Save