From d5535b19bed9471a7a47f26e3ff49b441b0bf686 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 21 Nov 2016 16:26:38 +0100 Subject: [PATCH] reverted changing silent action name as JANI identifiers need to be non-empty --- src/storm/storage/jani/Edge.h | 2 ++ src/storm/storage/jani/Model.cpp | 2 +- src/storm/storage/prism/ToJaniConverter.cpp | 7 ++++++- 3 files changed, 9 insertions(+), 2 deletions(-) diff --git a/src/storm/storage/jani/Edge.h b/src/storm/storage/jani/Edge.h index a61c2b7bd..212e7656f 100644 --- a/src/storm/storage/jani/Edge.h +++ b/src/storm/storage/jani/Edge.h @@ -13,6 +13,8 @@ namespace storm { class Edge { public: + Edge() = default; + Edge(uint64_t sourceLocationIndex, uint64_t actionIndex, boost::optional const& rate, storm::expressions::Expression const& guard, std::vector destinations = {}); /*! diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index ab41dd999..281f8d1de 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 = "__SILENT_ACTION__"; + const std::string Model::SILENT_ACTION_NAME = ""; const uint64_t Model::SILENT_ACTION_INDEX = 0; Model::Model() { diff --git a/src/storm/storage/prism/ToJaniConverter.cpp b/src/storm/storage/prism/ToJaniConverter.cpp index 9d466d87d..4cc2ed78a 100644 --- a/src/storm/storage/prism/ToJaniConverter.cpp +++ b/src/storm/storage/prism/ToJaniConverter.cpp @@ -216,7 +216,12 @@ namespace storm { } // Create the edge object so we can add transient assignments. - storm::jani::Edge newEdge(onlyLocationIndex, janiModel.getActionIndex(command.getActionName()), rateExpression, command.getGuardExpression(), destinations); + storm::jani::Edge newEdge; + if (command.getActionName().empty()) { + newEdge = storm::jani::Edge(onlyLocationIndex, storm::jani::Model::SILENT_ACTION_INDEX, rateExpression, command.getGuardExpression(), destinations); + } else { + newEdge = storm::jani::Edge(onlyLocationIndex, janiModel.getActionIndex(command.getActionName()), rateExpression, command.getGuardExpression(), destinations); + } // Then add the transient assignments for the rewards. Note that we may do this only for the first // module that has this action, so we remove the assignments from the global list of assignments