diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index d3bb66863..59b17f563 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -9,7 +9,7 @@ #include "src/storage/jani/Model.h" #include "src/storage/jani/AutomatonComposition.h" #include "src/storage/jani/ParallelComposition.h" -#include "src/storage/jani/CompositionActionInformationVisitor.h" +#include "src/storage/jani/CompositionInformationVisitor.h" #include "src/storage/dd/Add.h" #include "src/storage/dd/Bdd.h" @@ -177,7 +177,7 @@ namespace storm { template class CompositionVariableCreator : public storm::jani::CompositionVisitor { public: - CompositionVariableCreator(storm::jani::Model const& model, storm::jani::ActionInformation const& actionInformation) : model(model), automata(), actionInformation(actionInformation) { + CompositionVariableCreator(storm::jani::Model const& model, storm::jani::CompositionInformation const& actionInformation) : model(model), automata(), actionInformation(actionInformation) { // Intentionally left empty. } @@ -356,7 +356,7 @@ namespace storm { storm::jani::Model const& model; std::set automata; - storm::jani::ActionInformation actionInformation; + storm::jani::CompositionInformation actionInformation; }; template @@ -612,18 +612,18 @@ namespace storm { }; - CombinedEdgesSystemComposer(storm::jani::Model const& model, storm::jani::ActionInformation const& actionInformation, CompositionVariables const& variables, std::vector const& transientVariables) : SystemComposer(model, variables, transientVariables), actionInformation(actionInformation) { + CombinedEdgesSystemComposer(storm::jani::Model const& model, storm::jani::CompositionInformation const& actionInformation, CompositionVariables const& variables, std::vector const& transientVariables) : SystemComposer(model, variables, transientVariables), actionInformation(actionInformation) { // Intentionally left empty. } - storm::jani::ActionInformation const& actionInformation; + storm::jani::CompositionInformation const& actionInformation; ComposerResult compose() override { std::map actionIndexToLocalNondeterminismVariableOffset; for (auto const& actionIndex : actionInformation.getNonSilentActionIndices()) { actionIndexToLocalNondeterminismVariableOffset[actionIndex] = 0; } - actionIndexToLocalNondeterminismVariableOffset[actionInformation.getSilentActionIndex()] = 0; + actionIndexToLocalNondeterminismVariableOffset[storm::jani::Model::getSilentActionIndex()] = 0; AutomatonDd globalAutomaton = boost::any_cast(this->model.getSystemComposition().accept(*this, actionIndexToLocalNondeterminismVariableOffset)); return buildSystemFromAutomaton(globalAutomaton); @@ -1659,8 +1659,8 @@ namespace storm { } // Determine the actions that will appear in the parallel composition. - storm::jani::CompositionActionInformationVisitor actionInformationVisitor(model); - storm::jani::ActionInformation actionInformation = actionInformationVisitor.getActionInformation(model.getSystemComposition()); + storm::jani::CompositionInformationVisitor visitor(model, model.getSystemComposition()); + storm::jani::CompositionInformation actionInformation = visitor.getInformation(); // Create all necessary variables. CompositionVariableCreator variableCreator(model, actionInformation); diff --git a/src/storage/jani/CompositionActionInformationVisitor.cpp b/src/storage/jani/CompositionActionInformationVisitor.cpp deleted file mode 100644 index 5b6f42a6f..000000000 --- a/src/storage/jani/CompositionActionInformationVisitor.cpp +++ /dev/null @@ -1,123 +0,0 @@ -#include "src/storage/jani/CompositionActionInformationVisitor.h" - -#include "src/storage/jani/Model.h" -#include "src/storage/jani/Compositions.h" - -namespace storm { - namespace jani { - - ActionInformation::ActionInformation(std::set const& nonsilentActionIndices, std::map const& indexToNameMap, std::map const& nameToIndexMap, uint64_t silentActionIndex) : silentActionIndex(silentActionIndex), nonsilentActionIndices(nonsilentActionIndices), indexToNameMap(indexToNameMap), nameToIndexMap(nameToIndexMap) { - // Intentionally left empty. - } - - std::string const& ActionInformation::getActionName(uint64_t index) const { - return indexToNameMap.at(index); - } - - uint64_t ActionInformation::getActionIndex(std::string const& name) const { - return nameToIndexMap.at(name); - } - - std::set const& ActionInformation::getNonSilentActionIndices() const { - return nonsilentActionIndices; - } - - uint64_t ActionInformation::getSilentActionIndex() const { - return silentActionIndex; - } - - CompositionActionInformationVisitor::CompositionActionInformationVisitor(storm::jani::Model const& model) : model(model), nextFreeActionIndex(0), nameToIndexMap(), indexToNameMap() { - // Intentionally left empty. - } - - ActionInformation CompositionActionInformationVisitor::getActionInformation(storm::jani::Composition const& composition) { - indexToNameMap.clear(); - nameToIndexMap.clear(); - - // Determine the next free index we can give out to a new action. - for (auto const& action : model.getActions()) { - uint64_t actionIndex = model.getActionIndex(action.getName()); - - nameToIndexMap[action.getName()] = model.getActionIndex(action.getName()); - indexToNameMap[actionIndex] = action.getName(); - - nextFreeActionIndex = std::max(nextFreeActionIndex, model.getActionIndex(action.getName())); - } - ++nextFreeActionIndex; - - std::set nonSilentActionIndices = boost::any_cast>(composition.accept(*this, boost::none)); - - return ActionInformation(nonSilentActionIndices, indexToNameMap, nameToIndexMap); - } - - boost::any CompositionActionInformationVisitor::visit(AutomatonComposition const& composition, boost::any const& data) { - std::set result = model.getAutomaton(composition.getAutomatonName()).getActionIndices(); - result.erase(model.getSilentActionIndex()); - return result; - } - - boost::any CompositionActionInformationVisitor::visit(ParallelComposition const& composition, boost::any const& data) { - std::vector> subresults; - for (auto const& subcomposition : composition.getSubcompositions()) { - subresults.push_back(boost::any_cast>(subcomposition->accept(*this, boost::none))); - } - - std::set effectiveSynchronizationVectors; - for (uint64_t index = 0; index < composition.getNumberOfSynchronizationVectors(); ++index) { - effectiveSynchronizationVectors.insert(index); - } - - // Determine all actions that do not take part in synchronization vectors. - std::set result; - for (uint64_t subresultIndex = 0; subresultIndex < subresults.size(); ++subresultIndex) { - std::set actionsInSynch; - std::set localEffectiveSynchVectors; - for (uint64_t synchVectorIndex = 0; synchVectorIndex < composition.getNumberOfSynchronizationVectors(); ++synchVectorIndex) { - auto const& synchVector = composition.getSynchronizationVector(synchVectorIndex); - - if (synchVector.isNoActionInput(synchVector.getInput(subresultIndex))) { - effectiveSynchronizationVectors.insert(synchVectorIndex); - } else { - uint64_t synchVectorActionIndex = nameToIndexMap.at(synchVector.getInput(subresultIndex)); - actionsInSynch.insert(synchVectorActionIndex); - - // If the action of they synchronization vector at this position is one that is actually contained - // in the corresponding subcomposition, the synchronization vector is effective. - if (subresults[subresultIndex].find(synchVectorActionIndex) != subresults[subresultIndex].end()) { - effectiveSynchronizationVectors.insert(synchVectorIndex); - } - } - } - - std::set_difference(subresults[subresultIndex].begin(), subresults[subresultIndex].end(), actionsInSynch.begin(), actionsInSynch.end(), std::inserter(result, result.begin())); - - // Intersect the previously effective synchronization vectors with the ones that were derived to be - // effective for the current subcomposition. - std::set newEffectiveSynchVectors; - std::set_intersection(effectiveSynchronizationVectors.begin(), effectiveSynchronizationVectors.end(), newEffectiveSynchVectors.begin(), newEffectiveSynchVectors.end(), std::inserter(newEffectiveSynchVectors, newEffectiveSynchVectors.begin())); - effectiveSynchronizationVectors = std::move(newEffectiveSynchVectors); - } - - // Now add all outputs of synchronization vectors. - for (auto const& synchVector : composition.getSynchronizationVectors()) { - if (synchVector.getOutput() != storm::jani::Model::getSilentActionName()) { - result.insert(addOrGetActionIndex(synchVector.getOutput())); - } - } - - return result; - } - - uint64_t CompositionActionInformationVisitor::addOrGetActionIndex(std::string const& name) { - auto it = nameToIndexMap.find(name); - if (it != nameToIndexMap.end()) { - return it->second; - } else { - nameToIndexMap[name] = nextFreeActionIndex; - indexToNameMap[nextFreeActionIndex] = name; - return nextFreeActionIndex++; - } - } - - } -} diff --git a/src/storage/jani/CompositionActionInformationVisitor.h b/src/storage/jani/CompositionActionInformationVisitor.h deleted file mode 100644 index 572d481d7..000000000 --- a/src/storage/jani/CompositionActionInformationVisitor.h +++ /dev/null @@ -1,49 +0,0 @@ -#pragma once - -#include -#include - -#include "src/storage/jani/CompositionVisitor.h" - -namespace storm { - namespace jani { - - class Model; - - class ActionInformation { - public: - ActionInformation(std::set const& nonsilentActionIndices, std::map const& indexToNameMap, std::map const& nameToIndexMap, uint64_t silentActionIndex = 0); - - std::string const& getActionName(uint64_t index) const; - uint64_t getActionIndex(std::string const& name) const; - std::set const& getNonSilentActionIndices() const; - uint64_t getSilentActionIndex() const; - - private: - uint64_t silentActionIndex; - std::set nonsilentActionIndices; - std::map indexToNameMap; - std::map nameToIndexMap; - }; - - class CompositionActionInformationVisitor : public CompositionVisitor { - public: - CompositionActionInformationVisitor(storm::jani::Model const& model); - - ActionInformation getActionInformation(storm::jani::Composition const& composition); - - virtual boost::any visit(AutomatonComposition const& composition, boost::any const& data) override; - virtual boost::any visit(ParallelComposition const& composition, boost::any const& data) override; - - private: - uint64_t addOrGetActionIndex(std::string const& name); - - storm::jani::Model const& model; - uint64_t nextFreeActionIndex; - std::map nameToIndexMap; - std::map indexToNameMap; - }; - - - } -} diff --git a/src/storage/jani/CompositionInformationVisitor.cpp b/src/storage/jani/CompositionInformationVisitor.cpp index 6c65e9613..6926a096d 100644 --- a/src/storage/jani/CompositionInformationVisitor.cpp +++ b/src/storage/jani/CompositionInformationVisitor.cpp @@ -3,53 +3,100 @@ #include "src/storage/jani/Model.h" #include "src/storage/jani/Compositions.h" +#include "src/utility/macros.h" +#include "src/exceptions/WrongFormatException.h" + namespace storm { namespace jani { - CompositionInformation::CompositionInformation() : automatonNameToMultiplicity(), nonsilentActions(), nonStandardParallelComposition(false) { - // Intentionally left empty. - } - - CompositionInformation::CompositionInformation(std::map const& automatonNameToMultiplicity, std::set const& nonsilentActions, bool nonStandardParallelComposition) : automatonNameToMultiplicity(automatonNameToMultiplicity), nonsilentActions(nonsilentActions), nonStandardParallelComposition(nonStandardParallelComposition) { + CompositionInformation::CompositionInformation() : nonStandardParallelComposition(false) { // Intentionally left empty. } void CompositionInformation::increaseAutomatonMultiplicity(std::string const& automatonName, uint64_t count) { automatonNameToMultiplicity[automatonName] += count; } - - void CompositionInformation::addNonsilentAction(std::string const& actionName) { - nonsilentActions.insert(actionName); + + std::map const& CompositionInformation::getAutomatonToMultiplicityMap() const { + return automatonNameToMultiplicity; + } + + void CompositionInformation::addMultiplicityMap(std::map const& multiplicityMap) { + automatonNameToMultiplicity = joinMultiplicityMaps(automatonNameToMultiplicity, multiplicityMap); } - std::set const& CompositionInformation::getNonsilentActions() const { - return nonsilentActions; + std::map CompositionInformation::joinMultiplicityMaps(std::map const& first, std::map const& second) { + std::map result = first; + for (auto const& element : second) { + result[element.first] += element.second; + } + return result; } - void CompositionInformation::setContainsNonStandardParallelComposition() { - nonStandardParallelComposition = true; + void CompositionInformation::setContainsNonStandardParallelComposition(bool value) { + nonStandardParallelComposition = value; } bool CompositionInformation::containsNonStandardParallelComposition() const { return nonStandardParallelComposition; } - std::map CompositionInformation::joinMultiplicityMaps(std::map const& first, std::map const& second) { - std::map result = first; - for (auto const& element : second) { - result[element.first] += element.second; - } - return result; + std::string const& CompositionInformation::getActionName(uint64_t index) const { + return indexToNameMap.at(index); } - std::map const& CompositionInformation::getAutomatonToMultiplicityMap() const { - return automatonNameToMultiplicity; + uint64_t CompositionInformation::getActionIndex(std::string const& name) const { + return nameToIndexMap.at(name); + } + + void CompositionInformation::addNonSilentActionIndex(uint64_t index) { + nonSilentActionIndices.insert(index); } - CompositionInformation CompositionInformationVisitor::getInformation(Composition const& composition, Model const& model) { - return boost::any_cast(composition.accept(*this, model)); + void CompositionInformation::addNonSilentActionIndices(std::set const& indices) { + nonSilentActionIndices.insert(indices.begin(), indices.end()); } + bool CompositionInformation::hasNonSilentActionIndex(uint64_t index) { + return nonSilentActionIndices.find(index) != nonSilentActionIndices.end(); + } + + void CompositionInformation::addInputEnabledActionIndex(uint64_t index) { + inputEnabledActionIndices.insert(index); + } + + std::set const& CompositionInformation::getNonSilentActionIndices() const { + return nonSilentActionIndices; + } + + std::set const& CompositionInformation::getInputEnabledActionIndices() const { + return inputEnabledActionIndices; + } + + void CompositionInformation::setMappings(std::map const& indexToNameMap, std::map const& nameToIndexMap) { + this->indexToNameMap = indexToNameMap; + this->nameToIndexMap = nameToIndexMap; + } + + CompositionInformationVisitor::CompositionInformationVisitor(Model const& model, Composition const& composition) : model(model), composition(composition), nextFreeActionIndex(0) { + // Determine the next free index we can give out to a new action. + for (auto const& action : model.getActions()) { + uint64_t actionIndex = model.getActionIndex(action.getName()); + + nameToIndexMap[action.getName()] = model.getActionIndex(action.getName()); + indexToNameMap[actionIndex] = action.getName(); + + nextFreeActionIndex = std::max(nextFreeActionIndex, model.getActionIndex(action.getName())); + } + ++nextFreeActionIndex; + } + + CompositionInformation CompositionInformationVisitor::getInformation() { + CompositionInformation result = boost::any_cast(composition.accept(*this, model)); + result.setMappings(indexToNameMap, nameToIndexMap); + return result; + } + boost::any CompositionInformationVisitor::visit(AutomatonComposition const& composition, boost::any const& data) { Model const& model = boost::any_cast(data); Automaton const& automaton = model.getAutomaton(composition.getAutomatonName()); @@ -58,27 +105,35 @@ namespace storm { result.increaseAutomatonMultiplicity(composition.getAutomatonName()); for (auto const& actionIndex : automaton.getActionIndices()) { if (actionIndex != model.getSilentActionIndex()) { - result.addNonsilentAction(model.getAction(actionIndex).getName()); + result.addNonSilentActionIndex(actionIndex); } } + for (auto const& action : composition.getInputEnabledActions()) { + auto it = nameToIndexMap.find(action); + STORM_LOG_THROW(it != nameToIndexMap.end(), storm::exceptions::WrongFormatException, "Illegal action name '" << action << "' in when input-enabling automaton '" << composition.getAutomatonName() << "'."); + uint64_t actionIndex = it->second; + STORM_LOG_THROW(result.hasNonSilentActionIndex(actionIndex), storm::exceptions::WrongFormatException, "Cannot make automaton '" << composition.getAutomatonName() << "' input enabled for action " << action << ", because it has no such action."); + result.addInputEnabledActionIndex(actionIndex); + } return result; } boost::any CompositionInformationVisitor::visit(ParallelComposition const& composition, boost::any const& data) { + CompositionInformation result; + std::vector subinformation; - std::set nonsilentSubActions; + std::set nonsilentSubActionIndices; for (auto const& subcomposition : composition.getSubcompositions()) { subinformation.push_back(boost::any_cast(subcomposition->accept(*this, data))); - nonsilentSubActions.insert(subinformation.back().getNonsilentActions().begin(), subinformation.back().getNonsilentActions().end()); + nonsilentSubActionIndices.insert(subinformation.back().getNonSilentActionIndices().begin(), subinformation.back().getNonSilentActionIndices().end()); } - std::map joinedAutomatonToMultiplicityMap; bool containsNonStandardParallelComposition = false; for (auto const& subinfo : subinformation) { containsNonStandardParallelComposition |= subinfo.containsNonStandardParallelComposition(); - joinedAutomatonToMultiplicityMap = CompositionInformation::joinMultiplicityMaps(joinedAutomatonToMultiplicityMap, subinfo.getAutomatonToMultiplicityMap()); + result.addMultiplicityMap(subinfo.getAutomatonToMultiplicityMap()); } // Keep track of the synchronization vectors that are effective, meaning that the subcompositions all have @@ -89,7 +144,7 @@ namespace storm { } // Now compute non-silent actions. - std::set nonsilentActions; + std::set nonSilentActionIndices; for (uint_fast64_t infoIndex = 0; infoIndex < subinformation.size(); ++infoIndex) { auto const& subinfo = subinformation[infoIndex]; @@ -98,10 +153,11 @@ namespace storm { for (uint64_t synchVectorIndex = 0; synchVectorIndex < composition.getNumberOfSynchronizationVectors(); ++synchVectorIndex) { auto const& synchVector = composition.getSynchronizationVector(synchVectorIndex); if (synchVector.getInput(infoIndex) != SynchronizationVector::getNoActionInput()) { - for (auto const& nonsilentAction : subinfo.getNonsilentActions()) { - if (synchVector.getInput(infoIndex) == nonsilentAction) { + for (auto const& nonsilentActionIndex : subinfo.getNonSilentActionIndices()) { + std::string const& nonSilentAction = indexToNameMap.at(nonsilentActionIndex); + if (synchVector.getInput(infoIndex) == nonSilentAction) { enabledSynchVectors.insert(synchVectorIndex); - actionsInSynch.insert(nonsilentAction); + actionsInSynch.insert(nonSilentAction); } } } else { @@ -109,7 +165,7 @@ namespace storm { } } - std::set_difference(subinfo.getNonsilentActions().begin(), subinfo.getNonsilentActions().end(), actionsInSynch.begin(), actionsInSynch.end(), std::inserter(nonsilentActions, nonsilentActions.begin())); + std::set_difference(subinfo.getNonSilentActionIndices().begin(), subinfo.getNonSilentActionIndices().end(), actionsInSynch.begin(), actionsInSynch.end(), std::inserter(nonSilentActionIndices, nonSilentActionIndices.begin())); std::set newEffectiveSynchVectors; std::set_intersection(effectiveSynchVectors.begin(), effectiveSynchVectors.end(), enabledSynchVectors.begin(), enabledSynchVectors.end(), std::inserter(newEffectiveSynchVectors, newEffectiveSynchVectors.begin())); @@ -128,19 +184,20 @@ namespace storm { // Construct the set of expected synchronization vectors. std::set expectedSynchVectorSetUnderApprox; std::set expectedSynchVectorSetOverApprox; - for (auto action : nonsilentSubActions) { + for (auto actionIndex : nonsilentSubActionIndices) { + std::string const& actionName = indexToNameMap.at(actionIndex); std::vector input; uint64_t numberOfParticipatingAutomata = 0; for (auto const& subcomposition : subinformation) { - if (subcomposition.getNonsilentActions().find(action) != subcomposition.getNonsilentActions().end()) { - input.push_back(action); + if (subcomposition.getNonSilentActionIndices().find(actionIndex) != subcomposition.getNonSilentActionIndices().end()) { + input.push_back(actionName); ++numberOfParticipatingAutomata; } else { input.push_back(SynchronizationVector::getNoActionInput()); } } - storm::jani::SynchronizationVector newSynchVector(input, action); + storm::jani::SynchronizationVector newSynchVector(input, actionName); expectedSynchVectorSetOverApprox.insert(newSynchVector); if (numberOfParticipatingAutomata > 1) { expectedSynchVectorSetUnderApprox.insert(newSynchVector); @@ -151,7 +208,21 @@ namespace storm { containsNonStandardParallelComposition |= !std::includes(synchVectorSet.begin(), synchVectorSet.end(), expectedSynchVectorSetUnderApprox.begin(), expectedSynchVectorSetUnderApprox.end(), SynchronizationVectorLexicographicalLess()); - return CompositionInformation(joinedAutomatonToMultiplicityMap, nonsilentActions, containsNonStandardParallelComposition); + result.setContainsNonStandardParallelComposition(containsNonStandardParallelComposition); + + result.addNonSilentActionIndices(nonSilentActionIndices); + return result; + } + + uint64_t CompositionInformationVisitor::addOrGetActionIndex(std::string const& name) { + auto it = nameToIndexMap.find(name); + if (it != nameToIndexMap.end()) { + return it->second; + } else { + nameToIndexMap[name] = nextFreeActionIndex; + indexToNameMap[nextFreeActionIndex] = name; + return nextFreeActionIndex++; + } } } diff --git a/src/storage/jani/CompositionInformationVisitor.h b/src/storage/jani/CompositionInformationVisitor.h index 804fa3ba0..7dfcb5a56 100644 --- a/src/storage/jani/CompositionInformationVisitor.h +++ b/src/storage/jani/CompositionInformationVisitor.h @@ -16,38 +16,65 @@ namespace storm { class CompositionInformation { public: CompositionInformation(); - CompositionInformation(std::map const& automatonNameToMultiplicity, std::set const& nonsilentActions, bool nonStandardParallelComposition); void increaseAutomatonMultiplicity(std::string const& automatonName, uint64_t count = 1); + std::map const& getAutomatonToMultiplicityMap() const; + static std::map joinMultiplicityMaps(std::map const& first, std::map const& second); + void addMultiplicityMap(std::map const& multiplicityMap); - void addNonsilentAction(std::string const& actionName); - std::set const& getNonsilentActions() const; - - void setContainsNonStandardParallelComposition(); + void setContainsNonStandardParallelComposition(bool value); bool containsNonStandardParallelComposition() const; - static std::map joinMultiplicityMaps(std::map const& first, std::map const& second); - std::map const& getAutomatonToMultiplicityMap() const; + std::string const& getActionName(uint64_t index) const; + uint64_t getActionIndex(std::string const& name) const; + + void addNonSilentActionIndex(uint64_t index); + void addNonSilentActionIndices(std::set const& indices); + bool hasNonSilentActionIndex(uint64_t index); + void addInputEnabledActionIndex(uint64_t index); + + std::set const& getNonSilentActionIndices() const; + std::set const& getInputEnabledActionIndices() const; + + void setMappings(std::map const& indexToNameMap, std::map const& nameToIndexMap); private: + /// The indices of the non-silent actions appearing in the topmost element of the composition. + std::set nonSilentActionIndices; + + /// The set of indices of actions for which the topmost element of the composition is input-enabled. + std::set inputEnabledActionIndices; + + /// A mapping from action indices to names. Since the composition may introduce new action names, this may + /// extend the one from the underlying model. + std::map indexToNameMap; + + /// A mapping from action names to their indices. + std::map nameToIndexMap; + /// A mapping from the automata's names to the amount of times they occur in the composition. std::map automatonNameToMultiplicity; - /// The set of non-silent actions contained in the composition. - std::set nonsilentActions; - /// A flag indicating whether the composition contains any non-standard parallel composition. bool nonStandardParallelComposition; }; class CompositionInformationVisitor : public CompositionVisitor { public: - CompositionInformationVisitor() = default; - - CompositionInformation getInformation(Composition const& composition, Model const& model); - + CompositionInformationVisitor(Model const& model, Composition const& composition); + CompositionInformation getInformation(); + virtual boost::any visit(AutomatonComposition const& composition, boost::any const& data) override; virtual boost::any visit(ParallelComposition const& composition, boost::any const& data) override; + + private: + uint64_t addOrGetActionIndex(std::string const& name); + + storm::jani::Model const& model; + Composition const& composition; + uint64_t nextFreeActionIndex; + std::map nameToIndexMap; + std::map indexToNameMap; }; } diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp index f0a6cb9ba..6cc98b329 100644 --- a/src/storage/jani/Model.cpp +++ b/src/storage/jani/Model.cpp @@ -277,7 +277,7 @@ namespace storm { } uint64_t Model::getSilentActionIndex() const { - return silentActionIndex; + return SILENT_ACTION_INDEX; } Model Model::defineUndefinedConstants(std::map const& constantDefinitions) const { diff --git a/src/storage/jani/Model.h b/src/storage/jani/Model.h index f36f1842f..146ad653f 100644 --- a/src/storage/jani/Model.h +++ b/src/storage/jani/Model.h @@ -232,11 +232,6 @@ namespace storm { */ std::set getActionNames(bool includeSilent = true) const; - /*! - * Retrieves the index of the silent action. - */ - uint64_t getSilentActionIndex() const; - /*! * Defines the undefined constants of the model by the given expressions. The original model is not modified, * but instead a new model is created. @@ -338,6 +333,11 @@ namespace storm { */ static bool isSilentAction(std::string const& name); + /*! + * Retrieves the index of the silent action. + */ + static uint64_t getSilentActionIndex(); + private: /// The name of the silent action. static const std::string SILENT_ACTION_NAME;