diff --git a/src/storage/jani/Action.cpp b/src/storage/jani/Action.cpp index 818a11a84..da1d652eb 100644 --- a/src/storage/jani/Action.cpp +++ b/src/storage/jani/Action.cpp @@ -9,6 +9,5 @@ namespace storm { std::string const& Action::getName() const { return this->name; } - } } \ No newline at end of file diff --git a/src/storage/jani/Action.h b/src/storage/jani/Action.h index 5b9b2567f..aa264c4b5 100644 --- a/src/storage/jani/Action.h +++ b/src/storage/jani/Action.h @@ -15,7 +15,6 @@ namespace storm { * Returns the name of the location. */ std::string const& getName() const; - private: /// The name of the action. std::string name; diff --git a/src/storage/jani/Edge.cpp b/src/storage/jani/Edge.cpp index cc63283ec..b0a7ef943 100644 --- a/src/storage/jani/Edge.cpp +++ b/src/storage/jani/Edge.cpp @@ -79,6 +79,10 @@ namespace storm { } } + bool Edge::hasSilentAction() const { + return actionIndex == Model::silentActionIndex; + } + bool Edge::addTransientAssignment(Assignment const& assignment) { STORM_LOG_THROW(assignment.isTransient(), storm::exceptions::InvalidArgumentException, "Must not add non-transient assignment to location."); return assignments.add(assignment); diff --git a/src/storage/jani/Edge.h b/src/storage/jani/Edge.h index 6ce6ef127..828f992a3 100644 --- a/src/storage/jani/Edge.h +++ b/src/storage/jani/Edge.h @@ -25,6 +25,11 @@ namespace storm { */ uint64_t getActionIndex() const; + /*! + * Returns whether it contains the silent action. + */ + bool hasSilentAction() const; + /*! * Retrieves whether this edge has an associated rate. */ diff --git a/src/storage/jani/JSONExporter.cpp b/src/storage/jani/JSONExporter.cpp index a45519ed9..14813a38a 100644 --- a/src/storage/jani/JSONExporter.cpp +++ b/src/storage/jani/JSONExporter.cpp @@ -160,7 +160,13 @@ namespace storm { modernjson::json buildActionArray(std::vector const& actions) { std::vector actionReprs; + uint64_t actIndex = 0; for(auto const& act : actions) { + if(actIndex == storm::jani::Model::silentActionIndex) { + actIndex++; + continue; + } + actIndex++; modernjson::json actEntry; actEntry["name"] = act.getName(); actionReprs.push_back(actEntry); @@ -270,7 +276,7 @@ namespace storm { for(auto const& destination : destinations) { modernjson::json destEntry; destEntry["location"] = locationNames.at(destination.getLocationIndex()); - destEntry["probability"] = buildExpression(destination.getProbability()); + destEntry["probability"]["exp"] = buildExpression(destination.getProbability()); destEntry["assignments"] = buildAssignmentArray(destination.getOrderedAssignments()); destDeclarations.push_back(destEntry); } @@ -282,10 +288,9 @@ namespace storm { for(auto const& edge : edges) { modernjson::json edgeEntry; edgeEntry["location"] = locationNames.at(edge.getSourceLocationIndex()); - // TODO silent action - //if(edge.nonSilentAction()) { - edgeEntry["action"] = actionNames.at(edge.getActionIndex()); - //} + if(!edge.hasSilentAction()) { + edgeEntry["action"] = actionNames.at(edge.getActionIndex()); + } if(edge.hasRate()) { edgeEntry["rate"]["exp"] = buildExpression(edge.getRate()); } diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp index 619324ae7..668e54528 100644 --- a/src/storage/jani/Model.cpp +++ b/src/storage/jani/Model.cpp @@ -14,6 +14,7 @@ namespace storm { namespace jani { static const std::string SILENT_ACTION_NAME = ""; + const uint64_t Model::silentActionIndex = 0; Model::Model() { // Intentionally left empty. @@ -31,7 +32,8 @@ namespace storm { initialStatesRestriction = this->expressionManager->boolean(true); // Add a prefined action that represents the silent action. - silentActionIndex = addAction(storm::jani::Action(SILENT_ACTION_NAME)); + uint64_t actionIndex = addAction(storm::jani::Action(SILENT_ACTION_NAME)); + assert(actionIndex == silentActionIndex); } storm::expressions::ExpressionManager& Model::getManager() const { diff --git a/src/storage/jani/Model.h b/src/storage/jani/Model.h index bade96875..b4f42a87c 100644 --- a/src/storage/jani/Model.h +++ b/src/storage/jani/Model.h @@ -17,8 +17,12 @@ namespace storm { class Exporter; + + class Model { public: + static const uint64_t silentActionIndex; + friend class Exporter; /*! @@ -348,9 +352,6 @@ namespace storm { /// The set of non-silent action indices. boost::container::flat_set nonsilentActionIndices; - /// The index of the silent action. - uint64_t silentActionIndex; - /// The constants defined by the model. std::vector constants;