From ccf28f726a79064d9297d5d15c23efb09f2dad93 Mon Sep 17 00:00:00 2001 From: Linus Heck Date: Mon, 9 Sep 2024 16:06:20 +0200 Subject: [PATCH 1/3] Re-introduce sampling of the derivative into CLI --- src/storm-pars-cli/sampling.h | 82 +++++++++++++++++++ src/storm-pars-cli/storm-pars.cpp | 17 +++- .../settings/modules/DerivativeSettings.cpp | 14 ---- .../settings/modules/DerivativeSettings.h | 5 -- .../settings/modules/SamplingSettings.cpp | 6 ++ .../settings/modules/SamplingSettings.h | 5 ++ 6 files changed, 106 insertions(+), 23 deletions(-) diff --git a/src/storm-pars-cli/sampling.h b/src/storm-pars-cli/sampling.h index b7ade2ffa2..33dfb91e1a 100644 --- a/src/storm-pars-cli/sampling.h +++ b/src/storm-pars-cli/sampling.h @@ -74,7 +74,78 @@ struct SampleInformation { bool exact; }; + template class ModelCheckerType, typename ModelType, typename ValueType, typename SolveValueType = double> +void verifyPropertiesAtSamplePointsDerivative(ModelType const& model, cli::SymbolicInput const& input, SampleInformation const& samples) { + // When samples are provided, we create an instantiation model checker. + ModelCheckerType modelchecker(model); + + for (auto const& property : input.properties) { + storm::cli::printModelCheckingProperty(property); + + modelchecker.specifyFormula(Environment(), storm::api::createTask(property.getRawFormula(), true)); + + storm::utility::parametric::Valuation valuation; + + std::vector::type> parameters; + std::vector::type>::const_iterator> iterators; + std::vector::type>::const_iterator> iteratorEnds; + + storm::utility::Stopwatch watch(true); + for (auto const& product : samples.cartesianProducts) { + parameters.clear(); + iterators.clear(); + iteratorEnds.clear(); + + for (auto const& entry : product) { + parameters.push_back(entry.first); + iterators.push_back(entry.second.cbegin()); + iteratorEnds.push_back(entry.second.cend()); + } + + bool done = false; + while (!done) { + // Read off valuation. + for (uint64_t i = 0; i < parameters.size(); ++i) { + valuation[parameters[i]] = *iterators[i]; + } + + for (auto const& parameter : parameters) { + storm::utility::Stopwatch valuationWatch(true); + std::unique_ptr result = modelchecker.check(Environment(), valuation, parameter); + valuationWatch.stop(); + + if (result) { + result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model.getInitialStates())); + } + STORM_PRINT_AND_LOG("Derivative w.r.t. " << parameter << ":\n"); + printInitialStatesResult(result, &valuationWatch, &valuation); + } + + for (uint64_t i = 0; i < parameters.size(); ++i) { + ++iterators[i]; + if (iterators[i] == iteratorEnds[i]) { + // Reset iterator and proceed to move next iterator. + iterators[i] = product.at(parameters[i]).cbegin(); + + // If the last iterator was removed, we are done. + if (i == parameters.size() - 1) { + done = true; + } + } else { + // If an iterator was moved but not reset, we have another valuation to check. + break; + } + } + } + } + + watch.stop(); + STORM_PRINT_AND_LOG("Overall time for sampling all instances: " << watch << "\n\n"); + } +} + +template class ModelCheckerType, typename ModelType, typename ValueType, typename SolveValueType = double, bool Derivative = false> void verifyPropertiesAtSamplePoints(ModelType const& model, cli::SymbolicInput const& input, SampleInformation const& samples) { // When samples are provided, we create an instantiation model checker. ModelCheckerType modelchecker(model); @@ -142,6 +213,17 @@ void verifyPropertiesAtSamplePoints(ModelType const& model, cli::SymbolicInput c } } +template +void verifyPropertiesAtSamplePointsWithSparseEngineDerivatives(std::shared_ptr> const& model, cli::SymbolicInput const& input, + SampleInformation const& samples) { + if (model->isOfType(storm::models::ModelType::Dtmc)) { + verifyPropertiesAtSamplePointsDerivative, ValueType, + SolveValueType>(*model->template as>(), input, samples); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Sampling the derivative is currently only supported for DTMCs."); + } +} + template void verifyPropertiesAtSamplePointsWithSparseEngine(std::shared_ptr> const& model, cli::SymbolicInput const& input, SampleInformation const& samples) { diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 3b10a43371..6734458720 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -510,11 +510,20 @@ void processInputWithValueTypeAndDdlib(cli::SymbolicInput& input, storm::cli::Mo if (!samples.empty()) { STORM_LOG_TRACE("Sampling the model at given points."); - if (samples.exact) { - verifyPropertiesAtSamplePointsWithSparseEngine(model->as>(), input, - samples); + if (sampleSettings.isSampleDerivativeSet()) { + if (samples.exact) { + verifyPropertiesAtSamplePointsWithSparseEngineDerivatives(model->as>(), input, + samples); + } else { + verifyPropertiesAtSamplePointsWithSparseEngineDerivatives(model->as>(), input, samples); + } } else { - verifyPropertiesAtSamplePointsWithSparseEngine(model->as>(), input, samples); + if (samples.exact) { + verifyPropertiesAtSamplePointsWithSparseEngine(model->as>(), input, + samples); + } else { + verifyPropertiesAtSamplePointsWithSparseEngine(model->as>(), input, samples); + } } } } else { diff --git a/src/storm-pars/settings/modules/DerivativeSettings.cpp b/src/storm-pars/settings/modules/DerivativeSettings.cpp index 13a0c7d80c..73360f9f19 100644 --- a/src/storm-pars/settings/modules/DerivativeSettings.cpp +++ b/src/storm-pars/settings/modules/DerivativeSettings.cpp @@ -16,7 +16,6 @@ namespace modules { const std::string DerivativeSettings::moduleName = "derivative"; const std::string DerivativeSettings::feasibleInstantiationSearch = "gradient-descent"; -const std::string DerivativeSettings::derivativeAtInstantiation = "compute-derivative"; const std::string DerivativeSettings::learningRate = "learning-rate"; const std::string DerivativeSettings::miniBatchSize = "batch-size"; const std::string DerivativeSettings::adamParams = "adam-params"; @@ -32,11 +31,6 @@ DerivativeSettings::DerivativeSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, feasibleInstantiationSearch, false, "Search for a feasible instantiation (restart with new instantiation while not feasible)") .build()); - this->addOption(storm::settings::OptionBuilder(moduleName, derivativeAtInstantiation, false, "Compute the derivative at an input instantiation") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument(derivativeAtInstantiation, - "Instantiation at which the derivative should be computed") - .build()) - .build()); this->addOption(storm::settings::OptionBuilder(moduleName, learningRate, false, "Sets the learning rate of gradient descent") .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument(learningRate, "The learning rate of the gradient descent") .setDefaultValueDouble(0.1) @@ -90,14 +84,6 @@ bool DerivativeSettings::isFeasibleInstantiationSearchSet() const { return this->getOption(feasibleInstantiationSearch).getHasOptionBeenSet(); } -boost::optional DerivativeSettings::getDerivativeAtInstantiation() const { - if (this->getOption(derivativeAtInstantiation).getHasOptionBeenSet()) { - return this->getOption(derivativeAtInstantiation).getArgumentByName(derivativeAtInstantiation).getValueAsString(); - } else { - return boost::none; - } -} - double DerivativeSettings::getLearningRate() const { return this->getOption(learningRate).getArgumentByName(learningRate).getValueAsDouble(); } diff --git a/src/storm-pars/settings/modules/DerivativeSettings.h b/src/storm-pars/settings/modules/DerivativeSettings.h index bda906f9ee..2048733b85 100644 --- a/src/storm-pars/settings/modules/DerivativeSettings.h +++ b/src/storm-pars/settings/modules/DerivativeSettings.h @@ -26,11 +26,6 @@ class DerivativeSettings : public ModuleSettings { */ bool isFeasibleInstantiationSearchSet() const; - /*! - * Retrieves whether an extremum should be found by Gradient Descent. - */ - boost::optional getDerivativeAtInstantiation() const; - /*! * Retrieves the learning rate for the gradient descent. */ diff --git a/src/storm-pars/settings/modules/SamplingSettings.cpp b/src/storm-pars/settings/modules/SamplingSettings.cpp index d52288a6bd..678c36cf63 100644 --- a/src/storm-pars/settings/modules/SamplingSettings.cpp +++ b/src/storm-pars/settings/modules/SamplingSettings.cpp @@ -11,6 +11,7 @@ const std::string SamplingSettings::moduleName = "sampling"; const std::string samplesOptionName = "samples"; const std::string samplesGraphPreservingOptionName = "samples-graph-preserving"; const std::string sampleExactOptionName = "sample-exact"; +const std::string sampleDerivativeOptionName = "sample-derivative"; SamplingSettings::SamplingSettings() : ModuleSettings(moduleName) { this->addOption( @@ -25,6 +26,7 @@ SamplingSettings::SamplingSettings() : ModuleSettings(moduleName) { "Sets whether it can be assumed that the samples are graph-preserving.") .build()); this->addOption(storm::settings::OptionBuilder(moduleName, sampleExactOptionName, false, "Sets whether to sample using exact arithmetic.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, sampleDerivativeOptionName, false, "Sets whether to sample the derivatives instead..").build()); } std::string SamplingSettings::getSamples() const { @@ -38,4 +40,8 @@ bool SamplingSettings::isSamplesAreGraphPreservingSet() const { bool SamplingSettings::isSampleExactSet() const { return this->getOption(sampleExactOptionName).getHasOptionBeenSet(); } + +bool SamplingSettings::isSampleDerivativeSet() const { + return this->getOption(sampleDerivativeOptionName).getHasOptionBeenSet(); +} } // namespace storm::settings::modules \ No newline at end of file diff --git a/src/storm-pars/settings/modules/SamplingSettings.h b/src/storm-pars/settings/modules/SamplingSettings.h index 1b9c69819f..81947ae224 100644 --- a/src/storm-pars/settings/modules/SamplingSettings.h +++ b/src/storm-pars/settings/modules/SamplingSettings.h @@ -23,6 +23,11 @@ class SamplingSettings : public ModuleSettings { */ bool isSampleExactSet() const; + /*! + * Retrieves whether samples are to be from the derivative. + */ + bool isSampleDerivativeSet() const; + static const std::string moduleName; }; From 1c57b8e6f0444107242d904a8fadbc0242102df6 Mon Sep 17 00:00:00 2001 From: Linus Heck Date: Mon, 9 Sep 2024 16:15:15 +0200 Subject: [PATCH 2/3] Format --- src/storm-pars-cli/sampling.h | 9 ++++----- src/storm-pars-cli/storm-pars.cpp | 11 ++++++----- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/storm-pars-cli/sampling.h b/src/storm-pars-cli/sampling.h index 33dfb91e1a..4c0bd8892e 100644 --- a/src/storm-pars-cli/sampling.h +++ b/src/storm-pars-cli/sampling.h @@ -74,7 +74,6 @@ struct SampleInformation { bool exact; }; - template class ModelCheckerType, typename ModelType, typename ValueType, typename SolveValueType = double> void verifyPropertiesAtSamplePointsDerivative(ModelType const& model, cli::SymbolicInput const& input, SampleInformation const& samples) { // When samples are provided, we create an instantiation model checker. @@ -214,11 +213,11 @@ void verifyPropertiesAtSamplePoints(ModelType const& model, cli::SymbolicInput c } template -void verifyPropertiesAtSamplePointsWithSparseEngineDerivatives(std::shared_ptr> const& model, cli::SymbolicInput const& input, - SampleInformation const& samples) { +void verifyPropertiesAtSamplePointsWithSparseEngineDerivatives(std::shared_ptr> const& model, + cli::SymbolicInput const& input, SampleInformation const& samples) { if (model->isOfType(storm::models::ModelType::Dtmc)) { - verifyPropertiesAtSamplePointsDerivative, ValueType, - SolveValueType>(*model->template as>(), input, samples); + verifyPropertiesAtSamplePointsDerivative, + ValueType, SolveValueType>(*model->template as>(), input, samples); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Sampling the derivative is currently only supported for DTMCs."); } diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 6734458720..454b9c1250 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -512,15 +512,16 @@ void processInputWithValueTypeAndDdlib(cli::SymbolicInput& input, storm::cli::Mo if (sampleSettings.isSampleDerivativeSet()) { if (samples.exact) { - verifyPropertiesAtSamplePointsWithSparseEngineDerivatives(model->as>(), input, - samples); + verifyPropertiesAtSamplePointsWithSparseEngineDerivatives( + model->as>(), input, samples); } else { - verifyPropertiesAtSamplePointsWithSparseEngineDerivatives(model->as>(), input, samples); + verifyPropertiesAtSamplePointsWithSparseEngineDerivatives(model->as>(), input, + samples); } } else { if (samples.exact) { - verifyPropertiesAtSamplePointsWithSparseEngine(model->as>(), input, - samples); + verifyPropertiesAtSamplePointsWithSparseEngine(model->as>(), + input, samples); } else { verifyPropertiesAtSamplePointsWithSparseEngine(model->as>(), input, samples); } From 731f1fa93fedaddbb5b92312ed355544cc7e2498 Mon Sep 17 00:00:00 2001 From: Linus Heck Date: Tue, 10 Sep 2024 10:57:14 +0200 Subject: [PATCH 3/3] Remove instead from help string --- src/storm-pars/settings/modules/SamplingSettings.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm-pars/settings/modules/SamplingSettings.cpp b/src/storm-pars/settings/modules/SamplingSettings.cpp index 678c36cf63..7ea182407a 100644 --- a/src/storm-pars/settings/modules/SamplingSettings.cpp +++ b/src/storm-pars/settings/modules/SamplingSettings.cpp @@ -26,7 +26,7 @@ SamplingSettings::SamplingSettings() : ModuleSettings(moduleName) { "Sets whether it can be assumed that the samples are graph-preserving.") .build()); this->addOption(storm::settings::OptionBuilder(moduleName, sampleExactOptionName, false, "Sets whether to sample using exact arithmetic.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, sampleDerivativeOptionName, false, "Sets whether to sample the derivatives instead..").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, sampleDerivativeOptionName, false, "Sets whether to sample the derivatives.").build()); } std::string SamplingSettings::getSamples() const {