Browse Source

Fixed parsing of edge assignments.

tempestpy_adaptions
TimQu 6 years ago
parent
commit
602d18d844
  1. 22
      src/storm-parsers/parser/JaniParser.cpp

22
src/storm-parsers/parser/JaniParser.cpp

@ -1447,9 +1447,29 @@ namespace storm {
STORM_LOG_THROW(guardExpr.hasBooleanType(), storm::exceptions::InvalidJaniException, "Guard " << guardExpr << " does not have Boolean type."); STORM_LOG_THROW(guardExpr.hasBooleanType(), storm::exceptions::InvalidJaniException, "Guard " << guardExpr << " does not have Boolean type.");
} }
assert(guardExpr.isInitialized()); assert(guardExpr.isInitialized());
std::shared_ptr<storm::jani::TemplateEdge> templateEdge = std::make_shared<storm::jani::TemplateEdge>(guardExpr); std::shared_ptr<storm::jani::TemplateEdge> templateEdge = std::make_shared<storm::jani::TemplateEdge>(guardExpr);
// edge assignments
if (edgeEntry.count("assignments") > 0) {
STORM_LOG_THROW(edgeEntry.count("assignments") == 1, storm::exceptions::InvalidJaniException, "Multiple edge assignments in edge from '" + sourceLoc + "' in automaton '" + name + "'.");
for (auto const& assignmentEntry : edgeEntry.at("assignments")) {
// ref
STORM_LOG_THROW(assignmentEntry.count("ref") == 1, storm::exceptions::InvalidJaniException, "Assignment in edge from '" << sourceLoc << "' in automaton '" << name << "' must have one ref field");
storm::jani::LValue lValue = parseLValue(assignmentEntry.at("ref"), scope.refine("Assignment variable in edge from '" + sourceLoc + "' in automaton '" + name + "'"));
// value
STORM_LOG_THROW(assignmentEntry.count("value") == 1, storm::exceptions::InvalidJaniException, "Assignment in edge from '" << sourceLoc << "' in automaton '" << name << "' must have one value field");
storm::expressions::Expression assignmentExpr = parseExpression(assignmentEntry.at("value"), scope.refine("assignment in edge from '" + sourceLoc + "' in automaton '" + name + "'"));
// TODO check types
// index
int64_t assignmentIndex = 0; // default.
if(assignmentEntry.count("index") > 0) {
assignmentIndex = getSignedInt(assignmentEntry.at("index"), "assignment index in edge from '" + sourceLoc + "' in automaton '" + name + "'");
}
templateEdge->getAssignments().add(storm::jani::Assignment(lValue, assignmentExpr, assignmentIndex));
}
}
// destinations
STORM_LOG_THROW(edgeEntry.count("destinations") == 1, storm::exceptions::InvalidJaniException, "A single list of destinations must be given in edge from '" << sourceLoc << "' in automaton '" << name << "'"); STORM_LOG_THROW(edgeEntry.count("destinations") == 1, storm::exceptions::InvalidJaniException, "A single list of destinations must be given in edge from '" << sourceLoc << "' in automaton '" << name << "'");
std::vector<std::pair<uint64_t, storm::expressions::Expression>> destinationLocationsAndProbabilities; std::vector<std::pair<uint64_t, storm::expressions::Expression>> destinationLocationsAndProbabilities;
for(auto const& destEntry : edgeEntry.at("destinations")) { for(auto const& destEntry : edgeEntry.at("destinations")) {

Loading…
Cancel
Save