diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index b4d67fce2..39e5e39b8 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -21,6 +21,7 @@ namespace storm { //////////// const bool JaniParser::defaultVariableTransient = false; const bool JaniParser::defaultBooleanInitialValue = false; + const double JaniParser::defaultRationalInitialValue = 0.0; const int64_t JaniParser::defaultIntegerInitialValue = 0; const std::set JaniParser::unsupportedOpstrings({"sin", "cos", "tan", "cot", "sec", "csc", "asin", "acos", "atan", "acot", "asec", "acsc", "sinh", "cosh", "tanh", "coth", "sech", "csch", "asinh", "acosh", "atanh", "asinh", "acosh"}); @@ -105,12 +106,12 @@ namespace storm { for(auto const& automataEntry : parsedStructure.at("automata")) { model.addAutomaton(parseAutomaton(automataEntry, model)); } - STORM_LOG_THROW(parsedStructure.count("system") == 1, storm::exceptions::InvalidJaniException, "Exactly one system description must be given"); + //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")); 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) { + if(parseProperties && parsedStructure.count("properties") == 1) { + STORM_LOG_THROW(parsedStructure.at("properties").is_array(), storm::exceptions::InvalidJaniException, "Properties should be an array"); for(auto const& propertyEntry : parsedStructure.at("properties")) { properties.push_back(this->parseProperty(propertyEntry)); } @@ -172,8 +173,11 @@ namespace storm { } else if(constantStructure.at("type").is_string()) { if(constantStructure.at("type") == "real") { - // expressionManager->declareRationalVariable(name); - // TODO something. + if(initExpr.isInitialized()) { + return std::make_shared(name, expressionManager->declareRationalVariable(exprManagerName), initExpr); + } else { + return std::make_shared(name, expressionManager->declareRationalVariable(exprManagerName)); + } } else if(constantStructure.at("type") == "bool") { if(initExpr.isInitialized()) { return std::make_shared(name, expressionManager->declareBooleanVariable(exprManagerName), initExpr); @@ -189,7 +193,7 @@ namespace storm { } } else { // TODO clocks. - STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description " << constantStructure.at("type").dump() << " for Variable '" << name << "' (scope: " << scopeDescription << ")"); + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description " << constantStructure.at("type").dump() << " for constant '" << name << "' (scope: " << scopeDescription << ")"); } } @@ -217,52 +221,27 @@ namespace storm { } STORM_LOG_THROW(variableStructure.count("type") == 1, storm::exceptions::InvalidJaniException, "Variable '" + name + "' (scope: " + scopeDescription + ") must have a (single) type-declaration."); boost::optional initVal; - if(variableStructure.at("type").is_object()) { - STORM_LOG_THROW(variableStructure.at("type").count("kind") == 1, storm::exceptions::InvalidJaniException, "For complex type as in variable " << name << "(scope: " << scopeDescription << ") kind must be given"); - std::string kind = getString(variableStructure.at("type").at("kind"), "kind for complex type as in variable " + name + "(scope: " + scopeDescription + ") "); - if(kind == "bounded") { - // First do the bounds, that makes the code a bit more streamlined - STORM_LOG_THROW(variableStructure.at("type").count("lower-bound") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scopeDescription << ") lower-bound must be given"); - storm::expressions::Expression lowerboundExpr = parseExpression(variableStructure.at("type").at("lower-bound"), "Lower bound for variable " + name + " (scope: " + scopeDescription + ")"); - assert(lowerboundExpr.isInitialized()); - STORM_LOG_THROW(variableStructure.at("type").count("upper-bound") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scopeDescription << ") upper-bound must be given"); - storm::expressions::Expression upperboundExpr = parseExpression(variableStructure.at("type").at("upper-bound"), "Upper bound for variable "+ name + " (scope: " + scopeDescription + ")"); - assert(upperboundExpr.isInitialized()); - STORM_LOG_THROW(variableStructure.at("type").count("base") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scopeDescription << ") base must be given"); + if(variableStructure.at("type").is_string()) { + if(variableStructure.at("type") == "real") { + expressionManager->declareRationalVariable(name); if(initvalcount == 1) { if(variableStructure.at("initial-value").is_null()) { - initVal = storm::expressions::ite(lowerboundExpr < 0 && upperboundExpr > 0, expressionManager->integer(0), lowerboundExpr); - // TODO as soon as we support half-open intervals, we have to change this. + initVal = expressionManager->rational(defaultRationalInitialValue); } else { initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") "); + STORM_LOG_THROW(initVal.get().hasRationalType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scopeDescription + ") should be a rational"); } + return std::make_shared(name, expressionManager->declareRationalVariable(exprManagerName), initVal.get(), transientVar); + } - std::string basictype = getString(variableStructure.at("type").at("base"), "base for bounded type as in variable " + name + "(scope: " + scopeDescription + ") "); - if(basictype == "int") { - if(initVal) { - STORM_LOG_THROW(initVal.get().hasIntegerType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scopeDescription + ") should be an integer"); - } - STORM_LOG_THROW(lowerboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Lower bound for bounded integer variable " << name << "(scope: " << scopeDescription << ") must be integer-typed"); - STORM_LOG_THROW(upperboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Upper bound for bounded integer variable " << name << "(scope: " << scopeDescription << ") must be integer-typed"); - return storm::jani::makeBoundedIntegerVariable(name, expressionManager->declareIntegerVariable(exprManagerName), initVal, transientVar, lowerboundExpr, upperboundExpr); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported base " << basictype << " for bounded variable " << name << "(scope: " << scopeDescription << ") "); - } - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported kind " << kind << " for complex type of variable " << name << "(scope: " << scopeDescription << ") "); - } - } - else if(variableStructure.at("type").is_string()) { - if(variableStructure.at("type") == "real") { - // expressionManager->declareRationalVariable(name); - // TODO something. + return std::make_shared(name, expressionManager->declareRationalVariable(exprManagerName), transientVar); } else if(variableStructure.at("type") == "bool") { if(initvalcount == 1) { if(variableStructure.at("initial-value").is_null()) { initVal = expressionManager->boolean(defaultBooleanInitialValue); } else { initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") "); - STORM_LOG_THROW(initVal.get().hasIntegerType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scopeDescription + ") should be a Boolean"); + STORM_LOG_THROW(initVal.get().hasBooleanType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scopeDescription + ") should be a Boolean"); } return std::make_shared(name, expressionManager->declareBooleanVariable(exprManagerName), initVal.get(), transientVar); } @@ -285,6 +264,40 @@ namespace storm { } else { STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description " << variableStructure.at("type").dump() << " for variable '" << name << "' (scope: " << scopeDescription << ")"); } + } else if(variableStructure.at("type").is_object()) { + STORM_LOG_THROW(variableStructure.at("type").count("kind") == 1, storm::exceptions::InvalidJaniException, "For complex type as in variable " << name << "(scope: " << scopeDescription << ") kind must be given"); + std::string kind = getString(variableStructure.at("type").at("kind"), "kind for complex type as in variable " + name + "(scope: " + scopeDescription + ") "); + if(kind == "bounded") { + // First do the bounds, that makes the code a bit more streamlined + STORM_LOG_THROW(variableStructure.at("type").count("lower-bound") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scopeDescription << ") lower-bound must be given"); + storm::expressions::Expression lowerboundExpr = parseExpression(variableStructure.at("type").at("lower-bound"), "Lower bound for variable " + name + " (scope: " + scopeDescription + ")"); + assert(lowerboundExpr.isInitialized()); + STORM_LOG_THROW(variableStructure.at("type").count("upper-bound") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scopeDescription << ") upper-bound must be given"); + storm::expressions::Expression upperboundExpr = parseExpression(variableStructure.at("type").at("upper-bound"), "Upper bound for variable "+ name + " (scope: " + scopeDescription + ")"); + assert(upperboundExpr.isInitialized()); + STORM_LOG_THROW(variableStructure.at("type").count("base") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scopeDescription << ") base must be given"); + if(initvalcount == 1) { + if(variableStructure.at("initial-value").is_null()) { + initVal = storm::expressions::ite(lowerboundExpr < 0 && upperboundExpr > 0, expressionManager->integer(0), lowerboundExpr); + // TODO as soon as we support half-open intervals, we have to change this. + } else { + initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") "); + } + } + std::string basictype = getString(variableStructure.at("type").at("base"), "base for bounded type as in variable " + name + "(scope: " + scopeDescription + ") "); + if(basictype == "int") { + if(initVal) { + STORM_LOG_THROW(initVal.get().hasIntegerType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scopeDescription + ") should be an integer"); + } + STORM_LOG_THROW(lowerboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Lower bound for bounded integer variable " << name << "(scope: " << scopeDescription << ") must be integer-typed"); + STORM_LOG_THROW(upperboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Upper bound for bounded integer variable " << name << "(scope: " << scopeDescription << ") must be integer-typed"); + return storm::jani::makeBoundedIntegerVariable(name, expressionManager->declareIntegerVariable(exprManagerName), initVal, transientVar, lowerboundExpr, upperboundExpr); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported base " << basictype << " for bounded variable " << name << "(scope: " << scopeDescription << ") "); + } + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported kind " << kind << " for complex type of variable " << name << "(scope: " << scopeDescription << ") "); + } } STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description, " << variableStructure.at("type").dump() << " for variable '" << name << "' (scope: " << scopeDescription << ")"); @@ -446,7 +459,7 @@ namespace storm { ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return arguments[0] - arguments[1]; - } else if (opstring == "--") { + } else if (opstring == "-") { arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); assert(arguments.size() == 1); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); @@ -482,12 +495,12 @@ namespace storm { ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return storm::expressions::minimum(arguments[0],arguments[1]); - } else if (opstring == "⌊⌋") { + } else if (opstring == "floor") { arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); assert(arguments.size() == 1); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); return storm::expressions::floor(arguments[0]); - } else if (opstring == "⌈⌉") { + } else if (opstring == "ceil") { arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); assert(arguments.size() == 1); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); @@ -535,7 +548,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown operator " << opstring << " in " << scopeDescription << "."); } } - STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Only standard operators are supported for complex expressions as " << expressionStructure.dump() << " in " << scopeDescription << "."); + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "No supported operator declaration found for complex expressions as " << expressionStructure.dump() << " in " << scopeDescription << "."); } assert(false); @@ -564,7 +577,7 @@ namespace storm { STORM_LOG_THROW(locEntry.count("name") == 1, 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 + "'"); - STORM_LOG_THROW(locEntry.count("invariant") > 0, storm::exceptions::InvalidJaniException, "Invariants in locations as in '" + locName + "' are not supported"); + STORM_LOG_THROW(locEntry.count("invariant") == 0, storm::exceptions::InvalidJaniException, "Invariants in locations as in '" + locName + "' in automaton '" + name + "' are not supported"); //STORM_LOG_THROW(locEntry.count("invariant") > 0 && !supportsInvariants(parentModel.getModelType()), storm::exceptions::InvalidJaniException, "Invariants are not supported in the model type " + to_string(parentModel.getModelType())); std::vector transientAssignments; for(auto const& transientValueEntry : locEntry.at("transient-values")) { @@ -585,7 +598,8 @@ namespace storm { STORM_LOG_THROW(automatonStructure.count("restrict-initial") < 2, storm::exceptions::InvalidJaniException, "Automaton '" << name << "' has multiple initial value restrictions"); storm::expressions::Expression initialValueRestriction = expressionManager->boolean(true); if(automatonStructure.count("restrict-initial") > 0) { - initialValueRestriction = parseExpression(automatonStructure.at("restrict-initial"), "Initial value restriction for automaton " + name); + STORM_LOG_THROW(automatonStructure.at("restrict-initial").count("exp") == 1, storm::exceptions::InvalidJaniException, "Automaton '" << name << "' needs an expression inside the initial restricion"); + initialValueRestriction = parseExpression(automatonStructure.at("restrict-initial").at("exp"), "Initial value restriction for automaton " + name); } automaton.setInitialStatesRestriction(initialValueRestriction); uint64_t varDeclCount = automatonStructure.count("variables"); @@ -645,7 +659,7 @@ namespace storm { if(probDeclCount == 0) { probExpr = expressionManager->rational(1.0); } else { - STORM_LOG_THROW(destEntry.at("probability").count("exp") == 1, storm::exceptions::InvalidJaniException, "Destination in edge from '" << sourceLoc << "' to '" << targetLoc << "' in automaton '" << name << "' must have one expression."); + STORM_LOG_THROW(destEntry.at("probability").count("exp") == 1, storm::exceptions::InvalidJaniException, "Destination in edge from '" << sourceLoc << "' to '" << targetLoc << "' in automaton '" << name << "' must have a probability expression."); probExpr = parseExpression(destEntry.at("probability").at("exp"), "probability expression in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'", localVars); } assert(probExpr.isInitialized()); diff --git a/src/parser/JaniParser.h b/src/parser/JaniParser.h index 80b4ca0d7..a033b7479 100644 --- a/src/parser/JaniParser.h +++ b/src/parser/JaniParser.h @@ -74,6 +74,7 @@ namespace storm { static const bool defaultVariableTransient; static const bool defaultBooleanInitialValue; + static const double defaultRationalInitialValue; static const int64_t defaultIntegerInitialValue; static const std::set unsupportedOpstrings;