diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 997113bd2..a1887a4ba 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -202,7 +202,7 @@ namespace storm { } // Build a single CTMC - STORM_LOG_DEBUG("Building Model..."); + STORM_LOG_DEBUG("Building Model from DFT with top level element " << ft.getElement(ft.getTopLevelIndex())->toString() << " ..."); storm::builder::ExplicitDFTModelBuilder builder(ft, symmetries, enableDC); typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties); builder.buildModel(labeloptions, 0, 0.0); diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index ad89354f3..e9ed0267b 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -328,14 +328,14 @@ namespace storm { STORM_LOG_ASSERT(mElements[rewrites[1]]->parents().front()->isGate(), "Rewritten element has no parent gate."); DFTGatePointer originalParent = std::static_pointer_cast>(mElements[rewrites[1]]->parents().front()); std::string newParentName = builder.getUniqueName(originalParent->name()); - + // Accumulate children names std::vector childrenNames; for (size_t i = 1; i < rewrites.size(); ++i) { - STORM_LOG_ASSERT(mElements[rewrites[i]]->parents().front()->id() == originalParent->id(), "Children have the same father"); + STORM_LOG_ASSERT(mElements[rewrites[i]]->parents().front()->id() == originalParent->id(), "Children have not the same father for rewrite " << mElements[rewrites[i]]->name()); childrenNames.push_back(mElements[rewrites[i]]->name()); } - + // Add element inbetween parent and children switch (originalParent->type()) { case DFTElementType::AND: