Silent actions fixed; probability exported correctly.

Former-commit-id: 20ef70c4b3 [formerly 7a4d7ee1d8]
Former-commit-id: 44f344d2a2

src/storage/jani/Action.cpp

@@ -9,6 +9,5 @@ namespace storm {
         std::string const& Action::getName() const {
             return this->name;
         }
-
     }
 }

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;

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);

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.
              */

src/storage/jani/JSONExporter.cpp

@@ -160,7 +160,13 @@ namespace storm {
         
         modernjson::json buildActionArray(std::vector<storm::jani::Action> const& actions) {
             std::vector<modernjson::json> 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());
                 }

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 {

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<uint64_t> nonsilentActionIndices;
             
-            /// The index of the silent action.
-            uint64_t silentActionIndex;
-            
             /// The constants defined by the model.
             std::vector<Constant> constants;