diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp
index 2f65a58b0..9a6a2681d 100644
--- a/src/builder/DdJaniModelBuilder.cpp
+++ b/src/builder/DdJaniModelBuilder.cpp
@@ -1032,6 +1032,7 @@ namespace storm {
for (auto const& actionIndex : actionInformation.getNonSilentActionIndices()) {
actionIndexToLocalNondeterminismVariableOffset[actionIndex] = 0;
}
+ actionIndexToLocalNondeterminismVariableOffset[actionInformation.getSilentActionIndex()] = 0;
AutomatonDd globalAutomaton = boost::any_cast<AutomatonDd>(this->model.getSystemComposition().accept(*this, actionIndexToLocalNondeterminismVariableOffset));
return buildSystemFromAutomaton(globalAutomaton);
diff --git a/src/storage/dd/Dd.cpp b/src/storage/dd/Dd.cpp
index bae32c108..ec6b8b2aa 100644
--- a/src/storage/dd/Dd.cpp
+++ b/src/storage/dd/Dd.cpp
@@ -14,6 +14,11 @@ namespace storm {
// Intentionally left empty.
}
+ template<DdType LibraryType>
+ Dd<LibraryType>::~Dd() {
+ // Intentionally left empty.
+ }
+
template<DdType LibraryType>
bool Dd<LibraryType>::containsMetaVariable(storm::expressions::Variable const& metaVariable) const {
return containedMetaVariables.find(metaVariable) != containedMetaVariables.end();
@@ -87,4 +92,4 @@ namespace storm {
template class Dd<storm::dd::DdType::CUDD>;
template class Dd<storm::dd::DdType::Sylvan>;
}
-}
\ No newline at end of file
+}
diff --git a/src/storage/dd/Dd.h b/src/storage/dd/Dd.h
index 18605c259..71f392dea 100644
--- a/src/storage/dd/Dd.h
+++ b/src/storage/dd/Dd.h
@@ -30,6 +30,8 @@ namespace storm {
Dd(Dd<LibraryType>&& other) = default;
Dd& operator=(Dd<LibraryType>&& other) = default;
+ virtual ~Dd();
+
/*!
* Retrieves the support of the current DD.
*
@@ -181,4 +183,4 @@ namespace storm {
}
}
-#endif /* STORM_STORAGE_DD_DD_H_ */
\ No newline at end of file
+#endif /* STORM_STORAGE_DD_DD_H_ */
diff --git a/src/storage/jani/Automaton.h b/src/storage/jani/Automaton.h
index f2c784084..9df752612 100644
--- a/src/storage/jani/Automaton.h
+++ b/src/storage/jani/Automaton.h
@@ -298,7 +298,7 @@ namespace storm {
* Retrieves the action indices appearing at some edge of the automaton.
*/
std::set<uint64_t> getUsedActionIndices() const;
-
+
private:
/// The name of the automaton.
std::string name;
@@ -330,4 +330,4 @@ namespace storm {
};
}
-}
\ No newline at end of file
+}
diff --git a/src/storage/jani/CompositionActionInformationVisitor.cpp b/src/storage/jani/CompositionActionInformationVisitor.cpp
index ad8812648..683995d07 100644
--- a/src/storage/jani/CompositionActionInformationVisitor.cpp
+++ b/src/storage/jani/CompositionActionInformationVisitor.cpp
@@ -6,7 +6,7 @@
namespace storm {
namespace jani {
- ActionInformation::ActionInformation(std::set<uint64_t> const& nonsilentActionIndices, std::map<uint64_t, std::string> const& indexToNameMap, std::map<std::string, uint64_t> const& nameToIndexMap) : nonsilentActionIndices(nonsilentActionIndices), indexToNameMap(indexToNameMap), nameToIndexMap(nameToIndexMap) {
+ ActionInformation::ActionInformation(std::set<uint64_t> const& nonsilentActionIndices, std::map<uint64_t, std::string> const& indexToNameMap, std::map<std::string, uint64_t> const& nameToIndexMap, uint64_t silentActionIndex) : silentActionIndex(silentActionIndex), nonsilentActionIndices(nonsilentActionIndices), indexToNameMap(indexToNameMap), nameToIndexMap(nameToIndexMap) {
// Intentionally left empty.
}
@@ -21,6 +21,10 @@ namespace storm {
std::set<uint64_t> 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.
@@ -32,6 +36,11 @@ namespace storm {
// 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;
@@ -42,7 +51,9 @@ namespace storm {
}
boost::any CompositionActionInformationVisitor::visit(AutomatonComposition const& composition, boost::any const& data) {
- return model.getAutomaton(composition.getAutomatonName()).getUsedActionIndices();
+ std::set<uint64_t> result = model.getAutomaton(composition.getAutomatonName()).getUsedActionIndices();
+ result.erase(model.getSilentActionIndex());
+ return result;
}
boost::any CompositionActionInformationVisitor::visit(RenameComposition const& composition, boost::any const& data) {
diff --git a/src/storage/jani/CompositionActionInformationVisitor.h b/src/storage/jani/CompositionActionInformationVisitor.h
index 93017b8a1..705773c27 100644
--- a/src/storage/jani/CompositionActionInformationVisitor.h
+++ b/src/storage/jani/CompositionActionInformationVisitor.h
@@ -12,13 +12,15 @@ namespace storm {
class ActionInformation {
public:
- ActionInformation(std::set<uint64_t> const& nonsilentActionIndices, std::map<uint64_t, std::string> const& indexToNameMap, std::map<std::string, uint64_t> const& nameToIndexMap);
+ ActionInformation(std::set<uint64_t> const& nonsilentActionIndices, std::map<uint64_t, std::string> const& indexToNameMap, std::map<std::string, uint64_t> const& nameToIndexMap, uint64_t silentActionIndex = 0);
std::string const& getActionName(uint64_t index) const;
uint64_t getActionIndex(std::string const& name) const;
std::set<uint64_t> const& getNonSilentActionIndices() const;
+ uint64_t getSilentActionIndex() const;
private:
+ uint64_t silentActionIndex;
std::set<uint64_t> nonsilentActionIndices;
std::map<uint64_t, std::string> indexToNameMap;
std::map<std::string, uint64_t> nameToIndexMap;
diff --git a/src/storage/sparse/StateValuations.cpp b/src/storage/sparse/StateValuations.cpp
index f3f98818f..a574d7a10 100644
--- a/src/storage/sparse/StateValuations.cpp
+++ b/src/storage/sparse/StateValuations.cpp
@@ -8,10 +8,14 @@ namespace storm {
// Intentionally left empty.
}
+ StateValuations::~StateValuations() {
+ // Intentionally left empty.
+ }
+
std::string StateValuations::stateInfo(state_type const& state) const {
return valuations[state].toString();
}
}
}
-}
\ No newline at end of file
+}
diff --git a/src/storage/sparse/StateValuations.h b/src/storage/sparse/StateValuations.h
index b64620efd..a378dcaf8 100644
--- a/src/storage/sparse/StateValuations.h
+++ b/src/storage/sparse/StateValuations.h
@@ -20,6 +20,8 @@ namespace storm {
*/
StateValuations(state_type const& numberOfStates);
+ virtual ~StateValuations();
+
// A mapping from state indices to their variable valuations.
std::vector<storm::expressions::SimpleValuation> valuations;
@@ -30,4 +32,4 @@ namespace storm {
}
}
-#endif /* STORM_STORAGE_SPARSE_STATEVALUATIONS_H_ */
\ No newline at end of file
+#endif /* STORM_STORAGE_SPARSE_STATEVALUATIONS_H_ */