diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp index 7e8397d9d..bd0f1c89c 100644 --- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp +++ b/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; diff --git a/src/storm/parser/JaniParser.cpp b/src/storm/parser/JaniParser.cpp index 4e1bf346d..9836f73d0 100644 --- a/src/storm/parser/JaniParser.cpp +++ b/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(rateExpr) : boost::none, guardExpr, edgeDestinations)); } - - return automaton; } diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 281f8d1de..ab41dd999 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/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() {