Browse Source

add state labeling

Former-commit-id: 892cf083c7
tempestpy_adaptions
ThomasH 9 years ago
parent
commit
cffb887c4f
  1. 27
      src/builder/ExplicitGspnModelBuilder.cpp
  2. 8
      src/builder/ExplicitGspnModelBuilder.h

27
src/builder/ExplicitGspnModelBuilder.cpp

@ -70,7 +70,7 @@ namespace storm {
}
auto matrix = builder.build();
const storm::models::sparse::StateLabeling labeling; // TODO
auto labeling = getStateLabeling();
return storm::models::sparse::MarkovAutomaton<double>(matrix, labeling, markovianStates, exitRates);
}
@ -244,6 +244,31 @@ namespace storm {
return index;
}
template<typename ValueType>
storm::models::sparse::StateLabeling ExplicitGspnModelBuilder<ValueType>::getStateLabeling() const {
storm::models::sparse::StateLabeling labeling(markings.size());
std::map<uint_fast64_t , std::string> idToName;
for (auto& place : gspn.getPlaces()) {
idToName[place.getID()] = place.getName();
labeling.addLabel(place.getName());
}
auto it = markings.begin();
for ( ; it != markings.end() ; ++it) {
auto bitvector = std::get<0>(*it);
storm::gspn::Marking marking(gspn.getNumberOfPlaces(), numberOfBits, bitvector);
for (auto i = 0; i < marking.getNumberOfPlaces(); i++) {
if (marking.getNumberOfTokensAt(i) > 0) {
std::cout << i << std::endl;
labeling.addLabelToState(idToName.at(i), i);
}
}
}
return labeling;
}
template class ExplicitGspnModelBuilder<double>;
}
}

8
src/builder/ExplicitGspnModelBuilder.h

@ -130,6 +130,14 @@ namespace storm {
*/
uint_fast64_t findOrAddBitvectorToMarkings(storm::storage::BitVector const& bitvector);
/*!
* Computes the state labeling and returns it.
* Every state is labeled with its name.
*
* @return The computed state labeling.
*/
storm::models::sparse::StateLabeling getStateLabeling() const;
// contains the number of bits which are used the store the number of tokens at each place
std::map<uint_fast64_t, uint_fast64_t> numberOfBits;

Loading…
Cancel
Save