From e322c568207240e1327963c7c42d03b0d232ee17 Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 2 Mar 2016 15:30:00 +0100 Subject: [PATCH 1/2] findModularisationRewrite Former-commit-id: ba948b7720f6742a8ebe2f101f17c422b30b24ab --- src/storage/dft/DFT.cpp | 35 +++++++++++++++++++++++++++++++++++ src/storage/dft/DFT.h | 2 ++ src/storm-dyftee.cpp | 8 ++++++++ 3 files changed, 45 insertions(+) diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index bf68a095c..890e2de25 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -436,6 +436,41 @@ namespace storm { } return DFTIndependentSymmetries(res); } + + template + std::vector DFT::findModularisationRewrite() const { + for(auto const& e : mElements) { + if(e->isGate() && (e->type() == DFTElementType::AND || e->type() == DFTElementType::OR) ) { + // suitable parent gate! - Lets check the independent submodules of the children + auto const& children = std::static_pointer_cast>(e)->children(); + for(auto const& child : children) { + //std::cout << "check idea for: " << child->id() << std::endl;; + auto ISD = std::static_pointer_cast>(child)->independentSubDft(true); + // In the ISD, check for other children: + //std::cout << "** subdft = "; + for(auto const& isdelemid : ISD) { + std::cout << isdelemid << " "; + } + std::cout << std::endl; + + std::vector rewrite = {e->id(), child->id()}; + for(size_t isdElemId : ISD) { + if(isdElemId == child->id()) continue; + if(std::find_if(children.begin(), children.end(), [&isdElemId](std::shared_ptr> const& e) { return e->id() == isdElemId; } ) != children.end()) { + //std::cout << "** found child in subdft: " << isdElemId << std::endl; + rewrite.push_back(isdElemId); + } + } + if(rewrite.size() > 2) { + return rewrite; + } + + } + } + } + return {}; + } + template std::pair, std::vector> DFT::getSortedParentAndOutDepIds(size_t index) const { diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h index 32e807197..75092e479 100644 --- a/src/storage/dft/DFT.h +++ b/src/storage/dft/DFT.h @@ -236,6 +236,8 @@ namespace storm { DFTIndependentSymmetries findSymmetries(DFTColouring const& colouring) const; std::vector immediateFailureCauses(size_t index) const; + + std::vector findModularisationRewrite() const; private: std::pair, std::vector> getSortedParentAndOutDepIds(size_t index) const; diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp index 13b43f5ff..c5997ddd3 100644 --- a/src/storm-dyftee.cpp +++ b/src/storm-dyftee.cpp @@ -29,6 +29,14 @@ void analyzeDFT(std::string filename, std::string property, bool symred = false) std::vector> formulas(parsedFormulas.begin(), parsedFormulas.end()); assert(formulas.size() == 1); std::cout << "Parsed formula." << std::endl; + auto modIdea = dft.findModularisationRewrite(); + std::cout << "Modularisation idea: " << std::endl; + + for( auto const& i : modIdea ) { + std::cout << i << ", "; + } + std::cout << std::endl; + std::map>> emptySymmetry; storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); if(symred) { From a6f8ba37168df42233eb5f33245514cd8d214165 Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 2 Mar 2016 15:30:22 +0100 Subject: [PATCH 2/2] seq examples Former-commit-id: 42c0f279b9c8dee9e8c03f342e42a58cf738ff5b --- examples/dft/seq1.dft | 2 +- examples/dft/seq2.dft | 6 ++++++ examples/dft/seq3.dft | 6 ++++++ examples/dft/seq3.txt | 6 ++++++ examples/dft/seq4.dft | 6 ++++++ examples/dft/seq5.dft | 7 +++++++ examples/dft/seq6.dft | 8 ++++++++ 7 files changed, 40 insertions(+), 1 deletion(-) create mode 100644 examples/dft/seq2.dft create mode 100644 examples/dft/seq3.dft create mode 100644 examples/dft/seq3.txt create mode 100644 examples/dft/seq4.dft create mode 100644 examples/dft/seq5.dft create mode 100644 examples/dft/seq6.dft diff --git a/examples/dft/seq1.dft b/examples/dft/seq1.dft index 8f5459fd2..6fd99bc3b 100644 --- a/examples/dft/seq1.dft +++ b/examples/dft/seq1.dft @@ -1,5 +1,5 @@ toplevel "A"; "A" and "B" "C"; -"X" seq "B" "C"; +"X" seq "B" "C" "B" lambda=0.5 dorm=0.3; "C" lambda=0.5 dorm=0.3; diff --git a/examples/dft/seq2.dft b/examples/dft/seq2.dft new file mode 100644 index 000000000..408d4c26d --- /dev/null +++ b/examples/dft/seq2.dft @@ -0,0 +1,6 @@ +toplevel "A"; +"A" and "B" "C" "D"; +"X" seq "B" "C" "D"; +"B" lambda=0.5 dorm=0.3; +"C" lambda=0.5 dorm=0.3; +"D" lambda=0.5 dorm=0.3; diff --git a/examples/dft/seq3.dft b/examples/dft/seq3.dft new file mode 100644 index 000000000..b22b9e8b6 --- /dev/null +++ b/examples/dft/seq3.dft @@ -0,0 +1,6 @@ +toplevel "A"; +"A" and "C" "D"; +"X" seq "B" "C" "D"; +"B" lambda=0.5 dorm=0.3; +"C" lambda=0.5 dorm=0.3; +"D" lambda=0.5 dorm=0.3; diff --git a/examples/dft/seq3.txt b/examples/dft/seq3.txt new file mode 100644 index 000000000..b22b9e8b6 --- /dev/null +++ b/examples/dft/seq3.txt @@ -0,0 +1,6 @@ +toplevel "A"; +"A" and "C" "D"; +"X" seq "B" "C" "D"; +"B" lambda=0.5 dorm=0.3; +"C" lambda=0.5 dorm=0.3; +"D" lambda=0.5 dorm=0.3; diff --git a/examples/dft/seq4.dft b/examples/dft/seq4.dft new file mode 100644 index 000000000..260a88266 --- /dev/null +++ b/examples/dft/seq4.dft @@ -0,0 +1,6 @@ +toplevel "A"; +"A" or "C" "D"; +"X" seq "B" "C" "D"; +"B" lambda=0.5 dorm=0.3; +"C" lambda=0.5 dorm=0.3; +"D" lambda=0.5 dorm=0.3; diff --git a/examples/dft/seq5.dft b/examples/dft/seq5.dft new file mode 100644 index 000000000..60bf149af --- /dev/null +++ b/examples/dft/seq5.dft @@ -0,0 +1,7 @@ +toplevel "A"; +"A" and "T1" "B3"; +"T1" or "B1" "B2"; +"X" seq "B1" "B2" "B3"; +"B1" lambda=0.5 dorm=0.3; +"B2" lambda=0.5 dorm=0.3; +"B3" lambda=0.5 dorm=0.3; diff --git a/examples/dft/seq6.dft b/examples/dft/seq6.dft new file mode 100644 index 000000000..8453cb411 --- /dev/null +++ b/examples/dft/seq6.dft @@ -0,0 +1,8 @@ +toplevel "A"; +"A" and "T1" "T2"; +"T1" pand "B1" "B2"; +"T2" pand "B3" "B4; +"B1" lambda=0.7 dorm=0.3; +"B2" lambda=0.5 dorm=0.3; +"B3" lambda=0.5 dorm=0.3; +"B4" lambda=0.7 dorm=0.3;