From f45b56e72566e3b4727c61218834f374448a91e1 Mon Sep 17 00:00:00 2001 From: Sebastian Junges 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 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(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 getModuleCommandIndexByGlobalCommandIndex(uint_fast64_t globalCommandIndex) const; - + + /* + * Get total number of unlabeled commands + */ + uint64_t getNumberOfUnlabeledCommands() const; + /*! * Retrieves whether the program has reward models. *