Added framework for DFT->GSPN Transformator

Former-commit-id: de0fd50573

src/storm/settings/modules/DFTSettings.cpp

@@ -33,6 +33,8 @@ namespace storm {
             const std::string DFTSettings::solveWithSmtOptionName = "smt";
 #endif
             
+            const std::string DFTSettings::transformToGspnOptionName = "gspn";
+
             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());
@@ -49,6 +51,7 @@ namespace storm {
 #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());
             }
             
             bool DFTSettings::isDftFileSet() const {
@@ -123,6 +126,10 @@ namespace storm {
             }
 #endif
             
+            bool DFTSettings::isTransformToGspn() const {
+                return this->getOption(transformToGspnOptionName).getHasOptionBeenSet();
+            }
+
             void DFTSettings::finalize() {
             }
 

src/storm/settings/modules/DFTSettings.h

@@ -117,6 +117,13 @@ namespace storm {
                  * @return The timebound.
                  */
                 double getPropTimebound() const;
+
+                /*!
+                 * Retrieves whether the DFT should be transformed into a GSPN.
+                 *
+                 * @return True iff the option was set.
+                 */
+                bool isTransformToGspn() const;
                 
 #ifdef STORM_HAVE_Z3
                 /*!
@@ -153,6 +160,7 @@ namespace storm {
 #ifdef STORM_HAVE_Z3
                 static const std::string solveWithSmtOptionName;
 #endif
+                static const std::string transformToGspnOptionName;
                 
             };
 

src/storm/storm-dyftee.cpp

@@ -9,6 +9,8 @@
 #include "storm/exceptions/BaseException.h"
 #include "storm/utility/macros.h"
 #include "storm/builder/DftSmtBuilder.h"
+#include "storm/transformations/dft/DftToGspnTransformator.h"
+
 
 #include "storm/settings/modules/GeneralSettings.h"
 #include "storm/settings/modules/DFTSettings.h"
@@ -34,6 +36,9 @@
  *
  * @param filename Path to DFT file in Galileo format.
  * @param property PCTC formula capturing the property to check.
+ * @param symred Flag whether symmetry reduction should be used.
+ * @param allowModularisation Flag whether modularisation should be applied if possible.
+ * @param enableDC Flag whether Don't Care propagation should be used.
  */
 template <typename ValueType>
 void analyzeDFT(std::string filename, std::string property, bool symred, bool allowModularisation, bool enableDC, double approximationError) {
@@ -68,6 +73,21 @@ void analyzeWithSMT(std::string filename) {
     //std::cout << "SMT result: " << sat << std::endl;
 }
 
+/*!
+ * Load DFT from filename and transform into a GSPN.
+ *
+ * @param filename Path to DFT file in Galileo format.
+ *
+ */
+template <typename ValueType>
+void transformDFT(std::string filename) {
+    std::cout << "Transforming DFT from file " << filename << std::endl;
+    storm::parser::DFTGalileoParser<ValueType> parser;
+    storm::storage::DFT<ValueType> dft = parser.parseDFT(filename);
+    storm::transformations::dft::DftToGspnTransformator<ValueType> gspnTransformator(dft);
+    gspnTransformator.transform();
+}
+
 /*!
  * Initialize the settings manager.
  */
@@ -116,6 +136,13 @@ int main(const int argc, const char** argv) {
         if (!dftSettings.isDftFileSet()) {
             STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
         }
+
+        if (dftSettings.isTransformToGspn()) {
+            // For now we only transform the DFT to a GSPN and then exit
+            transformDFT<double>(dftSettings.getDftFilename());
+            storm::utility::cleanUp();
+            return 0;
+        }
         
         bool parametric = false;
 #ifdef STORM_HAVE_CARL

src/transformations/dft/DftToGspnTransformator.cpp

@@ -1,4 +1,5 @@
 #include "src/transformations/dft/DftToGspnTransformator.h"
+#include "src/exceptions/NotImplementedException.h"
 
 namespace storm {
     namespace transformations {
@@ -9,12 +10,35 @@ namespace storm {
                 // Intentionally left empty
             }
 
+            template <typename ValueType>
+            void DftToGspnTransformator<ValueType>::transform() {
+                mGspn = storm::gspn::GSPN();
+                
+                // For debugging purposes
+                writeGspn(false);
+
+                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The transformation to GSPN is not yet implemented.");
+            }
+
+            template <typename ValueType>
+            void DftToGspnTransformator<ValueType>::writeGspn(bool toFile) {
+                if (toFile) {
+                    // Writing to file
+                    std::ofstream file;
+                    file.open("gspn.dot");
+                    mGspn.writeDotToStream(file);
+                    file.close();
+                } else {
+                    // Writing to console
+                    mGspn.writeDotToStream(std::cout);
+                }
+            }
 
             // Explicitly instantiate the class.
             template class DftToGspnTransformator<double>;
 
     #ifdef STORM_HAVE_CARL
-            template class DftToGspnTransformator<storm::RationalFunction>;
+            // template class DftToGspnTransformator<storm::RationalFunction>;
     #endif
 
         } // namespace dft

src/transformations/dft/DftToGspnTransformator.h

@@ -2,21 +2,43 @@
 #define DFTTOGSPNTRANSFORMATOR_H
 
 #include <src/storage/dft/DFT.h>
+#include "src/storage/gspn/GSPN.h"
 
 namespace storm {
     namespace transformations {
         namespace dft {
 
+            /*!
+             * Transformator for DFT -> GSPN.
+             */
             template<typename ValueType>
             class DftToGspnTransformator {
 
             public:
+                /*!
+                 * Constructor.
+                 *
+                 * @param dft DFT
+                 */
                 DftToGspnTransformator(storm::storage::DFT<ValueType> const& dft);
 
+                /*!
+                 * Transform the DFT to a GSPN.
+                 */
+                void transform();
+
             private:
 
                 storm::storage::DFT<ValueType> const& mDft;
-
+                storm::gspn::GSPN mGspn;
+                
+                /*!
+                 * Write Gspn to file or console.
+                 *
+                 * @param toFile If true, the GSPN will be written to a file, otherwise it will
+                                 be written to the console.
+                 */
+                void writeGspn(bool toFile);
             };
         }
     }