From 369d106f995845c2292aa13b184a895650693b52 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 8 Aug 2018 13:16:42 +0200 Subject: [PATCH] DFT: load json from string --- resources/examples/testfiles/dft/and.json | 71 +++++++++++++++++++ src/storm-dft-cli/storm-dft.cpp | 4 +- src/storm-dft/api/storm-dft.h | 19 ++++- src/storm-dft/parser/DFTJsonParser.cpp | 70 +++++++++--------- src/storm-dft/parser/DFTJsonParser.h | 8 ++- .../storm-dft/api/DftModelCheckerTest.cpp | 2 +- src/test/storm-dft/api/DftParserTest.cpp | 12 +++- 7 files changed, 142 insertions(+), 44 deletions(-) create mode 100644 resources/examples/testfiles/dft/and.json diff --git a/resources/examples/testfiles/dft/and.json b/resources/examples/testfiles/dft/and.json new file mode 100644 index 000000000..e6c0c0f2e --- /dev/null +++ b/resources/examples/testfiles/dft/and.json @@ -0,0 +1,71 @@ +{ + "toplevel": "2", + "parameters": {}, + "nodes": [ + { + "data": { + "id": "0", + "name": "A", + "type": "be", + "rate": "1", + "dorm": "1", + "label": "A (1)" + }, + "position": { + "x": 440, + "y": 260 + }, + "group": "nodes", + "removed": false, + "selected": false, + "selectable": true, + "locked": false, + "grabbable": true, + "classes": "be" + }, + { + "data": { + "id": "1", + "name": "B", + "type": "be", + "rate": "1", + "dorm": "1", + "label": "B (1)" + }, + "position": { + "x": 548, + "y": 265 + }, + "group": "nodes", + "removed": false, + "selected": false, + "selectable": true, + "locked": false, + "grabbable": true, + "classes": "be" + }, + { + "data": { + "id": "2", + "name": "Z", + "type": "and", + "children": [ + "0", + "1" + ], + "label": "Z" + }, + "position": { + "x": 505, + "y": 119 + }, + "group": "nodes", + "removed": false, + "selected": false, + "selectable": true, + "locked": false, + "grabbable": true, + "classes": "and" + } + ] +} diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index 395985f7e..261193ff3 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -32,10 +32,10 @@ void processOptions() { std::shared_ptr> dft; if (dftIOSettings.isDftJsonFileSet()) { STORM_LOG_DEBUG("Loading DFT from file " << dftIOSettings.getDftJsonFilename()); - dft = storm::api::loadDFTJson(dftIOSettings.getDftJsonFilename()); + dft = storm::api::loadDFTJsonFile(dftIOSettings.getDftJsonFilename()); } else { STORM_LOG_DEBUG("Loading DFT from file " << dftIOSettings.getDftFilename()); - dft = storm::api::loadDFTGalileo(dftIOSettings.getDftFilename()); + dft = storm::api::loadDFTGalileoFile(dftIOSettings.getDftFilename()); } if (dftIOSettings.isDisplayStatsSet()) { diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h index db6d7b3e4..79831edbc 100644 --- a/src/storm-dft/api/storm-dft.h +++ b/src/storm-dft/api/storm-dft.h @@ -23,10 +23,23 @@ namespace storm { * @return DFT. */ template - std::shared_ptr> loadDFTGalileo(std::string const& file) { + std::shared_ptr> loadDFTGalileoFile(std::string const& file) { return std::make_shared>(storm::parser::DFTGalileoParser::parseDFT(file)); } + /*! + * Load DFT from JSON string. + * + * @param jsonString String containing DFT description in JSON format. + * + * @return DFT. + */ + template + std::shared_ptr> loadDFTJsonString(std::string const& jsonString) { + storm::parser::DFTJsonParser parser; + return std::make_shared>(parser.parseJsonFromString(jsonString)); + } + /*! * Load DFT from JSON file. * @@ -35,9 +48,9 @@ namespace storm { * @return DFT. */ template - std::shared_ptr> loadDFTJson(std::string const& file) { + std::shared_ptr> loadDFTJsonFile(std::string const& file) { storm::parser::DFTJsonParser parser; - return std::make_shared>(parser.parseJson(file)); + return std::make_shared>(parser.parseJsonFromFile(file)); } /*! diff --git a/src/storm-dft/parser/DFTJsonParser.cpp b/src/storm-dft/parser/DFTJsonParser.cpp index 6a8197fee..813c2a13e 100644 --- a/src/storm-dft/parser/DFTJsonParser.cpp +++ b/src/storm-dft/parser/DFTJsonParser.cpp @@ -15,34 +15,27 @@ 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; + storm::storage::DFT DFTJsonParser::parseJsonFromFile(std::string const& filename) { + STORM_LOG_DEBUG("Parsing from JSON file"); + std::ifstream file; + storm::utility::openFile(filename, file); + json jsonInput; + jsonInput << file; + storm::utility::closeFile(file); + return parseJson(jsonInput); } template - std::string DFTJsonParser::generateUniqueName(std::string const& id, std::string const& name) { - std::string newId = name; - std::replace(newId.begin(), newId.end(), ' ', '_'); - std::replace(newId.begin(), newId.end(), '-', '_'); - return newId + "_" + id; + storm::storage::DFT DFTJsonParser::parseJsonFromString(std::string const& jsonString) { + STORM_LOG_DEBUG("Parsing from JSON string"); + json jsonInput = json::parse(jsonString); + return parseJson(jsonInput); } template - void DFTJsonParser::readFile(const std::string& filename) { - STORM_LOG_DEBUG("Parsing from JSON"); - - std::ifstream file; - storm::utility::openFile(filename, file); - json parsedJson; - parsedJson << file; - storm::utility::closeFile(file); - - json parameters = parsedJson.at("parameters"); -#ifdef STORM_HAVE_CARL + storm::storage::DFT DFTJsonParser::parseJson(json const& jsonInput) { + // Parse parameters + json parameters = jsonInput.at("parameters"); for (auto it = parameters.begin(); it != parameters.end(); ++it) { STORM_LOG_THROW((std::is_same::value), storm::exceptions::NotSupportedException, "Parameters only allowed when using rational functions."); std::string parameter = it.key(); @@ -51,18 +44,17 @@ namespace storm { parser.setIdentifierMapping(identifierMapping); STORM_LOG_TRACE("Added parameter: " << var.getName()); } -#endif - - json nodes = parsedJson.at("nodes"); + json nodes = jsonInput.at("nodes"); // Start by building mapping from ids to their unique names std::map nameMapping; - for (auto& element: nodes) { + for (auto& element : nodes) { json data = element.at("data"); std::string id = data.at("id"); nameMapping[id] = generateUniqueName(id, data.at("name")); } + // Parse nodes for (auto& element : nodes) { STORM_LOG_TRACE("Parsing: " << element); bool success = true; @@ -123,10 +115,25 @@ namespace storm { STORM_LOG_THROW(success, storm::exceptions::FileIoException, "Error while adding element '" << element << "'."); } - std::string toplevelName = nameMapping[parseJsonNumber(parsedJson.at("toplevel"))]; + std::string toplevelName = nameMapping[parseJsonNumber(jsonInput.at("toplevel"))]; if(!builder.setTopLevel(toplevelName)) { STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Top level id unknown."); } + + // Build DFT + 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::generateUniqueName(std::string const& id, std::string const& name) { + std::string newId = name; + std::replace(newId.begin(), newId.end(), ' ', '_'); + std::replace(newId.begin(), newId.end(), '-', '_'); + return newId + "_" + id; } template @@ -151,10 +158,6 @@ namespace storm { 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); @@ -165,8 +168,9 @@ namespace storm { return rationalFunction; } + + // Explicitly instantiate the class. + template class DFTJsonParser; template class DFTJsonParser; -#endif - } } diff --git a/src/storm-dft/parser/DFTJsonParser.h b/src/storm-dft/parser/DFTJsonParser.h index 6100d69dc..5187e3cc3 100644 --- a/src/storm-dft/parser/DFTJsonParser.h +++ b/src/storm-dft/parser/DFTJsonParser.h @@ -33,10 +33,12 @@ namespace storm { DFTJsonParser() : manager(new storm::expressions::ExpressionManager()), parser(*manager), evaluator(*manager) { } - storm::storage::DFT parseJson(std::string const& filename); - + storm::storage::DFT parseJsonFromString(std::string const& jsonString); + + storm::storage::DFT parseJsonFromFile(std::string const& filename); + private: - void readFile(std::string const& filename); + storm::storage::DFT parseJson(json const& jsonInput); std::string generateUniqueName(std::string const& id, std::string const& name); diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp index b4e9534f9..71c440abd 100644 --- a/src/test/storm-dft/api/DftModelCheckerTest.cpp +++ b/src/test/storm-dft/api/DftModelCheckerTest.cpp @@ -63,7 +63,7 @@ namespace { } double analyzeMTTF(std::string const& file) { - std::shared_ptr> dft = storm::api::loadDFTGalileo(file); + std::shared_ptr> dft = storm::api::loadDFTGalileoFile(file); std::string property = "Tmin=? [F \"failed\"]"; std::vector> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property)); typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFT(*dft, properties, config.useSR, config.useMod, config.useDC, false); diff --git a/src/test/storm-dft/api/DftParserTest.cpp b/src/test/storm-dft/api/DftParserTest.cpp index 48a621ac1..93df569d1 100644 --- a/src/test/storm-dft/api/DftParserTest.cpp +++ b/src/test/storm-dft/api/DftParserTest.cpp @@ -5,9 +5,17 @@ namespace { - TEST(DftParserTest, LoadFromGalileo) { + TEST(DftParserTest, LoadFromGalileoFile) { std::string file = STORM_TEST_RESOURCES_DIR "/dft/and.dft"; - std::shared_ptr> dft = storm::api::loadDFTGalileo(file); + std::shared_ptr> dft = storm::api::loadDFTGalileoFile(file); + EXPECT_EQ(3ul, dft->nrElements()); + EXPECT_EQ(2ul, dft->nrBasicElements()); } + TEST(DftParserTest, LoadFromJsonFile) { + std::string file = STORM_TEST_RESOURCES_DIR "/dft/and.json"; + std::shared_ptr> dft = storm::api::loadDFTJsonFile(file); + EXPECT_EQ(3ul, dft->nrElements()); + EXPECT_EQ(2ul, dft->nrBasicElements()); + } }