diff --git a/examples/dft/and_3_inputs.dft b/examples/dft/and_3_inputs.dft deleted file mode 100644 index e99729079..000000000 --- a/examples/dft/and_3_inputs.dft +++ /dev/null @@ -1,5 +0,0 @@ -toplevel "A"; -"A" and "B" "C" "D"; -"B" lambda=0.5 dorm=0.2; -"C" lambda=0.4 dorm=0.1; -"D" lambda=0.3 dorm=0.05; diff --git a/examples/dft/and_or_mix.dft b/examples/dft/and_or_mix.dft deleted file mode 100644 index 9a6a85a41..000000000 --- a/examples/dft/and_or_mix.dft +++ /dev/null @@ -1,9 +0,0 @@ -toplevel "A"; -"A" and "B" "C"; -"B" or "BE1" "BE2"; -"C" and "BE3" "D"; -"D" or "BE1" "BE4"; -"BE1" lambda=0.5 dorm=0.3; -"BE2" lambda=0.5 dorm=0.3; -"BE3" lambda=0.5 dorm=0.3; -"BE4" lambda=0.5 dorm=0.3; diff --git a/examples/dft/be.dft b/examples/dft/be.dft deleted file mode 100644 index f7636d080..000000000 --- a/examples/dft/be.dft +++ /dev/null @@ -1,2 +0,0 @@ -toplevel "A"; -"A" lambda=0.5 dorm=0.3; diff --git a/examples/dft/pand2.dft b/examples/dft/pand2.dft deleted file mode 100644 index c2e875bda..000000000 --- a/examples/dft/pand2.dft +++ /dev/null @@ -1,6 +0,0 @@ -toplevel "A"; -"A" pand "B" "C" "D" "E"; -"B" lambda=0.4 dorm=0.3; -"C" lambda=0.2 dorm=0.3; -"D" lambda=0.1 dorm=0.3; -"E" lambda=0.05 dorm=0.3; diff --git a/examples/dft/pdep5.dft b/examples/dft/pdep5.dft deleted file mode 100644 index 6fd912b59..000000000 --- a/examples/dft/pdep5.dft +++ /dev/null @@ -1,5 +0,0 @@ -toplevel "A"; -"A" and "B" "C"; -"PDEP" pdep=0.2 "B" "C"; -"B" lambda=0.5 dorm=0; -"C" lambda=0.5 dorm=0; diff --git a/examples/dft/por2.dft b/examples/dft/por2.dft deleted file mode 100644 index cd37e0c21..000000000 --- a/examples/dft/por2.dft +++ /dev/null @@ -1,4 +0,0 @@ -toplevel "A"; -"A" por "B" "C"; -"B" lambda=0.4 dorm=0.0; -"C" lambda=0.2 dorm=0.0; diff --git a/examples/dft/por_mix.dft b/examples/dft/por_mix.dft deleted file mode 100644 index d2fafe18e..000000000 --- a/examples/dft/por_mix.dft +++ /dev/null @@ -1,6 +0,0 @@ -toplevel "A"; -"A" por "B" "C" "D"; -"B" and "C" "E"; -"C" lambda=0.2 dorm=0.0; -"D" lambda=0.2 dorm=0.0; -"E" lambda=0.2 dorm=0.0; diff --git a/examples/dft/seq6.dft b/examples/dft/seq6.dft deleted file mode 100644 index 0aa9924cc..000000000 --- a/examples/dft/seq6.dft +++ /dev/null @@ -1,7 +0,0 @@ -toplevel "A"; -"A" and "B" "C"; -"X" seq "B" "C" -"B" lambda=0.5 dorm=0.3; -"C" and "D" "E"; -"D" lambda=0.5 dorm=0.3; -"E" lambda=0.5 dorm=0.3; diff --git a/examples/dft/voting3.dft b/examples/dft/voting3.dft deleted file mode 100644 index 19c6883de..000000000 --- a/examples/dft/voting3.dft +++ /dev/null @@ -1,11 +0,0 @@ -toplevel "A"; -"A" 5of9 "B" "C" "D" "E" "F" "G" "H" "I" "J"; -"B" lambda=0.1 dorm=0; -"C" lambda=0.2 dorm=0; -"D" lambda=0.3 dorm=0; -"E" lambda=0.4 dorm=0; -"F" lambda=0.5 dorm=0; -"G" lambda=0.5 dorm=0; -"H" lambda=0.5 dorm=0; -"I" lambda=0.5 dorm=0; -"J" lambda=0.5 dorm=0; diff --git a/examples/dft/voting_mix.dft b/examples/dft/voting_mix.dft deleted file mode 100644 index c599db903..000000000 --- a/examples/dft/voting_mix.dft +++ /dev/null @@ -1,9 +0,0 @@ -toplevel "A"; -"A" and "B" "F"; -"B" 2of3 "C" "D" "E"; -"C" lambda=0.1 dorm=0; -"D" lambda=0.2 dorm=0; -"E" lambda=0.3 dorm=0; -"F" 2of3 "G" "H" "C"; -"G" lambda=0.4 dorm=0; -"H" lambda=0.5 dorm=0; diff --git a/src/transformations/dft/DftToGspnTransformator.cpp b/src/transformations/dft/DftToGspnTransformator.cpp index 486e872c0..4c03b2767 100644 --- a/src/transformations/dft/DftToGspnTransformator.cpp +++ b/src/transformations/dft/DftToGspnTransformator.cpp @@ -241,7 +241,7 @@ namespace storm { mGspn.addPlace(placeChildClaimed); storm::gspn::ImmediateTransition immediateTransitionSpareChildActivating; - immediateTransitionSpareChildActivating.setName(dftSpare->children()[i]->name() + STR_ACTIVATING); + immediateTransitionSpareChildActivating.setName(children[i]->name() + STR_ACTIVATING); immediateTransitionSpareChildActivating.setPriority(priority); immediateTransitionSpareChildActivating.setWeight(0.0); immediateTransitionSpareChildActivating.setInputArcMultiplicity(placeChildClaimed, 1); @@ -256,13 +256,27 @@ namespace storm { placeSPAREClaimedChild.setNumberOfInitialTokens(0); mGspn.addPlace(placeSPAREClaimedChild); + storm::gspn::ImmediateTransition immediateTransitionChildClaiming; + immediateTransitionChildClaiming.setName(children[i]->name() + "_claiming"); + immediateTransitionChildClaiming.setPriority(priority + 1); // Higher priority needed! + immediateTransitionChildClaiming.setWeight(0.0); + immediateTransitionChildClaiming.setInhibitionArcMultiplicity(placeChildClaimedExist.second, 1); + immediateTransitionChildClaiming.setOutputArcMultiplicity(placeChildClaimedExist.second, 1); + immediateTransitionChildClaiming.setOutputArcMultiplicity(placeSPAREClaimedChild, 1); + mGspn.addImmediateTransition(immediateTransitionChildClaiming); + storm::gspn::Place placeSPAREChildConsumed; - placeSPAREChildConsumed.setName(children[i]->name() + "_consumed"); // TODO: If its the last child, this label must be "SPARE_failed". + if (i < children.size() - 1) { + placeSPAREChildConsumed.setName(children[i]->name() + "_consumed"); + } + else { + placeSPAREChildConsumed.setName(dftSpare->name() + STR_FAILED); + } placeSPAREChildConsumed.setNumberOfInitialTokens(0); mGspn.addPlace(placeSPAREChildConsumed); storm::gspn::ImmediateTransition immediateTransitionChildConsuming1; - immediateTransitionChildConsuming1.setName(dftSpare->children()[i]->name() + "_consuming1"); + immediateTransitionChildConsuming1.setName(children[i]->name() + "_consuming1"); immediateTransitionChildConsuming1.setPriority(priority); immediateTransitionChildConsuming1.setWeight(0.0); immediateTransitionChildConsuming1.setOutputArcMultiplicity(placeSPAREChildConsumed, 1); @@ -271,7 +285,7 @@ namespace storm { mGspn.addImmediateTransition(immediateTransitionChildConsuming1); storm::gspn::ImmediateTransition immediateTransitionChildConsuming2; - immediateTransitionChildConsuming2.setName(dftSpare->children()[i]->name() + "_consuming2"); + immediateTransitionChildConsuming2.setName(children[i]->name() + "_consuming2"); immediateTransitionChildConsuming2.setPriority(priority); immediateTransitionChildConsuming2.setWeight(0.0); immediateTransitionChildConsuming2.setOutputArcMultiplicity(placeSPAREChildConsumed, 1); @@ -734,6 +748,20 @@ namespace storm { } } + template + std::vector DftToGspnTransformator::getAllBEIDsOfElement(std::vector ids, std::shared_ptr const> dftElement) { + std::vector newIds; + + if (dftElement->type() == storm::storage::DFTElementType::BE) { + newIds.push_back(dftElement->id()); + } + else { + // TODO: Check all children: If they are BEs, add them to the list. Else, check the children again. + } + + return newIds; + } + template void DftToGspnTransformator::writeGspn(bool toFile) { if (toFile) { diff --git a/src/transformations/dft/DftToGspnTransformator.h b/src/transformations/dft/DftToGspnTransformator.h index 3f1e09636..fcfe24139 100644 --- a/src/transformations/dft/DftToGspnTransformator.h +++ b/src/transformations/dft/DftToGspnTransformator.h @@ -199,6 +199,13 @@ namespace storm { * @param dftElement The element whose priority shall be determined. */ uint_fast64_t getPriority(uint_fast64_t priority, std::shared_ptr const> dFTElement); + + /* + * Return all ids of BEs, that are successors of the given element. + * + * @param dftElement The element which + */ + std::vector getAllBEIDsOfElement(std::vector ids, std::shared_ptr const> dftElement); }; } }