Browse Source

Introduced setting for DFT approximation

Former-commit-id: 03a2c0ca0c
tempestpy_adaptions
Mavo 9 years ago
parent
commit
a0cd149054
  1. 4
      src/builder/ExplicitDFTModelBuilder.cpp
  2. 9
      src/settings/modules/DFTSettings.cpp
  3. 9
      src/settings/modules/DFTSettings.h

4
src/builder/ExplicitDFTModelBuilder.cpp

@ -4,7 +4,7 @@
#include <src/utility/constants.h> #include <src/utility/constants.h>
#include <src/utility/vector.h> #include <src/utility/vector.h>
#include <src/exceptions/UnexpectedException.h> #include <src/exceptions/UnexpectedException.h>
#include "src/settings/modules/DebugSettings.h"
#include "src/settings/modules/DFTSettings.h"
#include "src/settings/SettingsManager.h" #include "src/settings/SettingsManager.h"
#include <map> #include <map>
@ -226,7 +226,7 @@ namespace storm {
STORM_LOG_ASSERT(nextBEPair.second == hasDependencies, "Failure due to dependencies does not match."); STORM_LOG_ASSERT(nextBEPair.second == hasDependencies, "Failure due to dependencies does not match.");
STORM_LOG_TRACE("With the failure of: " << nextBE->name() << " [" << nextBE->id() << "] in " << mDft.getStateString(state)); STORM_LOG_TRACE("With the failure of: " << nextBE->name() << " [" << nextBE->id() << "] in " << mDft.getStateString(state));
if (storm::settings::getModule<storm::settings::modules::DebugSettings>().isTestSet()) {
if (storm::settings::getModule<storm::settings::modules::DFTSettings>().computeApproximation()) {
if (!storm::utility::isZero(exitRate)) { if (!storm::utility::isZero(exitRate)) {
ValueType rate = nextBE->activeFailureRate(); ValueType rate = nextBE->activeFailureRate();
ValueType div = rate / exitRate; ValueType div = rate / exitRate;

9
src/settings/modules/DFTSettings.cpp

@ -21,6 +21,8 @@ namespace storm {
const std::string DFTSettings::symmetryReductionOptionShortName = "symred"; const std::string DFTSettings::symmetryReductionOptionShortName = "symred";
const std::string DFTSettings::modularisationOptionName = "modularisation"; const std::string DFTSettings::modularisationOptionName = "modularisation";
const std::string DFTSettings::disableDCOptionName = "disabledc"; const std::string DFTSettings::disableDCOptionName = "disabledc";
const std::string DFTSettings::computeApproximationOptionName = "approximation";
const std::string DFTSettings::computeApproximationOptionShortName = "approx";
const std::string DFTSettings::propExpectedTimeOptionName = "expectedtime"; const std::string DFTSettings::propExpectedTimeOptionName = "expectedtime";
const std::string DFTSettings::propExpectedTimeOptionShortName = "mttf"; const std::string DFTSettings::propExpectedTimeOptionShortName = "mttf";
const std::string DFTSettings::propProbabilityOptionName = "probability"; const std::string DFTSettings::propProbabilityOptionName = "probability";
@ -37,6 +39,7 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, symmetryReductionOptionName, false, "Exploit symmetric structure of model.").setShortName(symmetryReductionOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, symmetryReductionOptionName, false, "Exploit symmetric structure of model.").setShortName(symmetryReductionOptionShortName).build());
this->addOption(storm::settings::OptionBuilder(moduleName, modularisationOptionName, false, "Use modularisation (not applicable for expected time).").build()); this->addOption(storm::settings::OptionBuilder(moduleName, modularisationOptionName, false, "Use modularisation (not applicable for expected time).").build());
this->addOption(storm::settings::OptionBuilder(moduleName, disableDCOptionName, false, "Disable Dont Care propagation.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, disableDCOptionName, false, "Disable Dont Care propagation.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, computeApproximationOptionName, false, "Compute an approximation.").setShortName(computeApproximationOptionShortName).build());
this->addOption(storm::settings::OptionBuilder(moduleName, propExpectedTimeOptionName, false, "Compute expected time of system failure.").setShortName(propExpectedTimeOptionShortName).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, 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.").addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleGreaterValidatorExcluding(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.").addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleGreaterValidatorExcluding(0.0)).build()).build());
@ -67,6 +70,10 @@ namespace storm {
return this->getOption(disableDCOptionName).getHasOptionBeenSet(); return this->getOption(disableDCOptionName).getHasOptionBeenSet();
} }
bool DFTSettings::computeApproximation() const {
return this->getOption(computeApproximationOptionName).getHasOptionBeenSet();
}
bool DFTSettings::usePropExpectedTime() const { bool DFTSettings::usePropExpectedTime() const {
return this->getOption(propExpectedTimeOptionName).getHasOptionBeenSet(); return this->getOption(propExpectedTimeOptionName).getHasOptionBeenSet();
} }
@ -116,4 +123,4 @@ namespace storm {
} // namespace modules } // namespace modules
} // namespace settings } // namespace settings
} // namespace storm
} // namespace storm

9
src/settings/modules/DFTSettings.h

@ -57,6 +57,13 @@ namespace storm {
*/ */
bool isDisableDC() const; bool isDisableDC() const;
/*!
* Retrieves whether the option to compute an approximation is set.
*
* @return True iff the option was set.
*/
bool computeApproximation() const;
/*! /*!
* Retrieves whether the property expected time should be used. * Retrieves whether the property expected time should be used.
* *
@ -122,6 +129,8 @@ namespace storm {
static const std::string symmetryReductionOptionShortName; static const std::string symmetryReductionOptionShortName;
static const std::string modularisationOptionName; static const std::string modularisationOptionName;
static const std::string disableDCOptionName; static const std::string disableDCOptionName;
static const std::string computeApproximationOptionName;
static const std::string computeApproximationOptionShortName;
static const std::string propExpectedTimeOptionName; static const std::string propExpectedTimeOptionName;
static const std::string propExpectedTimeOptionShortName; static const std::string propExpectedTimeOptionShortName;
static const std::string propProbabilityOptionName; static const std::string propProbabilityOptionName;

Loading…
Cancel
Save