From 510d51e5c1896813ad36be37942e606b5e9a3c9c Mon Sep 17 00:00:00 2001 From: sjunges Date: Tue, 24 May 2016 18:24:49 +0200 Subject: [PATCH] parser support for bounded ints Former-commit-id: d1d020dc8301f7da895a20e24110223ce010f985 --- src/parser/JaniParser.cpp | 26 ++++++++++++++++++++++++-- 1 file changed, 24 insertions(+), 2 deletions(-) diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index 916611aff..b7af7772d 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -99,11 +99,33 @@ namespace storm { 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 { + // TODO clocks. STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description " << variableStructure.at("type").dump() << " for Variable '" << name << "' (scope: " << scopeDescription << ")"); } - } // TODO support other types. + } if(variableStructure.at("type").is_object()) { - // STORM_LOG_THROW(variableStructure.at("type").count("kind") == 1, storm::excepti + 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"); + std::string basictype = getString(variableStructure.at("type").at("base"), "base for bounded type as in variable " + name + "(scope: " + scopeDescription + ") "); + if(basictype == "int") { + 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 std::make_shared(name, expressionManager->declareIntegerVariable(name), lowerboundExpr, upperboundExpr, initExpr); + } 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 { STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description, " << variableStructure.at("type").dump() << " for Variable '" << name << "' (scope: " << scopeDescription << ")");