Re-introduce sampling of the derivative into CLI

src/storm-pars-cli/sampling.h

@@ -75,6 +75,76 @@ struct SampleInformation {
 };
 
 template<template<typename, typename> class ModelCheckerType, typename ModelType, typename ValueType, typename SolveValueType = double>
+void verifyPropertiesAtSamplePointsDerivative(ModelType const& model, cli::SymbolicInput const& input, SampleInformation<ValueType> const& samples) {
+    // When samples are provided, we create an instantiation model checker.
+    ModelCheckerType<ValueType, SolveValueType> modelchecker(model);
+
+    for (auto const& property : input.properties) {
+        storm::cli::printModelCheckingProperty(property);
+
+        modelchecker.specifyFormula(Environment(), storm::api::createTask<ValueType>(property.getRawFormula(), true));
+
+        storm::utility::parametric::Valuation<ValueType> valuation;
+
+        std::vector<typename storm::utility::parametric::VariableType<ValueType>::type> parameters;
+        std::vector<typename std::vector<typename storm::utility::parametric::CoefficientType<ValueType>::type>::const_iterator> iterators;
+        std::vector<typename std::vector<typename storm::utility::parametric::CoefficientType<ValueType>::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<storm::modelchecker::CheckResult> 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<ValueType>(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<template<typename, typename> class ModelCheckerType, typename ModelType, typename ValueType, typename SolveValueType = double, bool Derivative = false>
 void verifyPropertiesAtSamplePoints(ModelType const& model, cli::SymbolicInput const& input, SampleInformation<ValueType> const& samples) {
     // When samples are provided, we create an instantiation model checker.
     ModelCheckerType<ModelType, SolveValueType> modelchecker(model);
@@ -142,6 +212,17 @@ void verifyPropertiesAtSamplePoints(ModelType const& model, cli::SymbolicInput c
     }
 }
 
+template<typename ValueType, typename SolveValueType = double>
+void verifyPropertiesAtSamplePointsWithSparseEngineDerivatives(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model,
+                                                               cli::SymbolicInput const& input, SampleInformation<ValueType> const& samples) {
+    if (model->isOfType(storm::models::ModelType::Dtmc)) {
+        verifyPropertiesAtSamplePointsDerivative<storm::derivative::SparseDerivativeInstantiationModelChecker, storm::models::sparse::Dtmc<ValueType>,
+                                                 ValueType, SolveValueType>(*model->template as<storm::models::sparse::Dtmc<ValueType>>(), input, samples);
+    } else {
+        STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Sampling the derivative is currently only supported for DTMCs.");
+    }
+}
+
 template<typename ValueType, typename SolveValueType = double>
 void verifyPropertiesAtSamplePointsWithSparseEngine(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, cli::SymbolicInput const& input,
                                                     SampleInformation<ValueType> const& samples) {

src/storm-pars-cli/storm-pars.cpp

@@ -510,11 +510,21 @@ void processInputWithValueTypeAndDdlib(cli::SymbolicInput& input, storm::cli::Mo
         if (!samples.empty()) {
             STORM_LOG_TRACE("Sampling the model at given points.");
 
-            if (samples.exact) {
-                verifyPropertiesAtSamplePointsWithSparseEngine<ValueType, storm::RationalNumber>(model->as<storm::models::sparse::Model<ValueType>>(), input,
+            if (sampleSettings.isSampleDerivativeSet()) {
+                if (samples.exact) {
+                    verifyPropertiesAtSamplePointsWithSparseEngineDerivatives<ValueType, storm::RationalNumber>(
+                        model->as<storm::models::sparse::Model<ValueType>>(), input, samples);
+                } else {
+                    verifyPropertiesAtSamplePointsWithSparseEngineDerivatives<ValueType, double>(model->as<storm::models::sparse::Model<ValueType>>(), input,
                                                                                                  samples);
+                }
             } else {
-                verifyPropertiesAtSamplePointsWithSparseEngine<ValueType, double>(model->as<storm::models::sparse::Model<ValueType>>(), input, samples);
+                if (samples.exact) {
+                    verifyPropertiesAtSamplePointsWithSparseEngine<ValueType, storm::RationalNumber>(model->as<storm::models::sparse::Model<ValueType>>(),
+                                                                                                     input, samples);
+                } else {
+                    verifyPropertiesAtSamplePointsWithSparseEngine<ValueType, double>(model->as<storm::models::sparse::Model<ValueType>>(), input, samples);
+                }
             }
         }
     } else {

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<std::string> 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();
 }

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<std::string> getDerivativeAtInstantiation() const;
-
     /*!
      * Retrieves the learning rate for the gradient descent.
      */

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

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