From ba1f6bf3d543bcb8d4016da8aeddfc0cc43f012c Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Sun, 7 Aug 2016 15:26:19 +0200
Subject: [PATCH] jani property stub
Former-commit-id: 37f8f63d43124a38f8875419055bc86b360c6de5 [formerly 54bc32bfd04bd26ecde1042e0e3da817636e7efb]
Former-commit-id: e934d063fd617ef89c592cbb4392af64b8becada
---
src/parser/JaniParser.cpp | 28 ++++++++++++++---
src/parser/JaniParser.h | 38 ++++++++++++++++-------
src/storage/jani/Property.cpp | 23 ++++++++++++++
src/storage/jani/Property.h | 38 +++++++++++++++++++++++
src/utility/storm.cpp | 10 +++---
src/utility/storm.h | 3 +-
test/functional/parser/JaniParserTest.cpp | 7 +++--
7 files changed, 122 insertions(+), 25 deletions(-)
create mode 100644 src/storage/jani/Property.cpp
create mode 100644 src/storage/jani/Property.h
diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp
index ab1cef0ad..f86f905f5 100644
--- a/src/parser/JaniParser.cpp
+++ b/src/parser/JaniParser.cpp
@@ -1,5 +1,6 @@
#include "JaniParser.h"
#include "src/storage/jani/Model.h"
+#include "src/storage/jani/Property.h"
#include "src/exceptions/FileIoException.h"
#include "src/exceptions/InvalidJaniException.h"
#include "src/exceptions/NotImplementedException.h"
@@ -29,13 +30,13 @@ namespace storm {
}
- storm::jani::Model JaniParser::parse(std::string const& path) {
+ std::pair<storm::jani::Model, std::vector<storm::jani::Property>> JaniParser::parse(std::string const& path) {
JaniParser parser;
parser.readFile(path);
return parser.parseModel();
}
- JaniParser::JaniParser(std::string &jsonstring) {
+ JaniParser::JaniParser(std::string const& jsonstring) {
parsedStructure = json::parse(jsonstring);
}
@@ -55,7 +56,7 @@ namespace storm {
file.close();
}
- storm::jani::Model JaniParser::parseModel() {
+ std::pair<storm::jani::Model, std::vector<storm::jani::Property>> JaniParser::parseModel(bool parseProperties) {
//jani-version
STORM_LOG_THROW(parsedStructure.count("jani-version") == 1, storm::exceptions::InvalidJaniException, "Jani-version must be given exactly once.");
uint64_t version = getUnsignedInt(parsedStructure.at("jani-version"), "jani version");
@@ -92,8 +93,27 @@ namespace storm {
}
STORM_LOG_THROW(parsedStructure.count("system") == 1, storm::exceptions::InvalidJaniException, "Exactly one system description must be given");
//std::shared_ptr<storm::jani::Composition> composition = parseComposition(parsedStructure.at("system"));
+ STORM_LOG_THROW(parsedStructure.count("properties") <= 1, storm::exceptions::InvalidJaniException, "At most one list of properties can be given");
+ STORM_LOG_THROW(parsedStructure.at("properties").is_array(), storm::exceptions::InvalidJaniException, "Properties should be an array");
+ PropertyVector properties;
+ if(parseProperties) {
+ for(auto const& propertyEntry : parsedStructure.at("properties")) {
+ properties.push_back(this->parseProperty(propertyEntry));
+ }
+ }
+ return {model, properties};
+ }
+
+
+ storm::jani::Property JaniParser::parseProperty(json const& propertyStructure) {
+ STORM_LOG_THROW(propertyStructure.count("name") == 1, storm::exceptions::InvalidJaniException, "Property must have a name");
+ // TODO check unique name
+ std::string name = getString(propertyStructure.at("name"), "property-name");
+ std::string comment = "";
+ if(propertyStructure.count("comment") > 0) {
+ comment = getString(propertyStructure.at("comment"), "comment for property named '" + name + "'.");
+ }
- return model;
}
std::shared_ptr<storm::jani::Constant> JaniParser::parseConstant(json const& constantStructure, std::string const& scopeDescription) {
diff --git a/src/parser/JaniParser.h b/src/parser/JaniParser.h
index 3e57b7e9f..09e195894 100644
--- a/src/parser/JaniParser.h
+++ b/src/parser/JaniParser.h
@@ -1,7 +1,6 @@
-#ifndef STORM_JANIPARSER_H
-#define STORM_JANIPARSER_H
-
+#pragma once
#include <src/storage/jani/Constant.h>
+#include <src/logic/Formula.h>
#include "src/exceptions/FileIoException.h"
#include "src/storage/expressions/ExpressionManager.h"
@@ -16,23 +15,31 @@ namespace storm {
class Automaton;
class Variable;
class Composition;
+ class Property;
}
namespace parser {
+ /*
+ * The JANI format parser.
+ * Parses Models and Properties
+ *
+ * TODO some parts are copy-heavy, a bit of cleaning is good as soon as the format is stable.
+ */
class JaniParser {
- json parsedStructure;
- std::shared_ptr<storm::expressions::ExpressionManager> expressionManager;
-
public:
+ typedef std::vector<storm::jani::Property> PropertyVector;
+
JaniParser() : expressionManager(new storm::expressions::ExpressionManager()) {}
- JaniParser(std::string& jsonstring);
- static storm::jani::Model parse(std::string const& path);
+ JaniParser(std::string const& jsonstring);
+ static std::pair<storm::jani::Model, PropertyVector> parse(std::string const& path);
+
protected:
void readFile(std::string const& path);
- storm::jani::Model parseModel();
+ std::pair<storm::jani::Model, PropertyVector> parseModel(bool parseProperties = true);
+ storm::jani::Property parseProperty(json const& propertyStructure);
storm::jani::Automaton parseAutomaton(json const& automatonStructure, storm::jani::Model const& parentModel);
std::shared_ptr<storm::jani::Variable> parseVariable(json const& variableStructure, std::string const& scopeDescription, bool prefWithScope = false);
storm::expressions::Expression parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {});
@@ -50,11 +57,18 @@ namespace storm {
storm::expressions::Variable getVariableOrConstantExpression(std::string const& ident, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {});
+ /**
+ * The overall structure currently under inspection.
+ */
+ json parsedStructure;
+ /**
+ * The expression manager to be used.
+ */
+ std::shared_ptr<storm::expressions::ExpressionManager> expressionManager;
+
+
};
}
}
-
-
-#endif //STORM_JANIPARSER_H
diff --git a/src/storage/jani/Property.cpp b/src/storage/jani/Property.cpp
new file mode 100644
index 000000000..294dfc549
--- /dev/null
+++ b/src/storage/jani/Property.cpp
@@ -0,0 +1,23 @@
+#include "Property.h"
+namespace storm {
+ namespace jani {
+ Property::Property(std::string const& name, std::shared_ptr<const storm::logic::Formula> const& formula, std::string const& comment)
+ : name(name), formula(formula), comment(comment)
+ {
+
+ }
+
+ std::string const& Property::getName() const {
+ return this->name;
+ }
+
+ std::string const& Property::getComment() const {
+ return this->comment;
+ }
+
+ std::shared_ptr<storm::logic::Formula const> Property::getFormula() const {
+ return this->formula;
+ }
+
+ }
+}
\ No newline at end of file
diff --git a/src/storage/jani/Property.h b/src/storage/jani/Property.h
new file mode 100644
index 000000000..30bddac60
--- /dev/null
+++ b/src/storage/jani/Property.h
@@ -0,0 +1,38 @@
+#pragma once
+
+#include "src/logic/formulas.h"
+
+namespace storm {
+ namespace jani {
+ class Property {
+ /**
+ * Constructs the property
+ * @param name the name
+ * @param formula the formula representation
+ * @param comment An optional comment
+ */
+ Property(std::string const& name, std::shared_ptr<storm::logic::Formula const> const& formula, std::string const& comment = "");
+ /**
+ * Get the provided name
+ * @return the name
+ */
+ std::string const& getName() const;
+ /**
+ * Get the provided comment, if any
+ * @return the comment
+ */
+ std::string const& getComment() const;
+ /**
+ * Get the formula
+ * @return the formula
+ */
+ std::shared_ptr<storm::logic::Formula const> const& getFormula() const;
+
+ private:
+ std::string name;
+ std::shared_ptr<storm::logic::Formula const> formula;
+ std::string comment;
+ };
+ }
+}
+
diff --git a/src/utility/storm.cpp b/src/utility/storm.cpp
index 5956e72c9..8ea25af28 100644
--- a/src/utility/storm.cpp
+++ b/src/utility/storm.cpp
@@ -5,7 +5,7 @@
#include "src/parser/PrismParser.h"
#include "src/parser/FormulaParser.h"
#include "src/utility/macros.h"
-
+#include "src/storage/jani/Property.h"
namespace storm {
@@ -15,12 +15,12 @@ namespace storm {
return program;
}
- storm::jani::Model parseJaniModel(std::string const& path) {
- storm::jani::Model model = storm::parser::JaniParser::parse(path);
- if(!model.checkValidity(true)) {
+ std::pair<storm::jani::Model, std::vector<storm::jani::Property>> parseJaniModel(std::string const& path) {
+ std::pair<storm::jani::Model, std::vector<storm::jani::Property>> modelAndFormulae = storm::parser::JaniParser::parse(path);
+ if(!modelAndFormulae.first.checkValidity(true)) {
STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Jani file parsing yields invalid model.");
}
- return model;
+ return modelAndFormulae;
}
/**
diff --git a/src/utility/storm.h b/src/utility/storm.h
index bc56585ee..fc6b2799b 100644
--- a/src/utility/storm.h
+++ b/src/utility/storm.h
@@ -42,6 +42,7 @@
#include "src/parser/AutoParser.h"
#include "src/storage/jani/Model.h"
+#include "src/storage/jani/Property.h"
// Headers of builders.
#include "src/builder/ExplicitModelBuilder.h"
@@ -92,7 +93,7 @@ namespace storm {
return storm::parser::AutoParser<>::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : "", choiceLabelingFile ? choiceLabelingFile.get() : "" );
}
- storm::jani::Model parseModel(std::string const& path);
+ std::pair<storm::jani::Model, std::vector<storm::jani::Property>> parseJaniModel(std::string const& path);
storm::prism::Program parseProgram(std::string const& path);
std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForExplicit(std::string const& inputString);
std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program);
diff --git a/test/functional/parser/JaniParserTest.cpp b/test/functional/parser/JaniParserTest.cpp
index 6d5d0712e..b2b6deead 100644
--- a/test/functional/parser/JaniParserTest.cpp
+++ b/test/functional/parser/JaniParserTest.cpp
@@ -2,19 +2,20 @@
#include "storm-config.h"
#include "src/parser/JaniParser.h"
#include "src/storage/jani/Model.h"
+#include "src/storage/jani/Property.h"
TEST(JaniParser, DieTest) {
std::string testFileInput = STORM_CPP_TESTS_BASE_PATH"/../examples/exported-jani-models/dice.jani";
- storm::jani::Model model = storm::parser::JaniParser::parse(testFileInput);
+ storm::jani::Model model = storm::parser::JaniParser::parse(testFileInput).first;
}
TEST(JaniParser, BrpTest) {
std::string testFileInput = STORM_CPP_TESTS_BASE_PATH"/../examples/exported-jani-models/brp.jani";
- storm::jani::Model model = storm::parser::JaniParser::parse(testFileInput);
+ storm::jani::Model model = storm::parser::JaniParser::parse(testFileInput).first;
}
TEST(JaniParser, ConsensusTest) {
std::string testFileInput = STORM_CPP_TESTS_BASE_PATH"/../examples/exported-jani-models/coin2.jani";
- storm::jani::Model model = storm::parser::JaniParser::parse(testFileInput);
+ storm::jani::Model model = storm::parser::JaniParser::parse(testFileInput).first;
}
\ No newline at end of file