Browse Source

fixed some bugs here and there

Former-commit-id: 0dbedbb011 [formerly 5a4bce00e8]
Former-commit-id: 7dd87b1155
main
dehnert 9 years ago
parent
commit
d2af83a98a
  1. 1
      src/builder/DdJaniModelBuilder.cpp
  2. 5
      src/storage/dd/Dd.cpp
  3. 2
      src/storage/dd/Dd.h
  4. 15
      src/storage/jani/CompositionActionInformationVisitor.cpp
  5. 4
      src/storage/jani/CompositionActionInformationVisitor.h
  6. 4
      src/storage/sparse/StateValuations.cpp
  7. 2
      src/storage/sparse/StateValuations.h

1
src/builder/DdJaniModelBuilder.cpp

@ -1032,6 +1032,7 @@ namespace storm {
for (auto const& actionIndex : actionInformation.getNonSilentActionIndices()) { for (auto const& actionIndex : actionInformation.getNonSilentActionIndices()) {
actionIndexToLocalNondeterminismVariableOffset[actionIndex] = 0; actionIndexToLocalNondeterminismVariableOffset[actionIndex] = 0;
} }
actionIndexToLocalNondeterminismVariableOffset[actionInformation.getSilentActionIndex()] = 0;
AutomatonDd globalAutomaton = boost::any_cast<AutomatonDd>(this->model.getSystemComposition().accept(*this, actionIndexToLocalNondeterminismVariableOffset)); AutomatonDd globalAutomaton = boost::any_cast<AutomatonDd>(this->model.getSystemComposition().accept(*this, actionIndexToLocalNondeterminismVariableOffset));
return buildSystemFromAutomaton(globalAutomaton); return buildSystemFromAutomaton(globalAutomaton);

5
src/storage/dd/Dd.cpp

@ -14,6 +14,11 @@ namespace storm {
// Intentionally left empty. // Intentionally left empty.
} }
template<DdType LibraryType>
Dd<LibraryType>::~Dd() {
// Intentionally left empty.
}
template<DdType LibraryType> template<DdType LibraryType>
bool Dd<LibraryType>::containsMetaVariable(storm::expressions::Variable const& metaVariable) const { bool Dd<LibraryType>::containsMetaVariable(storm::expressions::Variable const& metaVariable) const {
return containedMetaVariables.find(metaVariable) != containedMetaVariables.end(); return containedMetaVariables.find(metaVariable) != containedMetaVariables.end();

2
src/storage/dd/Dd.h

@ -30,6 +30,8 @@ namespace storm {
Dd(Dd<LibraryType>&& other) = default; Dd(Dd<LibraryType>&& other) = default;
Dd& operator=(Dd<LibraryType>&& other) = default; Dd& operator=(Dd<LibraryType>&& other) = default;
virtual ~Dd();
/*! /*!
* Retrieves the support of the current DD. * Retrieves the support of the current DD.
* *

15
src/storage/jani/CompositionActionInformationVisitor.cpp

@ -6,7 +6,7 @@
namespace storm { namespace storm {
namespace jani { 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. // Intentionally left empty.
} }
@ -22,6 +22,10 @@ namespace storm {
return nonsilentActionIndices; return nonsilentActionIndices;
} }
uint64_t ActionInformation::getSilentActionIndex() const {
return silentActionIndex;
}
CompositionActionInformationVisitor::CompositionActionInformationVisitor(storm::jani::Model const& model) : model(model), nextFreeActionIndex(0), nameToIndexMap(), indexToNameMap() { CompositionActionInformationVisitor::CompositionActionInformationVisitor(storm::jani::Model const& model) : model(model), nextFreeActionIndex(0), nameToIndexMap(), indexToNameMap() {
// Intentionally left empty. // Intentionally left empty.
} }
@ -32,6 +36,11 @@ namespace storm {
// Determine the next free index we can give out to a new action. // Determine the next free index we can give out to a new action.
for (auto const& action : model.getActions()) { 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::max(nextFreeActionIndex, model.getActionIndex(action.getName()));
} }
++nextFreeActionIndex; ++nextFreeActionIndex;
@ -42,7 +51,9 @@ namespace storm {
} }
boost::any CompositionActionInformationVisitor::visit(AutomatonComposition const& composition, boost::any const& data) { 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) { boost::any CompositionActionInformationVisitor::visit(RenameComposition const& composition, boost::any const& data) {

4
src/storage/jani/CompositionActionInformationVisitor.h

@ -12,13 +12,15 @@ namespace storm {
class ActionInformation { class ActionInformation {
public: 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; std::string const& getActionName(uint64_t index) const;
uint64_t getActionIndex(std::string const& name) const; uint64_t getActionIndex(std::string const& name) const;
std::set<uint64_t> const& getNonSilentActionIndices() const; std::set<uint64_t> const& getNonSilentActionIndices() const;
uint64_t getSilentActionIndex() const;
private: private:
uint64_t silentActionIndex;
std::set<uint64_t> nonsilentActionIndices; std::set<uint64_t> nonsilentActionIndices;
std::map<uint64_t, std::string> indexToNameMap; std::map<uint64_t, std::string> indexToNameMap;
std::map<std::string, uint64_t> nameToIndexMap; std::map<std::string, uint64_t> nameToIndexMap;

4
src/storage/sparse/StateValuations.cpp

@ -8,6 +8,10 @@ namespace storm {
// Intentionally left empty. // Intentionally left empty.
} }
StateValuations::~StateValuations() {
// Intentionally left empty.
}
std::string StateValuations::stateInfo(state_type const& state) const { std::string StateValuations::stateInfo(state_type const& state) const {
return valuations[state].toString(); return valuations[state].toString();
} }

2
src/storage/sparse/StateValuations.h

@ -20,6 +20,8 @@ namespace storm {
*/ */
StateValuations(state_type const& numberOfStates); StateValuations(state_type const& numberOfStates);
virtual ~StateValuations();
// A mapping from state indices to their variable valuations. // A mapping from state indices to their variable valuations.
std::vector<storm::expressions::SimpleValuation> valuations; std::vector<storm::expressions::SimpleValuation> valuations;

Loading…
Cancel
Save