Adapted GSPN output

Former-commit-id: 1106962695

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) {

src/transformations/dft/DftToGspnTransformator.cpp

@@ -1,5 +1,6 @@
 #include "src/transformations/dft/DftToGspnTransformator.h"
 #include "src/exceptions/NotImplementedException.h"
+#include <memory>
 
 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<storm::storage::DFTAnd<ValueType> const>(dftElement));
 							break;
 						case storm::storage::DFTElementType::OR:
-							drawOR(dftElement->name(), 2); // TODO: set parameters correctly.
+							drawOR(std::static_pointer_cast<storm::storage::DFTOr<ValueType> 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<storm::storage::DFTVot<ValueType> 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<storm::storage::DFTPand<ValueType> 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<storm::storage::DFTSpare<ValueType> 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<storm::storage::DFTPor<ValueType> 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<storm::storage::DFTBE<ValueType> 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 <typename ValueType>
-            void DftToGspnTransformator<ValueType>::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 <typename ValueType>
-            void DftToGspnTransformator<ValueType>::drawBE(std::string name, bool activated, double activeFailureRate, double passiveFailureRate) {
+            void DftToGspnTransformator<ValueType>::drawBE(std::shared_ptr<storm::storage::DFTBE<ValueType> 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<double> 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<double> 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 <typename ValueType>
-            void DftToGspnTransformator<ValueType>::drawAND(std::string name) {
+            void DftToGspnTransformator<ValueType>::drawAND(std::shared_ptr<storm::storage::DFTAnd<ValueType> const> dftAnd) {
 				storm::gspn::Place placeANDFailed;
-				placeANDFailed.setName(name + "_failed");
+				placeANDFailed.setName(dftAnd->name() + "_failed");
 				placeANDFailed.setNumberOfInitialTokens(0);
 				mGspn.addPlace(placeANDFailed);
 				
 				storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> 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 <typename ValueType>
-            void DftToGspnTransformator<ValueType>::drawOR(std::string name, std::size_t numberOfChildren) {
+            void DftToGspnTransformator<ValueType>::drawOR(std::shared_ptr<storm::storage::DFTOr<ValueType> 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<storm::gspn::GSPN::WeightType> 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 <typename ValueType>
+            void DftToGspnTransformator<ValueType>::drawVOT(std::shared_ptr<storm::storage::DFTVot<ValueType> const> dftVot) {
+				STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The transformation of a VOT is not yet implemented.");
+			}
 
+			template <typename ValueType>
+            void DftToGspnTransformator<ValueType>::drawPAND(std::shared_ptr<storm::storage::DFTPand<ValueType> const> dftPand) {
+				STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The transformation of a PAND is not yet implemented.");
+			}
+			
+			template <typename ValueType>
+            void DftToGspnTransformator<ValueType>::drawSPARE(std::shared_ptr<storm::storage::DFTSpare<ValueType> const> dftSpare) {
+				STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The transformation of a SPARE is not yet implemented.");
+			}
+			
+			template <typename ValueType>
+            void DftToGspnTransformator<ValueType>::drawPOR(std::shared_ptr<storm::storage::DFTPor<ValueType> const> dftPor) {
+				STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The transformation of a POR is not yet implemented.");
+			}
+			
+			template <typename ValueType>
+            void DftToGspnTransformator<ValueType>::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<double>;
 

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<storm::storage::DFTBE<ValueType> 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<storm::storage::DFTAnd<ValueType> 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<storm::storage::DFTOr<ValueType> 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<storm::storage::DFTVot<ValueType> 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<storm::storage::DFTPand<ValueType> const> dftPand);
 				
 				/*
-				 * Draw a Petri net OR.
+				 * Draw a Petri net SPARE.
+				 * 
+				 * @param dftSpare The SPARE gate.
+				 */
+				void drawSPARE(std::shared_ptr<storm::storage::DFTSpare<ValueType> 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<storm::storage::DFTPor<ValueType> const> dftPor);
             };
         }
     }