diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index ed7b5873f..93c380048 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -51,14 +51,16 @@ namespace storm { parsedStructure << file; file.close(); - } storm::jani::Model JaniParser::parseModel() { + //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"); + //name STORM_LOG_THROW(parsedStructure.count("name") == 1, storm::exceptions::InvalidJaniException, "A model must have a (single) name"); std::string name = getString(parsedStructure.at("name"), "model name"); + //model type STORM_LOG_THROW(parsedStructure.count("type") == 1, storm::exceptions::InvalidJaniException, "A type must be given exactly once"); std::string modeltypestring = getString(parsedStructure.at("type"), "type of the model"); storm::jani::ModelType type = storm::jani::getModelType(modeltypestring); @@ -91,7 +93,7 @@ namespace storm { // TODO store prefix in variable. std::string exprManagerName = pref + name; STORM_LOG_THROW(variableStructure.count("type") == 1, storm::exceptions::InvalidJaniException, "Variable '" + name + "' (scope: " + scopeDescription + ") must have a (single) type-declaration."); - // TODO DEPRECATED make initial value optional? --- still rpesent in files, so keep it for now + // TODO DEPRECATED make initial value optional? --- still present in files, so keep it for now 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 + ")"); @@ -167,7 +169,7 @@ namespace storm { return expressionManager->boolean(false); } } else if(expressionStructure.is_number_integer()) { - return expressionManager->integer(expressionStructure.get()); + return expressionManager->integer(expressionStructure.get()); } else if(expressionStructure.is_number_float()) { // For now, just take the double. // TODO make this a rational number @@ -423,7 +425,18 @@ namespace storm { assert(probExpr.isInitialized()); STORM_LOG_THROW(probExpr.hasRationalType(), storm::exceptions::InvalidJaniException, "Probability expr " << probExpr << " does not have rational type." ); // assignments - + unsigned assignmentDeclCount = destEntry.count("assignments"); + STORM_LOG_THROW(assignmentDeclCount < 2, storm::exceptions::InvalidJaniException, "Destination in edge from '" << sourceLoc << "' to '" << targetLoc << "' in automaton '" << name << "' has multiple assignment lists"); + for(auto const& assignmentEntry : destEntry.at("assignments")) { + // ref + STORM_LOG_THROW(assignmentEntry.count("ref") == 1, storm::exceptions::InvalidJaniException, "Assignment in edge from '" << sourceLoc << "' to '" << targetLoc << "' in automaton '" << name << "' must have one ref field"); + std::string refstring = getString(assignmentEntry.at("ref"), "assignment in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'"); + + // TODO check types + // value + STORM_LOG_THROW(assignmentEntry.count("value") == 1, storm::exceptions::InvalidJaniException, "Assignment in edge from '" << sourceLoc << "' to '" << targetLoc << "' in automaton '" << name << "' must have one value field"); + storm::expressions::Expression assignmentExpr = parseExpression(assignmentEntry.at("value"), "assignment in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'"); + } } }