Browse Source

even more modularisation oppurtunaties are now taken

Former-commit-id: de8fd4c848
tempestpy_adaptions
sjunges 9 years ago
parent
commit
d688296022
  1. 5
      src/modelchecker/DFTAnalyser.h
  2. 4
      src/storage/dft/DFT.cpp

5
src/modelchecker/DFTAnalyser.h

@ -21,15 +21,14 @@ class DFTAnalyser {
std::chrono::duration<double> totalTime = std::chrono::duration<double>::zero();
ValueType checkResult = storm::utility::zero<ValueType>();
public:
void check(storm::storage::DFT<ValueType> dft , std::shared_ptr<const storm::logic::Formula> const& formula, bool symred = true, bool allowModularisation = true, bool enableDC = true) {
void check(storm::storage::DFT<ValueType> const& origDft , std::shared_ptr<const storm::logic::Formula> const& formula, bool symred = true, bool allowModularisation = true, bool enableDC = true) {
// Building DFT
std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
// Optimizing DFT
dft = dft.optimize();
std::vector<storm::storage::DFT<ValueType>> dfts;
storm::storage::DFT<ValueType> dft = origDft.optimize();
checkResult = checkHelper(dft, formula, symred, allowModularisation, enableDC);
totalTime = std::chrono::high_resolution_clock::now() - totalStart;

4
src/storage/dft/DFT.cpp

@ -255,6 +255,7 @@ namespace storm {
for(auto const& child : children) {
std::vector<size_t> isubdft;
if(child->nrParents() > 1 || child->hasOutgoingDependencies()) {
STORM_LOG_TRACE("child " << child->name() << "does not allow modularisation.");
return {*this};
}
if (isGate(child->id())) {
@ -262,7 +263,10 @@ namespace storm {
} else {
assert(isBasicElement(child->id()));
if(getBasicElement(child->id())->hasIngoingDependencies()) {
STORM_LOG_TRACE("child " << child->name() << "does not allow modularisation.");
return {*this};
} else {
isubdft = {child->id()};
}
}
Loading…
Cancel
Save