Precision as argument

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

@@ -598,10 +598,6 @@ namespace storm {
             if (parSettings.isMonotonicityAnalysisSet()) {
                 // Simplify the model
                 storm::utility::Stopwatch simplifyingWatch(true);
-                std::ofstream outfile;
-                outfile.open("results.txt", std::ios_base::app);
-                outfile << ioSettings.getPrismInputFilename() << ", ";
-
                 if (model->isOfType(storm::models::ModelType::Dtmc)) {
                     auto consideredModel = (model->as<storm::models::sparse::Dtmc<ValueType>>());
                     auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<ValueType>>(*consideredModel);
@@ -631,11 +627,9 @@ namespace storm {
                 simplifyingWatch.stop();
                 STORM_PRINT(std::endl << "Time for model simplification: " << simplifyingWatch << "." << std::endl << std::endl);
                 model->printModelInformationToStream(std::cout);
-                outfile << simplifyingWatch << ", ";
-                outfile.close();
             }
 
-            if (parSettings.isMonotonicityAnalysisSet() && model) {
+            if (model) {
                 auto preprocessingResult = storm::pars::preprocessModel<DdType, ValueType>(model, input);
                 if (preprocessingResult.changed) {
                     model = preprocessingResult.model;
@@ -722,20 +716,13 @@ namespace storm {
 
             if (parSettings.isMonotonicityAnalysisSet()) {
                 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(input.properties);
-
                 // Monotonicity
-                std::ofstream outfile;
-                outfile.open("results.txt", std::ios_base::app);
                 storm::utility::Stopwatch monotonicityWatch(true);
-                auto numberOfSamples = parSettings.getNumberOfSamples();
-                auto monotonicityChecker = storm::analysis::MonotonicityChecker<ValueType>(model, formulas, parSettings.isValidateAssumptionsSet(), numberOfSamples);
+                auto monotonicityChecker = storm::analysis::MonotonicityChecker<ValueType>(model, formulas, parSettings.isValidateAssumptionsSet(), parSettings.getNumberOfSamples(), parSettings.getMonotonicityAnalysisPrecision());
                 monotonicityChecker.checkMonotonicity();
                 monotonicityWatch.stop();
                 STORM_PRINT(std::endl << "Total time for monotonicity checking: " << monotonicityWatch << "." << std::endl
                                     << std::endl);
-
-                outfile << monotonicityWatch << std::endl;
-                outfile.close();
             }
 
             std::vector<storm::storage::ParameterRegion<ValueType>> regions = parseRegions<ValueType>(model);

src/storm-pars/analysis/MonotonicityChecker.cpp

@@ -522,11 +522,13 @@ namespace storm {
                                     (*itr2), storm::utility::convertNumber<typename utility::parametric::CoefficientType<ValueType>::type>(
                                             boost::lexical_cast<std::string>((i + 1) / (double(numberOfSamples + 1)))));
                             valuation.insert(val);
+                            assert (0 < val.second && val.second < 1);
                         } else {
                             auto val = std::pair<typename utility::parametric::VariableType<ValueType>::type, typename utility::parametric::CoefficientType<ValueType>::type>(
                                     (*itr2), storm::utility::convertNumber<typename utility::parametric::CoefficientType<ValueType>::type>(
                                             boost::lexical_cast<std::string>((1) / (double(numberOfSamples + 1)))));
                             valuation.insert(val);
+                            assert (0 < val.second && val.second < 1);
                         }
                     }
                     storm::models::sparse::Dtmc<double> sampleModel = instantiator.instantiate(valuation);
@@ -551,10 +553,12 @@ namespace storm {
                     std::vector<double> values = quantitativeResult.getValueVector();
                     auto initialStates = model->getInitialStates();
                     double initial = 0;
-                    for (auto i = initialStates.getNextSetIndex(0); i < model->getNumberOfStates(); i = initialStates.getNextSetIndex(i+1)) {
-                        initial += values[i];
+                    for (auto j = initialStates.getNextSetIndex(0); j < model->getNumberOfStates(); j = initialStates.getNextSetIndex(j+1)) {
+                        initial += values[j];
                     }
+                    assert (initial >= precision && initial <= 1+precision);
                     double diff = previous - initial;
+                    assert (previous == -1 || diff >= -1-precision && diff <= 1 + precision);
                     if (previous != -1 && (diff > precision || diff < -precision)) {
                         monDecr &= diff > precision; // then previous value is larger than the current value from the initial states
                         monIncr &= diff < -precision;
@@ -625,9 +629,12 @@ namespace storm {
                     for (auto i = initialStates.getNextSetIndex(0); i < model->getNumberOfStates(); i = initialStates.getNextSetIndex(i+1)) {
                         initial += values[i];
                     }
-                    if (previous != -1) {
-                        monDecr &= previous >= initial;
-                        monIncr &= previous <= initial;
+                    assert (initial >= precision && initial <= 1+precision);
+                    double diff = previous - initial;
+                    assert (previous == -1 || diff >= -1-precision && diff <= 1 + precision);
+                    if (previous != -1 && (diff > precision || diff < -precision)) {
+                        monDecr &= diff > precision; // then previous value is larger than the current value from the initial states
+                        monIncr &= diff < -precision;
                     }
                     previous = initial;
                 }

src/storm-pars/settings/modules/ParametricSettings.cpp

@@ -25,6 +25,7 @@ namespace storm {
             const std::string ParametricSettings::sccElimination = "mon-elim-scc";
             const std::string ParametricSettings::validateAssumptions = "mon-validate-assumptions";
             const std::string ParametricSettings::samplesMonotonicityAnalysis = "mon-samples";
+            const std::string ParametricSettings::precision = "mon-precision";
 
             ParametricSettings::ParametricSettings() : ModuleSettings(moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportResultOptionName, false, "A path to a file where the parametric result should be saved.")
@@ -41,6 +42,8 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, validateAssumptions, false, "Sets whether assumptions made in monotonicity analysis are validated").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, samplesMonotonicityAnalysis, false, "Sets whether monotonicity should be checked on samples")
                                 .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("mon-samples", "The number of samples taken in monotonicity-analysis can be given, default is 0, no samples").setDefaultValueUnsignedInteger(0).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, precision, false, "Sets precision of monotonicity checking on samples")
+                                        .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("mon-precision", "The precision of checking monotonicity on samples, default is 1e-6").setDefaultValueDouble(0.000001).build()).build());
 
             }
             
@@ -91,6 +94,10 @@ namespace storm {
             uint_fast64_t ParametricSettings::getNumberOfSamples() const {
                 return this->getOption(samplesMonotonicityAnalysis).getArgumentByName("mon-samples").getValueAsUnsignedInteger();
             }
+
+            double ParametricSettings::getMonotonicityAnalysisPrecision() const {
+                return this->getOption(precision).getArgumentByName("mon-precision").getValueAsDouble();
+            }
         } // namespace modules
     } // namespace settings
 } // namespace storm

src/storm-pars/settings/modules/ParametricSettings.h

@@ -84,6 +84,11 @@ namespace storm {
                  */
                 uint_fast64_t getNumberOfSamples() const;
 
+                /*!
+				 * Retrieves the precision for the extremal value
+				 */
+                double getMonotonicityAnalysisPrecision() const;
+
                 const static std::string moduleName;
                 
             private:
@@ -99,6 +104,7 @@ namespace storm {
                 const static std::string sccElimination;
                 const static std::string validateAssumptions;
                 const static std::string samplesMonotonicityAnalysis;
+                const static std::string precision;
             };
             
         } // namespace modules