From 87b6182ea3638264ca84304e54f0e3bac2320f59 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 15 Dec 2016 10:53:04 +0100 Subject: [PATCH] build n-ary pdeps for transformation --- src/storm-dft-cli/storm-dyftee.cpp | 2 +- src/storm-dft/parser/DFTGalileoParser.h | 2 +- src/storm-dft/storage/dft/DFTBuilder.cpp | 8 +++++--- src/storm-dft/storage/dft/DFTBuilder.h | 7 +++++-- src/storm-dft/storage/dft/elements/DFTDependency.h | 4 ++-- 5 files changed, 14 insertions(+), 9 deletions(-) diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp index 13f048a55..61959158a 100644 --- a/src/storm-dft-cli/storm-dyftee.cpp +++ b/src/storm-dft-cli/storm-dyftee.cpp @@ -136,7 +136,7 @@ int main(const int argc, const char** argv) { storm::parser::DFTJsonParser parser; dft = std::make_shared>(parser.parseJson(dftSettings.getDftJsonFilename())); } else { - storm::parser::DFTGalileoParser parser; + storm::parser::DFTGalileoParser parser(true, false); dft = std::make_shared>(parser.parseDFT(dftSettings.getDftFilename())); } storm::transformations::dft::DftToGspnTransformator gspnTransformator(*dft); diff --git a/src/storm-dft/parser/DFTGalileoParser.h b/src/storm-dft/parser/DFTGalileoParser.h index 04b822914..c2a35bc50 100644 --- a/src/storm-dft/parser/DFTGalileoParser.h +++ b/src/storm-dft/parser/DFTGalileoParser.h @@ -26,7 +26,7 @@ namespace storm { std::unordered_map identifierMapping; public: - DFTGalileoParser(bool defaultInclusive = true) : builder(defaultInclusive), manager(new storm::expressions::ExpressionManager()), parser(*manager), evaluator(*manager) { + DFTGalileoParser(bool defaultInclusive = true, bool binaryDependencies = true) : builder(defaultInclusive, binaryDependencies), manager(new storm::expressions::ExpressionManager()), parser(*manager), evaluator(*manager) { } storm::storage::DFT parseDFT(std::string const& filename); diff --git a/src/storm-dft/storage/dft/DFTBuilder.cpp b/src/storm-dft/storage/dft/DFTBuilder.cpp index f2a17541a..0bff9bd2b 100644 --- a/src/storm-dft/storage/dft/DFTBuilder.cpp +++ b/src/storm-dft/storage/dft/DFTBuilder.cpp @@ -70,9 +70,11 @@ namespace storm { if (binaryDependencies) { assert(dependencies.size() == 1); } - assert(binaryDependencies); - elem.first->setDependentEvent(dependencies[0]); - dependencies[0]->addIngoingDependency(elem.first); + elem.first->setDependentEvents(dependencies); + for (auto& dependency : dependencies) { + dependency->addIngoingDependency(elem.first); + } + } diff --git a/src/storm-dft/storage/dft/DFTBuilder.h b/src/storm-dft/storage/dft/DFTBuilder.h index 9f216720c..636b5e5a1 100644 --- a/src/storm-dft/storage/dft/DFTBuilder.h +++ b/src/storm-dft/storage/dft/DFTBuilder.h @@ -37,7 +37,7 @@ namespace storm { std::unordered_map mLayoutInfo; public: - DFTBuilder(bool defaultInclusive = true) : pandDefaultInclusive(defaultInclusive), porDefaultInclusive(defaultInclusive) { + DFTBuilder(bool defaultInclusive = true, bool binaryDependencies = true) : pandDefaultInclusive(defaultInclusive), porDefaultInclusive(defaultInclusive), binaryDependencies(binaryDependencies) { } @@ -133,7 +133,10 @@ namespace storm { mDependencies.push_back(element); } } else { - + DFTDependencyPointer element = std::make_shared>(mNextId++, name, probability); + mElements[element->name()] = element; + mDependencyChildNames[element] = children; + mDependencies.push_back(element); } return true; } diff --git a/src/storm-dft/storage/dft/elements/DFTDependency.h b/src/storm-dft/storage/dft/elements/DFTDependency.h index e389f519e..7d11bae2a 100644 --- a/src/storm-dft/storage/dft/elements/DFTDependency.h +++ b/src/storm-dft/storage/dft/elements/DFTDependency.h @@ -29,8 +29,8 @@ namespace storm { } - void setDependentEvent(DFTBEPointer const& dependentEvent) { - mDependentEvents = { dependentEvent }; + void setDependentEvents(std::vector const& dependentEvents) { + mDependentEvents = dependentEvents; }