Browse Source

convenience operation on prism programs

tempestpy_adaptions
Sebastian Junges 4 years ago
parent
commit
f45b56e725
  1. 10
      src/storm/storage/prism/Module.cpp
  2. 5
      src/storm/storage/prism/Module.h
  3. 10
      src/storm/storage/prism/Program.cpp
  4. 7
      src/storm/storage/prism/Program.h

10
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 != "";

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

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

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

Loading…
Cancel
Save