diff --git a/examples/dft/and_3_inputs.dft b/examples/dft/and_3_inputs.dft new file mode 100644 index 000000000..e99729079 --- /dev/null +++ b/examples/dft/and_3_inputs.dft @@ -0,0 +1,5 @@ +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 new file mode 100644 index 000000000..9a6a85a41 --- /dev/null +++ b/examples/dft/and_or_mix.dft @@ -0,0 +1,9 @@ +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/src/transformations/dft/DftToGspnTransformator.cpp b/src/transformations/dft/DftToGspnTransformator.cpp index 5c287c584..83fee7878 100644 --- a/src/transformations/dft/DftToGspnTransformator.cpp +++ b/src/transformations/dft/DftToGspnTransformator.cpp @@ -8,7 +8,7 @@ namespace storm { template DftToGspnTransformator::DftToGspnTransformator(storm::storage::DFT const& dft) : mDft(dft) { - // Intentionally left empty + // Intentionally left empty. } template @@ -16,60 +16,21 @@ namespace storm { mGspn = storm::gspn::GSPN(); mGspn.setName("DftToGspnTransformation"); - /* - // Testing place. - storm::gspn::Place place; - place.setName("Left"); - place.setID(0); - place.setNumberOfInitialTokens(2); - mGspn.addPlace(place); + // TODO: Do I need to check if every DFT element has an unique name? + // TODO: GSPN elements are picked by their name in method drawGSPNConnections(), so this might cause problems... - storm::gspn::Place place2; - place2.setName("Right"); - place2.setID(1); - place2.setNumberOfInitialTokens(0); - mGspn.addPlace(place2); - - // Testing transition. - storm::gspn::ImmediateTransition immediateTransition; - immediateTransition.setName("ImmediateTransition"); - immediateTransition.setPriority(2); - immediateTransition.setWeight(0.0); - immediateTransition.setInputArcMultiplicity(place, 1); - immediateTransition.setOutputArcMultiplicity(place2, 1); - mGspn.addImmediateTransition(immediateTransition); - - storm::gspn::TimedTransition timedTransition; - timedTransition.setName("TimedTransition"); - timedTransition.setPriority(1); - timedTransition.setRate(0.3); - timedTransition.setInhibitionArcMultiplicity(place2, 1); - timedTransition.setOutputArcMultiplicity(place, 1); - mGspn.addTimedTransition(timedTransition); - - // Testing DFT. - std::cout << "-------------------------------------------------------------------------" << std::endl; - std::cout << "Number of elements in DFT: " << mDft.nrElements() << std::endl; - std::cout << "Number of basic elements in DFT: " << mDft.nrBasicElements() << std::endl; - std::cout << "Toplevel index of DFT: " << mDft.getTopLevelIndex() << std::endl; + // Loop through every DFT element and draw them as a GSPN. + drawGSPNElements(); - for (std::size_t i = 0; i < mDft.nrElements(); i++) { - auto dftElement = mDft.getElement(i); - std::cout << "Index: " << i - << " Gate: " << dftElement->isGate() - << " Dependency: " << dftElement->isDependency() - << " Restriction: " << dftElement->isRestriction() - << " String: " << dftElement->toString() - << " Name: " << dftElement->name() << std::endl; - - auto parents = dftElement->parentIds(); - for (std::size_t j = 0; j < parents.size(); j++) { - std::cout << "Parents of " << j << ": " << parents[j] << std::endl; - } - } - std::cout << "-------------------------------------------------------------------------" << std::endl; - */ + // When all DFT elements are drawn, draw the connections between them. + drawGSPNConnections(); + // Write GSPN to file. + writeGspn(true); + } + + template + void DftToGspnTransformator::drawGSPNElements() { // Loop through every DFT element and draw them as a GSPN. for (std::size_t i = 0; i < mDft.nrElements(); i++) { auto dftElement = mDft.getElement(i); @@ -117,11 +78,7 @@ namespace storm { break; } } - - // Output. - writeGspn(true); - writeGspn(false); - } + } template void DftToGspnTransformator::drawBE(std::shared_ptr const> dftBE) { @@ -178,9 +135,10 @@ namespace storm { placeORFailed.setNumberOfInitialTokens(0); mGspn.addPlace(placeORFailed); + auto children = dftOr->children(); for (std::size_t i = 0; i < dftOr->nrChildren(); i++) { storm::gspn::ImmediateTransition immediateTransitionORFailing; - immediateTransitionORFailing.setName(dftOr->name() + std::to_string((int)i) + "_failing"); + immediateTransitionORFailing.setName(dftOr->name() + "_" + children[i]->name() + "_failing"); immediateTransitionORFailing.setPriority(1); immediateTransitionORFailing.setWeight(0.0); immediateTransitionORFailing.setInhibitionArcMultiplicity(placeORFailed, 1); @@ -209,6 +167,70 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The transformation of a POR is not yet implemented."); } + template + void DftToGspnTransformator::drawGSPNConnections() { + // Check for every element, if they have parents (all will have at least 1, except the top event). + for (std::size_t i = 0; i < mDft.nrElements(); i++) { + auto child = mDft.getElement(i); + auto parents = child->parentIds(); + + // Draw a connection to every parent. + for (std::size_t j = 0; j < parents.size(); j++) { + // Check the type of the parent and act accordingly (every parent gate has different entry points...). + switch (mDft.getElement(parents[j])->type()) { + case storm::storage::DFTElementType::AND: + { + auto andEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_failing"); + auto childExit = mGspn.getPlace(child->name() + "_failed"); + if (andEntry.first && childExit.first) { // Only add arcs if the objects have been found. + andEntry.second->setInputArcMultiplicity(childExit.second, 1); + andEntry.second->setOutputArcMultiplicity(childExit.second, 1); + } + break; + } + case storm::storage::DFTElementType::OR: + { + auto orEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + child->name() + "_failing"); + auto childExit = mGspn.getPlace(child->name() + "_failed"); + if (orEntry.first && childExit.first) { // Only add arcs if the objects have been found. + orEntry.second->setInputArcMultiplicity(childExit.second, 1); + orEntry.second->setOutputArcMultiplicity(childExit.second, 1); + } + break; + } + case storm::storage::DFTElementType::VOT: + break; + case storm::storage::DFTElementType::PAND: + break; + case storm::storage::DFTElementType::SPARE: + break; + case storm::storage::DFTElementType::POR: + break; + case storm::storage::DFTElementType::SEQ: + break; + case storm::storage::DFTElementType::MUTEX: + break; + case storm::storage::DFTElementType::BE: + { + // The parent is never a Basic Event. + break; + } + case storm::storage::DFTElementType::CONSTF: + break; + case storm::storage::DFTElementType::CONSTS: + break; + case storm::storage::DFTElementType::PDEP: + break; + default: + { + STORM_LOG_ASSERT(false, "DFT type unknown."); + break; + } + } + } + } + } + template void DftToGspnTransformator::writeGspn(bool toFile) { if (toFile) { diff --git a/src/transformations/dft/DftToGspnTransformator.h b/src/transformations/dft/DftToGspnTransformator.h index 264541817..ce87472ea 100644 --- a/src/transformations/dft/DftToGspnTransformator.h +++ b/src/transformations/dft/DftToGspnTransformator.h @@ -40,6 +40,16 @@ namespace storm { */ void writeGspn(bool toFile); + /* + * Draw all elements of the GSPN. + */ + void drawGSPNElements(); + + /* + * Draw the connections between the elements of the GSPN. + */ + void drawGSPNConnections(); + /* * Draw a Petri net Basic Event. *