From b178703a884709bd2aa8340f2ae143b750ee9f61 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Mon, 13 Feb 2017 15:33:39 +0100
Subject: [PATCH] Check for set of timepoints
---
.../settings/modules/DFTSettings.cpp | 36 ++++++++++++-------
src/storm-dft/settings/modules/DFTSettings.h | 33 ++++++++++++-----
2 files changed, 47 insertions(+), 22 deletions(-)
diff --git a/src/storm-dft/settings/modules/DFTSettings.cpp b/src/storm-dft/settings/modules/DFTSettings.cpp
index 8b62833a1..e20df83ec 100644
--- a/src/storm-dft/settings/modules/DFTSettings.cpp
+++ b/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,13 +121,28 @@ 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 {
return this->getOption(minValueOptionName).getHasOptionBeenSet();
}
@@ -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;
diff --git a/src/storm-dft/settings/modules/DFTSettings.h b/src/storm-dft/settings/modules/DFTSettings.h
index 0d8695e2a..662039e0f 100644
--- a/src/storm-dft/settings/modules/DFTSettings.h
+++ b/src/storm-dft/settings/modules/DFTSettings.h
@@ -110,7 +110,28 @@ namespace storm {
* @return True iff the option was set.
*/
bool usePropTimebound() const;
-
+
+ /*!
+ * 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 usePropTimepoints() const;
+
+ /*!
+ * 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.
*
@@ -124,13 +145,6 @@ namespace storm {
* @return True iff the option was set.
*/
bool isComputeMaximalValue() const;
-
- /*!
- * Retrieves the timebound for the timebound property.
- *
- * @return The timebound.
- */
- double getPropTimebound() 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