diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp index 81553f3c9..caa40191e 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.cpp +++ b/src/storm-dft/transformations/DftToGspnTransformator.cpp @@ -37,10 +37,13 @@ namespace storm { template std::map DftToGspnTransformator::computePriorities() { std::map priorities; + // Set priority for PDEP and FDEP according to Monolithic MA semantics + uint64_t dependency_priority = 2; for (std::size_t i = 0; i < mDft.nrElements(); i++) { - // Give all elements the same priority - priorities[i] = (-(mDft.getElement(i)->rank()) + mDft.maxRank()) * 2 + 2; - + if (mDft.getElement(i)->type() == storm::storage::DFTElementType::PDEP) + priorities[i] = dependency_priority; + else + priorities[i] = (-(mDft.getElement(i)->rank()) + mDft.maxRank()) * 2 + 5; } return priorities; } @@ -126,7 +129,6 @@ namespace storm { dftBE->name() + STR_ACTIVATED); activePlaces.emplace(dftBE->id(), activePlace); builder.setPlaceLayoutInfo(activePlace, storm::gspn::LayoutInfo(xcenter - 3.0, ycenter)); - uint64_t tActive = builder.addTimedTransition(getFailPriority(dftBE), dftBE->activeFailureRate(), dftBE->name() + "_activeFailing"); builder.setTransitionLayoutInfo(tActive, storm::gspn::LayoutInfo(xcenter, ycenter + 3.0)); diff --git a/src/storm-gspn/storage/gspn/GSPN.cpp b/src/storm-gspn/storage/gspn/GSPN.cpp index 7b623b9de..1f3e5a627 100644 --- a/src/storm-gspn/storage/gspn/GSPN.cpp +++ b/src/storm-gspn/storage/gspn/GSPN.cpp @@ -433,7 +433,8 @@ namespace storm { stream << space3 << " 0) { stream << "x=\"" << transitionLayout.at(trans.getID()).x << "\" "; stream << "y=\"" << transitionLayout.at(trans.getID()).y << "\" "; @@ -449,6 +450,7 @@ namespace storm { stream << space3 << " 0) { stream << "x=\"" << transitionLayout.at(trans.getID()).x << "\" "; stream << "y=\"" << transitionLayout.at(trans.getID()).y << "\" ";