diff --git a/src/transformations/dft/DftToGspnTransformator.cpp b/src/transformations/dft/DftToGspnTransformator.cpp index db5d930ec..53efdbde0 100644 --- a/src/transformations/dft/DftToGspnTransformator.cpp +++ b/src/transformations/dft/DftToGspnTransformator.cpp @@ -16,8 +16,6 @@ namespace storm { mGspn = storm::gspn::GSPN(); mGspn.setName("DftToGspnTransformation"); - // TODO: Reconsider priorities! - // Loop through every DFT element and draw them as a GSPN. drawGSPNElements(); @@ -77,7 +75,6 @@ namespace storm { break; case storm::storage::DFTElementType::PDEP: drawPDEP(std::static_pointer_cast const>(dftElement)); - //STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The transformation of a PDEP is not yet implemented."); break; default: STORM_LOG_ASSERT(false, "DFT type unknown."); @@ -403,22 +400,22 @@ namespace storm { } case storm::storage::DFTElementType::MUTEX: { - // MUTEX is not implemented yet. Nothing to do here. + // MUTEX are realized with restrictions. Nothing to do here. break; } case storm::storage::DFTElementType::BE: { - // The parent is never a Basic Event (Except for SPAREs?). + // The parent is never a Basic Event. break; } case storm::storage::DFTElementType::CONSTF: { - // The parent is never a Basic Event (Except for SPAREs?). + // The parent is never a Basic Event. break; } case storm::storage::DFTElementType::CONSTS: { - // The parent is never a Basic Event (Except for SPAREs?). + // The parent is never a Basic Event. break; } case storm::storage::DFTElementType::PDEP: @@ -525,7 +522,6 @@ namespace storm { } } } - // TODO: Does the DEP has a parent? } template @@ -570,10 +566,14 @@ namespace storm { } break; } + case storm::storage::DFTElementType::MUTEX: + { + // MUTEX is not implemented by the DFTGalileoParser yet. Nothing to do here. + STORM_LOG_ASSERT(false, "MUTEX is not supported by DftToGspnTransformator."); + break; + } default: { - // TODO: Are there other restrictions than SEQ? - // TODO: There is: MUTEX. break; } } diff --git a/src/transformations/dft/DftToGspnTransformator.h b/src/transformations/dft/DftToGspnTransformator.h index babbcfce9..eb1bdc8f3 100644 --- a/src/transformations/dft/DftToGspnTransformator.h +++ b/src/transformations/dft/DftToGspnTransformator.h @@ -63,7 +63,7 @@ namespace storm { void drawGSPNDependencies(); /* - * Draw restrictions between the elements of the GSPN (i.e. SEQ). + * Draw restrictions between the elements of the GSPN (i.e. SEQ or MUTEX). */ void drawGSPNRestrictions();