Browse Source

some more fixes to jit model builder

tempestpy_adaptions
dehnert 8 years ago
parent
commit
a6beda6a82
  1. 12
      src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
  2. 4
      src/storm/parser/JaniParser.cpp
  3. 2
      src/storm/storage/jani/Model.cpp

12
src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp

@ -1322,7 +1322,11 @@ namespace storm {
++destinationIndex;
}
edgeData["guard"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(edge.getGuard()) && getLocationVariable(automaton) == model.getManager().integer(edge.getSourceLocationIndex()), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName));
if (automaton.getNumberOfLocations() > 1) {
edgeData["guard"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(edge.getGuard()) && getLocationVariable(automaton) == model.getManager().integer(edge.getSourceLocationIndex()), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName));
} else {
edgeData["guard"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(edge.getGuard()), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName));
}
edgeData["destinations"] = cpptempl::make_data(destinations);
edgeData["name"] = automaton.getName() + "_" + std::to_string(edgeIndex);
edgeData["transient_assignments"] = cpptempl::make_data(edgeAssignments);
@ -1399,12 +1403,14 @@ namespace storm {
// Close the last (open) level.
cpptempl::data_map level;
nonTransientAssignmentData.push_back(generateLocationAssignment(automaton, destinationLocationIndex));
if (automaton.getNumberOfLocations() > 1) {
nonTransientAssignmentData.push_back(generateLocationAssignment(automaton, destinationLocationIndex));
}
level["non_transient_assignments"] = cpptempl::make_data(nonTransientAssignmentData);
level["transient_assignments"] = cpptempl::make_data(transientAssignmentData);
level["index"] = asString(currentLevel);
levels.push_back(level);
} else {
} else if (automaton.getNumberOfLocations() > 1) {
// Create (an otherwise) empty level to perform the location assignment.
cpptempl::data_map level;
cpptempl::data_list nonTransientAssignmentData;

4
src/storm/parser/JaniParser.cpp

@ -1013,7 +1013,7 @@ namespace storm {
STORM_LOG_THROW(locIds.count(sourceLoc) == 1, storm::exceptions::InvalidJaniException, "Source of edge has unknown location '" << sourceLoc << "' in automaton '" << name << "'.");
// action
STORM_LOG_THROW(edgeEntry.count("action") < 2, storm::exceptions::InvalidJaniException, "Edge from " << sourceLoc << " in automaton " << name << " has multiple actions");
std::string action = ""; // def is tau
std::string action = storm::jani::Model::SILENT_ACTION_NAME; // def is tau
if(edgeEntry.count("action") > 0) {
action = getString(edgeEntry.at("action"), "action name in edge from '" + sourceLoc + "' in automaton '" + name + "'");
// TODO check if action is known
@ -1077,8 +1077,6 @@ namespace storm {
automaton.addEdge(storm::jani::Edge(locIds.at(sourceLoc), parentModel.getActionIndex(action), rateExpr.isInitialized() ? boost::optional<storm::expressions::Expression>(rateExpr) : boost::none, guardExpr, edgeDestinations));
}
return automaton;
}

2
src/storm/storage/jani/Model.cpp

@ -14,7 +14,7 @@
namespace storm {
namespace jani {
const std::string Model::SILENT_ACTION_NAME = "";
const std::string Model::SILENT_ACTION_NAME = "__SILENT_ACTION__";
const uint64_t Model::SILENT_ACTION_INDEX = 0;
Model::Model() {

Loading…
Cancel
Save