Merge remote-tracking branch 'origin/dft_gspn' into dft_gspn

src/storm-dft-cli/storm-dft.cpp

@@ -3,6 +3,7 @@
 #include "storm-dft/settings/DftSettings.h"
 #include "storm-dft/settings/modules/DftIOSettings.h"
 #include "storm-dft/settings/modules/FaultTreeSettings.h"
+#include "storm-dft/settings/modules/DftGspnSettings.h"
 #include "storm/settings/modules/IOSettings.h"
 #include "storm/settings/modules/ResourceSettings.h"
 
@@ -20,6 +21,8 @@ void processOptions() {
     storm::settings::modules::DftIOSettings const& dftIOSettings = storm::settings::getModule<storm::settings::modules::DftIOSettings>();
     storm::settings::modules::FaultTreeSettings const& faultTreeSettings = storm::settings::getModule<storm::settings::modules::FaultTreeSettings>();
     storm::settings::modules::IOSettings const& ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
+    storm::settings::modules::DftGspnSettings const& dftGspnSettings = storm::settings::getModule<storm::settings::modules::DftGspnSettings>();
+
 
     if (!dftIOSettings.isDftFileSet() && !dftIOSettings.isDftJsonFileSet()) {
         STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
@@ -47,7 +50,7 @@ void processOptions() {
         return;
     }
 
-        if (dftIOSettings.isTransformToGspn()) {
+    if (dftGspnSettings.isTransformToGspn()) {
         // Transform to GSPN
         storm::api::transformToGSPN(*dft);
         return;
@@ -107,7 +110,8 @@ void processOptions() {
     // Carry out the actual analysis
     if (faultTreeSettings.isApproximationErrorSet()) {
         // Approximate analysis
-            storm::api::analyzeDFTApprox<ValueType>(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), faultTreeSettings.getApproximationError(), true);
+        storm::api::analyzeDFTApprox<ValueType>(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(),
+                                                faultTreeSettings.getApproximationError(), true);
     } else {
         storm::api::analyzeDFT<ValueType>(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), true);
     }

src/storm-dft/api/storm-dft.cpp

@@ -1,6 +1,7 @@
 #include "storm-dft/api/storm-dft.h"
 
 #include "storm-dft/settings/modules/FaultTreeSettings.h"
+#include "storm-dft/settings/modules/DftGspnSettings.h"
 
 namespace storm {
     namespace api {
@@ -29,13 +30,11 @@ namespace storm {
 
         template<>
         void transformToGSPN(storm::storage::DFT<double> const& dft) {
-            // TODO make choosable
-            bool smart = true;
-            bool mergeDCFailed = true;
+            storm::settings::modules::FaultTreeSettings const& ftSettings = storm::settings::getModule<storm::settings::modules::FaultTreeSettings>();
+            storm::settings::modules::DftGspnSettings const& dftGspnSettings = storm::settings::getModule<storm::settings::modules::DftGspnSettings>();
 
             // Set Don't Care elements
             std::set<uint64_t> dontCareElements;
-            storm::settings::modules::FaultTreeSettings const& ftSettings = storm::settings::getModule<storm::settings::modules::FaultTreeSettings>();
             if (!ftSettings.isDisableDC()) {
                 // Insert all elements as Don't Care elements
                 for (std::size_t i = 0; i < dft.nrElements(); i++) {
@@ -46,7 +45,7 @@ namespace storm {
             // Transform to GSPN
             storm::transformations::dft::DftToGspnTransformator<double> gspnTransformator(dft);
             auto priorities = gspnTransformator.computePriorities();
-            gspnTransformator.transform(priorities, dontCareElements, smart, mergeDCFailed);
+            gspnTransformator.transform(priorities, dontCareElements, !dftGspnSettings.isDisableSmartTransformation(), dftGspnSettings.isMergeDCFailed());
             storm::gspn::GSPN* gspn = gspnTransformator.obtainGSPN();
             uint64_t toplevelFailedPlace = gspnTransformator.toplevelFailedPlaceId();
 

src/storm-dft/settings/DftSettings.cpp

@@ -2,6 +2,7 @@
 
 #include "storm-dft/settings/modules/DftIOSettings.h"
 #include "storm-dft/settings/modules/FaultTreeSettings.h"
+#include "storm-dft/settings/modules/DftGspnSettings.h"
 
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/GeneralSettings.h"
@@ -33,6 +34,7 @@ namespace storm {
             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::DftGspnSettings>();
             storm::settings::addModule<storm::settings::modules::IOSettings>();
             storm::settings::addModule<storm::settings::modules::CoreSettings>();
 

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

@@ -0,0 +1,52 @@
+#include "DftGspnSettings.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 DftGspnSettings::moduleName = "dftGspn";
+            const std::string DftGspnSettings::transformToGspnOptionName = "to-gspn";
+            const std::string DftGspnSettings::disableSmartTransformationOptionName = "disable-smart";
+            const std::string DftGspnSettings::mergeDCFailedOptionName = "merge-dc-failed";
+
+
+            DftGspnSettings::DftGspnSettings() : ModuleSettings(moduleName) {
+                this->addOption(storm::settings::OptionBuilder(moduleName, transformToGspnOptionName, false, "Transform DFT to GSPN.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, disableSmartTransformationOptionName, false, "Disable smart transformation.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, mergeDCFailedOptionName, false, "Enable merging of Don't Care and Failed places into a combined place.").build());
+            }
+
+            bool DftGspnSettings::isTransformToGspn() const {
+                return this->getOption(transformToGspnOptionName).getHasOptionBeenSet();
+            }
+
+            bool DftGspnSettings::isDisableSmartTransformation() const {
+                return this->getOption(disableSmartTransformationOptionName).getHasOptionBeenSet();
+            }
+
+            bool DftGspnSettings::isMergeDCFailed() const {
+                return this->getOption(mergeDCFailedOptionName).getHasOptionBeenSet();
+            }
+
+            void DftGspnSettings::finalize() {
+            }
+
+            bool DftGspnSettings::check() const {
+                // Ensure that GSPN option is set if other options are set.
+                STORM_LOG_THROW(isTransformToGspn() || (!isDisableSmartTransformation() && !isMergeDCFailed()), storm::exceptions::InvalidSettingsException,
+                                "GSPN transformation should be enabled when giving options for the transformation.");
+                return true;
+            }
+
+        } // namespace modules
+    } // namespace settings
+} // namespace storm
+

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

@@ -0,0 +1,58 @@
+#pragma once
+
+#include "storm/settings/modules/ModuleSettings.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+
+            /*!
+             * This class represents the settings for operations concerning the DFT to GSPN transformation.
+             */
+            class DftGspnSettings : public ModuleSettings {
+            public:
+
+                /*!
+                 * Creates a new set of DFT-GSPN settings.
+                 */
+                DftGspnSettings();
+
+                /*!
+                 * Retrieves whether the DFT should be transformed into a GSPN.
+                 *
+                 * @return True iff the option was set.
+                 */
+                bool isTransformToGspn() const;
+
+                /*!
+                 * Retrieves whether the smart transformation should be disabled.
+                 *
+                 * @return True if the smart transformation should be disabled.
+                 */
+                bool isDisableSmartTransformation() const;
+
+                /*!
+                 * Retrieves whether the DC and failed place should be merged.
+                 *
+                 * @return True if the merge of DC and failed place is enabled.
+                 */
+                bool isMergeDCFailed() 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 transformToGspnOptionName;
+                static const std::string disableSmartTransformationOptionName;
+                static const std::string mergeDCFailedOptionName;
+
+            };
+
+        } // namespace modules
+    } // namespace settings
+} // namespace storm

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

@@ -24,26 +24,39 @@ namespace storm {
             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";
             const std::string DftIOSettings::displayStatsOptionName = "show-dft-stats";
 
 
             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());
+                                        .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());
+                                        .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, 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());
+                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());
                 this->addOption(storm::settings::OptionBuilder(moduleName, displayStatsOptionName, false, "Print stats to stdout").build());
-
             }
 
             bool DftIOSettings::isDftFileSet() const {
@@ -101,10 +114,6 @@ namespace storm {
                 return this->getOption(maxValueOptionName).getHasOptionBeenSet();
             }
 
-            bool DftIOSettings::isTransformToGspn() const {
-                return this->getOption(transformToGspnOptionName).getHasOptionBeenSet();
-            }
-
             bool DftIOSettings::isExportToJson() const {
                 return this->getOption(exportToJsonOptionName).getHasOptionBeenSet();
             }

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

@@ -101,13 +101,6 @@ namespace storm {
                  */
                 bool isComputeMaximalValue() const;
 
-                /*!
-                 * Retrieves whether the DFT should be transformed into a GSPN.
-                 *
-                 * @return True iff the option was set.
-                 */
-                bool isTransformToGspn() const;
-
                 /*!
                  * Retrieves whether the export to Json file option was set.
                  *
@@ -148,7 +141,6 @@ namespace storm {
                 static const std::string propTimepointsOptionName;
                 static const std::string minValueOptionName;
                 static const std::string maxValueOptionName;
-                static const std::string transformToGspnOptionName;
                 static const std::string exportToJsonOptionName;
                 static const std::string displayStatsOptionName;
 

src/storm-dft/transformations/DftToGspnTransformator.cpp

@@ -23,7 +23,7 @@ namespace storm {
                 this->priorities = priorities;
                 this->dontCareElements = dontCareElements;
                 this->smart = smart;
-                this->mergedDCFailed = false;//mergeDCFailed;
+                this->mergedDCFailed = mergeDCFailed;
                 this->dontCarePriority = 1;
                 builder.setGspnName("DftToGspnTransformation");