From 581b1cc392b4adda744f3710997333bf183d5c21 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@gmail.com>
Date: Wed, 26 Aug 2020 16:56:09 -0700
Subject: [PATCH] convenience operation on prism programs

---
 src/storm/storage/prism/Module.cpp  | 10 ++++++++++
 src/storm/storage/prism/Module.h    |  5 +++++
 src/storm/storage/prism/Program.cpp | 10 +++++++++-
 src/storm/storage/prism/Program.h   |  7 ++++++-
 4 files changed, 30 insertions(+), 2 deletions(-)

diff --git a/src/storm/storage/prism/Module.cpp b/src/storm/storage/prism/Module.cpp
index 4f141e1aa..512985ded 100644
--- a/src/storm/storage/prism/Module.cpp
+++ b/src/storm/storage/prism/Module.cpp
@@ -114,6 +114,16 @@ namespace storm {
         bool Module::hasActionIndex(uint_fast64_t actionIndex) const {
             return this->actionIndicesToCommandIndexMap.find(actionIndex) != this->actionIndicesToCommandIndexMap.end();
         }
+
+        uint64_t Module::getNumberOfUnlabeledCommands() const {
+            uint64_t result = 0;
+            for (auto const& cmd : commands) {
+                if(!cmd.isLabeled()) {
+                    result++;
+                }
+            }
+            return result;
+        }
         
         bool Module::isRenamedFromModule() const {
             return this->renamedFromModule != "";
diff --git a/src/storm/storage/prism/Module.h b/src/storm/storage/prism/Module.h
index 202788816..138dfbe09 100644
--- a/src/storm/storage/prism/Module.h
+++ b/src/storm/storage/prism/Module.h
@@ -263,6 +263,11 @@ namespace storm {
              * Equips all of the modules' variables without initial values with initial values based on their type.
              */
             void createMissingInitialValues();
+
+            /*
+             * Gets the number of commands without a label
+             */
+            uint64_t getNumberOfUnlabeledCommands() const;
             
             /*!
              * Returns true, if an invariant was specified (only relevant for PTA models)
diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp
index dfba08050..cdd41f7c3 100644
--- a/src/storm/storage/prism/Program.cpp
+++ b/src/storm/storage/prism/Program.cpp
@@ -508,7 +508,15 @@ namespace storm {
         std::map<std::string, uint_fast64_t> const& Program::getActionNameToIndexMapping() const {
             return actionToIndexMap;
         }
-        
+
+        uint64_t Program::getNumberOfUnlabeledCommands() const {
+            uint64_t result = 0;
+            for (auto const& m : modules) {
+                result += m.getNumberOfUnlabeledCommands();
+            }
+            return result;
+        }
+
         bool Program::hasInitialConstruct() const {
             return static_cast<bool>(initialConstruct);
         }
diff --git a/src/storm/storage/prism/Program.h b/src/storm/storage/prism/Program.h
index 502cd2a46..0860dd913 100644
--- a/src/storm/storage/prism/Program.h
+++ b/src/storm/storage/prism/Program.h
@@ -462,7 +462,12 @@ namespace storm {
              * @return the index of the module and the (local) index of the found command
              */
             std::pair<uint_fast64_t, uint_fast64_t> getModuleCommandIndexByGlobalCommandIndex(uint_fast64_t globalCommandIndex) const;
-            
+
+            /*
+             * Get total number of unlabeled commands
+             */
+            uint64_t getNumberOfUnlabeledCommands() const;
+
             /*!
              * Retrieves whether the program has reward models.
              *