From 63d594fb45decd7cd590104253f64a9a8868252b Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 15 Dec 2016 00:48:58 +0100 Subject: [PATCH] Rudimentary DFT parser from Cytoscape's JSON --- src/storm-dft-cli/storm-dyftee.cpp | 17 +- src/storm-dft/parser/DFTJsonParser.cpp | 168 ++++++++++++++++++ src/storm-dft/parser/DFTJsonParser.h | 48 +++++ .../settings/modules/DFTSettings.cpp | 14 +- src/storm-dft/settings/modules/DFTSettings.h | 16 ++ src/storm-dft/storage/dft/DFT.h | 15 +- src/storm-dft/storage/dft/DFTBuilder.cpp | 10 +- src/storm-dft/storage/dft/DFTBuilder.h | 8 +- src/storm-dft/storage/dft/DFTLayoutInfo.h | 15 ++ .../DftToGspnTransformator.cpp | 8 +- 10 files changed, 304 insertions(+), 15 deletions(-) create mode 100644 src/storm-dft/parser/DFTJsonParser.cpp create mode 100644 src/storm-dft/parser/DFTJsonParser.h create mode 100644 src/storm-dft/storage/dft/DFTLayoutInfo.h diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp index 7be07940c..37b048b96 100644 --- a/src/storm-dft-cli/storm-dyftee.cpp +++ b/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 +#include /*! * 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::GeneralSettings const& generalSettings = storm::settings::getModule(); - if (!dftSettings.isDftFileSet()) { + if (!dftSettings.isDftFileSet() && !dftSettings.isDftJsonFileSet()) { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); } if (dftSettings.isTransformToGspn()) { - - storm::parser::DFTGalileoParser parser; - storm::storage::DFT dft = parser.parseDFT(dftSettings.getDftFilename()); - storm::transformations::dft::DftToGspnTransformator gspnTransformator(dft); + std::shared_ptr> dft; + if (dftSettings.isDftJsonFileSet()) { + storm::parser::DFTJsonParser parser; + dft = std::make_shared>(parser.parseJson(dftSettings.getDftJsonFilename())); + } else { + storm::parser::DFTGalileoParser parser; + dft = std::make_shared>(parser.parseDFT(dftSettings.getDftFilename())); + } + storm::transformations::dft::DftToGspnTransformator gspnTransformator(*dft); gspnTransformator.transform(); storm::gspn::GSPN* gspn = gspnTransformator.obtainGSPN(); uint64_t toplevelFailedPlace = gspnTransformator.toplevelFailedPlaceId(); diff --git a/src/storm-dft/parser/DFTJsonParser.cpp b/src/storm-dft/parser/DFTJsonParser.cpp new file mode 100644 index 000000000..4bedbe7ac --- /dev/null +++ b/src/storm-dft/parser/DFTJsonParser.cpp @@ -0,0 +1,168 @@ +#include "DFTJsonParser.h" + +#include +#include +#include +#include +#include +#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 + storm::storage::DFT DFTJsonParser::parseJson(const std::string& filename) { + readFile(filename); + storm::storage::DFT dft = builder.build(); + STORM_LOG_DEBUG("Elements:" << std::endl << dft.getElementsString()); + STORM_LOG_DEBUG("Spare Modules:" << std::endl << dft.getSpareModulesString()); + return dft; + } + + template + std::string DFTJsonParser::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 + std::string DFTJsonParser::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 + std::string DFTJsonParser::parseNodeIdentifier(std::string const& name) { + return boost::replace_all_copy(name, "'", "__prime__"); + } + + template + void DFTJsonParser::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 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 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()); + } 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 + ValueType DFTJsonParser::parseRationalExpression(std::string const& expr) { + STORM_LOG_ASSERT(false, "Specialized method should be called."); + return 0; + } + + template<> + double DFTJsonParser::parseRationalExpression(std::string const& expr) { + return boost::lexical_cast(expr); + } + + // Explicitly instantiate the class. + template class DFTJsonParser; + +#ifdef STORM_HAVE_CARL + template<> + storm::RationalFunction DFTJsonParser::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; +#endif + + } +} diff --git a/src/storm-dft/parser/DFTJsonParser.h b/src/storm-dft/parser/DFTJsonParser.h new file mode 100644 index 000000000..cf2e83826 --- /dev/null +++ b/src/storm-dft/parser/DFTJsonParser.h @@ -0,0 +1,48 @@ +#pragma once + +#include + +#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 + class DFTJsonParser { + storm::storage::DFTBuilder builder; + + std::shared_ptr manager; + + storm::parser::ExpressionParser parser; + + storm::expressions::ExpressionEvaluator evaluator; + + std::unordered_map identifierMapping; + + public: + DFTJsonParser() : manager(new storm::expressions::ExpressionManager()), parser(*manager), evaluator(*manager) { + } + + storm::storage::DFT 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); + }; + } +} diff --git a/src/storm-dft/settings/modules/DFTSettings.cpp b/src/storm-dft/settings/modules/DFTSettings.cpp index 5bf705d8a..898360c4b 100644 --- a/src/storm-dft/settings/modules/DFTSettings.cpp +++ b/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(); } diff --git a/src/storm-dft/settings/modules/DFTSettings.h b/src/storm-dft/settings/modules/DFTSettings.h index 1b1b097f9..c1a9df7e5 100644 --- a/src/storm-dft/settings/modules/DFTSettings.h +++ b/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; diff --git a/src/storm-dft/storage/dft/DFT.h b/src/storm-dft/storage/dft/DFT.h index 9ef232a65..1304bbfa9 100644 --- a/src/storm-dft/storage/dft/DFT.h +++ b/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 mTopModule; std::map mRepresentants; // id element -> id representative std::vector> mSymmetries; - + std::map mLayoutInfo; + public: DFT(DFTElementVector const& elements, DFTElementPointer const& tle); @@ -263,7 +264,15 @@ namespace storm { std::vector immediateFailureCauses(size_t index) const; std::vector 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> getSortedParentAndOutDepIds(size_t index) const; diff --git a/src/storm-dft/storage/dft/DFTBuilder.cpp b/src/storm-dft/storage/dft/DFTBuilder.cpp index 10c84f5f6..68ffce742 100644 --- a/src/storm-dft/storage/dft/DFTBuilder.cpp +++ b/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(elems, mElements[mTopLevelIdentifier]); + DFT dft(elems, mElements[mTopLevelIdentifier]); + + // Set layout info + for (auto& elem : mElements) { + dft.setElementLayoutInfo(elem.second->id(), mLayoutInfo.at(elem.first)); + } + + return dft; } template diff --git a/src/storm-dft/storage/dft/DFTBuilder.h b/src/storm-dft/storage/dft/DFTBuilder.h index 55c1cb588..baa9232a0 100644 --- a/src/storm-dft/storage/dft/DFTBuilder.h +++ b/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> mRestrictionChildNames; std::vector mDependencies; std::vector mRestrictions; + std::unordered_map mLayoutInfo; public: DFTBuilder(bool defaultInclusive = true) : pandDefaultInclusive(defaultInclusive), porDefaultInclusive(defaultInclusive) { @@ -154,6 +155,11 @@ namespace storm { mElements[name] = std::make_shared>(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; diff --git a/src/storm-dft/storage/dft/DFTLayoutInfo.h b/src/storm-dft/storage/dft/DFTLayoutInfo.h new file mode 100644 index 000000000..c61de0f6d --- /dev/null +++ b/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; + }; + } +} diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp index f3a113215..caed44166 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.cpp +++ b/src/storm-dft/transformations/DftToGspnTransformator.cpp @@ -90,8 +90,8 @@ namespace storm { template void DftToGspnTransformator::drawBE(std::shared_ptr 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 void DftToGspnTransformator::drawAND(std::shared_ptr 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);