Matthias Volk
7 years ago
12 changed files with 432 additions and 357 deletions
-
124src/storm-dft-cli/storm-dft.cpp
-
2src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
-
4src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
-
4src/storm-dft/generator/DftNextStateGenerator.cpp
-
4src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
-
51src/storm-dft/settings/DftSettings.cpp
-
11src/storm-dft/settings/DftSettings.h
-
189src/storm-dft/settings/modules/DFTSettings.cpp
-
123src/storm-dft/settings/modules/DftIOSettings.cpp
-
80src/storm-dft/settings/modules/DftIOSettings.h
-
93src/storm-dft/settings/modules/FaultTreeSettings.cpp
-
104src/storm-dft/settings/modules/FaultTreeSettings.h
@ -0,0 +1,51 @@ |
|||||
|
#include "storm-dft/settings/DftSettings.h"
|
||||
|
|
||||
|
#include "storm-dft/settings/modules/DftIOSettings.h"
|
||||
|
#include "storm-dft/settings/modules/FaultTreeSettings.h"
|
||||
|
|
||||
|
#include "storm/settings/SettingsManager.h"
|
||||
|
#include "storm/settings/modules/GeneralSettings.h"
|
||||
|
#include "storm/settings/modules/CoreSettings.h"
|
||||
|
#include "storm/settings/modules/IOSettings.h"
|
||||
|
#include "storm/settings/modules/DebugSettings.h"
|
||||
|
#include "storm/settings/modules/EigenEquationSolverSettings.h"
|
||||
|
#include "storm/settings/modules/GmmxxEquationSolverSettings.h"
|
||||
|
#include "storm/settings/modules/NativeEquationSolverSettings.h"
|
||||
|
#include "storm/settings/modules/EliminationSettings.h"
|
||||
|
#include "storm/settings/modules/MinMaxEquationSolverSettings.h"
|
||||
|
#include "storm/settings/modules/BisimulationSettings.h"
|
||||
|
#include "storm/settings/modules/ResourceSettings.h"
|
||||
|
#include "storm/settings/modules/JaniExportSettings.h"
|
||||
|
#include "storm/settings/modules/GSPNSettings.h"
|
||||
|
#include "storm/settings/modules/GSPNExportSettings.h"
|
||||
|
|
||||
|
|
||||
|
namespace storm { |
||||
|
namespace settings { |
||||
|
void initializeDftSettings(std::string const& name, std::string const& executableName) { |
||||
|
storm::settings::mutableManager().setName(name, executableName); |
||||
|
|
||||
|
// Register relevant settings modules.
|
||||
|
storm::settings::addModule<storm::settings::modules::GeneralSettings>(); |
||||
|
storm::settings::addModule<storm::settings::modules::DftIOSettings>(); |
||||
|
storm::settings::addModule<storm::settings::modules::FaultTreeSettings>(); |
||||
|
storm::settings::addModule<storm::settings::modules::IOSettings>(); |
||||
|
storm::settings::addModule<storm::settings::modules::CoreSettings>(); |
||||
|
|
||||
|
storm::settings::addModule<storm::settings::modules::DebugSettings>(); |
||||
|
storm::settings::addModule<storm::settings::modules::NativeEquationSolverSettings>(); |
||||
|
storm::settings::addModule<storm::settings::modules::GmmxxEquationSolverSettings>(); |
||||
|
storm::settings::addModule<storm::settings::modules::EigenEquationSolverSettings>(); |
||||
|
storm::settings::addModule<storm::settings::modules::EliminationSettings>(); |
||||
|
storm::settings::addModule<storm::settings::modules::MinMaxEquationSolverSettings>(); |
||||
|
// storm::settings::addModule<storm::settings::modules::BisimulationSettings>();
|
||||
|
storm::settings::addModule<storm::settings::modules::ResourceSettings>(); |
||||
|
|
||||
|
// For translation into JANI via GSPN.
|
||||
|
storm::settings::addModule<storm::settings::modules::JaniExportSettings>(); |
||||
|
storm::settings::addModule<storm::settings::modules::GSPNSettings>(); |
||||
|
storm::settings::addModule<storm::settings::modules::GSPNExportSettings>(); |
||||
|
} |
||||
|
|
||||
|
} |
||||
|
} |
||||
@ -0,0 +1,11 @@ |
|||||
|
#pragma once |
||||
|
|
||||
|
#include <string> |
||||
|
|
||||
|
namespace storm { |
||||
|
namespace settings { |
||||
|
|
||||
|
void initializeDftSettings(std::string const& name, std::string const& executableName); |
||||
|
|
||||
|
} |
||||
|
} |
||||
@ -1,189 +0,0 @@ |
|||||
#include "DFTSettings.h"
|
|
||||
|
|
||||
#include "storm/settings/SettingsManager.h"
|
|
||||
#include "storm/settings/SettingMemento.h"
|
|
||||
#include "storm/settings/Option.h"
|
|
||||
#include "storm/settings/OptionBuilder.h"
|
|
||||
#include "storm/settings/ArgumentBuilder.h"
|
|
||||
#include "storm/settings/Argument.h"
|
|
||||
|
|
||||
#include "storm/exceptions/InvalidSettingsException.h"
|
|
||||
#include "storm/exceptions/IllegalArgumentValueException.h"
|
|
||||
|
|
||||
namespace storm { |
|
||||
namespace settings { |
|
||||
namespace modules { |
|
||||
|
|
||||
const std::string DFTSettings::moduleName = "dft"; |
|
||||
const std::string DFTSettings::dftFileOptionName = "dftfile"; |
|
||||
const std::string DFTSettings::dftFileOptionShortName = "dft"; |
|
||||
const std::string DFTSettings::dftJsonFileOptionName = "dftfile-json"; |
|
||||
const std::string DFTSettings::dftJsonFileOptionShortName = "dftjson"; |
|
||||
const std::string DFTSettings::symmetryReductionOptionName = "symmetryreduction"; |
|
||||
const std::string DFTSettings::symmetryReductionOptionShortName = "symred"; |
|
||||
const std::string DFTSettings::modularisationOptionName = "modularisation"; |
|
||||
const std::string DFTSettings::disableDCOptionName = "disabledc"; |
|
||||
const std::string DFTSettings::approximationErrorOptionName = "approximation"; |
|
||||
const std::string DFTSettings::approximationErrorOptionShortName = "approx"; |
|
||||
const std::string DFTSettings::approximationHeuristicOptionName = "approximationheuristic"; |
|
||||
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::propTimepointsOptionName = "timepoints"; |
|
||||
const std::string DFTSettings::minValueOptionName = "min"; |
|
||||
const std::string DFTSettings::maxValueOptionName = "max"; |
|
||||
const std::string DFTSettings::firstDependencyOptionName = "firstdep"; |
|
||||
const std::string DFTSettings::transformToGspnOptionName = "gspn"; |
|
||||
const std::string DFTSettings::exportToJsonOptionName = "export-json"; |
|
||||
#ifdef STORM_HAVE_Z3
|
|
||||
const std::string DFTSettings::solveWithSmtOptionName = "smt"; |
|
||||
#endif
|
|
||||
|
|
||||
DFTSettings::DFTSettings() : ModuleSettings(moduleName) { |
|
||||
this->addOption(storm::settings::OptionBuilder(moduleName, dftFileOptionName, false, "Parses the model given in the Galileo format.").setShortName(dftFileOptionShortName) |
|
||||
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the DFT model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); |
|
||||
this->addOption(storm::settings::OptionBuilder(moduleName, dftJsonFileOptionName, false, "Parses the model given in the Cytoscape JSON format.").setShortName(dftJsonFileOptionShortName) |
|
||||
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file from which to read the DFT model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).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, disableDCOptionName, false, "Disable Dont Care propagation.").build()); |
|
||||
this->addOption(storm::settings::OptionBuilder(moduleName, firstDependencyOptionName, false, "Avoid non-determinism by always taking the first possible dependency.").build()); |
|
||||
this->addOption(storm::settings::OptionBuilder(moduleName, approximationErrorOptionName, false, "Approximation error allowed.").setShortName(approximationErrorOptionShortName).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("error", "The relative approximation error to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build()); |
|
||||
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, 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
|
|
||||
this->addOption(storm::settings::OptionBuilder(moduleName, solveWithSmtOptionName, true, "Solve the DFT with SMT.").build()); |
|
||||
#endif
|
|
||||
this->addOption(storm::settings::OptionBuilder(moduleName, transformToGspnOptionName, false, "Transform DFT to GSPN.").build()); |
|
||||
this->addOption(storm::settings::OptionBuilder(moduleName, exportToJsonOptionName, false, "Export the model to the Cytoscape JSON format.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file to export to.").build()).build()); |
|
||||
} |
|
||||
|
|
||||
bool DFTSettings::isDftFileSet() const { |
|
||||
return this->getOption(dftFileOptionName).getHasOptionBeenSet(); |
|
||||
} |
|
||||
|
|
||||
std::string DFTSettings::getDftFilename() const { |
|
||||
return this->getOption(dftFileOptionName).getArgumentByName("filename").getValueAsString(); |
|
||||
} |
|
||||
|
|
||||
bool DFTSettings::isDftJsonFileSet() const { |
|
||||
return this->getOption(dftJsonFileOptionName).getHasOptionBeenSet(); |
|
||||
} |
|
||||
|
|
||||
std::string DFTSettings::getDftJsonFilename() const { |
|
||||
return this->getOption(dftJsonFileOptionName).getArgumentByName("filename").getValueAsString(); |
|
||||
} |
|
||||
|
|
||||
bool DFTSettings::useSymmetryReduction() const { |
|
||||
return this->getOption(symmetryReductionOptionName).getHasOptionBeenSet(); |
|
||||
} |
|
||||
|
|
||||
bool DFTSettings::useModularisation() const { |
|
||||
return this->getOption(modularisationOptionName).getHasOptionBeenSet(); |
|
||||
} |
|
||||
|
|
||||
bool DFTSettings::isDisableDC() const { |
|
||||
return this->getOption(disableDCOptionName).getHasOptionBeenSet(); |
|
||||
} |
|
||||
|
|
||||
bool DFTSettings::isApproximationErrorSet() const { |
|
||||
return this->getOption(approximationErrorOptionName).getHasOptionBeenSet(); |
|
||||
} |
|
||||
|
|
||||
double DFTSettings::getApproximationError() const { |
|
||||
return this->getOption(approximationErrorOptionName).getArgumentByName("error").getValueAsDouble(); |
|
||||
} |
|
||||
|
|
||||
storm::builder::ApproximationHeuristic DFTSettings::getApproximationHeuristic() const { |
|
||||
if (!isApproximationErrorSet() || getApproximationError() == 0.0) { |
|
||||
// No approximation is done
|
|
||||
return storm::builder::ApproximationHeuristic::NONE; |
|
||||
} |
|
||||
std::string heuristicAsString = this->getOption(approximationHeuristicOptionName).getArgumentByName("heuristic").getValueAsString(); |
|
||||
if (heuristicAsString == "depth") { |
|
||||
return storm::builder::ApproximationHeuristic::DEPTH; |
|
||||
} else if (heuristicAsString == "probability") { |
|
||||
return storm::builder::ApproximationHeuristic::PROBABILITY; |
|
||||
} |
|
||||
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal value '" << heuristicAsString << "' set as heuristic for approximation."); |
|
||||
} |
|
||||
|
|
||||
bool DFTSettings::usePropExpectedTime() const { |
|
||||
return this->getOption(propExpectedTimeOptionName).getHasOptionBeenSet(); |
|
||||
} |
|
||||
|
|
||||
bool DFTSettings::usePropProbability() const { |
|
||||
return this->getOption(propProbabilityOptionName).getHasOptionBeenSet(); |
|
||||
} |
|
||||
|
|
||||
bool DFTSettings::usePropTimebound() const { |
|
||||
return this->getOption(propTimeboundOptionName).getHasOptionBeenSet(); |
|
||||
} |
|
||||
|
|
||||
double DFTSettings::getPropTimebound() const { |
|
||||
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(); |
|
||||
} |
|
||||
|
|
||||
bool DFTSettings::isComputeMaximalValue() const { |
|
||||
return this->getOption(maxValueOptionName).getHasOptionBeenSet(); |
|
||||
} |
|
||||
|
|
||||
bool DFTSettings::isTakeFirstDependency() const { |
|
||||
return this->getOption(firstDependencyOptionName).getHasOptionBeenSet(); |
|
||||
} |
|
||||
|
|
||||
#ifdef STORM_HAVE_Z3
|
|
||||
bool DFTSettings::solveWithSMT() const { |
|
||||
return this->getOption(solveWithSmtOptionName).getHasOptionBeenSet(); |
|
||||
} |
|
||||
#endif
|
|
||||
|
|
||||
bool DFTSettings::isTransformToGspn() const { |
|
||||
return this->getOption(transformToGspnOptionName).getHasOptionBeenSet(); |
|
||||
} |
|
||||
|
|
||||
bool DFTSettings::isExportToJson() const { |
|
||||
return this->getOption(exportToJsonOptionName).getHasOptionBeenSet(); |
|
||||
} |
|
||||
|
|
||||
std::string DFTSettings::getExportJsonFilename() const { |
|
||||
return this->getOption(exportToJsonOptionName).getArgumentByName("filename").getValueAsString(); |
|
||||
} |
|
||||
|
|
||||
void DFTSettings::finalize() { |
|
||||
} |
|
||||
|
|
||||
bool DFTSettings::check() const { |
|
||||
// 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; |
|
||||
} |
|
||||
|
|
||||
} // namespace modules
|
|
||||
} // namespace settings
|
|
||||
} // namespace storm
|
|
||||
@ -0,0 +1,123 @@ |
|||||
|
#include "DftIOSettings.h"
|
||||
|
|
||||
|
#include "storm/settings/SettingsManager.h"
|
||||
|
#include "storm/settings/SettingMemento.h"
|
||||
|
#include "storm/settings/Option.h"
|
||||
|
#include "storm/settings/OptionBuilder.h"
|
||||
|
#include "storm/settings/ArgumentBuilder.h"
|
||||
|
#include "storm/settings/Argument.h"
|
||||
|
#include "storm/exceptions/InvalidSettingsException.h"
|
||||
|
|
||||
|
namespace storm { |
||||
|
namespace settings { |
||||
|
namespace modules { |
||||
|
|
||||
|
const std::string DftIOSettings::moduleName = "dftIO"; |
||||
|
const std::string DftIOSettings::dftFileOptionName = "dftfile"; |
||||
|
const std::string DftIOSettings::dftFileOptionShortName = "dft"; |
||||
|
const std::string DftIOSettings::dftJsonFileOptionName = "dftfile-json"; |
||||
|
const std::string DftIOSettings::dftJsonFileOptionShortName = "dftjson"; |
||||
|
const std::string DftIOSettings::propExpectedTimeOptionName = "expectedtime"; |
||||
|
const std::string DftIOSettings::propExpectedTimeOptionShortName = "mttf"; |
||||
|
const std::string DftIOSettings::propProbabilityOptionName = "probability"; |
||||
|
const std::string DftIOSettings::propTimeboundOptionName = "timebound"; |
||||
|
const std::string DftIOSettings::propTimepointsOptionName = "timepoints"; |
||||
|
const std::string DftIOSettings::minValueOptionName = "min"; |
||||
|
const std::string DftIOSettings::maxValueOptionName = "max"; |
||||
|
const std::string DftIOSettings::transformToGspnOptionName = "gspn"; |
||||
|
const std::string DftIOSettings::exportToJsonOptionName = "export-json"; |
||||
|
|
||||
|
DftIOSettings::DftIOSettings() : ModuleSettings(moduleName) { |
||||
|
this->addOption(storm::settings::OptionBuilder(moduleName, dftFileOptionName, false, "Parses the model given in the Galileo format.").setShortName(dftFileOptionShortName) |
||||
|
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the DFT model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); |
||||
|
this->addOption(storm::settings::OptionBuilder(moduleName, dftJsonFileOptionName, false, "Parses the model given in the Cytoscape JSON format.").setShortName(dftJsonFileOptionShortName) |
||||
|
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file from which to read the DFT model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).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, 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()); |
||||
|
this->addOption(storm::settings::OptionBuilder(moduleName, transformToGspnOptionName, false, "Transform DFT to GSPN.").build()); |
||||
|
this->addOption(storm::settings::OptionBuilder(moduleName, exportToJsonOptionName, false, "Export the model to the Cytoscape JSON format.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file to export to.").build()).build()); |
||||
|
} |
||||
|
|
||||
|
bool DftIOSettings::isDftFileSet() const { |
||||
|
return this->getOption(dftFileOptionName).getHasOptionBeenSet(); |
||||
|
} |
||||
|
|
||||
|
std::string DftIOSettings::getDftFilename() const { |
||||
|
return this->getOption(dftFileOptionName).getArgumentByName("filename").getValueAsString(); |
||||
|
} |
||||
|
|
||||
|
bool DftIOSettings::isDftJsonFileSet() const { |
||||
|
return this->getOption(dftJsonFileOptionName).getHasOptionBeenSet(); |
||||
|
} |
||||
|
|
||||
|
std::string DftIOSettings::getDftJsonFilename() const { |
||||
|
return this->getOption(dftJsonFileOptionName).getArgumentByName("filename").getValueAsString(); |
||||
|
} |
||||
|
|
||||
|
bool DftIOSettings::usePropExpectedTime() const { |
||||
|
return this->getOption(propExpectedTimeOptionName).getHasOptionBeenSet(); |
||||
|
} |
||||
|
|
||||
|
bool DftIOSettings::usePropProbability() const { |
||||
|
return this->getOption(propProbabilityOptionName).getHasOptionBeenSet(); |
||||
|
} |
||||
|
|
||||
|
bool DftIOSettings::usePropTimebound() const { |
||||
|
return this->getOption(propTimeboundOptionName).getHasOptionBeenSet(); |
||||
|
} |
||||
|
|
||||
|
double DftIOSettings::getPropTimebound() const { |
||||
|
return this->getOption(propTimeboundOptionName).getArgumentByName("time").getValueAsDouble(); |
||||
|
} |
||||
|
|
||||
|
bool DftIOSettings::usePropTimepoints() const { |
||||
|
return this->getOption(propTimepointsOptionName).getHasOptionBeenSet(); |
||||
|
} |
||||
|
|
||||
|
std::vector<double> DftIOSettings::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 DftIOSettings::isComputeMinimalValue() const { |
||||
|
return this->getOption(minValueOptionName).getHasOptionBeenSet(); |
||||
|
} |
||||
|
|
||||
|
bool DftIOSettings::isComputeMaximalValue() const { |
||||
|
return this->getOption(maxValueOptionName).getHasOptionBeenSet(); |
||||
|
} |
||||
|
|
||||
|
bool DftIOSettings::isTransformToGspn() const { |
||||
|
return this->getOption(transformToGspnOptionName).getHasOptionBeenSet(); |
||||
|
} |
||||
|
|
||||
|
bool DftIOSettings::isExportToJson() const { |
||||
|
return this->getOption(exportToJsonOptionName).getHasOptionBeenSet(); |
||||
|
} |
||||
|
|
||||
|
std::string DftIOSettings::getExportJsonFilename() const { |
||||
|
return this->getOption(exportToJsonOptionName).getArgumentByName("filename").getValueAsString(); |
||||
|
} |
||||
|
|
||||
|
void DftIOSettings::finalize() { |
||||
|
} |
||||
|
|
||||
|
bool DftIOSettings::check() const { |
||||
|
// 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; |
||||
|
} |
||||
|
|
||||
|
} // namespace modules
|
||||
|
} // namespace settings
|
||||
|
} // namespace storm
|
||||
@ -0,0 +1,93 @@ |
|||||
|
#include "FaultTreeSettings.h"
|
||||
|
|
||||
|
#include "storm/settings/SettingsManager.h"
|
||||
|
#include "storm/settings/SettingMemento.h"
|
||||
|
#include "storm/settings/Option.h"
|
||||
|
#include "storm/settings/OptionBuilder.h"
|
||||
|
#include "storm/settings/ArgumentBuilder.h"
|
||||
|
#include "storm/settings/Argument.h"
|
||||
|
#include "storm/exceptions/IllegalArgumentValueException.h"
|
||||
|
|
||||
|
namespace storm { |
||||
|
namespace settings { |
||||
|
namespace modules { |
||||
|
|
||||
|
const std::string FaultTreeSettings::moduleName = "dft"; |
||||
|
const std::string FaultTreeSettings::symmetryReductionOptionName = "symmetryreduction"; |
||||
|
const std::string FaultTreeSettings::symmetryReductionOptionShortName = "symred"; |
||||
|
const std::string FaultTreeSettings::modularisationOptionName = "modularisation"; |
||||
|
const std::string FaultTreeSettings::disableDCOptionName = "disabledc"; |
||||
|
const std::string FaultTreeSettings::approximationErrorOptionName = "approximation"; |
||||
|
const std::string FaultTreeSettings::approximationErrorOptionShortName = "approx"; |
||||
|
const std::string FaultTreeSettings::approximationHeuristicOptionName = "approximationheuristic"; |
||||
|
const std::string FaultTreeSettings::firstDependencyOptionName = "firstdep"; |
||||
|
#ifdef STORM_HAVE_Z3
|
||||
|
const std::string FaultTreeSettings::solveWithSmtOptionName = "smt"; |
||||
|
#endif
|
||||
|
|
||||
|
FaultTreeSettings::FaultTreeSettings() : ModuleSettings(moduleName) { |
||||
|
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, disableDCOptionName, false, "Disable Dont Care propagation.").build()); |
||||
|
this->addOption(storm::settings::OptionBuilder(moduleName, firstDependencyOptionName, false, "Avoid non-determinism by always taking the first possible dependency.").build()); |
||||
|
this->addOption(storm::settings::OptionBuilder(moduleName, approximationErrorOptionName, false, "Approximation error allowed.").setShortName(approximationErrorOptionShortName).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("error", "The relative approximation error to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build()); |
||||
|
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()); |
||||
|
#ifdef STORM_HAVE_Z3
|
||||
|
this->addOption(storm::settings::OptionBuilder(moduleName, solveWithSmtOptionName, true, "Solve the DFT with SMT.").build()); |
||||
|
#endif
|
||||
|
} |
||||
|
|
||||
|
bool FaultTreeSettings::useSymmetryReduction() const { |
||||
|
return this->getOption(symmetryReductionOptionName).getHasOptionBeenSet(); |
||||
|
} |
||||
|
|
||||
|
bool FaultTreeSettings::useModularisation() const { |
||||
|
return this->getOption(modularisationOptionName).getHasOptionBeenSet(); |
||||
|
} |
||||
|
|
||||
|
bool FaultTreeSettings::isDisableDC() const { |
||||
|
return this->getOption(disableDCOptionName).getHasOptionBeenSet(); |
||||
|
} |
||||
|
|
||||
|
bool FaultTreeSettings::isApproximationErrorSet() const { |
||||
|
return this->getOption(approximationErrorOptionName).getHasOptionBeenSet(); |
||||
|
} |
||||
|
|
||||
|
double FaultTreeSettings::getApproximationError() const { |
||||
|
return this->getOption(approximationErrorOptionName).getArgumentByName("error").getValueAsDouble(); |
||||
|
} |
||||
|
|
||||
|
storm::builder::ApproximationHeuristic FaultTreeSettings::getApproximationHeuristic() const { |
||||
|
if (!isApproximationErrorSet() || getApproximationError() == 0.0) { |
||||
|
// No approximation is done
|
||||
|
return storm::builder::ApproximationHeuristic::NONE; |
||||
|
} |
||||
|
std::string heuristicAsString = this->getOption(approximationHeuristicOptionName).getArgumentByName("heuristic").getValueAsString(); |
||||
|
if (heuristicAsString == "depth") { |
||||
|
return storm::builder::ApproximationHeuristic::DEPTH; |
||||
|
} else if (heuristicAsString == "probability") { |
||||
|
return storm::builder::ApproximationHeuristic::PROBABILITY; |
||||
|
} |
||||
|
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal value '" << heuristicAsString << "' set as heuristic for approximation."); |
||||
|
} |
||||
|
|
||||
|
bool FaultTreeSettings::isTakeFirstDependency() const { |
||||
|
return this->getOption(firstDependencyOptionName).getHasOptionBeenSet(); |
||||
|
} |
||||
|
|
||||
|
#ifdef STORM_HAVE_Z3
|
||||
|
bool FaultTreeSettings::solveWithSMT() const { |
||||
|
return this->getOption(solveWithSmtOptionName).getHasOptionBeenSet(); |
||||
|
} |
||||
|
#endif
|
||||
|
|
||||
|
void FaultTreeSettings::finalize() { |
||||
|
} |
||||
|
|
||||
|
bool FaultTreeSettings::check() const { |
||||
|
return true; |
||||
|
} |
||||
|
|
||||
|
} // namespace modules
|
||||
|
} // namespace settings
|
||||
|
} // namespace storm
|
||||
@ -0,0 +1,104 @@ |
|||||
|
#pragma once |
||||
|
|
||||
|
#include "storm/settings/modules/ModuleSettings.h" |
||||
|
#include "storm-dft/builder/DftExplorationHeuristic.h" |
||||
|
#include "storm-config.h" |
||||
|
|
||||
|
namespace storm { |
||||
|
namespace settings { |
||||
|
namespace modules { |
||||
|
|
||||
|
/*! |
||||
|
* This class represents the settings for DFT model checking. |
||||
|
*/ |
||||
|
class FaultTreeSettings : public ModuleSettings { |
||||
|
public: |
||||
|
|
||||
|
/*! |
||||
|
* Creates a new set of DFT settings. |
||||
|
*/ |
||||
|
FaultTreeSettings(); |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves whether the option to use symmetry reduction is set. |
||||
|
* |
||||
|
* @return True iff the option was set. |
||||
|
*/ |
||||
|
bool useSymmetryReduction() const; |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves whether the option to use modularisation is set. |
||||
|
* |
||||
|
* @return True iff the option was set. |
||||
|
*/ |
||||
|
bool useModularisation() const; |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves whether the option to disable Dont Care propagation is set. |
||||
|
* |
||||
|
* @return True iff the option was set. |
||||
|
*/ |
||||
|
bool isDisableDC() const; |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves whether the option to compute an approximation is set. |
||||
|
* |
||||
|
* @return True iff the option was set. |
||||
|
*/ |
||||
|
bool isApproximationErrorSet() const; |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves the relative error allowed for approximating the model checking result. |
||||
|
* |
||||
|
* @return The allowed errorbound. |
||||
|
*/ |
||||
|
double getApproximationError() const; |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves the heuristic used for approximation. |
||||
|
* |
||||
|
* @return The heuristic to use. |
||||
|
*/ |
||||
|
storm::builder::ApproximationHeuristic getApproximationHeuristic() const; |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves whether the non-determinism should be avoided by always taking the first possible dependency. |
||||
|
* |
||||
|
* @return True iff the option was set. |
||||
|
*/ |
||||
|
bool isTakeFirstDependency() const; |
||||
|
|
||||
|
#ifdef STORM_HAVE_Z3 |
||||
|
/*! |
||||
|
* Retrieves whether the DFT should be checked via SMT. |
||||
|
* |
||||
|
* @return True iff the option was set. |
||||
|
*/ |
||||
|
bool solveWithSMT() const; |
||||
|
#endif |
||||
|
|
||||
|
bool check() const override; |
||||
|
void finalize() override; |
||||
|
|
||||
|
// The name of the module. |
||||
|
static const std::string moduleName; |
||||
|
|
||||
|
private: |
||||
|
// Define the string names of the options as constants. |
||||
|
static const std::string symmetryReductionOptionName; |
||||
|
static const std::string symmetryReductionOptionShortName; |
||||
|
static const std::string modularisationOptionName; |
||||
|
static const std::string disableDCOptionName; |
||||
|
static const std::string approximationErrorOptionName; |
||||
|
static const std::string approximationErrorOptionShortName; |
||||
|
static const std::string approximationHeuristicOptionName; |
||||
|
static const std::string firstDependencyOptionName; |
||||
|
#ifdef STORM_HAVE_Z3 |
||||
|
static const std::string solveWithSmtOptionName; |
||||
|
#endif |
||||
|
|
||||
|
}; |
||||
|
|
||||
|
} // namespace modules |
||||
|
} // namespace settings |
||||
|
} // namespace storm |
||||
Write
Preview
Loading…
Cancel
Save
Reference in new issue