diff --git a/src/storm/storage/gspn/GSPN.cpp b/src/storm/storage/gspn/GSPN.cpp index 761bbdec5..7a2ed6bb4 100644 --- a/src/storm/storage/gspn/GSPN.cpp +++ b/src/storm/storage/gspn/GSPN.cpp @@ -131,61 +131,82 @@ namespace storm { void GSPN::writeDotToStream(std::ostream& outStream) const { outStream << "digraph " << this->getName() << " {" << std::endl; - + // print places with initial marking (not printed is the capacity) outStream << "\t" << "node [shape=ellipse]" << std::endl; for (auto& place : this->getPlaces()) { outStream << "\t" << place.getName() << " [label=\"" << place.getName() << "(" << place.getNumberOfInitialTokens(); - outStream << ")"; - if(place.hasRestrictedCapacity()) { - outStream << "c " << place.getCapacity(); - } - - outStream << "\"];" << std::endl; + outStream << ")\"];" << std::endl; } - + // print transitions with weight/rate outStream << "\t" << "node [shape=box]" << std::endl; + for (auto& trans : this->getImmediateTransitions()) { - outStream << "\t" << trans.getName() << " [fontcolor=white, style=filled, fillcolor=black, label=\"" << trans.getName() << "\"];" << std::endl; + outStream << "\t" << trans->getName() << " [fontcolor=white, style=filled, fillcolor=black, label=\"" << trans->getName() << "\"];" << std::endl; } - + for (auto& trans : this->getTimedTransitions()) { - outStream << "\t" << trans.getName() << " [label=\"" << trans.getName(); - outStream << " (" << trans.getRate() << ")\"];" << std::endl; + outStream << "\t" << trans->getName() << " [label=\"" << trans->getName(); + outStream << "(" << trans->getRate() << ")\"];" << std::endl; } - + // print arcs for (auto& trans : this->getImmediateTransitions()) { - - for (auto const& inEntry : trans.getInputPlaces()) { - outStream << "\t" << places.at(inEntry.first).getName() << " -> " << trans.getName() << "[label=\"" << inEntry.second << "\"];" << std::endl; + auto it = trans->getInputPlacesCBegin(); + while (it != trans->getInputPlacesCEnd()) { + outStream << "\t" << (**it).getName() << " -> " << trans->getName() << "[label=\"" << + ((trans->getInputArcMultiplicity(**it) == 1) ? "" : std::to_string(trans->getInputArcMultiplicity(**it))) + << "\"];" << std::endl; + + ++it; } - - for (auto const& inhEntry : trans.getInhibitionPlaces()) { - outStream << "\t" << places.at(inhEntry.first).getName() << " -> " << trans.getName() << "[arrowhead=\"dot\", label=\"" << inhEntry.second << "\"];" << std::endl; + + it = trans->getInhibitionPlacesCBegin(); + while (it != trans->getInhibitionPlacesCEnd()) { + outStream << "\t" << (**it).getName() << " -> " << trans->getName() << "[arrowhead=\"dot\", label=\"" << + ((trans->getInhibitionArcMultiplicity(**it) == 1) ? "" : std::to_string(trans->getInhibitionArcMultiplicity(**it))) + << "\"];" << std::endl; + ++it; } - - for (auto const& outEntry : trans.getOutputPlaces()) { - outStream << "\t" << trans.getName() << " -> " << places.at(outEntry.first).getName() << "[label=\"" << outEntry.second << "\"];" << std::endl; + + it = trans->getOutputPlacesCBegin(); + while (it != trans->getOutputPlacesCEnd()) { + outStream << "\t" << trans->getName() << " -> " << (**it).getName() << "[label=\"" << + ((trans->getOutputArcMultiplicity(**it) == 1) ? "" : std::to_string(trans->getOutputArcMultiplicity(**it))) + << "\"];" << std::endl; + ++it; } } - + for (auto& trans : this->getTimedTransitions()) { - for (auto const& inEntry : trans.getInputPlaces()) { - outStream << "\t" << places.at(inEntry.first).getName() << " -> " << trans.getName() << "[label=\"" << inEntry.second << "\"];" << std::endl; + auto it = trans->getInputPlacesCBegin(); + while (it != trans->getInputPlacesCEnd()) { + outStream << "\t" << (**it).getName() << " -> " << trans->getName() << "[label=\"" << + ((trans->getInputArcMultiplicity(**it) == 1) ? "" : std::to_string(trans->getInputArcMultiplicity(**it))) + << "\"];" << std::endl; + ++it; } - for (auto const& inhEntry : trans.getInhibitionPlaces()) { - outStream << "\t" << places.at(inhEntry.first).getName() << " -> " << trans.getName() << "[arrowhead=\"dot\", label=\"" << inhEntry.second << "\"];" << std::endl; + it = trans->getInhibitionPlacesCBegin(); + while (it != trans->getInhibitionPlacesCEnd()) { + outStream << "\t" << (**it).getName() << " -> " << trans->getName() << "[arrowhead=\"dot\", label=\"" << + ((trans->getInhibitionArcMultiplicity(**it) == 1) ? "" : std::to_string(trans->getInhibitionArcMultiplicity(**it))) + << "\"];" << std::endl; + ++it; } - for (auto const& outEntry : trans.getOutputPlaces()) { - outStream << "\t" << trans.getName() << " -> " << places.at(outEntry.first).getName() << "[label=\"" << outEntry.second << "\"];" << std::endl; + it = trans->getOutputPlacesCBegin(); + while (it != trans->getOutputPlacesCEnd()) { + outStream << "\t" << trans->getName() << " -> " << (**it).getName() << "[label=\"" << + ((trans->getOutputArcMultiplicity(**it) == 1) ? "" : std::to_string(trans->getOutputArcMultiplicity(**it))) + << "\"];" << std::endl; + ++it; } } - + outStream << "}" << std::endl; + } void GSPN::setName(std::string const& name) { diff --git a/src/transformations/dft/DftToGspnTransformator.cpp b/src/transformations/dft/DftToGspnTransformator.cpp index 69952cbfd..5c287c584 100644 --- a/src/transformations/dft/DftToGspnTransformator.cpp +++ b/src/transformations/dft/DftToGspnTransformator.cpp @@ -1,5 +1,6 @@ #include "src/transformations/dft/DftToGspnTransformator.h" #include "src/exceptions/NotImplementedException.h" +#include namespace storm { namespace transformations { @@ -76,22 +77,22 @@ namespace storm { // Check which type the element is and call the corresponding drawing-function. switch (dftElement->type()) { case storm::storage::DFTElementType::AND: - drawAND(dftElement->name()); + drawAND(std::static_pointer_cast const>(dftElement)); break; case storm::storage::DFTElementType::OR: - drawOR(dftElement->name(), 2); // TODO: set parameters correctly. + drawOR(std::static_pointer_cast const>(dftElement)); break; case storm::storage::DFTElementType::VOT: - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The transformation of a VOT is not yet implemented."); + drawVOT(std::static_pointer_cast const>(dftElement)); break; case storm::storage::DFTElementType::PAND: - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The transformation of a PAND is not yet implemented."); + drawPAND(std::static_pointer_cast const>(dftElement)); break; case storm::storage::DFTElementType::SPARE: - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The transformation of a SPARE is not yet implemented."); + drawSPARE(std::static_pointer_cast const>(dftElement)); break; case storm::storage::DFTElementType::POR: - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The transformation of a POR is not yet implemented."); + drawPOR(std::static_pointer_cast const>(dftElement)); break; case storm::storage::DFTElementType::SEQ: STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The transformation of a SEQ is not yet implemented."); @@ -100,7 +101,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The transformation of a MUTEX is not yet implemented."); break; case storm::storage::DFTElementType::BE: - drawBE(dftElement->name(), true, 0.5, 0.25); // TODO: set parameters correctly. + drawBE(std::static_pointer_cast const>(dftElement)); break; case storm::storage::DFTElementType::CONSTF: STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The transformation of a CONSTF is not yet implemented."); @@ -123,35 +124,21 @@ namespace storm { } template - void DftToGspnTransformator::writeGspn(bool toFile) { - if (toFile) { - // Writing to file - std::ofstream file; - file.open("gspn.dot"); - mGspn.writeDotToStream(file); - file.close(); - } else { - // Writing to console - mGspn.writeDotToStream(std::cout); - } - } - - template - void DftToGspnTransformator::drawBE(std::string name, bool activated, double activeFailureRate, double passiveFailureRate) { + void DftToGspnTransformator::drawBE(std::shared_ptr const> dftBE) { storm::gspn::Place placeBEActivated; - placeBEActivated.setName(name + "_activated"); - placeBEActivated.setNumberOfInitialTokens(activated ? 1 : 0); + placeBEActivated.setName(dftBE->name() + "_activated"); + placeBEActivated.setNumberOfInitialTokens(false ? 1 : 0); // TODO: How can I check if BE is activated? mGspn.addPlace(placeBEActivated); storm::gspn::Place placeBEFailed; - placeBEFailed.setName(name + "_failed"); + placeBEFailed.setName(dftBE->name() + "_failed"); placeBEFailed.setNumberOfInitialTokens(0); mGspn.addPlace(placeBEFailed); storm::gspn::TimedTransition timedTransitionActiveFailure; - timedTransitionActiveFailure.setName(name + "_activeFailure"); + timedTransitionActiveFailure.setName(dftBE->name() + "_activeFailing"); timedTransitionActiveFailure.setPriority(1); - timedTransitionActiveFailure.setRate(activeFailureRate); + timedTransitionActiveFailure.setRate(dftBE->activeFailureRate()); timedTransitionActiveFailure.setInputArcMultiplicity(placeBEActivated, 1); timedTransitionActiveFailure.setInhibitionArcMultiplicity(placeBEFailed, 1); timedTransitionActiveFailure.setOutputArcMultiplicity(placeBEActivated, 1); @@ -159,9 +146,9 @@ namespace storm { mGspn.addTimedTransition(timedTransitionActiveFailure); storm::gspn::TimedTransition timedTransitionPassiveFailure; - timedTransitionPassiveFailure.setName(name + "_passiveFailure"); + timedTransitionPassiveFailure.setName(dftBE->name() + "_passiveFailing"); timedTransitionPassiveFailure.setPriority(1); - timedTransitionPassiveFailure.setRate(passiveFailureRate); + timedTransitionPassiveFailure.setRate(dftBE->passiveFailureRate()); timedTransitionPassiveFailure.setInhibitionArcMultiplicity(placeBEActivated, 1); timedTransitionPassiveFailure.setInhibitionArcMultiplicity(placeBEFailed, 1); timedTransitionPassiveFailure.setOutputArcMultiplicity(placeBEFailed, 1); @@ -169,14 +156,14 @@ namespace storm { } template - void DftToGspnTransformator::drawAND(std::string name) { + void DftToGspnTransformator::drawAND(std::shared_ptr const> dftAnd) { storm::gspn::Place placeANDFailed; - placeANDFailed.setName(name + "_failed"); + placeANDFailed.setName(dftAnd->name() + "_failed"); placeANDFailed.setNumberOfInitialTokens(0); mGspn.addPlace(placeANDFailed); storm::gspn::ImmediateTransition immediateTransitionANDFailing; - immediateTransitionANDFailing.setName(name + "_failing"); + immediateTransitionANDFailing.setName(dftAnd->name() + "_failing"); immediateTransitionANDFailing.setPriority(1); immediateTransitionANDFailing.setWeight(0.0); immediateTransitionANDFailing.setInhibitionArcMultiplicity(placeANDFailed, 1); @@ -185,15 +172,15 @@ namespace storm { } template - void DftToGspnTransformator::drawOR(std::string name, std::size_t numberOfChildren) { + void DftToGspnTransformator::drawOR(std::shared_ptr const> dftOr) { storm::gspn::Place placeORFailed; - placeORFailed.setName(name + "_failed"); + placeORFailed.setName(dftOr->name() + "_failed"); placeORFailed.setNumberOfInitialTokens(0); mGspn.addPlace(placeORFailed); - for (std::size_t i = 0; i < numberOfChildren; i++) { + for (std::size_t i = 0; i < dftOr->nrChildren(); i++) { storm::gspn::ImmediateTransition immediateTransitionORFailing; - immediateTransitionORFailing.setName(name + std::to_string((int)i) + "_failing"); + immediateTransitionORFailing.setName(dftOr->name() + std::to_string((int)i) + "_failing"); immediateTransitionORFailing.setPriority(1); immediateTransitionORFailing.setWeight(0.0); immediateTransitionORFailing.setInhibitionArcMultiplicity(placeORFailed, 1); @@ -201,7 +188,41 @@ namespace storm { mGspn.addImmediateTransition(immediateTransitionORFailing); } } + + template + void DftToGspnTransformator::drawVOT(std::shared_ptr const> dftVot) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The transformation of a VOT is not yet implemented."); + } + template + void DftToGspnTransformator::drawPAND(std::shared_ptr const> dftPand) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The transformation of a PAND is not yet implemented."); + } + + template + void DftToGspnTransformator::drawSPARE(std::shared_ptr const> dftSpare) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The transformation of a SPARE is not yet implemented."); + } + + template + void DftToGspnTransformator::drawPOR(std::shared_ptr const> dftPor) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The transformation of a POR is not yet implemented."); + } + + template + void DftToGspnTransformator::writeGspn(bool toFile) { + if (toFile) { + // Writing to file + std::ofstream file; + file.open("gspn.dot"); + mGspn.writeDotToStream(file); + file.close(); + } else { + // Writing to console + mGspn.writeDotToStream(std::cout); + } + } + // Explicitly instantiate the class. template class DftToGspnTransformator; diff --git a/src/transformations/dft/DftToGspnTransformator.h b/src/transformations/dft/DftToGspnTransformator.h index 33b366648..264541817 100644 --- a/src/transformations/dft/DftToGspnTransformator.h +++ b/src/transformations/dft/DftToGspnTransformator.h @@ -43,30 +43,51 @@ namespace storm { /* * Draw a Petri net Basic Event. * - * @param name The name of the Basic Event. + * @param dftBE The Basic Event. + */ + void drawBE(std::shared_ptr const> dftBE); + + /* + * Draw a Petri net AND. * - * @param activated If true, the Basic Event is activated. If false, the Basic Event - * is inactive, i.e. in a nested SPARE. + * @param dftAnd The AND gate. + */ + void drawAND(std::shared_ptr const> dftAnd); + + /* + * Draw a Petri net OR. * - * @param activeFailureRate The failure rate of the Basic Event, if it is activated. + * @param dftOr The OR gate. + */ + void drawOR(std::shared_ptr const> dftOr); + + /* + * Draw a Petri net VOT. * - * @pparam passiveFailureRate The failure rate of the Basic Event, if it is not activated. + * @param dftVot The VOT gate. */ - void drawBE(std::string name, bool activated, double activeFailureRate, double passiveFailureRate); + void drawVOT(std::shared_ptr const> dftVot); /* - * Draw a Petri net AND. + * Draw a Petri net PAND. * - * @param name The name of the AND. + * @param dftPand The PAND gate. */ - void drawAND(std::string name); + void drawPAND(std::shared_ptr const> dftPand); /* - * Draw a Petri net OR. + * Draw a Petri net SPARE. + * + * @param dftSpare The SPARE gate. + */ + void drawSPARE(std::shared_ptr const> dftSpare); + + /* + * Draw a Petri net POR. * - * @param name The name of the OR. + * @param dftPor The POR gate. */ - void drawOR(std::string name, std::size_t numberOfChildren); + void drawPOR(std::shared_ptr const> dftPor); }; } }