From c12c0352f7f386ff45650f852bff0d6e48206ba8 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 10 Nov 2020 16:52:28 +0100 Subject: [PATCH] Support for parsing jani model from string --- src/storm-parsers/api/model_descriptions.cpp | 25 +- src/storm-parsers/api/model_descriptions.h | 2 + src/storm-parsers/parser/JaniParser.cpp | 8 +- src/storm-parsers/parser/JaniParser.h | 1 + src/test/storm/parser/JaniParserTest.cpp | 385 +++++++++++++++++++ 5 files changed, 415 insertions(+), 6 deletions(-) create mode 100644 src/test/storm/parser/JaniParserTest.cpp diff --git a/src/storm-parsers/api/model_descriptions.cpp b/src/storm-parsers/api/model_descriptions.cpp index 2c25a5fb3..098ce5952 100644 --- a/src/storm-parsers/api/model_descriptions.cpp +++ b/src/storm-parsers/api/model_descriptions.cpp @@ -22,10 +22,7 @@ namespace storm { return program; } - std::pair> parseJaniModel(std::string const& filename, boost::optional> const& propertyFilter) { - bool parseProperties = !propertyFilter.is_initialized() || !propertyFilter.get().empty(); - std::pair> modelAndFormulae = storm::parser::JaniParser::parse(filename, parseProperties); - + std::pair> filterProperties(std::pair>& modelAndFormulae, boost::optional> const& propertyFilter) { // eliminate unselected properties. if (propertyFilter.is_initialized()) { std::vector newProperties; @@ -46,13 +43,31 @@ namespace storm { modelAndFormulae.first.checkValid(); return modelAndFormulae; } + + std::pair> parseJaniModel(std::string const& filename, boost::optional> const& propertyFilter) { + bool parseProperties = !propertyFilter.is_initialized() || !propertyFilter.get().empty(); + auto modelAndFormulae = storm::parser::JaniParser::parse(filename, parseProperties); + return filterProperties(modelAndFormulae, propertyFilter); + } + std::pair> parseJaniModelFromString(std::string const& jsonstring, boost::optional> const& propertyFilter) { + bool parseProperties = !propertyFilter.is_initialized() || !propertyFilter.get().empty(); + auto modelAndFormulae = storm::parser::JaniParser::parseFromString(jsonstring, parseProperties); + return filterProperties(modelAndFormulae, propertyFilter); + } + std::pair> parseJaniModel(std::string const& filename, storm::jani::ModelFeatures const& supportedFeatures, boost::optional> const& propertyFilter) { auto modelAndFormulae = parseJaniModel(filename, propertyFilter); simplifyJaniModel(modelAndFormulae.first, modelAndFormulae.second, supportedFeatures); return modelAndFormulae; } - + + std::pair> parseJaniModelFromString(std::string const& jsonstring, storm::jani::ModelFeatures const& supportedFeatures, boost::optional> const& propertyFilter) { + auto modelAndFormulae = parseJaniModelFromString(jsonstring, propertyFilter); + simplifyJaniModel(modelAndFormulae.first, modelAndFormulae.second, supportedFeatures); + return modelAndFormulae; + } + void simplifyJaniModel(storm::jani::Model& model, std::vector& properties , storm::jani::ModelFeatures const& supportedFeatures) { auto nonEliminatedFeatures = model.restrictToFeatures(supportedFeatures, properties); STORM_LOG_THROW(nonEliminatedFeatures.empty(), storm::exceptions::NotSupportedException, "The used model feature(s) " << nonEliminatedFeatures.toString() << " is/are not in the list of supported features."); diff --git a/src/storm-parsers/api/model_descriptions.h b/src/storm-parsers/api/model_descriptions.h index de098ee80..c3947a014 100644 --- a/src/storm-parsers/api/model_descriptions.h +++ b/src/storm-parsers/api/model_descriptions.h @@ -21,6 +21,8 @@ namespace storm { std::pair> parseJaniModel(std::string const& filename, boost::optional> const& propertyFilter = boost::none); std::pair> parseJaniModel(std::string const& filename, storm::jani::ModelFeatures const& allowedFeatures, boost::optional> const& propertyFilter = boost::none); + std::pair> parseJaniModelFromString(std::string const& jsonstring, boost::optional> const& propertyFilter = boost::none); + std::pair> parseJaniModelFromString(std::string const& jsonstring, storm::jani::ModelFeatures const& allowedFeatures, boost::optional> const& propertyFilter = boost::none); void simplifyJaniModel(storm::jani::Model& model, std::vector& properties , storm::jani::ModelFeatures const& supportedFeatures); } diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp index dc146ffdf..06d99c4d2 100644 --- a/src/storm-parsers/parser/JaniParser.cpp +++ b/src/storm-parsers/parser/JaniParser.cpp @@ -84,7 +84,13 @@ namespace storm { } template - JaniParser::JaniParser(std::string const& jsonstring) { + std::pair> JaniParser::parseFromString(std::string const& jsonstring, bool parseProperties) { + JaniParser parser(jsonstring); + return parser.parseModel(parseProperties); + } + + template + JaniParser::JaniParser(std::string const& jsonstring) : expressionManager(new storm::expressions::ExpressionManager()) { parsedStructure = Json::parse(jsonstring); } diff --git a/src/storm-parsers/parser/JaniParser.h b/src/storm-parsers/parser/JaniParser.h index 5e2ba447a..18b0f7240 100644 --- a/src/storm-parsers/parser/JaniParser.h +++ b/src/storm-parsers/parser/JaniParser.h @@ -42,6 +42,7 @@ namespace storm { JaniParser() : expressionManager(new storm::expressions::ExpressionManager()) {} JaniParser(std::string const& jsonstring); static std::pair> parse(std::string const& path, bool parseProperties = true); + static std::pair> parseFromString(std::string const& jsonstring, bool parseProperties = true); protected: void readFile(std::string const& path); diff --git a/src/test/storm/parser/JaniParserTest.cpp b/src/test/storm/parser/JaniParserTest.cpp new file mode 100644 index 000000000..709d71a4b --- /dev/null +++ b/src/test/storm/parser/JaniParserTest.cpp @@ -0,0 +1,385 @@ +#include +#include "test/storm_gtest.h" +#include "storm-config.h" +#include "storm-parsers/parser/JaniParser.h" +#include "storm-parsers/api/model_descriptions.h" +#include "storm/storage/jani/Property.h" +#include "storm/storage/jani/Model.h" +#include "storm/storage/jani/ModelType.h" + + +TEST(JaniParser, DieExampleTest) { + std::string testInput = R"({ + "jani-version": 1, + "name": "die.jani", + "type": "dtmc", + "features": [ "derived-operators" ], + "variables": [ + { + "name": "s", + "type": { + "base": "int", + "kind": "bounded", + "lower-bound": 0, + "upper-bound": 7 + }, + "initial-value": 0 + }, + { + "name": "d", + "type": { + "base": "int", + "kind": "bounded", + "lower-bound": 0, + "upper-bound": 6 + }, + "initial-value": 0 + } + ], + "properties": [ + { + "name": "Probability to throw a six", + "expression": { + "op": "filter", + "fun": "max", + "states": { "op": "initial" }, + "values": { + "op": "Pmin", + "exp": { + "op": "U", + "left": true, + "right": { + "op": "∧", + "left": { + "op": "=", + "left": "s", + "right": 7 + }, + "right": { + "op": "=", + "left": "d", + "right": 6 + } + } + } + } + } + }, + { + "name": "Expected number of coin flips", + "expression": { + "op": "filter", + "fun": "max", + "states": { "op": "initial" }, + "values": { + "op": "Emin", + "accumulate": [ "steps" ], + "exp": 1, + "reach": { + "op": "=", + "left": "s", + "right": 7 + } + } + } + } + ], + "automata": [ + { + "name": "die", + "locations": [{ "name": "l" }], + "initial-locations": ["l"], + "edges": [ + { + "location": "l", + "guard": { + "exp": { + "op": "=", + "left": "s", + "right": 0 + } + }, + "destinations": [ + { + "location": "l", + "probability": { "exp": 0.5 }, + "assignments": [ + { + "ref": "s", + "value": 1 + } + ] + }, + { + "location": "l", + "probability": { "exp": 0.5 }, + "assignments": [ + { + "ref": "s", + "value": 2 + } + ] + } + ] + }, + { + "location": "l", + "guard": { + "exp": { + "left": "s", + "op": "=", + "right": 1 + } + }, + "destinations": [ + { + "location": "l", + "probability": { "exp": 0.5 }, + "assignments": [ + { + "ref": "s", + "value": 3 + } + ] + }, + { + "location": "l", + "probability": { "exp": 0.5 }, + "assignments": [ + { + "ref": "s", + "value": 4 + } + ] + } + ] + }, + { + "location": "l", + "guard": { + "exp": { + "left": "s", + "op": "=", + "right": 2 + } + }, + "destinations": [ + { + "location": "l", + "probability": { "exp": 0.5 }, + "assignments": [ + { + "ref": "s", + "value": 5 + } + ] + }, + { + "location": "l", + "probability": { "exp": 0.5 }, + "assignments": [ + { + "ref": "s", + "value": 6 + } + ] + } + ] + }, + { + "location": "l", + "guard": { + "exp": { + "left": "s", + "op": "=", + "right": 3 + } + }, + "destinations": [ + { + "location": "l", + "probability": { "exp": 0.5 }, + "assignments": [ + { + "ref": "s", + "value": 1 + } + ] + }, + { + "location": "l", + "probability": { "exp": 0.5 }, + "assignments": [ + { + "ref": "s", + "value": 7 + }, + { + "ref": "d", + "value": 1 + } + ] + } + ] + }, + { + "location": "l", + "guard": { + "exp": { + "left": "s", + "op": "=", + "right": 4 + } + }, + "destinations": [ + { + "location": "l", + "probability": { "exp": 0.5 }, + "assignments": [ + { + "ref": "s", + "value": 7 + }, + { + "ref": "d", + "value": 2 + } + ] + }, + { + "location": "l", + "probability": { "exp": 0.5 }, + "assignments": [ + { + "ref": "s", + "value": 7 + }, + { + "ref": "d", + "value": 3 + } + ] + } + ] + }, + { + "location": "l", + "guard": { + "exp": { + "left": "s", + "op": "=", + "right": 5 + } + }, + "destinations": [ + { + "location": "l", + "probability": { "exp": 0.5 }, + "assignments": [ + { + "ref": "s", + "value": 7 + }, + { + "ref": "d", + "value": 4 + } + ] + }, + { + "location": "l", + "probability": { "exp": 0.5 }, + "assignments": [ + { + "ref": "s", + "value": 7 + }, + { + "ref": "d", + "value": 5 + } + ] + } + ] + }, + { + "location": "l", + "guard": { + "exp": { + "left": "s", + "op": "=", + "right": 6 + } + }, + "destinations": [ + { + "location": "l", + "probability": { "exp": 0.5 }, + "assignments": [ + { + "ref": "s", + "value": 2 + } + ] + }, + { + "location": "l", + "probability": { "exp": 0.5 }, + "assignments": [ + { + "ref": "s", + "value": 7 + }, + { + "ref": "d", + "value": 6 + } + ] + } + ] + }, + { + "location": "l", + "guard": { + "exp": { + "left": "s", + "op": "=", + "right": 7 + } + }, + "destinations": [ + { + "location": "l", + "assignments": [ + { + "ref": "s", + "value": 7 + } + ] + } + ] + } + ] + + } + ], + "system": { + "elements": [ { "automaton": "die" } ] + } + })"; + + std::pair> result; + EXPECT_NO_THROW(result = storm::api::parseJaniModelFromString(testInput)); + EXPECT_EQ(storm::jani::ModelType::DTMC, result.first.getModelType()); + EXPECT_TRUE(result.first.hasGlobalVariable("s")); + EXPECT_EQ(1ul, result.first.getNumberOfAutomata()); +} + +TEST(JaniParser, UnassignedVariablesTest) { + std::pair> result; + EXPECT_NO_THROW(result = storm::api::parseJaniModel(STORM_TEST_RESOURCES_DIR "/mdp/unassigned-variables.jani")); + EXPECT_EQ(storm::jani::ModelType::MDP, result.first.getModelType()); + EXPECT_TRUE(result.first.hasConstant("c")); + EXPECT_EQ(2ul, result.first.getNumberOfAutomata()); +} +