Browse Source

Merge branch 'monolithic-dft' of https://sselab.de/lab9/private/git/storm into monolithic-dft

Former-commit-id: 551931d79a
main
sjunges 9 years ago
parent
commit
ad1dbb95db
  1. 12
      benchmark_dft.py
  2. 6
      src/storage/dft/DFT.cpp
  3. 1
      src/storage/dft/DFTBuilder.cpp

12
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]),

6
src/storage/dft/DFT.cpp

@ -1,6 +1,7 @@
#include <boost/container/flat_set.hpp>
#include "DFT.h"
#include "src/exceptions/NotSupportedException.h"
namespace storm {
namespace storage {
@ -28,7 +29,12 @@ namespace storm {
std::set<size_t> module = {spareReprs->id()};
spareReprs->extendSpareModule(module);
std::vector<size_t> 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()));

1
src/storage/dft/DFTBuilder.cpp

@ -38,6 +38,7 @@ namespace storm {
// Initialize dependencies
for (auto& dependency : mDependencies) {
DFTGatePointer triggerEvent = std::static_pointer_cast<DFTGate<ValueType>>(mElements[dependency->nameTrigger()]);
assert(mElements[dependency->nameDependent()]->isBasicElement());
std::shared_ptr<DFTBE<ValueType>> dependentEvent = std::static_pointer_cast<DFTBE<ValueType>>(mElements[dependency->nameDependent()]);
dependency->initialize(triggerEvent, dependentEvent);
triggerEvent->addDependency(dependency);

Loading…
Cancel
Save