diff --git a/src/modelchecker/DFTAnalyser.h b/src/modelchecker/DFTAnalyser.h
index 519b8090a..189338b70 100644
--- a/src/modelchecker/DFTAnalyser.h
+++ b/src/modelchecker/DFTAnalyser.h
@@ -159,7 +159,7 @@ private:
explorationTime += explorationEnd -buildingEnd;
// Bisimulation
- if (model->isOfType(storm::models::ModelType::Ctmc)) {
+ if (model->isOfType(storm::models::ModelType::Ctmc) && storm::settings::getModule<storm::settings::modules::GeneralSettings>().isBisimulationSet()) {
std::cout << "Bisimulation..." << std::endl;
model = storm::performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(model->template as<storm::models::sparse::Ctmc<ValueType>>(), {formula}, storm::storage::BisimulationType::Weak)->template as<storm::models::sparse::Ctmc<ValueType>>();
//model->printModelInformationToStream(std::cout);
diff --git a/src/settings/ArgumentValidators.h b/src/settings/ArgumentValidators.h
index 6e1b4aa02..60a36b55b 100644
--- a/src/settings/ArgumentValidators.h
+++ b/src/settings/ArgumentValidators.h
@@ -46,6 +46,26 @@ namespace storm {
return rangeValidatorExcluding<int_fast64_t>(lowerBound, upperBound);
}
+ /*!
+ * Creates a validation function that checks whether an integer is greater than or equal to the given threshold.
+ *
+ * @param threshold The threshold.
+ * @return The resulting validation function.
+ */
+ static std::function<bool (int_fast64_t const&)> integerGreaterValidatorIncluding(int_fast64_t threshold) {
+ return greaterValidatorIncluding<int_fast64_t>(threshold);
+ }
+
+ /*!
+ * Creates a validation function that checks whether an integer is greater than the given threshold.
+ *
+ * @param threshold The threshold.
+ * @return The resulting validation function.
+ */
+ static std::function<bool (int_fast64_t const&)> integerGreaterValidatorExcluding(int_fast64_t threshold) {
+ return greaterValidatorExcluding<int_fast64_t>(threshold);
+ }
+
/*!
* Creates a validation function that checks whether an unsigned integer is in the given range (including the bounds).
*
@@ -67,6 +87,26 @@ namespace storm {
static std::function<bool (uint_fast64_t const&)> unsignedIntegerRangeValidatorExcluding(uint_fast64_t lowerBound, uint_fast64_t upperBound) {
return rangeValidatorExcluding<uint_fast64_t>(lowerBound, upperBound);
}
+
+ /*!
+ * Creates a validation function that checks whether an unsigned integer is greater than or equal to the given threshold.
+ *
+ * @param threshold The threshold.
+ * @return The resulting validation function.
+ */
+ static std::function<bool (uint_fast64_t const&)> unsignedIntegerGreaterValidatorIncluding(uint_fast64_t threshold) {
+ return greaterValidatorIncluding<uint_fast64_t>(threshold);
+ }
+
+ /*!
+ * Creates a validation function that checks whether an unsigned integer is greater than the given threshold.
+ *
+ * @param threshold The threshold.
+ * @return The resulting validation function.
+ */
+ static std::function<bool (uint_fast64_t const&)> unsignedIntegerGreaterValidatorExcluding(uint_fast64_t threshold) {
+ return greaterValidatorExcluding<uint_fast64_t>(threshold);
+ }
/*!
* Creates a validation function that checks whether a double is in the given range (including the bounds).
@@ -89,6 +129,26 @@ namespace storm {
static std::function<bool (double const&)> doubleRangeValidatorExcluding(double lowerBound, double upperBound) {
return rangeValidatorExcluding<double>(lowerBound, upperBound);
}
+
+ /*!
+ * Creates a validation function that checks whether a double is greater than or equal to the given threshold.
+ *
+ * @param threshold The threshold.
+ * @return The resulting validation function.
+ */
+ static std::function<bool (double const&)> doubleGreaterValidatorIncluding(double threshold) {
+ return greaterValidatorIncluding<double>(threshold);
+ }
+
+ /*!
+ * Creates a validation function that checks whether a double is greater than the given threshold.
+ *
+ * @param threshold The threshold.
+ * @return The resulting validation function.
+ */
+ static std::function<bool (double const&)> doubleGreaterValidatorExcluding(double threshold) {
+ return greaterValidatorExcluding<double>(threshold);
+ }
/*!
* Creates a validation function that checks whether a given string corresponds to an existing and readable
@@ -141,7 +201,7 @@ namespace storm {
template<typename T>
static std::function<bool (T const&)> rangeValidatorIncluding(T lowerBound, T upperBound) {
return std::bind([](T lowerBound, T upperBound, T value) -> bool {
- STORM_LOG_THROW(lowerBound <= value && value <= upperBound, storm::exceptions::InvalidArgumentException, "Value " << value << " is out range.");
+ STORM_LOG_THROW(lowerBound <= value && value <= upperBound, storm::exceptions::InvalidArgumentException, "Value " << value << " is out of range.");
return true;
}, lowerBound, upperBound, std::placeholders::_1);
}
@@ -156,10 +216,38 @@ namespace storm {
template<typename T>
static std::function<bool (T const&)> rangeValidatorExcluding(T lowerBound, T upperBound) {
return std::bind([](T lowerBound, T upperBound, T value) -> bool {
- STORM_LOG_THROW(lowerBound < value && value < upperBound, storm::exceptions::InvalidArgumentException, "Value " << value << " is out range.");
+ STORM_LOG_THROW(lowerBound < value && value < upperBound, storm::exceptions::InvalidArgumentException, "Value " << value << " is out of range.");
return true;
}, lowerBound, upperBound, std::placeholders::_1);
}
+
+ /*!
+ * Creates a validation function that checks whether its argument is greater than the given threshold.
+ *
+ * @param threshold The threshold.
+ * @return The resulting validation function.
+ */
+ template<typename T>
+ static std::function<bool (T const&)> greaterValidatorExcluding(T threshold) {
+ return std::bind([](T threshold, T value) -> bool {
+ STORM_LOG_THROW(threshold < value, storm::exceptions::InvalidArgumentException, "Value " << value << " is out of range.");
+ return true;
+ }, threshold, std::placeholders::_1);
+ }
+
+ /*!
+ * Creates a validation function that checks whether its argument is greater than or equal to the given threshold.
+ *
+ * @param threshold The threshold.
+ * @return The resulting validation function.
+ */
+ template<typename T>
+ static std::function<bool (T const&)> greaterValidatorIncluding(T threshold) {
+ return std::bind([](T threshold, T value) -> bool {
+ STORM_LOG_THROW(threshold <= value, storm::exceptions::InvalidArgumentException, "Value " << value << " is out of range.");
+ return true;
+ }, threshold, std::placeholders::_1);
+ }
};
}
}
diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp
index 2f2cb33d1..b3987f776 100644
--- a/src/settings/SettingsManager.cpp
+++ b/src/settings/SettingsManager.cpp
@@ -499,8 +499,8 @@ namespace storm {
// Register all known settings modules.
storm::settings::addModule<storm::settings::modules::GeneralSettings>();
- storm::settings::addModule<storm::settings::modules::MarkovChainSettings>();
storm::settings::addModule<storm::settings::modules::IOSettings>();
+ storm::settings::addModule<storm::settings::modules::MarkovChainSettings>();
storm::settings::addModule<storm::settings::modules::DebugSettings>();
storm::settings::addModule<storm::settings::modules::CounterexampleGeneratorSettings>();
storm::settings::addModule<storm::settings::modules::CuddSettings>();
diff --git a/src/settings/modules/DFTSettings.cpp b/src/settings/modules/DFTSettings.cpp
new file mode 100644
index 000000000..365ba0271
--- /dev/null
+++ b/src/settings/modules/DFTSettings.cpp
@@ -0,0 +1,107 @@
+#include "src/settings/modules/DFTSettings.h"
+
+#include "src/settings/SettingsManager.h"
+#include "src/settings/SettingMemento.h"
+#include "src/settings/Option.h"
+#include "src/settings/OptionBuilder.h"
+#include "src/settings/ArgumentBuilder.h"
+#include "src/settings/Argument.h"
+
+#include "src/exceptions/InvalidSettingsException.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::symmetryReductionOptionName = "symmetryreduction";
+ const std::string DFTSettings::symmetryReductionOptionShortName = "symred";
+ const std::string DFTSettings::modularisationOptionName = "modularisation";
+ const std::string DFTSettings::disableDCOptionName = "disabledc";
+ 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::minValueOptionName = "min";
+ const std::string DFTSettings::maxValueOptionName = "max";
+
+ 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.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).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, 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.").addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleGreaterValidatorExcluding(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());
+ }
+
+ bool DFTSettings::isDftFileSet() const {
+ return this->getOption(dftFileOptionName).getHasOptionBeenSet();
+ }
+
+ std::string DFTSettings::getDftFilename() const {
+ return this->getOption(dftFileOptionName).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::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::isComputeMinimalValue() const {
+ return this->getOption(minValueOptionName).getHasOptionBeenSet();
+ }
+
+ bool DFTSettings::isComputeMaximalValue() const {
+ return this->getOption(maxValueOptionName).getHasOptionBeenSet();
+ }
+
+ void DFTSettings::finalize() {
+
+ }
+
+ 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;
+ }
+
+ } // namespace modules
+ } // namespace settings
+} // namespace storm
\ No newline at end of file
diff --git a/src/settings/modules/DFTSettings.h b/src/settings/modules/DFTSettings.h
new file mode 100644
index 000000000..844953c2c
--- /dev/null
+++ b/src/settings/modules/DFTSettings.h
@@ -0,0 +1,129 @@
+#ifndef STORM_SETTINGS_MODULES_DFTSETTINGS_H_
+#define STORM_SETTINGS_MODULES_DFTSETTINGS_H_
+
+#include "storm-config.h"
+#include "src/settings/modules/ModuleSettings.h"
+
+namespace storm {
+ namespace settings {
+ namespace modules {
+
+ /*!
+ * This class represents the settings for DFT model checking.
+ */
+ class DFTSettings : public ModuleSettings {
+ public:
+
+ /*!
+ * Creates a new set of DFT settings.
+ */
+ DFTSettings();
+
+ /*!
+ * Retrieves whether the dft file option was set.
+ *
+ * @return True if the dft file option was set.
+ */
+ bool isDftFileSet() const;
+
+ /*!
+ * Retrieves the name of the file that contains the dft specification.
+ *
+ * @return The name of the file that contains the dft specification.
+ */
+ std::string getDftFilename() const;
+
+ //expectedtime, probability, timebound, prob
+ //min, max
+
+ /*!
+ * 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 property expected time should be used.
+ *
+ * @return True iff the option was set.
+ */
+ bool usePropExpectedTime() const;
+
+ /*!
+ * Retrieves whether the property probability should be used.
+ *
+ * @return True iff the option was set.
+ */
+ bool usePropProbability() const;
+
+ /*!
+ * Retrieves whether the property timebound should be used.
+ *
+ * @return True iff the option was set.
+ */
+ bool usePropTimebound() const;
+
+ /*!
+ * Retrieves whether the minimal value should be computed for non-determinism.
+ *
+ * @return True iff the option was set.
+ */
+ bool isComputeMinimalValue() const;
+
+ /*!
+ * Retrieves whether the maximal value should be computed for non-determinism.
+ *
+ * @return True iff the option was set.
+ */
+ bool isComputeMaximalValue() const;
+
+ /*!
+ * Retrieves the timebound for the timebound property.
+ *
+ * @return The timebound.
+ */
+ double getPropTimebound() const;
+
+ 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 dftFileOptionName;
+ static const std::string dftFileOptionShortName;
+ static const std::string symmetryReductionOptionName;
+ static const std::string symmetryReductionOptionShortName;
+ static const std::string modularisationOptionName;
+ static const std::string disableDCOptionName;
+ static const std::string propExpectedTimeOptionName;
+ static const std::string propExpectedTimeOptionShortName;
+ static const std::string propProbabilityOptionName;
+ static const std::string propTimeBoundOptionName;
+ static const std::string minValueOptionName;
+ static const std::string maxValueOptionName;
+
+ };
+
+ } // namespace modules
+ } // namespace settings
+} // namespace storm
+
+#endif /* STORM_SETTINGS_MODULES_DFTSETTINGS_H_ */
diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp
index 4f6c1f7e0..b71ff44e7 100644
--- a/src/storm-dyftee.cpp
+++ b/src/storm-dyftee.cpp
@@ -2,8 +2,27 @@
#include "utility/initialize.h"
#include "utility/storm.h"
#include "modelchecker/DFTAnalyser.h"
+#include "src/cli/cli.h"
+#include "src/exceptions/BaseException.h"
+#include "src/utility/macros.h"
#include <boost/lexical_cast.hpp>
+#include "src/settings/modules/GeneralSettings.h"
+#include "src/settings/modules/DFTSettings.h"
+#include "src/settings/modules/MarkovChainSettings.h"
+#include "src/settings/modules/DebugSettings.h"
+//#include "src/settings/modules/CounterexampleGeneratorSettings.h"
+//#include "src/settings/modules/CuddSettings.h"
+//#include "src/settings/modules/SylvanSettings.h"
+#include "src/settings/modules/GmmxxEquationSolverSettings.h"
+#include "src/settings/modules/NativeEquationSolverSettings.h"
+//#include "src/settings/modules/BisimulationSettings.h"
+//#include "src/settings/modules/GlpkSettings.h"
+//#include "src/settings/modules/GurobiSettings.h"
+//#include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h"
+//#include "src/settings/modules/ParametricSettings.h"
+#include "src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h"
+
/*!
* Load DFT from filename, build corresponding Model and check against given property.
*
@@ -12,8 +31,7 @@
*/
template <typename ValueType>
void analyzeDFT(std::string filename, std::string property, bool symred = false, bool allowModularisation = false, bool enableDC = true) {
- storm::settings::SettingsManager& manager = storm::settings::mutableManager();
- manager.setFromString("");
+ std::cout << "Running DFT analysis on file " << filename << " with property " << property << std::endl;
storm::parser::DFTGalileoParser<ValueType> parser;
storm::storage::DFT<ValueType> dft = parser.parseDFT(filename);
@@ -27,6 +45,30 @@ void analyzeDFT(std::string filename, std::string property, bool symred = false,
analyser.printResult();
}
+/*!
+ * Initialize the settings manager.
+ */
+void initializeSettings() {
+ storm::settings::mutableManager().setName("StoRM-DyFTeE", "storm-dft");
+
+ // Register all known settings modules.
+ storm::settings::addModule<storm::settings::modules::GeneralSettings>();
+ storm::settings::addModule<storm::settings::modules::DFTSettings>();
+ storm::settings::addModule<storm::settings::modules::MarkovChainSettings>();
+ storm::settings::addModule<storm::settings::modules::DebugSettings>();
+ //storm::settings::addModule<storm::settings::modules::CounterexampleGeneratorSettings>();
+ //storm::settings::addModule<storm::settings::modules::CuddSettings>();
+ //storm::settings::addModule<storm::settings::modules::SylvanSettings>();
+ storm::settings::addModule<storm::settings::modules::GmmxxEquationSolverSettings>();
+ storm::settings::addModule<storm::settings::modules::NativeEquationSolverSettings>();
+ //storm::settings::addModule<storm::settings::modules::BisimulationSettings>();
+ //storm::settings::addModule<storm::settings::modules::GlpkSettings>();
+ //storm::settings::addModule<storm::settings::modules::GurobiSettings>();
+ //storm::settings::addModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>();
+ //storm::settings::addModule<storm::settings::modules::ParametricSettings>();
+ storm::settings::addModule<storm::settings::modules::SparseDtmcEliminationModelCheckerSettings>();
+}
+
/*!
* Entry point for the DyFTeE backend.
*
@@ -34,91 +76,81 @@ void analyzeDFT(std::string filename, std::string property, bool symred = false,
* @param argv The argv argument of main().
* @return Return code, 0 if successfull, not 0 otherwise.
*/
-int main(int argc, char** argv) {
- if(argc < 2) {
- std::cout << "Storm-DyFTeE should be called with a filename as argument." << std::endl;
- std::cout << "./storm-dft <filename> <--prop pctl-formula> <--parametric>" << std::endl;
- return 1;
- }
-
- // Parse cli arguments
- bool parametric = false;
- bool symred = false;
- bool minimal = true;
- bool allowModular = true;
- bool enableModularisation = false;
- bool disableDC = false;
- std::string filename = argv[1];
- std::string operatorType = "";
- std::string targetFormula = "";
- std::string pctlFormula = "";
- for (int i = 2; i < argc; ++i) {
- std::string option = argv[i];
- if (option == "--parametric") {
- parametric = true;
- } else if (option == "--expectedtime") {
- assert(targetFormula.empty());
+int main(const int argc, const char** argv) {
+ try {
+ storm::utility::setUp();
+ storm::cli::printHeader("StoRM-DyFTeE", argc, argv);
+ initializeSettings();
+
+ bool optionsCorrect = storm::cli::parseOptions(argc, argv);
+ if (!optionsCorrect) {
+ return -1;
+ }
+
+ storm::settings::modules::DFTSettings const& dftSettings = storm::settings::getModule<storm::settings::modules::DFTSettings>();
+ storm::settings::modules::GeneralSettings const& generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
+ if (!dftSettings.isDftFileSet()) {
+ STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
+ }
+
+ // Set min or max
+ bool minimal = true;
+ if (dftSettings.isComputeMaximalValue()) {
+ assert(!dftSettings.isComputeMinimalValue());
+ minimal = false;
+ }
+
+ // Construct pctlFormula
+ std::string pctlFormula = "";
+ bool allowModular = true;
+ std::string operatorType = "";
+ std::string targetFormula = "";
+
+ if (generalSettings.isPropertySet()) {
+ STORM_LOG_THROW(!dftSettings.usePropExpectedTime() && !dftSettings.usePropProbability() && !dftSettings.usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given.");
+ pctlFormula = generalSettings.getProperty();
+ } else if (dftSettings.usePropExpectedTime()) {
+ STORM_LOG_THROW(!dftSettings.usePropProbability() && !dftSettings.usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given.");
operatorType = "T";
targetFormula = "F \"failed\"";
allowModular = false;
- } else if (option == "--probability") {
- assert(targetFormula.empty());
+ } else if (dftSettings.usePropProbability()) {
+ STORM_LOG_THROW(!dftSettings.usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given.");
operatorType = "P";;
targetFormula = "F \"failed\"";
- } else if (option == "--timebound") {
- assert(targetFormula.empty());
- ++i;
- assert(i < argc);
- double timeBound;
- try {
- timeBound = boost::lexical_cast<double>(argv[i]);
- } catch (boost::bad_lexical_cast e) {
- std::cerr << "The time bound '" << argv[i] << "' is not valid." << std::endl;
- return 2;
- }
+ } else {
+ STORM_LOG_THROW(dftSettings.usePropTimebound(), storm::exceptions::InvalidSettingsException, "No property given.");
std::stringstream stream;
- stream << "F<=" << timeBound << " \"failed\"";
+ stream << "F<=" << dftSettings.getPropTimebound() << " \"failed\"";
operatorType = "P";
targetFormula = stream.str();
- } else if (option == "--trace") {
- STORM_GLOBAL_LOGLEVEL_TRACE();
- } else if (option == "--debug") {
- STORM_GLOBAL_LOGLEVEL_DEBUG();
- } else if (option == "--prop") {
+ }
+
+ if (!targetFormula.empty()) {
assert(pctlFormula.empty());
- ++i;
- assert(i < argc);
- pctlFormula = argv[i];
- } else if (option == "--symred") {
- symred = true;
- } else if (option == "--modularisation") {
- enableModularisation = true;
- } else if (option == "--disabledc") {
- disableDC = true;
- } else if (option == "--min") {
- minimal = true;
- } else if (option == "--max") {
- minimal = false;
- } else {
- std::cout << "Option '" << option << "' not recognized." << std::endl;
- return 1;
+ pctlFormula = operatorType + (minimal ? "min" : "max") + "=?[" + targetFormula + "]";
}
- }
-
- // Construct pctlFormula
- if (!targetFormula.empty()) {
- assert(pctlFormula.empty());
- pctlFormula = operatorType + (minimal ? "min" : "max") + "=?[" + targetFormula + "]";
- }
-
- assert(!pctlFormula.empty());
-
- storm::utility::setUp();
- std::cout << "Running " << (parametric ? "parametric " : "") << "DFT analysis on file " << filename << " with property " << pctlFormula << std::endl;
+
+ assert(!pctlFormula.empty());
- if (parametric) {
- analyzeDFT<storm::RationalFunction>(filename, pctlFormula, symred, allowModular && enableModularisation, !disableDC );
- } else {
- analyzeDFT<double>(filename, pctlFormula, symred, allowModular && enableModularisation, !disableDC);
+ bool parametric = false;
+#ifdef STORM_HAVE_CARL
+ parametric = generalSettings.isParametricSet();
+#endif
+
+ // From this point on we are ready to carry out the actual computations.
+ if (parametric) {
+ analyzeDFT<storm::RationalFunction>(dftSettings.getDftFilename(), pctlFormula, dftSettings.useSymmetryReduction(), allowModular && dftSettings.useModularisation(), !dftSettings.isDisableDC() );
+ } else {
+ analyzeDFT<double>(dftSettings.getDftFilename(), pctlFormula, dftSettings.useSymmetryReduction(), allowModular && dftSettings.useModularisation(), !dftSettings.isDisableDC());
+ }
+
+ // All operations have now been performed, so we clean up everything and terminate.
+ storm::utility::cleanUp();
+ return 0;
+ } catch (storm::exceptions::BaseException const& exception) {
+ STORM_LOG_ERROR("An exception caused StoRM-DyFTeE to terminate. The message of the exception is: " << exception.what());
+ } catch (std::exception const& exception) {
+ STORM_LOG_ERROR("An unexpected exception occurred and caused StoRM-DyFTeE to terminate. The message of this exception is: " << exception.what());
}
}