Rudimentary DFT parser from Cytoscape's JSON

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

@@ -15,6 +15,7 @@
 #include "storm/settings/modules/EliminationSettings.h"
 
 #include "storm-dft/parser/DFTGalileoParser.h"
+#include "storm-dft/parser/DFTJsonParser.h"
 #include "storm-dft/modelchecker/dft/DFTModelChecker.h"
 #include "storm-dft/modelchecker/dft/DFTASFChecker.h"
 #include "storm-dft/transformations/DftToGspnTransformator.h"
@@ -29,6 +30,7 @@
 
 
 #include <boost/lexical_cast.hpp>
+#include <memory>
 
 /*!
  * Load DFT from filename, build corresponding Model and check against given property.
@@ -123,16 +125,21 @@ int main(const int argc, const char** argv) {
         
         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()) {
+        if (!dftSettings.isDftFileSet() && !dftSettings.isDftJsonFileSet()) {
             STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
         }
 
         
         if (dftSettings.isTransformToGspn()) {
-            
-            storm::parser::DFTGalileoParser<double> parser;
-            storm::storage::DFT<double> dft = parser.parseDFT(dftSettings.getDftFilename());
-            storm::transformations::dft::DftToGspnTransformator<double> gspnTransformator(dft);
+            std::shared_ptr<storm::storage::DFT<double>> dft;
+            if (dftSettings.isDftJsonFileSet()) {
+                storm::parser::DFTJsonParser<double> parser;
+                dft = std::make_shared<storm::storage::DFT<double>>(parser.parseJson(dftSettings.getDftJsonFilename()));
+            } else {
+                storm::parser::DFTGalileoParser<double> parser;
+                dft = std::make_shared<storm::storage::DFT<double>>(parser.parseDFT(dftSettings.getDftFilename()));
+            }
+            storm::transformations::dft::DftToGspnTransformator<double> gspnTransformator(*dft);
             gspnTransformator.transform();
             storm::gspn::GSPN* gspn = gspnTransformator.obtainGSPN();
             uint64_t toplevelFailedPlace = gspnTransformator.toplevelFailedPlaceId();

src/storm-dft/parser/DFTJsonParser.cpp

@@ -0,0 +1,168 @@
+#include "DFTJsonParser.h"
+
+#include <iostream>
+#include <fstream>
+#include <boost/algorithm/string.hpp>
+#include <boost/lexical_cast.hpp>
+#include <boost/algorithm/string/replace.hpp>
+#include "storm/storage/expressions/ExpressionManager.h"
+#include "storm/exceptions/NotImplementedException.h"
+#include "storm/exceptions/FileIoException.h"
+#include "storm/exceptions/NotSupportedException.h"
+#include "storm/utility/macros.h"
+
+namespace storm {
+    namespace parser {
+
+        template<typename ValueType>
+        storm::storage::DFT<ValueType> DFTJsonParser<ValueType>::parseJson(const std::string& filename) {
+            readFile(filename);
+            storm::storage::DFT<ValueType> dft = builder.build();
+            STORM_LOG_DEBUG("Elements:" << std::endl << dft.getElementsString());
+            STORM_LOG_DEBUG("Spare Modules:" << std::endl << dft.getSpareModulesString());
+            return dft;
+        }
+
+        template<typename ValueType>
+        std::string DFTJsonParser<ValueType>::stripQuotsFromName(std::string const& name) {
+            size_t firstQuots = name.find("\"");
+            size_t secondQuots = name.find("\"", firstQuots+1);
+            
+            if(firstQuots == std::string::npos) {
+                return name;
+            } else {
+                STORM_LOG_THROW(secondQuots != std::string::npos, storm::exceptions::FileIoException, "No ending quotation mark found in " << name);
+                return name.substr(firstQuots+1,secondQuots-1);
+            }
+        }
+
+        template<typename ValueType>
+        std::string DFTJsonParser<ValueType>::getString(json const& structure, std::string const& errorInfo) {
+            STORM_LOG_THROW(structure.is_string(), storm::exceptions::FileIoException, "Expected a string in " << errorInfo << ", got '" << structure.dump() << "'");
+            return structure.front();
+        }
+
+        template<typename ValueType>
+        std::string DFTJsonParser<ValueType>::parseNodeIdentifier(std::string const& name) {
+            return boost::replace_all_copy(name, "'", "__prime__");
+        }
+
+        template<typename ValueType>
+        void DFTJsonParser<ValueType>::readFile(const std::string& filename) {
+            std::cout << "Parsing from JSON" << std::endl;
+
+            std::ifstream file;
+            file.exceptions ( std::ifstream::failbit );
+            try {
+                file.open(filename);
+            }
+            catch (std::ifstream::failure e) {
+                STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Exception during file opening on " << filename << ".");
+                return;
+            }
+            file.exceptions( std::ifstream::goodbit );
+
+            json parsedJson;
+            parsedJson << file;
+            file.close();
+
+            // Start by building mapping from ids to names
+            std::map<std::string, std::string> nameMapping;
+            for (auto& element: parsedJson) {
+                if (element.at("classes") != "") {
+                    json data = element.at("data");
+                    std::string id = data.at("id");
+                    std::string name = data.at("name");
+                    nameMapping[id] = name;
+                }
+            }
+
+            // TODO: avoid hack
+            std::string toplevelId = nameMapping["1"];
+
+            for (auto& element : parsedJson) {
+                std::cout << element << std::endl;
+
+                bool success = true;
+                if (element.at("classes") == "") {
+                    continue;
+                }
+                json data = element.at("data");
+                std::string name = data.at("name");
+                std::vector<std::string> childNames;
+                if (data.count("children") > 0) {
+                    for (auto& child : data.at("children")) {
+                        childNames.push_back(nameMapping[child]);
+                    }
+                }
+
+                std::string type = getString(element.at("classes"), "classes");
+
+                if(type == "and") {
+                    success = builder.addAndElement(name, childNames);
+                } else if (type == "or") {
+                    success = builder.addOrElement(name, childNames);
+                } else if (type == "pand") {
+                    success = builder.addPandElement(name, childNames);
+                } else if (type == "por") {
+                    success = builder.addPorElement(name, childNames);
+                } else if (type == "spare") {
+                    success = builder.addSpareElement(name, childNames);
+                } else if (type == "seq") {
+                    success = builder.addSequenceEnforcer(name, childNames);
+                } else if (type== "fdep") {
+                    success = builder.addDepElement(name, childNames, storm::utility::one<ValueType>());
+                } else if (type== "pdep") {
+                    ValueType probability = parseRationalExpression(data.at("prob"));
+                    success = builder.addDepElement(name, childNames, probability);
+                } else if (type == "be") {
+                    ValueType failureRate = parseRationalExpression(data.at("rate"));
+                    ValueType dormancyFactor = parseRationalExpression(data.at("dorm"));
+                    success = builder.addBasicElement(name, failureRate, dormancyFactor);
+                } else {
+                    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Type name: " << type << "  not recognized.");
+                    success = false;
+                }
+
+                json position = element.at("position");
+                double x = position.at("x");
+                double y = position.at("y");
+                builder.addLayoutInfo(name, x, y);
+                STORM_LOG_THROW(success, storm::exceptions::FileIoException, "Error while adding element '" << element << "'.");
+            }
+
+            if(!builder.setTopLevel(toplevelId)) {
+                STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Top level id unknown.");
+            }
+        }
+
+        template<typename ValueType>
+        ValueType DFTJsonParser<ValueType>::parseRationalExpression(std::string const& expr) {
+            STORM_LOG_ASSERT(false, "Specialized method should be called.");
+            return 0;
+        }
+
+        template<>
+        double DFTJsonParser<double>::parseRationalExpression(std::string const& expr) {
+            return boost::lexical_cast<double>(expr);
+        }
+
+        // Explicitly instantiate the class.
+        template class DFTJsonParser<double>;
+
+#ifdef STORM_HAVE_CARL
+        template<>
+        storm::RationalFunction DFTJsonParser<storm::RationalFunction>::parseRationalExpression(std::string const& expr) {
+            STORM_LOG_TRACE("Translating expression: " << expr);
+            storm::expressions::Expression expression = parser.parseFromString(expr);
+            STORM_LOG_TRACE("Expression: " << expression);
+            storm::RationalFunction rationalFunction = evaluator.asRational(expression);
+            STORM_LOG_TRACE("Parsed expression: " << rationalFunction);
+            return rationalFunction;
+        }
+
+        template class DFTJsonParser<RationalFunction>;
+#endif
+        
+    }
+}

src/storm-dft/parser/DFTJsonParser.h

@@ -0,0 +1,48 @@
+#pragma  once
+
+#include <map>
+
+#include "storm/storage/expressions/ExpressionManager.h"
+#include "storm/parser/ExpressionParser.h"
+#include "storm/storage/expressions/ExpressionEvaluator.h"
+
+#include "storm-dft/storage/dft/DFT.h"
+#include "storm-dft/storage/dft/DFTBuilder.h"
+
+// JSON parser
+#include "json.hpp"
+
+using json = nlohmann::json;
+
+namespace storm {
+    namespace parser {
+
+        template<typename ValueType>
+        class DFTJsonParser {
+            storm::storage::DFTBuilder<ValueType> builder;
+
+            std::shared_ptr<storm::expressions::ExpressionManager> manager;
+
+            storm::parser::ExpressionParser parser;
+
+            storm::expressions::ExpressionEvaluator<ValueType> evaluator;
+
+            std::unordered_map<std::string, storm::expressions::Expression> identifierMapping;
+
+        public:
+            DFTJsonParser() : manager(new storm::expressions::ExpressionManager()), parser(*manager), evaluator(*manager) {
+            }
+
+            storm::storage::DFT<ValueType> parseJson(std::string const& filename);
+            
+        private:
+            void readFile(std::string const& filename);
+
+            std::string stripQuotsFromName(std::string const& name);
+            std::string parseNodeIdentifier(std::string const& name);
+            std::string getString(json const& structure, std::string const& errorInfo);
+
+            ValueType parseRationalExpression(std::string const& expr);
+        };
+    }
+}

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

@@ -16,6 +16,8 @@ namespace storm {
             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";
@@ -37,6 +39,8 @@ namespace storm {
             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, 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.").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());
@@ -60,7 +64,15 @@ namespace storm {
             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();
             }

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

@@ -34,6 +34,20 @@ namespace storm {
                  */
                 std::string getDftFilename() const;
 
+                /*!
+                 * Retrieves whether the dft file option for Json was set.
+                 *
+                 * @return True if the dft file option was set.
+                 */
+                bool isDftJsonFileSet() const;
+
+                /*!
+                 * Retrieves the name of the json file that contains the dft specification.
+                 *
+                 * @return The name of the json file that contains the dft specification.
+                 */
+                std::string getDftJsonFilename() const;
+
                 /*!
                  * Retrieves whether the option to use symmetry reduction is set.
                  *
@@ -144,6 +158,8 @@ namespace storm {
                // Define the string names of the options as constants.
                 static const std::string dftFileOptionName;
                 static const std::string dftFileOptionShortName;
+                static const std::string dftJsonFileOptionName;
+                static const std::string dftJsonFileOptionShortName;
                 static const std::string symmetryReductionOptionName;
                 static const std::string symmetryReductionOptionShortName;
                 static const std::string modularisationOptionName;

src/storm-dft/storage/dft/DFT.h

@@ -15,7 +15,7 @@
 #include "storm-dft/storage/dft/DFTElements.h"
 #include "storm-dft/storage/dft/SymmetricUnits.h"
 #include "storm-dft/storage/dft/DFTStateGenerationInfo.h"
-
+#include "storm-dft/storage/dft/DFTLayoutInfo.h"
 
 namespace storm {
     namespace storage {
@@ -63,7 +63,8 @@ namespace storm {
             std::vector<size_t> mTopModule;
             std::map<size_t, size_t> mRepresentants; // id element -> id representative
             std::vector<std::vector<size_t>> mSymmetries;
-            
+            std::map<size_t, DFTLayoutInfo> mLayoutInfo;
+
         public:
             DFT(DFTElementVector const& elements, DFTElementPointer const& tle);
             
@@ -263,7 +264,15 @@ namespace storm {
             std::vector<size_t> immediateFailureCauses(size_t index) const;
             
             std::vector<size_t> findModularisationRewrite() const;
-        
+
+            void setElementLayoutInfo(size_t id, DFTLayoutInfo const& layoutInfo) {
+                mLayoutInfo[id] = layoutInfo;
+            }
+
+            DFTLayoutInfo const& getElementLayoutInfo(size_t id) const {
+                return mLayoutInfo.at(id);
+            }
+
         private:
             std::pair<std::vector<size_t>, std::vector<size_t>> getSortedParentAndOutDepIds(size_t index) const;
             

src/storm-dft/storage/dft/DFTBuilder.cpp

@@ -73,8 +73,16 @@ namespace storm {
             for(DFTElementPointer e : elems) {
                 e->setId(id++);
             }
+
             STORM_LOG_ASSERT(!mTopLevelIdentifier.empty(), "No top level element.");
-            return DFT<ValueType>(elems, mElements[mTopLevelIdentifier]);
+            DFT<ValueType> dft(elems, mElements[mTopLevelIdentifier]);
+
+            // Set layout info
+            for (auto& elem : mElements) {
+                dft.setElementLayoutInfo(elem.second->id(), mLayoutInfo.at(elem.first));
+            }
+
+            return dft;
         }
 
         template<typename ValueType>

src/storm-dft/storage/dft/DFTBuilder.h

@@ -7,7 +7,7 @@
 
 #include "storm-dft/storage/dft/DFTElements.h"
 #include "storm-dft/storage/dft/elements/DFTRestriction.h"
-
+#include "storm-dft/storage/dft/DFTLayoutInfo.h"
 
 namespace storm {
     namespace storage {
@@ -33,6 +33,7 @@ namespace storm {
             std::unordered_map<DFTRestrictionPointer, std::vector<std::string>> mRestrictionChildNames;
             std::vector<DFTDependencyPointer> mDependencies;
             std::vector<DFTRestrictionPointer> mRestrictions;
+            std::unordered_map<std::string, DFTLayoutInfo> mLayoutInfo;
             
         public:
             DFTBuilder(bool defaultInclusive = true) : pandDefaultInclusive(defaultInclusive), porDefaultInclusive(defaultInclusive) {
@@ -154,6 +155,11 @@ namespace storm {
                 mElements[name] = std::make_shared<DFTBE<ValueType>>(mNextId++, name, failureRate, dormancyFactor);
                 return true;
             }
+
+            void addLayoutInfo(std::string const& name, double x, double y) {
+                STORM_LOG_ASSERT(mElements.count(name) > 0, "Element '" << name << "' not found.");
+                mLayoutInfo[name] = storm::storage::DFTLayoutInfo(x, y);
+            }
             
             bool setTopLevel(std::string const& tle) {
                 mTopLevelIdentifier = tle;

src/storm-dft/storage/dft/DFTLayoutInfo.h

@@ -0,0 +1,15 @@
+#pragma once
+
+namespace storm {
+    namespace storage {
+        struct DFTLayoutInfo {
+            DFTLayoutInfo() {};
+            DFTLayoutInfo(double x, double y) : x(x), y(y) {};
+            
+            // x location
+            double x = 0.0;
+            // y location
+            double y = 0.0;
+        };
+    }
+}

src/storm-dft/transformations/DftToGspnTransformator.cpp

@@ -90,8 +90,8 @@ namespace storm {
             
             template <typename ValueType>
             void DftToGspnTransformator<ValueType>::drawBE(std::shared_ptr<storm::storage::DFTBE<ValueType> const> dftBE, bool isRepresentative) {
-                double xcenter = 10.0;
-                double ycenter = 10.0;
+                double xcenter = mDft.getElementLayoutInfo(dftBE->id()).x;
+                double ycenter = mDft.getElementLayoutInfo(dftBE->id()).y;
 				uint64_t beActive = builder.addPlace(defaultCapacity, isBEActive(dftBE) ? 1 : 0, dftBE->name() + STR_ACTIVATED);
                 activeNodes.emplace(dftBE->id(), beActive);
                 uint64_t beFailed = builder.addPlace(defaultCapacity, 0, dftBE->name() + STR_FAILED);
@@ -137,8 +137,8 @@ namespace storm {
 			
 			template <typename ValueType>
             void DftToGspnTransformator<ValueType>::drawAND(std::shared_ptr<storm::storage::DFTAnd<ValueType> const> dftAnd, bool isRepresentative) {
-                double xcenter = 10.0;
-                double ycenter = 20.0;
+                double xcenter = mDft.getElementLayoutInfo(dftAnd->id()).x;
+                double ycenter = mDft.getElementLayoutInfo(dftAnd->id()).y;
                 uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftAnd->name() + STR_FAILED);
                 assert(failedNodes.size() == dftAnd->id());
                 failedNodes.push_back(nodeFailed);