diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 8546f81d1..ff7c075f8 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -41,6 +41,69 @@ namespace storm { return result; } + template + std::map::type, std::vector::type>> parseSamples(std::shared_ptr const& model, std::string const& sampleString) { + STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::NotSupportedException, "Sampling is only supported for sparse models."); + + std::map::type, std::vector::type>> samplesForVariables; + if (sampleString.empty()) { + return samplesForVariables; + } + + // Get all parameters from the model. + std::set::type> modelParameters; + auto const& sparseModel = *model->as>(); + 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 valuesForVariables; + boost::split(valuesForVariables, sampleString, boost::is_any_of(",")); + for (auto& values : valuesForVariables) { + boost::trim(values); + } + + std::set::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::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 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::type>(value)); + } + } + + STORM_LOG_THROW(encounteredParameters == modelParameters, storm::exceptions::WrongFormatException, "Variables for all parameters are required when providing samples.") + + return samplesForVariables; + } + template std::pair, bool> preprocessSparseModel(std::shared_ptr> const& model, SymbolicInput const& input) { auto generalSettings = storm::settings::getModule(); @@ -152,23 +215,65 @@ namespace storm { } template - void verifyPropertiesWithSparseEngine(std::shared_ptr> const& model, SymbolicInput const& input) { - verifyProperties(input.properties, - [&model] (std::shared_ptr const& formula) { - std::unique_ptr result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(formula, true)); - if (result) { - result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); - } - return result; - }, - [&model] (std::unique_ptr const& result) { - auto parametricSettings = storm::settings::getModule(); - if (parametricSettings.exportResultToFile() && model->isOfType(storm::models::ModelType::Dtmc)) { - auto dtmc = model->template as>(); - boost::optional rationalFunction = result->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()]; - storm::api::exportParametricResultToFile(rationalFunction, storm::analysis::ConstraintCollector(*dtmc), parametricSettings.exportResultPath()); - } - }); + void verifyPropertiesWithSparseEngine(std::shared_ptr> const& model, SymbolicInput const& input, std::map::type, std::vector::type>> const& samples) { + + if (samples.empty()) { + verifyProperties(input.properties, + [&model] (std::shared_ptr const& formula) { + std::unique_ptr result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(formula, true)); + if (result) { + result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); + } + return result; + }, + [&model] (std::unique_ptr const& result) { + auto parametricSettings = storm::settings::getModule(); + if (parametricSettings.exportResultToFile() && model->isOfType(storm::models::ModelType::Dtmc)) { + auto dtmc = model->template as>(); + boost::optional rationalFunction = result->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()]; + storm::api::exportParametricResultToFile(rationalFunction, storm::analysis::ConstraintCollector(*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, double>> modelchecker(*model->template as>()); + + for (auto const& property : input.properties) { + storm::cli::printModelCheckingProperty(property); + + modelchecker->specifyFormula(property.getRawFormula(storm::api::createTask(property.getRawFormula(), true))); + + // TODO: check. + modelchecker->setInstantiationsAreGraphPreserving(true); + + storm::utility::parametric::Valuation 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 result = modelchecker->check(Environment(), valuation); + watch.stop(); + + printInitialStatesResult(result, property, &watch); + } + } + } } template @@ -226,18 +331,18 @@ namespace storm { } template - void verifyWithSparseEngine(std::shared_ptr> const& model, SymbolicInput const& input, std::vector> const& regions) { + void verifyWithSparseEngine(std::shared_ptr> const& model, SymbolicInput const& input, std::vector> const& regions, std::map::type, std::vector::type>> const& samples) { if (regions.empty()) { - storm::pars::verifyPropertiesWithSparseEngine(model, input); + storm::pars::verifyPropertiesWithSparseEngine(model, input, samples); } else { storm::pars::verifyRegionsWithSparseEngine(model, input, regions); } } template - void verifyParametricModel(std::shared_ptr const& model, SymbolicInput const& input, std::vector> const& regions) { + void verifyParametricModel(std::shared_ptr const& model, SymbolicInput const& input, std::vector> const& regions, std::map::type, std::vector::type>> const& samples) { STORM_LOG_ASSERT(model->isSparseModel(), "Unexpected model type."); - storm::pars::verifyWithSparseEngine(model->as>(), input, regions); + storm::pars::verifyWithSparseEngine(model->as>(), input, regions, samples); } template @@ -271,9 +376,8 @@ namespace storm { } std::vector> regions = parseRegions(model); - - - + std::map::type, std::vector::type>> samples = parseSamples(model, parSettings.getSamples()); + if (model) { storm::cli::exportModel(model, input); } @@ -285,7 +389,7 @@ namespace storm { } if (model) { - verifyParametricModel(model, input, regions); + verifyParametricModel(model, input, regions, samples); } } diff --git a/src/storm-pars/settings/modules/ParametricSettings.cpp b/src/storm-pars/settings/modules/ParametricSettings.cpp index 28975aa5c..a02851dac 100644 --- a/src/storm-pars/settings/modules/ParametricSettings.cpp +++ b/src/storm-pars/settings/modules/ParametricSettings.cpp @@ -18,6 +18,7 @@ namespace storm { const std::string ParametricSettings::transformContinuousOptionName = "transformcontinuous"; const std::string ParametricSettings::transformContinuousShortOptionName = "tc"; const std::string ParametricSettings::onlyWellformednessConstraintsOptionName = "onlyconstraints"; + const std::string ParametricSettings::samplesOptionName = "samples"; ParametricSettings::ParametricSettings() : ModuleSettings(moduleName) { 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, 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, 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 { @@ -46,7 +49,11 @@ namespace storm { bool ParametricSettings::onlyObtainConstraints() const { return this->getOption(onlyWellformednessConstraintsOptionName).getHasOptionBeenSet(); } - + + std::string ParametricSettings::getSamples() const { + return this->getOption(samplesOptionName).getArgumentByName("samples").getValueAsString(); + } + } // namespace modules } // namespace settings } // namespace storm diff --git a/src/storm-pars/settings/modules/ParametricSettings.h b/src/storm-pars/settings/modules/ParametricSettings.h index e610f033d..195b0936c 100644 --- a/src/storm-pars/settings/modules/ParametricSettings.h +++ b/src/storm-pars/settings/modules/ParametricSettings.h @@ -47,6 +47,13 @@ namespace storm { */ 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; private: @@ -55,6 +62,7 @@ namespace storm { const static std::string transformContinuousOptionName; const static std::string transformContinuousShortOptionName; const static std::string onlyWellformednessConstraintsOptionName; + const static std::string samplesOptionName; }; } // namespace modules