sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

parsing of jani-arrays

main
TimQu 7 years ago
parent
a9274d841c
commit
dac431b263
26 changed files with 479 additions and 163 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 230
      src/storm-parsers/parser/JaniParser.cpp
  2. 15
      src/storm-parsers/parser/JaniParser.h
  3. 3
      src/storm/storage/expressions/Expression.cpp
  4. 2
      src/storm/storage/expressions/SubstitutionVisitor.h
  5. 6
      src/storm/storage/jani/ArrayVariable.cpp
  6. 4
      src/storm/storage/jani/ArrayVariable.h
  7. 45
      src/storm/storage/jani/Assignment.cpp
  8. 41
      src/storm/storage/jani/Assignment.h
  9. 96
      src/storm/storage/jani/LValue.cpp
  10. 41
      src/storm/storage/jani/LValue.h
  11. 4
      src/storm/storage/jani/OrderedAssignments.cpp
  12. 4
      src/storm/storage/jani/Variable.h
  13. 17
      src/storm/storage/jani/expressions/ArrayAccessExpression.cpp
  14. 3
      src/storm/storage/jani/expressions/ArrayAccessExpression.h
  15. 1
      src/storm/storage/jani/expressions/ArrayExpression.h
  16. 22
      src/storm/storage/jani/expressions/ConstructorArrayExpression.cpp
  17. 5
      src/storm/storage/jani/expressions/ConstructorArrayExpression.h
  18. 6
      src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.cpp
  19. 8
      src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h
  20. 3
      src/storm/storage/jani/expressions/JaniExpressionVisitor.h
  21. 7
      src/storm/storage/jani/expressions/ValueArrayExpression.cpp
  22. 4
      src/storm/storage/jani/expressions/ValueArrayExpression.h
  23. 56
      src/storm/storage/jani/traverser/ArrayEliminator.h
  24. 8
      src/storm/storage/jani/traverser/JaniTraverser.cpp
  25. 1
      src/storm/storage/jani/traverser/JaniTraverser.h
  26. 10
      src/storm/storage/prism/ToJaniConverter.cpp

230
src/storm-parsers/parser/JaniParser.cpp
View File

@ -644,7 +644,7 @@ namespace storm {
} else if (typeStructure == "int") {
result.basicType = ParsedType::BasicType::Int;
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported type " << typeStructure.dump() << " for variable '" << name << "' (scope: " << scopeDescription << ")");
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported type " << typeStructure.dump() << " for variable '" << variableName << "' (scope: " << scopeDescription << ")");
}
} else if (typeStructure.is_object()) {
STORM_LOG_THROW(typeStructure.count("kind") == 1, storm::exceptions::InvalidJaniException, "For complex type as in variable " << variableName << "(scope: " << scopeDescription << ") kind must be given");
@ -671,10 +671,10 @@ namespace storm {
}
} else if (kind == "array") {
STORM_LOG_THROW(typeStructure.count("base") == 1, storm::exceptions::InvalidJaniException, "For array type as in variable " << variableName << "(scope: " << scopeDescription << ") base must be given");
result.arrayBase = ParsedType();
parseType(result.arrayBase.get(), typeStructure.at("base"), variableName, scopeDescription, globalVars, constants, localVars);
result.arrayBase = std::make_unique<ParsedType>();
parseType(*result.arrayBase, typeStructure.at("base"), variableName, scopeDescription, globalVars, constants, localVars);
} 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, "Unsupported kind " << kind << " for complex type of variable " << variableName << "(scope: " << scopeDescription << ") ");
}
}
}
@ -763,29 +763,31 @@ namespace storm {
} else if (type.arrayBase) {
STORM_LOG_THROW(type.arrayBase->basicType, storm::exceptions::InvalidJaniException, "Array base type for variable " + name + "(scope " + scopeDescription + ") should be a BasicType or a BoundedType.");
storm::jani::ArrayVariable::ElementType elementType;
storm::expressions::Type* exprVariableType;
storm::expressions::Type exprVariableType;
switch (type.arrayBase->basicType.get()) {
case ParsedType::BasicType::Real:
elementType = storm::jani::ArrayVariable::ElementType::Real;
exprVariableType = &expressionManager->getArrayType(expressionManager->getRationalType());
exprVariableType = expressionManager->getArrayType(expressionManager->getRationalType());
break;
case ParsedType::BasicType::Bool:
elementType = storm::jani::ArrayVariable::ElementType::Bool;
exprVariableType = &expressionManager->getArrayType(expressionManager->getBooleanType());
exprVariableType = expressionManager->getArrayType(expressionManager->getBooleanType());
break;
case ParsedType::BasicType::Int:
elementType = storm::jani::ArrayVariable::ElementType::Int;
exprVariableType = &expressionManager->getArrayType(expressionManager->getIntegerType());
exprVariableType = expressionManager->getArrayType(expressionManager->getIntegerType());
break;
default:
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Unsupported type");
}
if (setInitValFromDefault) {
initVal = storm::expressions::ValueArrayExpression(expressionManager, *exprVariableType, {});
initVal = storm::expressions::ValueArrayExpression(*expressionManager, exprVariableType, {}).toExpression();
}
if (initVal) {
STORM_LOG_THROW(initVal.get().hasArrayType(), storm::exceptions::InvalidJaniException, "Initial value for array variable " + name + "(scope " + scopeDescription + ") should be an Array");
return std::make_shared<storm::jani::ArrayVariable>(name, expressionManager->declareArrayVariable(exprManagerName, exprVariableType->getElementType()), elementType, initVal.get(), transientVar);
STORM_LOG_THROW(initVal->getType().isArrayType(), storm::exceptions::InvalidJaniException, "Initial value for array variable " + name + "(scope " + scopeDescription + ") should be an Array");
return std::make_shared<storm::jani::ArrayVariable>(name, expressionManager->declareArrayVariable(exprManagerName, exprVariableType.getElementType()), elementType, initVal.get(), transientVar);
} else {
return std::make_shared<storm::jani::ArrayVariable>(name, expressionManager->declareArrayVariable(exprManagerName, exprVariableType->getElementType()), elementType);
return std::make_shared<storm::jani::ArrayVariable>(name, expressionManager->declareArrayVariable(exprManagerName, exprVariableType.getElementType()), elementType);
}
}
@ -799,14 +801,14 @@ namespace storm {
STORM_LOG_THROW(expected == actual, storm::exceptions::InvalidJaniException, "Operator " << opstring << " expects " << expected << " arguments, but got " << actual << " in " << errorInfo << ".");
}
std::vector<storm::expressions::Expression> JaniParser::parseUnaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars, bool returnNoneInitializedOnUnknownOperator) {
storm::expressions::Expression left = parseExpression(expressionDecl.at("exp"), "Argument of operator " + opstring + " in " + scopeDescription, globalVars, constants, localVars,returnNoneInitializedOnUnknownOperator);
std::vector<storm::expressions::Expression> JaniParser::parseUnaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars, bool returnNoneInitializedOnUnknownOperator, std::unordered_map<std::string, storm::expressions::Variable> const& auxiliaryVariables) {
storm::expressions::Expression left = parseExpression(expressionDecl.at("exp"), "Argument of operator " + opstring + " in " + scopeDescription, globalVars, constants, localVars,returnNoneInitializedOnUnknownOperator, auxiliaryVariables);
return {left};
}
std::vector<storm::expressions::Expression> JaniParser::parseBinaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars, bool returnNoneInitializedOnUnknownOperator) {
storm::expressions::Expression left = parseExpression(expressionDecl.at("left"), "Left argument of operator " + opstring + " in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator);
storm::expressions::Expression right = parseExpression(expressionDecl.at("right"), "Right argument of operator " + opstring + " in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator);
std::vector<storm::expressions::Expression> JaniParser::parseBinaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars, bool returnNoneInitializedOnUnknownOperator, std::unordered_map<std::string, storm::expressions::Variable> const& auxiliaryVariables) {
storm::expressions::Expression left = parseExpression(expressionDecl.at("left"), "Left argument of operator " + opstring + " in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables);
storm::expressions::Expression right = parseExpression(expressionDecl.at("right"), "Right argument of operator " + opstring + " in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables);
return {left, right};
}
/**
@ -823,29 +825,79 @@ namespace storm {
STORM_LOG_THROW(expr.hasNumericalType(), storm::exceptions::InvalidJaniException, "Operator " << opstring << " expects argument " + std::to_string(argNr) + " to be numerical in " << errorInfo << ".");
}
storm::jani::Variable const& getLValue(std::string const& ident, storm::jani::VariableSet const& globalVars, storm::jani::VariableSet const& localVars, std::string const& scopeDescription) {
if(localVars.hasVariable(ident)) {
return localVars.getVariable(ident);
} else if(globalVars.hasVariable(ident)) {
return globalVars.getVariable(ident);
/**
* Helper for parse expression.
*/
void ensureIntegerType(storm::expressions::Expression const& expr, std::string const& opstring, unsigned argNr, std::string const& errorInfo) {
STORM_LOG_THROW(expr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Operator " << opstring << " expects argument " + std::to_string(argNr) + " to be numerical in " << errorInfo << ".");
}
/**
* Helper for parse expression.
*/
void ensureArrayType(storm::expressions::Expression const& expr, std::string const& opstring, unsigned argNr, std::string const& errorInfo) {
STORM_LOG_THROW(expr.getType().isArrayType(), storm::exceptions::InvalidJaniException, "Operator " << opstring << " expects argument " + std::to_string(argNr) + " to be of type 'array' in " << errorInfo << ".");
}
storm::jani::LValue JaniParser::parseLValue(json const& lValueStructure, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars) {
if (lValueStructure.is_string()) {
std::string ident = getString(lValueStructure, scopeDescription);
auto localVar = localVars.find(ident);
if (localVar != localVars.end()) {
return storm::jani::LValue(*localVar->second);
}
auto globalVar = globalVars.find(ident);
if (globalVar != globalVars.end()) {
return storm::jani::LValue(*globalVar->second);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown identifier '" << ident << "' occurs in " << scopeDescription);
}
} else if (lValueStructure.count("op") == 1) {
std::string opstring = getString(lValueStructure.at("op"), scopeDescription);
STORM_LOG_THROW(opstring == "aa", storm::exceptions::InvalidJaniException, "Unknown operation '" << opstring << "' occurs in " << scopeDescription);
STORM_LOG_THROW(lValueStructure.count("exp"), storm::exceptions::InvalidJaniException, "Missing 'exp' in array access at " << scopeDescription);
storm::jani::LValue exp = parseLValue(lValueStructure.at("exp"), "LValue description of array expression in " + scopeDescription, globalVars, constants, localVars);
STORM_LOG_THROW(lValueStructure.count("index"), storm::exceptions::InvalidJaniException, "Missing 'index' in array access at " << scopeDescription);
storm::expressions::Expression index = parseExpression(lValueStructure.at("index"), "Index expression of array access at " + scopeDescription, globalVars, constants, localVars);
return storm::jani::LValue(exp, index);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown identifier '" << ident << "' occurs in " << scopeDescription);
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown LValue '" << lValueStructure.dump() << "' occurs in " << scopeDescription);
// Silly warning suppression.
return storm::jani::LValue(*localVars.end()->second);
}
}
storm::expressions::Variable JaniParser::getVariableOrConstantExpression(std::string const& ident, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars) {
if(localVars.count(ident) == 1) {
return localVars.at(ident)->getExpressionVariable();
} else if(globalVars.count(ident) == 1) {
return globalVars.at(ident)->getExpressionVariable();
} else if(constants.count(ident) == 1) {
return constants.at(ident)->getExpressionVariable();
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown identifier '" << ident << "' occurs in " << scopeDescription);
storm::expressions::Variable JaniParser::getVariableOrConstantExpression(std::string const& ident, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars, std::unordered_map<std::string, storm::expressions::Variable> const& auxiliaryVariables) {
{
auto it = auxiliaryVariables.find(ident);
if (it != auxiliaryVariables.end()) {
return it->second;
}
}
{
auto it = localVars.find(ident);
if (it != localVars.end()) {
return it->second->getExpressionVariable();
}
}
{
auto it = globalVars.find(ident);
if (it != globalVars.end()) {
return it->second->getExpressionVariable();
}
}
{
auto it = constants.find(ident);
if (it != constants.end()) {
return it->second->getExpressionVariable();
}
}
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown identifier '" << ident << "' occurs in " << scopeDescription);
// Silly warning suppression.
return storm::expressions::Variable();
}
storm::expressions::Expression JaniParser::parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars, bool returnNoneInitializedOnUnknownOperator) {
storm::expressions::Expression JaniParser::parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars, bool returnNoneInitializedOnUnknownOperator, std::unordered_map<std::string, storm::expressions::Variable> const& auxiliaryVariables) {
if(expressionStructure.is_boolean()) {
if(expressionStructure.get<bool>()) {
return expressionManager->boolean(true);
@ -872,15 +924,15 @@ namespace storm {
STORM_LOG_THROW(expressionStructure.count("if") == 1, storm::exceptions::InvalidJaniException, "If operator required");
STORM_LOG_THROW(expressionStructure.count("else") == 1, storm::exceptions::InvalidJaniException, "Else operator required");
STORM_LOG_THROW(expressionStructure.count("then") == 1, storm::exceptions::InvalidJaniException, "Then operator required");
arguments.push_back(parseExpression(expressionStructure.at("if"), "if-formula in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator));
arguments.push_back(parseExpression(expressionStructure.at("then"), "then-formula in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator));
arguments.push_back(parseExpression(expressionStructure.at("else"), "else-formula in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator));
arguments.push_back(parseExpression(expressionStructure.at("if"), "if-formula in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables));
arguments.push_back(parseExpression(expressionStructure.at("then"), "then-formula in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables));
arguments.push_back(parseExpression(expressionStructure.at("else"), "else-formula in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables));
ensureNumberOfArguments(3, arguments.size(), opstring, scopeDescription);
assert(arguments.size() == 3);
ensureBooleanType(arguments[0], opstring, 0, scopeDescription);
return storm::expressions::ite(arguments[0], arguments[1], arguments[2]);
} else if (opstring == "∨") {
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator);
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables);
assert(arguments.size() == 2);
if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) {
return storm::expressions::Expression();
@ -889,7 +941,7 @@ namespace storm {
ensureBooleanType(arguments[1], opstring, 1, scopeDescription);
return arguments[0] || arguments[1];
} else if (opstring == "∧") {
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator);
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables);
assert(arguments.size() == 2);
if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) {
return storm::expressions::Expression();
@ -898,7 +950,7 @@ namespace storm {
ensureBooleanType(arguments[1], opstring, 1, scopeDescription);
return arguments[0] && arguments[1];
} else if (opstring == "⇒") {
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator);
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables);
assert(arguments.size() == 2);
if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) {
return storm::expressions::Expression();
@ -907,7 +959,7 @@ namespace storm {
ensureBooleanType(arguments[1], opstring, 1, scopeDescription);
return (!arguments[0]) || arguments[1];
} else if (opstring == "¬") {
arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator);
arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables);
assert(arguments.size() == 1);
if(!arguments[0].isInitialized()) {
return storm::expressions::Expression();
@ -915,7 +967,7 @@ namespace storm {
ensureBooleanType(arguments[0], opstring, 0, scopeDescription);
return !arguments[0];
} else if (opstring == "=") {
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator);
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables);
assert(arguments.size() == 2);
if(arguments[0].hasBooleanType()) {
ensureBooleanType(arguments[1], opstring, 1, scopeDescription);
@ -925,7 +977,7 @@ namespace storm {
return arguments[0] == arguments[1];
}
} else if (opstring == "≠") {
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator);
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables);
assert(arguments.size() == 2);
if(arguments[0].hasBooleanType()) {
ensureBooleanType(arguments[1], opstring, 1, scopeDescription);
@ -935,7 +987,7 @@ namespace storm {
return arguments[0] != arguments[1];
}
} else if (opstring == "<") {
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator);
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables);
assert(arguments.size() == 2);
if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) {
return storm::expressions::Expression();
@ -944,7 +996,7 @@ namespace storm {
ensureNumericalType(arguments[1], opstring, 1, scopeDescription);
return arguments[0] < arguments[1];
} else if (opstring == "≤") {
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator);
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables);
assert(arguments.size() == 2);
if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) {
return storm::expressions::Expression();
@ -953,7 +1005,7 @@ namespace storm {
ensureNumericalType(arguments[1], opstring, 1, scopeDescription);
return arguments[0] <= arguments[1];
} else if (opstring == ">") {
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator);
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables);
assert(arguments.size() == 2);
if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) {
return storm::expressions::Expression();
@ -962,7 +1014,7 @@ namespace storm {
ensureNumericalType(arguments[1], opstring, 1, scopeDescription);
return arguments[0] > arguments[1];
} else if (opstring == "≥") {
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator);
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables);
assert(arguments.size() == 2);
if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) {
return storm::expressions::Expression();
@ -971,97 +1023,137 @@ namespace storm {
ensureNumericalType(arguments[1], opstring, 1, scopeDescription);
return arguments[0] >= arguments[1];
} else if (opstring == "+") {
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator);
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables);
assert(arguments.size() == 2);
ensureNumericalType(arguments[0], opstring, 0, scopeDescription);
ensureNumericalType(arguments[1], opstring, 1, scopeDescription);
return arguments[0] + arguments[1];
} else if (opstring == "-") {
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator);
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables);
assert(arguments.size() == 2);
ensureNumericalType(arguments[0], opstring, 0, scopeDescription);
ensureNumericalType(arguments[1], opstring, 1, scopeDescription);
return arguments[0] - arguments[1];
} else if (opstring == "-") {
arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription,globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator);
arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription,globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables);
assert(arguments.size() == 1);
ensureNumericalType(arguments[0], opstring, 0, scopeDescription);
return -arguments[0];
} else if (opstring == "*") {
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator);
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables);
assert(arguments.size() == 2);
ensureNumericalType(arguments[0], opstring, 0, scopeDescription);
ensureNumericalType(arguments[1], opstring, 1, scopeDescription);
return arguments[0] * arguments[1];
} else if (opstring == "/") {
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator);
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables);
assert(arguments.size() == 2);
ensureNumericalType(arguments[0], opstring, 0, scopeDescription);
ensureNumericalType(arguments[1], opstring, 1, scopeDescription);
return arguments[0] / arguments[1];
} else if (opstring == "%") {
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator);
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables);
assert(arguments.size() == 2);
ensureNumericalType(arguments[0], opstring, 0, scopeDescription);
ensureNumericalType(arguments[1], opstring, 1, scopeDescription);
return arguments[0] % arguments[1];
} else if (opstring == "max") {
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator);
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables);
assert(arguments.size() == 2);
ensureNumericalType(arguments[0], opstring, 0, scopeDescription);
ensureNumericalType(arguments[1], opstring, 1, scopeDescription);
return storm::expressions::maximum(arguments[0],arguments[1]);
} else if (opstring == "min") {
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator);
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables);
assert(arguments.size() == 2);
ensureNumericalType(arguments[0], opstring, 0, scopeDescription);
ensureNumericalType(arguments[1], opstring, 1, scopeDescription);
return storm::expressions::minimum(arguments[0],arguments[1]);
} else if (opstring == "floor") {
arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator);
arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables);
assert(arguments.size() == 1);
ensureNumericalType(arguments[0], opstring, 0, scopeDescription);
return storm::expressions::floor(arguments[0]);
} else if (opstring == "ceil") {
arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator);
arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables);
assert(arguments.size() == 1);
ensureNumericalType(arguments[0], opstring, 0, scopeDescription);
return storm::expressions::ceil(arguments[0]);
} else if (opstring == "abs") {
arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator);
arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables);
assert(arguments.size() == 1);
ensureNumericalType(arguments[0], opstring, 0, scopeDescription);
return storm::expressions::abs(arguments[0]);
} else if (opstring == "sgn") {
arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator);
arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables);
assert(arguments.size() == 1);
ensureNumericalType(arguments[0], opstring, 0, scopeDescription);
return storm::expressions::sign(arguments[0]);
} else if (opstring == "trc") {
arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator);
arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables);
assert(arguments.size() == 1);
ensureNumericalType(arguments[0], opstring, 0, scopeDescription);
return storm::expressions::truncate(arguments[0]);
} else if (opstring == "pow") {
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator);
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables);
assert(arguments.size() == 2);
ensureNumericalType(arguments[0], opstring, 0, scopeDescription);
ensureNumericalType(arguments[1], opstring, 1, scopeDescription);
return arguments[0]^arguments[1];
} else if (opstring == "exp") {
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator);
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables);
assert(arguments.size() == 2);
ensureNumericalType(arguments[0], opstring, 0, scopeDescription);
ensureNumericalType(arguments[1], opstring, 1, scopeDescription);
// TODO implement
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "exp operation is not yet implemented");
} else if (opstring == "log") {
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator);
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables);
assert(arguments.size() == 2);
ensureNumericalType(arguments[0], opstring, 0, scopeDescription);
ensureNumericalType(arguments[1], opstring, 1, scopeDescription);
// TODO implement
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "log operation is not yet implemented");
} else if (opstring == "aa") {
STORM_LOG_THROW(expressionStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Array access operator requires exactly one exp (at " + scopeDescription + ").");
storm::expressions::Expression exp = parseExpression(expressionStructure.at("exp"), "exp in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables);
STORM_LOG_THROW(expressionStructure.count("index") == 1, storm::exceptions::InvalidJaniException, "Array access operator requires exactly one index (at " + scopeDescription + ").");
storm::expressions::Expression index = parseExpression(expressionStructure.at("index"), "index in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables);
ensureArrayType(exp, opstring, 0, scopeDescription);
ensureIntegerType(index, opstring, 1, scopeDescription);
return std::make_shared<storm::expressions::ArrayAccessExpression>(exp.getManager(), exp.getType().getElementType(), exp.getBaseExpressionPointer(), index.getBaseExpressionPointer())->toExpression();
} else if (opstring == "av") {
STORM_LOG_THROW(expressionStructure.count("elements") == 1, storm::exceptions::InvalidJaniException, "Array value operator requires exactly one 'elements' (at " + scopeDescription + ").");
std::vector<std::shared_ptr<storm::expressions::BaseExpression const>> elements;
storm::expressions::Type commonType;
bool first = true;
for (auto const& element : expressionStructure.at("elements")) {
elements.push_back(parseExpression(element, "element " + std::to_string(elements.size()) + " in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables).getBaseExpressionPointer());
if (first) {
commonType = elements.back()->getType();
first = false;
} else if (!(commonType == elements.back()->getType())) {
if (commonType.isIntegerType() && elements.back()->getType().isRationalType()) {
commonType = elements.back()->getType();
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Incompatible element types " << commonType << " and " << elements.back()->getType() << " of array value expression at " << scopeDescription);
}
}
}
return std::make_shared<storm::expressions::ValueArrayExpression>(*expressionManager, expressionManager->getArrayType(commonType), elements)->toExpression();
} else if (opstring == "ac") {
STORM_LOG_THROW(expressionStructure.count("length") == 1, storm::exceptions::InvalidJaniException, "Array access operator requires exactly one length (at " + scopeDescription + ").");
storm::expressions::Expression length = parseExpression(expressionStructure.at("length"), "index in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables);
ensureIntegerType(length, opstring, 1, scopeDescription);
STORM_LOG_THROW(expressionStructure.count("var") == 1, storm::exceptions::InvalidJaniException, "Array access operator requires exactly one var (at " + scopeDescription + ").");
std::string indexVarName = getString(expressionStructure.at("var"), "Field 'var' of Array access operator (at " + scopeDescription + ").");
STORM_LOG_THROW(auxiliaryVariables.find(indexVarName) == auxiliaryVariables.end(), storm::exceptions::InvalidJaniException, "Index variable " << indexVarName << " is already defined as an auxiliary variable (at " + scopeDescription + ").");
auto newAuxVars = auxiliaryVariables;
storm::expressions::Variable indexVar = expressionManager->declareIntegerVariable(indexVarName);
newAuxVars.emplace(indexVarName, indexVar);
STORM_LOG_THROW(expressionStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Array access operator requires exactly one exp (at " + scopeDescription + ").");
storm::expressions::Expression exp = parseExpression(expressionStructure.at("exp"), "exp in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, newAuxVars);
return std::make_shared<storm::expressions::ConstructorArrayExpression>(*expressionManager, expressionManager->getArrayType(exp.getType()), length.getBaseExpressionPointer(), indexVar, exp.getBaseExpressionPointer())->toExpression();
} else if (unsupportedOpstrings.count(opstring) > 0){
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Opstring " + opstring + " is not supported by storm");
@ -1080,8 +1172,6 @@ namespace storm {
}
void JaniParser::parseActions(json const& actionStructure, storm::jani::Model& parentModel) {
std::set<std::string> actionNames;
for(auto const& actionEntry : actionStructure) {
@ -1125,10 +1215,10 @@ namespace storm {
for(auto const& transientValueEntry : locEntry.at("transient-values")) {
STORM_LOG_THROW(transientValueEntry.count("ref") == 1, storm::exceptions::InvalidJaniException, "Transient values in location " << locName << " need exactly one ref that is assigned to");
STORM_LOG_THROW(transientValueEntry.count("value") == 1, storm::exceptions::InvalidJaniException, "Transient values in location " << locName << " need exactly one assigned value");
storm::jani::Variable const& lhs = getLValue(transientValueEntry.at("ref"), parentModel.getGlobalVariables(), automaton.getVariables(), "LHS of assignment in location " + locName + " (automaton '" + name + "')");
STORM_LOG_THROW(lhs.isTransient(), storm::exceptions::InvalidJaniException, "Assigned non-transient variable " + lhs.getName() + " in location " + locName + " (automaton: '" + name + "')");
storm::expressions::Expression rhs = parseExpression(transientValueEntry.at("value"), "Assignment of variable " + lhs.getName() + " in location " + locName + " (automaton: '" + name + "')", globalVars, constants, localVars);
transientAssignments.emplace_back(lhs, rhs);
storm::jani::LValue lValue = parseLValue(transientValueEntry.at("ref"), "LHS of assignment in location " + locName + " (automaton '" + name + "')", globalVars, constants, localVars);
STORM_LOG_THROW(lValue.isTransient(), storm::exceptions::InvalidJaniException, "Assigned non-transient variable " << lValue << " in location " + locName + " (automaton: '" + name + "')");
storm::expressions::Expression rhs = parseExpression(transientValueEntry.at("value"), "Assignment of lValue in location " + locName + " (automaton: '" + name + "')", globalVars, constants, localVars);
transientAssignments.emplace_back(lValue, rhs);
}
}
uint64_t id = automaton.addLocation(storm::jani::Location(locName, transientAssignments));
@ -1210,7 +1300,7 @@ namespace storm {
// 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 + "'");
storm::jani::Variable const& lhs = getLValue(refstring, parentModel.getGlobalVariables(), automaton.getVariables(), "Assignment variable in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'");
storm::jani::LValue lValue = parseLValue(refstring, "Assignment variable in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'", globalVars, constants, localVars);
// 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 + "'", globalVars, constants, localVars);
@ -1220,7 +1310,7 @@ namespace storm {
if(assignmentEntry.count("index") > 0) {
assignmentIndex = getUnsignedInt(assignmentEntry.at("index"), "assignment index in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'");
}
assignments.emplace_back(lhs, assignmentExpr, assignmentIndex);
assignments.emplace_back(lValue, assignmentExpr, assignmentIndex);
}
}
destinationLocationsAndProbabilities.emplace_back(locIds.at(targetLoc), probExpr);

15
src/storm-parsers/parser/JaniParser.h
View File

@ -1,5 +1,6 @@
#pragma once
#include "storm/storage/jani/Constant.h"
#include "storm/storage/jani/LValue.h"
#include "storm/logic/Formula.h"
#include "storm/logic/Bound.h"
#include "storm/logic/RewardAccumulation.h"
@ -51,14 +52,14 @@ namespace storm {
storm::jani::Automaton parseAutomaton(json const& automatonStructure, storm::jani::Model const& parentModel, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants);
struct ParsedType {
enum class BasicType {Bool, Int, Real};
boost::optional<BasicType> basicType;
boost::optional<std::pair<storm::expressions::Expression, storm::expressions::Expression>> bounds;
boost::optional<ParsedType> arrayBase;
std::unique_ptr<ParsedType> arrayBase;
};
void JaniParser::parseType(ParsedType& result, json const& typeStructure, std::string variableName, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars);
void parseType(ParsedType& result, json const& typeStructure, std::string variableName, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars);
storm::jani::LValue parseLValue(json const& lValueStructure, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {});
std::shared_ptr<storm::jani::Variable> parseVariable(json const& variableStructure, bool requireInitialValues, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {}, 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& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {}, bool returnNoneOnUnknownOpString = false);
storm::expressions::Expression parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {}, bool returnNoneOnUnknownOpString = false, std::unordered_map<std::string, storm::expressions::Variable> const& auxiliaryVariables = {});
private:
std::shared_ptr<storm::jani::Constant> parseConstant(json const& constantStructure, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::string const& scopeDescription = "global");
@ -68,8 +69,8 @@ namespace storm {
*/
void parseActions(json const& actionStructure, storm::jani::Model& parentModel);
std::shared_ptr<storm::logic::Formula const> parseFormula(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::string const& context, boost::optional<storm::logic::Bound> bound = boost::none);
std::vector<storm::expressions::Expression> parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars= {}, bool returnNoneOnUnknownOpString = false);
std::vector<storm::expressions::Expression> parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {}, bool returnNoneOnUnknownOpString = false);
std::vector<storm::expressions::Expression> parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars= {}, bool returnNoneOnUnknownOpString = false, std::unordered_map<std::string, storm::expressions::Variable> const& auxiliaryVariables = {});
std::vector<storm::expressions::Expression> parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {}, bool returnNoneOnUnknownOpString = false, std::unordered_map<std::string, storm::expressions::Variable> const& auxiliaryVariables = {});
std::vector<std::shared_ptr<storm::logic::Formula const>> parseUnaryFormulaArgument(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::string const& context);
@ -79,7 +80,7 @@ namespace storm {
std::shared_ptr<storm::jani::Composition> parseComposition(json const& compositionStructure);
storm::expressions::Variable getVariableOrConstantExpression(std::string const& ident, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {});
storm::expressions::Variable getVariableOrConstantExpression(std::string const& ident, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {}, std::unordered_map<std::string, storm::expressions::Variable> const& auxiliaryVariables = {});

3
src/storm/storage/expressions/Expression.cpp
View File

@ -451,8 +451,5 @@ namespace storm {
return result;
}
}
}

2
src/storm/storage/expressions/SubstitutionVisitor.h
View File

@ -39,7 +39,7 @@ namespace storm {
virtual boost::any visit(IntegerLiteralExpression const& expression, boost::any const& data) override;
virtual boost::any visit(RationalLiteralExpression const& expression, boost::any const& data) override;
private:
protected:
// A mapping of variables to expressions with which they shall be replaced.
MapType const& variableToExpressionMapping;
};

6
src/storm/storage/jani/ArrayVariable.cpp
View File

@ -3,11 +3,11 @@
namespace storm {
namespace jani {
ArrayVariable::ArrayVariable(std::string const& name, storm::expressions::Variable const& variable) : Variable(name, variable) {
ArrayVariable::ArrayVariable(std::string const& name, storm::expressions::Variable const& variable, ElementType const& elementType) : Variable(name, variable), elementType(elementType) {
// Intentionally left empty.
}
ArrayVariable::ArrayVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initValue) : Variable(name, variable, initValue, transient) {
ArrayVariable::ArrayVariable(std::string const& name, storm::expressions::Variable const& variable, ElementType const& elementType, storm::expressions::Expression const& initValue, bool transient) : Variable(name, variable, initValue, transient), elementType(elementType) {
// Intentionally left empty.
}
@ -35,7 +35,7 @@ namespace storm {
return maxSize.get();
}
ElementType ArrayVariable::getElementType() const {
typename ArrayVariable::ElementType ArrayVariable::getElementType() const {
return elementType;
}

4
src/storm/storage/jani/ArrayVariable.h
View File

@ -13,12 +13,12 @@ namespace storm {
/*!
* Creates an Array variable
*/
ArrayVariable(std::string const& name, storm::expressions::Variable const& variable, ElementType elementType);
ArrayVariable(std::string const& name, storm::expressions::Variable const& variable, ElementType const& elementType);
/*!
* Creates an Array variable with initial value
*/
ArrayVariable(std::string const& name, storm::expressions::Variable const& variable, ElementType elementType, storm::expressions::Expression const& initialValue, bool transient);
ArrayVariable(std::string const& name, storm::expressions::Variable const& variable, ElementType const& elementType, storm::expressions::Expression const& initValue, bool transient);
/*!
* Sets/Gets bounds to the values stored in this array

45
src/storm/storage/jani/Assignment.cpp
View File

@ -1,5 +1,7 @@
#include "storm/storage/jani/Assignment.h"
#include "storm/storage/jani/LValue.h"
#include "storm/storage/expressions/LinearityCheckVisitor.h"
#include "storm/utility/macros.h"
@ -8,20 +10,32 @@
namespace storm {
namespace jani {
Assignment::Assignment(storm::jani::Variable const& variable, storm::expressions::Expression const& expression, uint64_t level) : variable(variable), expression(expression), level(level) {
Assignment::Assignment(storm::jani::LValue const& lValue, storm::expressions::Expression const& expression, uint64_t level) : lValue(lValue), expression(expression), level(level) {
// Intentionally left empty
}
bool Assignment::operator==(Assignment const& other) const {
return this->isTransient() == other.isTransient() && this->getExpressionVariable() == other.getExpressionVariable() && this->getAssignedExpression().isSyntacticallyEqual(other.getAssignedExpression()) && this->getLevel() == other.getLevel();
}
bool Assignment::lValueIsVariable() const {
return lValue.isVariable();
}
bool Assignment::lValueIsArrayAccess() const {
return lValue.isArrayAccess();
}
storm::jani::LValue const& Assignment::getLValue() const {
return lValue;
}
storm::jani::Variable const& Assignment::getVariable() const {
return variable.get();
return lValue.getVariable();
}
storm::expressions::Variable const& Assignment::getExpressionVariable() const {
return variable.get().getExpressionVariable();
return getVariable().getExpressionVariable();
}
storm::expressions::Expression const& Assignment::getAssignedExpression() const {
@ -33,11 +47,14 @@ namespace storm {
}
bool Assignment::isTransient() const {
return this->variable.get().isTransient();
return lValue.isTransient();
}
void Assignment::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
this->setAssignedExpression(this->getAssignedExpression().substitute(substitution).simplify());
if (lValue.isArrayAccess()) {
lValue = LValue(LValue(lValue.getArray()), lValue.getArrayIndex().substitute(substitution).simplify());
}
}
int64_t Assignment::getLevel() const {
@ -54,24 +71,24 @@ namespace storm {
}
std::ostream& operator<<(std::ostream& stream, Assignment const& assignment) {
stream << assignment.getVariable().getName() << " := " << assignment.getAssignedExpression();
stream << assignment.getLValue() << " := " << assignment.getAssignedExpression();
return stream;
}
bool AssignmentPartialOrderByLevelAndVariable::operator()(Assignment const& left, Assignment const& right) const {
return left.getLevel() < right.getLevel() || (left.getLevel() == right.getLevel() && left.getExpressionVariable() < right.getExpressionVariable());
bool AssignmentPartialOrderByLevelAndLValue::operator()(Assignment const& left, Assignment const& right) const {
return left.getLevel() < right.getLevel() || (left.getLevel() == right.getLevel() && left.getLValue() < right.getLValue());
}
bool AssignmentPartialOrderByLevelAndVariable::operator()(Assignment const& left, std::shared_ptr<Assignment> const& right) const {
return left.getLevel() < right->getLevel() || (left.getLevel() == right->getLevel() && left.getExpressionVariable() < right->getExpressionVariable());
bool AssignmentPartialOrderByLevelAndLValue::operator()(Assignment const& left, std::shared_ptr<Assignment> const& right) const {
return left.getLevel() < right->getLevel() || (left.getLevel() == right->getLevel() && left.getLValue() < right->getLValue());
}
bool AssignmentPartialOrderByLevelAndVariable::operator()(std::shared_ptr<Assignment> const& left, std::shared_ptr<Assignment> const& right) const {
return left->getLevel() < right->getLevel() || (left->getLevel() == right->getLevel() && left->getExpressionVariable() < right->getExpressionVariable());
bool AssignmentPartialOrderByLevelAndLValue::operator()(std::shared_ptr<Assignment> const& left, std::shared_ptr<Assignment> const& right) const {
return left->getLevel() < right->getLevel() || (left->getLevel() == right->getLevel() && left->getLValue() < right->getLValue());
}
bool AssignmentPartialOrderByLevelAndVariable::operator()(std::shared_ptr<Assignment> const& left, Assignment const& right) const {
return left->getLevel() < right.getLevel() || (left->getLevel() == right.getLevel() && left->getExpressionVariable() < right.getExpressionVariable());
bool AssignmentPartialOrderByLevelAndLValue::operator()(std::shared_ptr<Assignment> const& left, Assignment const& right) const {
return left->getLevel() < right.getLevel() || (left->getLevel() == right.getLevel() && left->getLValue() < right.getLValue());
}
}
}

41
src/storm/storage/jani/Assignment.h
View File

@ -2,7 +2,7 @@
#include <functional>
#include "storm/storage/jani/Variable.h"
#include "storm/storage/jani/LValue.h"
#include "storm/storage/expressions/Expression.h"
namespace storm {
@ -11,20 +11,39 @@ namespace storm {
class Assignment {
public:
/*!
* Creates an assignment of the given expression to the given variable.
* Creates an assignment of the given expression to the given LValue.
*/
Assignment(storm::jani::Variable const& variable, storm::expressions::Expression const& expression, uint64_t index = 0);
Assignment(storm::jani::LValue const& lValue, storm::expressions::Expression const& expression, uint64_t index = 0);
Assignment(Assignment const&) = default;
bool operator==(Assignment const& other) const;
/*!
* Retrieves the expression variable that is written in this assignment.
* Returns true if the lValue is a variable
*/
bool lValueIsVariable() const;
/*!
* Returns true if the lValue is an array access
*/
bool lValueIsArrayAccess() const;
/*!
* Retrieves the lValue that is written in this assignment.
* @return
*/
storm::jani::LValue const& getLValue() const;
/*!
* Retrieves the Variable that is written in this assignment.
* This assumes that the lValue is a variable.
*/
storm::jani::Variable const& getVariable() const;
/*!
* Retrieves the expression variable that is written in this assignment.
* This assumes that the lValue is a variable.
*/
storm::expressions::Variable const& getExpressionVariable() const;
@ -34,7 +53,7 @@ namespace storm {
storm::expressions::Expression const& getAssignedExpression() const;
/*!
* Sets a new expression that is assigned to the target variable.
* Sets a new expression that is assigned to the target LValue.
*/
void setAssignedExpression(storm::expressions::Expression const& expression);
@ -66,10 +85,10 @@ namespace storm {
friend std::ostream& operator<<(std::ostream& stream, Assignment const& assignment);
private:
// The variable being assigned.
std::reference_wrapper<storm::jani::Variable const> variable;
// The lValue being assigned.
LValue lValue;
// The expression that is being assigned to the variable.
// The expression that is being assigned to the lValue.
storm::expressions::Expression expression;
// The level of the assignment.
@ -77,10 +96,10 @@ namespace storm {
};
/*!
* This functor enables ordering the assignments first by the assignment level and then by variable.
* This functor enables ordering the assignments first by the assignment level and then by lValue.
* Note that this is a partial order.
*/
struct AssignmentPartialOrderByLevelAndVariable {
struct AssignmentPartialOrderByLevelAndLValue {
bool operator()(Assignment const& left, Assignment const& right) const;
bool operator()(Assignment const& left, std::shared_ptr<Assignment> const& right) const;
bool operator()(std::shared_ptr<Assignment> const& left, std::shared_ptr<Assignment> const& right) const;

96
src/storm/storage/jani/LValue.cpp
View File

@ -0,0 +1,96 @@
#include "storm/storage/jani/LValue.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/NotSupportedException.h"
namespace storm {
namespace jani {
LValue::LValue(storm::jani::Variable const& variable) : variable(&variable) {
// Intentionally left empty
}
LValue::LValue(LValue const& array, storm::expressions::Expression const& index) : arrayIndex(index) {
STORM_LOG_THROW(array.isVariable(), storm::exceptions::NotSupportedException, "Nested arrays as LValues are currently not implemented.");
variable = &array.getVariable();
}
bool LValue::isVariable() const {
return !arrayIndex.isInitialized();
}
storm::jani::Variable const& LValue::getVariable() const {
STORM_LOG_ASSERT(isVariable(), "Tried to get the variable of an LValue, that actually is not a variable.");
return *variable;
}
bool LValue::isArrayAccess() const {
return arrayIndex.isInitialized();
}
storm::jani::ArrayVariable const& LValue::getArray() const {
STORM_LOG_ASSERT(isArrayAccess(), "Tried to get the array variable of an LValue that is not an array access.");
STORM_LOG_ASSERT(variable->isArrayVariable(), "Tried to get the array variable of an array access LValue, but the variable is not of type array.");
return variable->asArrayVariable();
}
storm::expressions::Expression const& LValue::getArrayIndex() const {
STORM_LOG_ASSERT(isArrayAccess(), "Tried to get the array index of an LValue, that is not an array access.");
return arrayIndex;
}
bool LValue::isTransient() const {
return variable->isTransient();
}
LValue LValue::changeAssignmentVariables(std::map<Variable const*, std::reference_wrapper<Variable const>> const& remapping) const {
if (isVariable()) {
return LValue(remapping.at(variable));
} else {
STORM_LOG_ASSERT(isArrayAccess(), "Unhandled LValue.");
return LValue(LValue(remapping.at(variable)), arrayIndex);
}
}
bool LValue::operator<(LValue const& other) const {
if (isVariable()) {
return !other.isVariable() || variable->getExpressionVariable() < other.getVariable().getExpressionVariable();
} else {
STORM_LOG_ASSERT(isArrayAccess(), "Unhandled LValue.");
if (other.isVariable()) {
return false;
}
STORM_LOG_ASSERT(other.isArrayAccess(), "Unhandled LValue.");
if (variable->getExpressionVariable() < other.getVariable().getExpressionVariable()) {
return true;
} else if (other.getVariable().getExpressionVariable() < variable->getExpressionVariable()) {
return false;
} else {
return std::less<storm::expressions::Expression>()(arrayIndex, other.getArrayIndex());
}
}
}
bool LValue::operator==(LValue const& other) const {
if (isVariable()) {
return other.isVariable() && getVariable().getExpressionVariable() == other.getVariable().getExpressionVariable();
} else {
STORM_LOG_ASSERT(isArrayAccess(), "Unhandled LValue.");
return other.isArrayAccess() && getVariable().getExpressionVariable() == other.getVariable().getExpressionVariable() && getArrayIndex().isSyntacticallyEqual(other.getArrayIndex());
}
}
std::ostream& operator<<(std::ostream& stream, LValue const& lValue) {
if (lValue.isVariable()) {
stream << lValue.getVariable().getName();
} else {
STORM_LOG_ASSERT(lValue.isArrayAccess(), "Unhandled LValue.");
stream << lValue.getArray().getName() << "[" << lValue.getArrayIndex() << "]";
}
return stream;
}
}
}

41
src/storm/storage/jani/LValue.h
View File

@ -0,0 +1,41 @@
#pragma once
#include "storm/storage/jani/ArrayVariable.h"
#include "storm/storage/expressions/Expressions.h"
namespace storm {
namespace jani {
class LValue {
public:
explicit LValue(storm::jani::Variable const& variable);
LValue(LValue const& array, storm::expressions::Expression const& index);
LValue(LValue const&) = default;
bool operator==(LValue const& other) const;
bool isVariable() const;
storm::jani::Variable const& getVariable() const;
bool isArrayAccess() const;
storm::jani::ArrayVariable const& getArray() const;
storm::expressions::Expression const& getArrayIndex() const;
bool isTransient() const;
bool operator< (LValue const& other) const;
LValue changeAssignmentVariables(std::map<Variable const*, std::reference_wrapper<Variable const>> const& remapping) const;
friend std::ostream& operator<<(std::ostream& stream, LValue const& lvalue);
private:
// The variable being assigned.
storm::jani::Variable const* variable;
// In case of an array access LValue, this is the accessed index of the array.
storm::expressions::Expression arrayIndex;
};
}
}

4
src/storm/storage/jani/OrderedAssignments.cpp
View File

@ -221,13 +221,13 @@ namespace storm {
void OrderedAssignments::changeAssignmentVariables(std::map<Variable const*, std::reference_wrapper<Variable const>> const& remapping) {
std::vector<Assignment> newAssignments;
for (auto& assignment : allAssignments) {
newAssignments.emplace_back(remapping.at(&assignment->getVariable()), assignment->getAssignedExpression(), assignment->getLevel());
newAssignments.emplace_back(assignment->getLValue().changeAssignmentVariables(remapping), assignment->getAssignedExpression(), assignment->getLevel());
}
*this = OrderedAssignments(newAssignments);
}
std::vector<std::shared_ptr<Assignment>>::const_iterator OrderedAssignments::lowerBound(Assignment const& assignment, std::vector<std::shared_ptr<Assignment>> const& assignments) {
return std::lower_bound(assignments.begin(), assignments.end(), assignment, storm::jani::AssignmentPartialOrderByLevelAndVariable());
return std::lower_bound(assignments.begin(), assignments.end(), assignment, storm::jani::AssignmentPartialOrderByLevelAndLValue());
}
uint64_t OrderedAssignments::isReadBeforeAssignment(Variable const& var, uint64_t assignmentNumber, uint64_t start) const {

4
src/storm/storage/jani/Variable.h
View File

@ -86,8 +86,8 @@ namespace storm {
UnboundedIntegerVariable const& asUnboundedIntegerVariable() const;
RealVariable& asRealVariable();
RealVariable const& asRealVariable() const;
RealVariable& asArrayVariable();
RealVariable const& asArrayVariable() const;
ArrayVariable& asArrayVariable();
ArrayVariable const& asArrayVariable() const;
/*!
* Substitutes all variables in all expressions according to the given substitution.

17
src/storm/storage/jani/expressions/ArrayAccessExpression.cpp
View File

@ -1,5 +1,8 @@
#include "storm/storage/jani/expressions/ArrayAccessExpression.h"
#include "storm/storage/jani/expressions/JaniExpressionVisitor.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/UnexpectedException.h"
namespace storm {
namespace expressions {
@ -11,7 +14,7 @@ namespace storm {
}
std::shared_ptr<BaseExpression const> ArrayAccessExpression::simplify() const {
return std::shared_ptr<BaseExpression const>(new ArrayAccessExpression(manager, type, getFirstOperand()->simplify(), getSecondOperand()->simplify()));
return std::shared_ptr<BaseExpression const>(new ArrayAccessExpression(getManager(), getType(), getFirstOperand()->simplify(), getSecondOperand()->simplify()));
}
boost::any ArrayAccessExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const {
@ -21,16 +24,12 @@ namespace storm {
}
void ArrayAccessExpression::printToStream(std::ostream& stream) const {
if (firstOperand->isVariable()) {
getFirstOperand()->printToStream(stream);
if (getFirstOperand()->isVariable()) {
stream << *getFirstOperand();
} else {
stream << "(";
getFirstOperand()->printToStream(stream);
stream << ")";
stream << "(" << *getFirstOperand() << ")";
}
stream << "[";
getSecondOperand()->printToStream(stream);
stream << "]";
stream << "[" << getSecondOperand() << "]";
}
}
}

3
src/storm/storage/jani/expressions/ArrayAccessExpression.h
View File

@ -1,7 +1,6 @@
#pragma once
#include "storm/storage/expressions/BaseExpression.h"
#include "storm/storage/jani/expressions/ExpressionManager.h"
#include "storm/storage/expressions/BinaryExpression.h"
namespace storm {
namespace expressions {

1
src/storm/storage/jani/expressions/ArrayExpression.h
View File

@ -1,7 +1,6 @@
#pragma once
#include "storm/storage/expressions/BaseExpression.h"
#include "storm/storage/jani/expressions/ExpressionManager.h"
namespace storm {
namespace expressions {

22
src/storm/storage/jani/expressions/ConstructorArrayExpression.cpp
View File

@ -1,6 +1,7 @@
#include "storm/storage/jani/expressions/ConstructorArrayExpression.h"
#include "storm/storage/jani/expressions/JaniExpressionVisitor.h"
#include "storm/storage/expressions/ExpressionManager.h"
#include "storm/exceptions/InvalidArgumentException.h"
#include "storm/exceptions/UnexpectedException.h"
@ -8,14 +9,14 @@
namespace storm {
namespace expressions {
ConstructorArrayExpression::ConstructorArrayExpression(ExpressionManager const& manager, Type const& type, std::shared_ptr<BaseExpression const> const& size, storm::expressions::Variable indexVar, std::shared_ptr<BaseExpression const> const& elementExpression) : ArrayExpression(manager, type), size(size), indexVar(indexVar), elementExpression(elementExpression) {
ConstructorArrayExpression::ConstructorArrayExpression(ExpressionManager const& manager, Type const& type, std::shared_ptr<BaseExpression const> const& size, storm::expressions::Variable indexVar, std::shared_ptr<BaseExpression const> const& elementExpression) : ArrayExpression(manager, type), sizeExpression(size), indexVar(indexVar), elementExpression(elementExpression) {
// Intentionally left empty
}
void ConstructorArrayExpression::gatherVariables(std::set<storm::expressions::Variable>& variables) const {
// The indexVar should not be gathered (unless it is already contained).
bool indexVarContained = variables.find(indexVar) != variables.end();
size->gatherVariables(variables);
sizeExpression->gatherVariables(variables);
elementExpression->gatherVariables(variables);
if (!indexVarContained) {
variables.erase(indexVar);
@ -23,7 +24,7 @@ namespace storm {
}
bool ConstructorArrayExpression::containsVariables() const {
if (size->containsVariables()) {
if (sizeExpression->containsVariables()) {
return true;
}
// The index variable should not count
@ -34,7 +35,7 @@ namespace storm {
}
std::shared_ptr<BaseExpression const> ConstructorArrayExpression::simplify() const {
return std::shared_ptr<BaseExpression const>(new ConstructorArrayExpression(manager, type, size->simplify(), indexVar, elementExpression->simplify()));
return std::shared_ptr<BaseExpression const>(new ConstructorArrayExpression(getManager(), getType(), sizeExpression->simplify(), indexVar, elementExpression->simplify()));
}
boost::any ConstructorArrayExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const {
@ -44,20 +45,17 @@ namespace storm {
}
void ConstructorArrayExpression::printToStream(std::ostream& stream) const {
stream << "array[ ";
elementExpression->printToStream(stream);
stream << " | " << indexVar << "<";
size->printToStream(stream);
stream << " ]";
stream << "array[ " << *elementExpression << " | " << indexVar.getExpression() << " < " << *sizeExpression << " ]";
}
std::shared_ptr<BaseExpression const> ConstructorArrayExpression::size() const {
return size;
return sizeExpression;
}
std::shared_ptr<BaseExpression const> ConstructorArrayExpression::at(uint64_t i) const {
STORM_LOG_THROW(i < elements.size(), storm::exceptions::InvalidArgumentException, "Tried to access the element with index " << i << " of an array of size " << elements.size() << ".");
return elements[i];
std::map<storm::expressions::Variable, storm::expressions::Expression> substitution;
substitution.emplace(indexVar, this->getManager().integer(i));
return elementExpression->toExpression().substitute(substitution).getBaseExpressionPointer();
}
std::shared_ptr<BaseExpression const> const& ConstructorArrayExpression::getElementExpression() const {

5
src/storm/storage/jani/expressions/ConstructorArrayExpression.h
View File

@ -1,6 +1,7 @@
#pragma once
#include "storm/storage/jani/expressions/ArrayExpression.h"
#include "storm/storage/expressions/Variable.h"
namespace storm {
namespace expressions {
@ -22,7 +23,7 @@ namespace storm {
virtual ~ConstructorArrayExpression() = default;
virtual void gatherVariables(std::set<storm::expressions::Variable>& variables) const override;
virtual bool containsVariables() const;
virtual bool containsVariables() const override;
virtual std::shared_ptr<BaseExpression const> simplify() const override;
virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override;
@ -38,7 +39,7 @@ namespace storm {
virtual void printToStream(std::ostream& stream) const override;
private:
std::shared_ptr<BaseExpression const> size;
std::shared_ptr<BaseExpression const> sizeExpression;
storm::expressions::Variable indexVar;
std::shared_ptr<BaseExpression const> const& elementExpression;
};

6
src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.cpp
View File

@ -6,7 +6,7 @@ namespace storm {
namespace expressions {
template<typename MapType>
boost::any JaniExpressionSubstitutionVisitor<MapType>::visit(ValueArrayExpression const& expression, boost::any const& data) {
uint64_t size = expression.getSize()->evaluateAsInt();
uint64_t size = expression.size()->evaluateAsInt();
std::vector<std::shared_ptr<BaseExpression const>> newElements;
newElements.reserve(size);
for (uint64_t i = 0; i < size; ++i) {
@ -17,12 +17,12 @@ namespace storm {
template<typename MapType>
boost::any JaniExpressionSubstitutionVisitor<MapType>::visit(ConstructorArrayExpression const& expression, boost::any const& data) {
std::shared_ptr<BaseExpression const> newSize = boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getSize()->accept(*this, data));
std::shared_ptr<BaseExpression const> newSize = boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.size()->accept(*this, data));
std::shared_ptr<BaseExpression const> elementExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(expression.getElementExpression()->accept(*this, data));
STORM_LOG_THROW(this->variableToExpressionMapping.find(expression.getIndexVar()) == this->variableToExpressionMapping.end(), storm::exceptions::InvalidArgumentException, "substitution of the index variable of a constructorArrayExpression is not possible.");
// If the arguments did not change, we simply push the expression itself.
if (newSize.get() == expression.getSize().get() && elementExpression.get() == expression.getElementExpression().get()) {
if (newSize.get() == expression.size().get() && elementExpression.get() == expression.getElementExpression().get()) {
return expression.getSharedPointer();
} else {
return std::const_pointer_cast<BaseExpression const>(std::shared_ptr<BaseExpression>(new ConstructorArrayExpression(expression.getManager(), expression.getType(), newSize, expression.getIndexVar(), elementExpression)));

8
src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h
View File

@ -2,12 +2,12 @@
#include "storm/storage/expressions/SubstitutionVisitor.h"
#include "storm/storage/jani/expressions/JaniExpressions.h"
#include "storm/storage/jani/expressions/JaniExpressionVisitor.h"
namespace storm {
namespace expressions {
template<typename MapType>
class JaniExpressionSubstitutionVisitor : public SubstitutionVisitor<MapType>, public ExpressionManager {
class JaniExpressionSubstitutionVisitor : public SubstitutionVisitor<MapType>, public JaniExpressionVisitor {
public:
/*!
* Creates a new substitution visitor that uses the given map to replace variables.
@ -21,6 +21,4 @@ namespace storm {
virtual boost::any visit(ArrayAccessExpression const& expression, boost::any const& data) override;
};
}
}
#endif /* STORM_STORAGE_EXPRESSIONS_SUBSTITUTIONVISITOR_H_ */
}

3
src/storm/storage/jani/expressions/JaniExpressionVisitor.h
View File

@ -6,7 +6,6 @@
namespace storm {
namespace expressions {
template<typename MapType>
class JaniExpressionVisitor{
public:
virtual boost::any visit(ValueArrayExpression const& expression, boost::any const& data) = 0;
@ -15,5 +14,3 @@ namespace storm {
};
}
}
#endif /* STORM_STORAGE_EXPRESSIONS_SUBSTITUTIONVISITOR_H_ */

7
src/storm/storage/jani/expressions/ValueArrayExpression.cpp
View File

@ -1,6 +1,7 @@
#include "storm/storage/jani/expressions/ValueArrayExpression.h"
#include "storm/storage/jani/expressions/JaniExpressionVisitor.h"
#include "storm/storage/expressions/ExpressionManager.h"
#include "storm/exceptions/InvalidArgumentException.h"
#include "storm/exceptions/UnexpectedException.h"
@ -33,7 +34,7 @@ namespace storm {
for (auto const& e : elements) {
simplifiedElements.push_back(e->simplify());
}
return std::shared_ptr<BaseExpression const>(new ValueArrayExpression(manager, type, simplifiedElements));
return std::shared_ptr<BaseExpression const>(new ValueArrayExpression(getManager(), getType(), simplifiedElements));
}
boost::any ValueArrayExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const {
@ -46,7 +47,7 @@ namespace storm {
stream << "array[ ";
bool first = true;
for (auto const& e : elements) {
e->printToStream(stream);
stream << *e;
if (!first) {
stream << " , ";
}
@ -56,7 +57,7 @@ namespace storm {
}
std::shared_ptr<BaseExpression const> ValueArrayExpression::size() const {
return this->manager.integer(elements.size()).getBaseExpressionPointer();
return getManager().integer(elements.size()).getBaseExpressionPointer();
}
std::shared_ptr<BaseExpression const> ValueArrayExpression::at(uint64_t i) const {

4
src/storm/storage/jani/expressions/ValueArrayExpression.h
View File

@ -10,7 +10,7 @@ namespace storm {
class ValueArrayExpression : public ArrayExpression {
public:
ValueArrayExpression(ExpressionManager const& manager, Type const& type, std::vector<std::shared_ptr<BaseExpression const>> elements);
ValueArrayExpression(ExpressionManager const& manager, Type const& type, std::vector<std::shared_ptr<BaseExpression const>> const& elements);
// Instantiate constructors and assignments with their default implementations.
@ -22,7 +22,7 @@ namespace storm {
virtual ~ValueArrayExpression() = default;
virtual void gatherVariables(std::set<storm::expressions::Variable>& variables) const override;
virtual bool containsVariables() const;
virtual bool containsVariables() const override;
virtual std::shared_ptr<BaseExpression const> simplify() const override;
virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override;

56
src/storm/storage/jani/traverser/ArrayEliminator.h
View File

@ -0,0 +1,56 @@
#pragma once
#include <boost/any.hpp>
#include "storm/storage/jani/traverser/JaniTraverser.h"
namespace storm {
namespace jani {
class ArrayEliminator {
/*
public:
void eliminate(Model& model);
private:
class ArrayVariableReplacer : public JaniTraverser {
public:
ArrayVariableReplacer() = default;
virtual ~ArrayVariableReplacer() = default;
std::unordered_map<storm::expressions::Variable, std::vector<reference_wrapper<storm::jani::Variable>> replace();
virtual void traverse(Assignment const& assignment, boost::any const& data) const override;
private:
void std::unordered_map<storm::expressions::Variable, std::size_t>::getMaxSizes(Model& model);
};
};
: public JaniTraverser {
public:
struct ResultType {
bool hasLocationAssignment, hasEdgeAssignment, hasEdgeDestinationAssignment;
};
AssignmentsFinder() = default;
ResultType find(Model const& model, Variable const& variable);
virtual ~AssignmentsFinder() = default;
virtual void traverse(Location const& location, boost::any const& data) const override;
virtual void traverse(TemplateEdge const& templateEdge, boost::any const& data) const override;
virtual void traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data) const override;
*/
};
}
}

8
src/storm/storage/jani/traverser/JaniTraverser.cpp
View File

@ -129,10 +129,16 @@ namespace storm {
traverse(assignment.getAssignedExpression(), data);
}
void JaniTraverser::traverse(LValue const& lValue, boost::any const& data) const {
if (lValue.isArrayAccess()) {
traverse(lValue.getArrayIndex(), data);
}
}
void JaniTraverser::traverse(storm::expressions::Expression const& expression, boost::any const& data) const {
// intentionally left empty.
}
}
}

1
src/storm/storage/jani/traverser/JaniTraverser.h
View File

@ -29,6 +29,7 @@ namespace storm {
virtual void traverse(EdgeDestination const& edgeDestination, boost::any const& data) const;
virtual void traverse(OrderedAssignments const& orderedAssignments, boost::any const& data) const;
virtual void traverse(Assignment const& assignment, boost::any const& data) const;
virtual void traverse(LValue const& lValue, boost::any const& data) const;
virtual void traverse(storm::expressions::Expression const& expression, boost::any const& data) const;
};
}

10
src/storm/storage/prism/ToJaniConverter.cpp
View File

@ -118,7 +118,7 @@ namespace storm {
}
auto newExpressionVariable = manager->declareBooleanVariable(finalLabelName);
storm::jani::BooleanVariable const& newTransientVariable = janiModel.addVariable(storm::jani::BooleanVariable(newExpressionVariable.getName(), newExpressionVariable, manager->boolean(false), true));
transientLocationAssignments.emplace_back(newTransientVariable, label.getStatePredicateExpression());
transientLocationAssignments.emplace_back(storm::jani::LValue(newTransientVariable), label.getStatePredicateExpression());
// Variables that are accessed in the label predicate expression should be made global.
std::set<storm::expressions::Variable> variables = label.getStatePredicateExpression().getVariables();
@ -156,7 +156,7 @@ namespace storm {
transientLocationExpression = rewardTerm;
}
}
transientLocationAssignments.emplace_back(newTransientVariable, transientLocationExpression);
transientLocationAssignments.emplace_back(storm::jani::LValue(newTransientVariable), transientLocationExpression);
// Variables that are accessed in a reward term should be made global.
std::set<storm::expressions::Variable> variables = transientLocationExpression.getVariables();
for (auto const& variable : variables) {
@ -178,9 +178,9 @@ namespace storm {
for (auto const& entry : actionIndexToExpression) {
auto it = transientEdgeAssignments.find(entry.first);
if (it != transientEdgeAssignments.end()) {
it->second.push_back(storm::jani::Assignment(newTransientVariable, entry.second));
it->second.push_back(storm::jani::Assignment(storm::jani::LValue(newTransientVariable), entry.second));
} else {
std::vector<storm::jani::Assignment> assignments = {storm::jani::Assignment(newTransientVariable, entry.second)};
std::vector<storm::jani::Assignment> assignments = {storm::jani::Assignment(storm::jani::LValue(newTransientVariable), entry.second)};
transientEdgeAssignments.emplace(entry.first, assignments);
}
// Variables that are accessed in a reward term should be made global.
@ -275,7 +275,7 @@ namespace storm {
for (auto const& update : command.getUpdates()) {
std::vector<storm::jani::Assignment> assignments;
for (auto const& assignment : update.getAssignments()) {
assignments.push_back(storm::jani::Assignment(variableToVariableMap.at(assignment.getVariable()).get(), assignment.getExpression()));
assignments.push_back(storm::jani::Assignment(storm::jani::LValue(variableToVariableMap.at(assignment.getVariable()).get()), assignment.getExpression()));
}
if (rateExpression) {

Write Preview
Loading…
Cancel
Save