Browse Source

Fixed FDEP/PDEP bug

Former-commit-id: 7ea9082d5a
tempestpy_adaptions
mdeutschen 8 years ago
committed by Sebastian Junges
parent
commit
c8495a1ca1
  1. 17
      src/transformations/dft/DftToGspnTransformator.cpp

17
src/transformations/dft/DftToGspnTransformator.cpp

@ -13,9 +13,7 @@ namespace storm {
template <typename ValueType> template <typename ValueType>
void DftToGspnTransformator<ValueType>::transform() { void DftToGspnTransformator<ValueType>::transform() {
// TODO: PDEP and FDEP are currently bugged.
mGspn = storm::gspn::GSPN();
mGspn = storm::gspn::GSPN();
mGspn.setName("DftToGspnTransformation"); mGspn.setName("DftToGspnTransformation");
// Loop through every DFT element and draw them as a GSPN. // Loop through every DFT element and draw them as a GSPN.
@ -213,6 +211,7 @@ namespace storm {
template <typename ValueType> template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawSPARE(std::shared_ptr<storm::storage::DFTSpare<ValueType> const> dftSpare) { void DftToGspnTransformator<ValueType>::drawSPARE(std::shared_ptr<storm::storage::DFTSpare<ValueType> const> dftSpare) {
// TODO: Implement.
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The transformation of a SPARE is not yet implemented."); STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The transformation of a SPARE is not yet implemented.");
} }
@ -544,25 +543,25 @@ namespace storm {
template <typename ValueType> template <typename ValueType>
uint_fast64_t DftToGspnTransformator<ValueType>::getPriority(uint_fast64_t priority, std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement) uint_fast64_t DftToGspnTransformator<ValueType>::getPriority(uint_fast64_t priority, std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement)
{ {
// TODO: This method is buggy for pdep2.dft and fdep.dft.
// If element is the top element, return current priority. // If element is the top element, return current priority.
if (dftElement->id() == mDft.getTopLevelIndex()) { if (dftElement->id() == mDft.getTopLevelIndex()) {
return priority; return priority;
} }
else if (dftElement->type() == storm::storage::DFTElementType::PDEP) { // TODO: Else if Necessary?
return UINT_FAST64_MAX;
}
else { // Else look at all parents. else { // Else look at all parents.
auto parents = dftElement->parents(); auto parents = dftElement->parents();
std::vector<uint_fast64_t> pathLengths; std::vector<uint_fast64_t> pathLengths;
// If the element has no parents, return.
if (parents.size() == 0) {
return UINT_FAST64_MAX / 2; // High enough value so that this priority is never used as the shortest path to the top event.
}
// Check priorities of all parents. // Check priorities of all parents.
for (std::size_t i = 0; i < parents.size(); i++) { for (std::size_t i = 0; i < parents.size(); i++) {
pathLengths.push_back(getPriority(priority + 2, parents[i])); pathLengths.push_back(getPriority(priority + 2, parents[i]));
} }
// And only use the lowest priority.
// And only use the path to the parent with the lowest priority.
return *std::min_element(pathLengths.begin(), pathLengths.end()); return *std::min_element(pathLengths.begin(), pathLengths.end());
} }

Loading…
Cancel
Save