Browse Source

Better debug output

tempestpy_adaptions
Matthias Volk 7 years ago
parent
commit
87edc3abe0
  1. 2
      src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
  2. 6
      src/storm-dft/storage/dft/DFT.cpp

2
src/storm-dft/modelchecker/dft/DFTModelChecker.cpp

@ -202,7 +202,7 @@ namespace storm {
} }
// Build a single CTMC // 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<ValueType> builder(ft, symmetries, enableDC); storm::builder::ExplicitDFTModelBuilder<ValueType> builder(ft, symmetries, enableDC);
typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties); typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties);
builder.buildModel(labeloptions, 0, 0.0); builder.buildModel(labeloptions, 0, 0.0);

6
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."); STORM_LOG_ASSERT(mElements[rewrites[1]]->parents().front()->isGate(), "Rewritten element has no parent gate.");
DFTGatePointer originalParent = std::static_pointer_cast<DFTGate<ValueType>>(mElements[rewrites[1]]->parents().front()); DFTGatePointer originalParent = std::static_pointer_cast<DFTGate<ValueType>>(mElements[rewrites[1]]->parents().front());
std::string newParentName = builder.getUniqueName(originalParent->name()); std::string newParentName = builder.getUniqueName(originalParent->name());
// Accumulate children names // Accumulate children names
std::vector<std::string> childrenNames; std::vector<std::string> childrenNames;
for (size_t i = 1; i < rewrites.size(); ++i) { 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()); childrenNames.push_back(mElements[rewrites[i]]->name());
} }
// Add element inbetween parent and children // Add element inbetween parent and children
switch (originalParent->type()) { switch (originalParent->type()) {
case DFTElementType::AND: case DFTElementType::AND:

Loading…
Cancel
Save