From 3f36c95baf393404080f83dba058376fe7254584 Mon Sep 17 00:00:00 2001 From: sjunges Date: Tue, 24 May 2016 17:21:44 +0200 Subject: [PATCH] JaniParser Constant expressions are now parsed Former-commit-id: b3c5cdf0918f7af4f58901b8db9d29bfc29fa347 --- src/parser/JaniParser.cpp | 32 +++++++++++++++++++++----- src/storage/expressions/Expression.cpp | 12 ++++++++-- src/storage/expressions/Expression.h | 7 +++++- 3 files changed, 42 insertions(+), 9 deletions(-) diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index 433c527ed..32362426f 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -7,6 +7,7 @@ #include #include #include +#include namespace storm { namespace parser { @@ -79,7 +80,7 @@ namespace storm { STORM_LOG_THROW(parsedStructure.count("system") == 1, storm::exceptions::InvalidJaniException, "Exactly one system description must be given"); std::shared_ptr composition = parseComposition(parsedStructure.at("system")); - + return model; } std::shared_ptr JaniParser::parseVariable(json const &variableStructure, std::string const& scopeDescription) { @@ -89,13 +90,15 @@ namespace storm { STORM_LOG_THROW(variableStructure.count("initial-value") == 1, storm::exceptions::InvalidJaniException, "Initial value for variable '" + name + "' + (scope: " + scopeDescription + ") must be given once."); // Read initial value before; that makes creation later on a bit easier, and has as an additional benefit that we do not need to check whether the variable occurs also on the assignment. storm::expressions::Expression initExpr = parseExpression(variableStructure.at("initial-value"), "Initial value of variable " + name + " (scope: " + scopeDescription + ")"); - + assert(initExpr.isInitialized()); if(variableStructure.at("type").is_string()) { if(variableStructure.at("type") == "real") { // expressionManager->declareRationalVariable(name); } else if(variableStructure.at("type") == "bool") { + STORM_LOG_THROW(initExpr.hasBooleanType(), storm::exceptions::InvalidJaniException, "Initial value for Boolean variable " << name << " (scope: " << scopeDescription << ") should have Boolean type."); return std::make_shared(name, expressionManager->declareBooleanVariable(name), initExpr); } else if(variableStructure.at("type") == "int") { + STORM_LOG_THROW(initExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Initial value for interger variable " << name << " (scope: " << scopeDescription << ") should have integer type."); return std::make_shared(name, expressionManager->declareIntegerVariable(name), initExpr); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description " << variableStructure.at("type").dump() << " for Variable '" << name << "' (scope: " << scopeDescription << ")"); @@ -110,9 +113,25 @@ namespace storm { } storm::expressions::Expression JaniParser::parseExpression(json const& expressionStructure, std::string const& scopeDescription) { - STORM_LOG_WARN(scopeDescription); - //TDOO FIX - return expressionManager->boolean(false); + if(expressionStructure.is_boolean()) { + if(expressionStructure.get()) { + return expressionManager->boolean(true); + } else { + return expressionManager->boolean(false); + } + } else if(expressionStructure.is_number()) { + std::string stringrepr = expressionStructure.get(); + try { + // It has to be an integer whenever it represents an integer. + int64_t intval = boost::lexical_cast(stringrepr); + return expressionManager->integer(intval); + } catch (boost::bad_lexical_cast const&) { + // For now, just take the double. + // TODO make this a rational number + return expressionManager->rational(expressionStructure.get()); + } + } + } @@ -134,7 +153,8 @@ namespace storm { STORM_LOG_THROW(automatonStructure.count("locations") > 0, storm::exceptions::InvalidJaniException, "Automaton " << name << " does not have locations."); std::unordered_map locIds; for(auto const& locEntry : automatonStructure.at("locations")) { - std::string locName = getString(locEntry, "location of automaton " + name); + STORM_LOG_THROW(locEntry.count("name"), storm::exceptions::InvalidJaniException, "Locations for automaton " << name << " must have exactly one name"); + std::string locName = getString(locEntry.at("name"), "location of automaton " + name); STORM_LOG_THROW(locIds.count(locName) == 0, storm::exceptions::InvalidJaniException, "Location with name '" + locName + "' already exists in automaton '" + name + "'"); uint64_t id = automaton.addLocation(storm::jani::Location(locName)); locIds.emplace(locName, id); diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp index bc539c795..755d3e5dc 100644 --- a/src/storage/expressions/Expression.cpp +++ b/src/storage/expressions/Expression.cpp @@ -161,7 +161,14 @@ namespace storm { boost::any Expression::accept(ExpressionVisitor& visitor) const { return this->getBaseExpression().accept(visitor); } - + + bool Expression::isInitialized() const { + if(this->getBaseExpressionPointer()) { + return true; + } + return false; + } + std::string Expression::toString() const { std::stringstream stream; stream << *this; @@ -311,7 +318,8 @@ namespace storm { return result; } - + + } } diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h index 0c18f122a..42ddd003e 100644 --- a/src/storage/expressions/Expression.h +++ b/src/storage/expressions/Expression.h @@ -298,7 +298,12 @@ namespace storm { * @return The string representation of the expression. */ std::string toString() const; - + + /** + * Checks whether the object encapsulates a base-expression. + */ + bool isInitialized() const; + friend std::ostream& operator<<(std::ostream& stream, Expression const& expression); private: