Check for set of timepoints

src/storm-dft/settings/modules/DFTSettings.cpp

@@ -29,7 +29,8 @@ namespace storm {
             const std::string DFTSettings::propExpectedTimeOptionName = "expectedtime";
             const std::string DFTSettings::propExpectedTimeOptionShortName = "mttf";
             const std::string DFTSettings::propProbabilityOptionName = "probability";
-            const std::string DFTSettings::propTimeBoundOptionName = "timebound";
+            const std::string DFTSettings::propTimeboundOptionName = "timebound";
+            const std::string DFTSettings::propTimepointsOptionName = "timepoints";
             const std::string DFTSettings::minValueOptionName = "min";
             const std::string DFTSettings::maxValueOptionName = "max";
             const std::string DFTSettings::transformToGspnOptionName = "gspn";
@@ -50,7 +51,8 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, approximationHeuristicOptionName, false, "Set the heuristic used for approximation.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("heuristic", "Sets which heuristic is used for approximation. Must be in {depth, probability}. Default is").setDefaultValueString("depth").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator({"depth", "rateratio"})).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, propExpectedTimeOptionName, false, "Compute expected time of system failure.").setShortName(propExpectedTimeOptionShortName).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, propProbabilityOptionName, false, "Compute probability of system failure.").build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, propTimeBoundOptionName, false, "Compute probability of system failure up to given timebound.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("time", "The timebound to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterValidator(0.0)).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, propTimeboundOptionName, false, "Compute probability of system failure up to given timebound.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("time", "The timebound to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterValidator(0.0)).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, propTimepointsOptionName, false, "Compute probability of system failure up to given timebound for a set of given timepoints [starttime, starttime+inc, starttime+2inc, ... ,endtime]").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("starttime", "The timebound to start from.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("endtime", "The timebound to end with.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("inc", "The value to increment with to get the next timepoint.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, minValueOptionName, false, "Compute minimal value in case of non-determinism.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, maxValueOptionName, false, "Compute maximal value in case of non-determinism.").build());
 #ifdef STORM_HAVE_Z3
@@ -119,11 +121,26 @@ namespace storm {
             }
             
             bool DFTSettings::usePropTimebound() const {
-                return this->getOption(propTimeBoundOptionName).getHasOptionBeenSet();
+                return this->getOption(propTimeboundOptionName).getHasOptionBeenSet();
             }
 
             double DFTSettings::getPropTimebound() const {
-                return this->getOption(propTimeBoundOptionName).getArgumentByName("time").getValueAsDouble();
+                return this->getOption(propTimeboundOptionName).getArgumentByName("time").getValueAsDouble();
+            }
+
+            bool DFTSettings::usePropTimepoints() const {
+                return this->getOption(propTimepointsOptionName).getHasOptionBeenSet();
+            }
+
+            std::vector<double> DFTSettings::getPropTimepoints() const {
+                double starttime = this->getOption(propTimepointsOptionName).getArgumentByName("starttime").getValueAsDouble();
+                double endtime = this->getOption(propTimepointsOptionName).getArgumentByName("endtime").getValueAsDouble();
+                double inc = this->getOption(propTimepointsOptionName).getArgumentByName("inc").getValueAsDouble();
+                std::vector<double> timepoints;
+                for (double time = starttime; time <= endtime; time += inc) {
+                    timepoints.push_back(time);
+                }
+                return timepoints;
             }
 
             bool DFTSettings::isComputeMinimalValue() const {
@@ -156,13 +173,6 @@ namespace storm {
             }
 
             bool DFTSettings::check() const {
-                // Ensure that only one property is given.
-                if (usePropExpectedTime()) {
-                    STORM_LOG_THROW(!usePropProbability() && !usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given.");
-                } else if (usePropProbability()) {
-                    STORM_LOG_THROW(!usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given.");
-                }
-                
                 // Ensure that at most one of min or max is set
                 STORM_LOG_THROW(!isComputeMinimalValue() || !isComputeMaximalValue(), storm::exceptions::InvalidSettingsException, "Min and max can not both be set.");
                 return true;

src/storm-dft/settings/modules/DFTSettings.h

@@ -112,25 +112,39 @@ namespace storm {
                 bool usePropTimebound() const;
 
                 /*!
-                 * Retrieves whether the minimal value should be computed for non-determinism.
+                 * Retrieves the timebound for the timebound property.
+                 *
+                 * @return The timebound.
+                 */
+                double getPropTimebound() const;
+
+                /*!
+                 * Retrieves whether the property timepoints should be used.
                  *
                  * @return True iff the option was set.
                  */
-                bool isComputeMinimalValue() const;
+                bool usePropTimepoints() const;
 
                 /*!
-                 * Retrieves whether the maximal value should be computed for non-determinism.
+                 * Retrieves the settings for the timepoints property.
+                 *
+                 * @return The timepoints.
+                 */
+                std::vector<double> getPropTimepoints() const;
+
+                /*!
+                 * Retrieves whether the minimal value should be computed for non-determinism.
                  *
                  * @return True iff the option was set.
                  */
-                bool isComputeMaximalValue() const;
+                bool isComputeMinimalValue() const;
 
                 /*!
-                 * Retrieves the timebound for the timebound property.
+                 * Retrieves whether the maximal value should be computed for non-determinism.
                  *
-                 * @return The timebound.
+                 * @return True iff the option was set.
                  */
-                double getPropTimebound() const;
+                bool isComputeMaximalValue() const;
 
                 /*!
                  * Retrieves whether the DFT should be transformed into a GSPN.
@@ -184,7 +198,8 @@ namespace storm {
                 static const std::string propExpectedTimeOptionName;
                 static const std::string propExpectedTimeOptionShortName;
                 static const std::string propProbabilityOptionName;
-                static const std::string propTimeBoundOptionName;
+                static const std::string propTimeboundOptionName;
+                static const std::string propTimepointsOptionName;
                 static const std::string minValueOptionName;
                 static const std::string maxValueOptionName;
 #ifdef STORM_HAVE_Z3