diff --git a/src/storm-dft/parser/DFTJsonParser.cpp b/src/storm-dft/parser/DFTJsonParser.cpp index 4bedbe7ac..2a1f3f1ac 100644 --- a/src/storm-dft/parser/DFTJsonParser.cpp +++ b/src/storm-dft/parser/DFTJsonParser.cpp @@ -49,7 +49,7 @@ namespace storm { template void DFTJsonParser::readFile(const std::string& filename) { - std::cout << "Parsing from JSON" << std::endl; + STORM_LOG_DEBUG("Parsing from JSON"); std::ifstream file; file.exceptions ( std::ifstream::failbit ); @@ -81,8 +81,6 @@ namespace storm { std::string toplevelId = nameMapping["1"]; for (auto& element : parsedJson) { - std::cout << element << std::endl; - bool success = true; if (element.at("classes") == "") { continue; @@ -124,10 +122,11 @@ namespace storm { success = false; } + // Set layout positions json position = element.at("position"); double x = position.at("x"); double y = position.at("y"); - builder.addLayoutInfo(name, x, y); + builder.addLayoutInfo(name, x / 10, y / 10); STORM_LOG_THROW(success, storm::exceptions::FileIoException, "Error while adding element '" << element << "'."); } diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp index 868ab652c..176ed3254 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.cpp +++ b/src/storm-dft/transformations/DftToGspnTransformator.cpp @@ -90,9 +90,7 @@ namespace storm { template void DftToGspnTransformator::drawBE(std::shared_ptr const> dftBE, bool isRepresentative) { - double xcenter = mDft.getElementLayoutInfo(dftBE->id()).x; - double ycenter = mDft.getElementLayoutInfo(dftBE->id()).y; - uint64_t beActive = builder.addPlace(defaultCapacity, isBEActive(dftBE) ? 1 : 0, dftBE->name() + STR_ACTIVATED); + uint64_t beActive = builder.addPlace(defaultCapacity, isBEActive(dftBE) ? 1 : 0, dftBE->name() + STR_ACTIVATED); activeNodes.emplace(dftBE->id(), beActive); uint64_t beFailed = builder.addPlace(defaultCapacity, 0, dftBE->name() + STR_FAILED); @@ -127,7 +125,10 @@ namespace storm { builder.addOutputArc(tActive, unavailableNode); builder.addOutputArc(tPassive, unavailableNode); } - + + double xcenter = mDft.getElementLayoutInfo(dftBE->id()).x; + double ycenter = mDft.getElementLayoutInfo(dftBE->id()).y; + builder.setPlaceLayoutInfo(beActive, storm::gspn::LayoutInfo(xcenter - 3.0, ycenter)); builder.setPlaceLayoutInfo(beFailed, storm::gspn::LayoutInfo(xcenter + 3.0, ycenter)); builder.setTransitionLayoutInfo(tActive, storm::gspn::LayoutInfo(xcenter, ycenter + 3.0)); @@ -137,8 +138,6 @@ namespace storm { template void DftToGspnTransformator::drawAND(std::shared_ptr const> dftAnd, bool isRepresentative) { - double xcenter = mDft.getElementLayoutInfo(dftAnd->id()).x; - double ycenter = mDft.getElementLayoutInfo(dftAnd->id()).y; uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftAnd->name() + STR_FAILED); assert(failedNodes.size() == dftAnd->id()); failedNodes.push_back(nodeFailed); @@ -160,7 +159,10 @@ namespace storm { builder.addInputArc(failedNodes[child->id()], tAndFailed); builder.addOutputArc(tAndFailed, failedNodes[child->id()]); } - + + double xcenter = mDft.getElementLayoutInfo(dftAnd->id()).x; + double ycenter = mDft.getElementLayoutInfo(dftAnd->id()).y; + builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter, ycenter-3.0)); builder.setTransitionLayoutInfo(tAndFailed, storm::gspn::LayoutInfo(xcenter, ycenter+3.0)); @@ -171,6 +173,11 @@ namespace storm { uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftOr->name() + STR_FAILED); assert(failedNodes.size() == dftOr->id()); failedNodes.push_back(nodeFailed); + + double xcenter = mDft.getElementLayoutInfo(dftOr->id()).x; + double ycenter = mDft.getElementLayoutInfo(dftOr->id()).y; + builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter, ycenter-3.0)); + uint64_t unavailableNode = 0; if (isRepresentative) { unavailableNode = addUnavailableNode(dftOr); @@ -188,6 +195,7 @@ namespace storm { builder.addInputArc(failedNodes[child->id()], tNodeFailed); builder.addOutputArc(tNodeFailed, failedNodes[child->id()]); ++i; + builder.setTransitionLayoutInfo(tNodeFailed, storm::gspn::LayoutInfo(xcenter-5+i*3, ycenter+3.0)); } } @@ -228,6 +236,11 @@ namespace storm { uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftPand->name() + STR_FAILED); assert(failedNodes.size() == dftPand->id()); failedNodes.push_back(nodeFailed); + + double xcenter = mDft.getElementLayoutInfo(dftPand->id()).x; + double ycenter = mDft.getElementLayoutInfo(dftPand->id()).y; + builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter, ycenter-3.0)); + uint64_t unavailableNode = 0; if (!smart || isRepresentative) { unavailableNode = addUnavailableNode(dftPand);