From eeff4d2e2ff2bc17aa2f3d5a248f37c4e141e513 Mon Sep 17 00:00:00 2001
From: mdeutschen <michael.deutschen@rwth-aachen.de>
Date: Thu, 18 Aug 2016 15:24:12 +0200
Subject: [PATCH] Implemented MUTEX dummy

Former-commit-id: 65e7777bb0c9a4708c055480aef3046d22615792
---
 src/transformations/dft/DftToGspnTransformator.cpp | 12 ++++++++++--
 src/transformations/dft/DftToGspnTransformator.h   |  7 +++++++
 2 files changed, 17 insertions(+), 2 deletions(-)

diff --git a/src/transformations/dft/DftToGspnTransformator.cpp b/src/transformations/dft/DftToGspnTransformator.cpp
index b9e984f62..133d7793f 100644
--- a/src/transformations/dft/DftToGspnTransformator.cpp
+++ b/src/transformations/dft/DftToGspnTransformator.cpp
@@ -59,7 +59,7 @@ namespace storm {
 							// No method call needed here. SEQ only consists of restrictions, which are handled later.
 							break;
 						case storm::storage::DFTElementType::MUTEX:
-							STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The transformation of a MUTEX is not yet implemented.");
+							drawMUTEX(dftElement);
 							break;
 						case storm::storage::DFTElementType::BE:
 							drawBE(std::static_pointer_cast<storm::storage::DFTBE<ValueType> const>(dftElement));
@@ -84,7 +84,7 @@ namespace storm {
             void DftToGspnTransformator<ValueType>::drawBE(std::shared_ptr<storm::storage::DFTBE<ValueType> const> dftBE) {
 				storm::gspn::Place placeBEActivated;
 				placeBEActivated.setName(dftBE->name() + "_activated");
-				placeBEActivated.setNumberOfInitialTokens(false ? 1 : 0); // TODO: Check if BE is spare child of a SPARE.
+				placeBEActivated.setNumberOfInitialTokens(true ? 1 : 0); // TODO: Check if BE is spare child of a SPARE.
 				mGspn.addPlace(placeBEActivated);
 				
 				storm::gspn::Place placeBEFailed;
@@ -235,6 +235,11 @@ namespace storm {
 				// TODO: Extend for more than 2 children.
 			}
 			
+			template <typename ValueType>
+            void DftToGspnTransformator<ValueType>::drawMUTEX(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftMutex) {				
+				// TODO: Not implemented because there is no corresponding MUTEX element yet.
+			}
+			
 			template <typename ValueType>
             void DftToGspnTransformator<ValueType>::drawCONSTF(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftConstF) {
 				storm::gspn::Place placeCONSTFFailed;
@@ -361,7 +366,10 @@ namespace storm {
 								break;
 							}
 							case storm::storage::DFTElementType::MUTEX:
+							{
+								// MUTEX is not implemented yet. Nothing to do here.
 								break;
+							}
 							case storm::storage::DFTElementType::BE:
 							{
 								// The parent is never a Basic Event (Except for SPAREs?).
diff --git a/src/transformations/dft/DftToGspnTransformator.h b/src/transformations/dft/DftToGspnTransformator.h
index 579879792..338ec622f 100644
--- a/src/transformations/dft/DftToGspnTransformator.h
+++ b/src/transformations/dft/DftToGspnTransformator.h
@@ -111,6 +111,13 @@ namespace storm {
 				 */
 				void drawPOR(std::shared_ptr<storm::storage::DFTPor<ValueType> const> dftPor);
 				
+				/*
+				 * Draw a Petri net MUTEX.
+				 * 
+				 * @param dftMutex The MUTEX gate.
+				 */
+				void drawMUTEX(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftMutex);
+				
 				/*
 				 * Draw a Petri net CONSTF (Constant Failure, a Basic Event that has already failed).
 				 *