From 5655766d36dd9e3d285bda206590e24f8c2364a3 Mon Sep 17 00:00:00 2001 From: Mavo Date: Wed, 17 Feb 2016 11:44:08 +0100 Subject: [PATCH 1/2] Small changes Former-commit-id: cc2a75289e633e71a3c590309939d70bdfe416c0 --- benchmark_dft.py | 12 ++++++------ src/storage/dft/DFTBuilder.cpp | 1 + 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/benchmark_dft.py b/benchmark_dft.py index 77880d951..6f25e08ed 100644 --- a/benchmark_dft.py +++ b/benchmark_dft.py @@ -13,13 +13,13 @@ EXAMPLE_DIR=os.path.join(DIR, "examples/dft/") benchmarks = [ ("and", False, [3, 1]), ("and_param", True, ["(4*x^2+2*x+1)/((x) * (2*x+1))", "1"]), - ("cardiac", False, [11378, 1]), + ("cardiac", False, [8597.360004, 1]), ("cas", False, [0.859736, 1]), ("cm2", False, [0.256272, 1]), - #("cm4", False, [0, 1]), + #("cm4", False, [0.338225, 1]), # big ("cps", False, ["inf", 0.333333]), - ("deathegg", False, [46.667, 1]), - ("fdep", False, [0.666667, 1]), + #("deathegg", False, [24.642857, 1]), # contains fdep to gate + #("fdep", False, [0.666667, 1]), # contains fdep to two elements ("fdep2", False, [2, 1]), ("fdep3", False, [2.5, 1]), #("ftpp_complex", False, [0, 1]), # Compute @@ -32,13 +32,13 @@ benchmarks = [ ("pand", False, ["inf", 0.666667]), ("pand_param", True, ["-1", "(x)/(y+x)"]), ("pdep", False, [2.66667, 1]), - ("pdep2", False, [0, 1]), #Compute + #("pdep2", False, [0, 1]), #Compute # contains pdep to two elements ("pdep3", False, [2.79167, 1]), ("spare", False, [3.53846, 1]), ("spare2", False, [1.86957, 1]), ("spare3", False, [1.27273, 1]), ("spare4", False, [4.8459, 1]), - ("spare5", False, [2.66667, 1]), # We discard the result 2.16667 from DFTCalc + ("spare5", False, [2.66667, 1]), ("spare6", False, [1.4, 1]), ("spare7", False, [3.67333, 1]), ("symmetry", False, [4.16667, 1]), diff --git a/src/storage/dft/DFTBuilder.cpp b/src/storage/dft/DFTBuilder.cpp index 13ed7d7b0..f35a09f0f 100644 --- a/src/storage/dft/DFTBuilder.cpp +++ b/src/storage/dft/DFTBuilder.cpp @@ -38,6 +38,7 @@ namespace storm { // Initialize dependencies for (auto& dependency : mDependencies) { DFTGatePointer triggerEvent = std::static_pointer_cast>(mElements[dependency->nameTrigger()]); + assert(mElements[dependency->nameDependent()]->isBasicElement()); std::shared_ptr> dependentEvent = std::static_pointer_cast>(mElements[dependency->nameDependent()]); dependency->initialize(triggerEvent, dependentEvent); triggerEvent->addDependency(dependency); From b51d997d5b545acb0d3a6fff9b1ffc83250907c2 Mon Sep 17 00:00:00 2001 From: Mavo Date: Wed, 17 Feb 2016 14:31:35 +0100 Subject: [PATCH 2/2] Detect error with more than one spare in a module Former-commit-id: a0812aa201fce62906f0d1ac054678476f101377 --- src/storage/dft/DFT.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index 83e287b3b..a23a70f71 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -1,6 +1,7 @@ #include #include "DFT.h" +#include "src/exceptions/NotSupportedException.h" namespace storm { namespace storage { @@ -28,7 +29,12 @@ namespace storm { std::set module = {spareReprs->id()}; spareReprs->extendSpareModule(module); std::vector sparesAndBes; + bool secondSpare = false; for(auto const& modelem : module) { + if (mElements[modelem]->isSpareGate()) { + STORM_LOG_THROW(!secondSpare, storm::exceptions::NotSupportedException, "Module for '" << spareReprs->name() << "' contains more than one spare."); + secondSpare = true; + } if(mElements[modelem]->isSpareGate() || mElements[modelem]->isBasicElement()) { sparesAndBes.push_back(modelem); mRepresentants.insert(std::make_pair(modelem, spareReprs->id()));