From cc1fc8a7beeb6541f69394d26df132d5d46b481b Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 12 Jul 2018 13:35:55 +0200
Subject: [PATCH] adding exact sampling for parametric systems

---
 src/storm-pars-cli/storm-pars.cpp             | 28 +++++++++++++------
 .../settings/modules/ParametricSettings.cpp   |  8 +++++-
 .../settings/modules/ParametricSettings.h     |  6 ++++
 3 files changed, 33 insertions(+), 9 deletions(-)

diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp
index 32d63ae52..ec3f65f29 100644
--- a/src/storm-pars-cli/storm-pars.cpp
+++ b/src/storm-pars-cli/storm-pars.cpp
@@ -33,7 +33,7 @@ namespace storm {
 
         template <typename ValueType>
         struct SampleInformation {
-            SampleInformation(bool graphPreserving = false) : graphPreserving(graphPreserving) {
+            SampleInformation(bool graphPreserving = false, bool exact = false) : graphPreserving(graphPreserving), exact(exact) {
                 // Intentionally left empty.
             }
             
@@ -43,6 +43,7 @@ namespace storm {
             
             std::vector<std::map<typename utility::parametric::VariableType<ValueType>::type, std::vector<typename utility::parametric::CoefficientType<ValueType>::type>>> cartesianProducts;
             bool graphPreserving;
+            bool exact;
         };
         
         template <typename ValueType>
@@ -320,6 +321,19 @@ namespace storm {
             }
         }
         
+        template <typename ValueType, typename SolveValueType = double>
+        void verifyPropertiesAtSamplePoints(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input, SampleInformation<ValueType> const& samples) {
+            if (model->isOfType(storm::models::ModelType::Dtmc)) {
+                verifyPropertiesAtSamplePoints<storm::modelchecker::SparseDtmcInstantiationModelChecker, storm::models::sparse::Dtmc<ValueType>, ValueType, SolveValueType>(*model->template as<storm::models::sparse::Dtmc<ValueType>>(), input, samples);
+            } else if (model->isOfType(storm::models::ModelType::Ctmc)) {
+                verifyPropertiesAtSamplePoints<storm::modelchecker::SparseCtmcInstantiationModelChecker, storm::models::sparse::Ctmc<ValueType>, ValueType, SolveValueType>(*model->template as<storm::models::sparse::Ctmc<ValueType>>(), input, samples);
+            } else if (model->isOfType(storm::models::ModelType::Ctmc)) {
+                verifyPropertiesAtSamplePoints<storm::modelchecker::SparseMdpInstantiationModelChecker, storm::models::sparse::Mdp<ValueType>, ValueType, SolveValueType>(*model->template as<storm::models::sparse::Mdp<ValueType>>(), input, samples);
+            } else {
+                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Sampling is currently only supported for DTMCs, CTMCs and MDPs.");
+            }
+        }
+        
         template <typename ValueType>
         void verifyPropertiesWithSparseEngine(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input, SampleInformation<ValueType> const& samples) {
             
@@ -342,14 +356,11 @@ namespace storm {
                                             });
             } else {
                 STORM_LOG_TRACE("Sampling the model at given points.");
-                if (model->isOfType(storm::models::ModelType::Dtmc)) {
-                    verifyPropertiesAtSamplePoints<storm::modelchecker::SparseDtmcInstantiationModelChecker, storm::models::sparse::Dtmc<ValueType>, ValueType, double>(*model->template as<storm::models::sparse::Dtmc<ValueType>>(), input, samples);
-                } else if (model->isOfType(storm::models::ModelType::Ctmc)) {
-                    verifyPropertiesAtSamplePoints<storm::modelchecker::SparseCtmcInstantiationModelChecker, storm::models::sparse::Ctmc<ValueType>, ValueType, double>(*model->template as<storm::models::sparse::Ctmc<ValueType>>(), input, samples);
-                } else if (model->isOfType(storm::models::ModelType::Ctmc)) {
-                    verifyPropertiesAtSamplePoints<storm::modelchecker::SparseMdpInstantiationModelChecker, storm::models::sparse::Mdp<ValueType>, ValueType, double>(*model->template as<storm::models::sparse::Mdp<ValueType>>(), input, samples);
+                
+                if (samples.exact) {
+                    verifyPropertiesAtSamplePoints<ValueType, storm::RationalNumber>(model, input, samples);
                 } else {
-                    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Sampling is currently only supported for DTMCs, CTMCs and MDPs.");
+                    verifyPropertiesAtSamplePoints<ValueType, double>(model, input, samples);
                 }
             }
         }
@@ -455,6 +466,7 @@ namespace storm {
             
             std::vector<storm::storage::ParameterRegion<ValueType>> regions = parseRegions<ValueType>(model);
             SampleInformation<ValueType> samples = parseSamples<ValueType>(model, parSettings.getSamples(), parSettings.isSamplesAreGraphPreservingSet());
+            samples.exact = parSettings.isSampleExactSet();
             
             if (model) {
                 storm::cli::exportModel<DdType, ValueType>(model, input);
diff --git a/src/storm-pars/settings/modules/ParametricSettings.cpp b/src/storm-pars/settings/modules/ParametricSettings.cpp
index d5b3c151d..7ecbd6166 100644
--- a/src/storm-pars/settings/modules/ParametricSettings.cpp
+++ b/src/storm-pars/settings/modules/ParametricSettings.cpp
@@ -20,7 +20,8 @@ namespace storm {
             const std::string ParametricSettings::onlyWellformednessConstraintsOptionName = "onlyconstraints";
             const std::string ParametricSettings::samplesOptionName = "samples";
             const std::string ParametricSettings::samplesGraphPreservingOptionName = "samples-graph-preserving";
-            
+            const std::string ParametricSettings::sampleExactOptionName = "sample-exact";
+
             ParametricSettings::ParametricSettings() : ModuleSettings(moduleName) {
                 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());
@@ -30,6 +31,7 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, samplesOptionName, false, "The points at which to sample the model.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("samples", "The samples are semicolon-separated entries of the form 'Var1=Val1:Val2:...:Valk,Var2=... that span the sample spaces.").setDefaultValueString("").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, samplesGraphPreservingOptionName, false, "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());
             }
             
             bool ParametricSettings::exportResultToFile() const {
@@ -60,6 +62,10 @@ namespace storm {
                 return this->getOption(samplesGraphPreservingOptionName).getHasOptionBeenSet();
             }
             
+            bool ParametricSettings::isSampleExactSet() const {
+                return this->getOption(sampleExactOptionName).getHasOptionBeenSet();
+            }
+            
         } // 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 374c8e839..1f10a4b35 100644
--- a/src/storm-pars/settings/modules/ParametricSettings.h
+++ b/src/storm-pars/settings/modules/ParametricSettings.h
@@ -59,6 +59,11 @@ namespace storm {
                  */
                 bool isSamplesAreGraphPreservingSet() const;
                 
+                /*!
+                 * Retrieves whether samples are to be computed exactly.
+                 */
+                bool isSampleExactSet() const;
+                
                 const static std::string moduleName;
                 
             private:
@@ -69,6 +74,7 @@ namespace storm {
                 const static std::string onlyWellformednessConstraintsOptionName;
                 const static std::string samplesOptionName;
                 const static std::string samplesGraphPreservingOptionName;
+                const static std::string sampleExactOptionName;
             };
             
         } // namespace modules