diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index 619754ba1..9a2546eae 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -90,46 +90,25 @@ void processOptions() { dft = storm::api::applyTransformations(*dft, faultTreeSettings.isUniqueFailedBE(), true); STORM_LOG_DEBUG(dft->getElementsString()); - - dft->setDynamicBehaviorInfo(); - - storm::api::PreprocessingResult preResults; + // Compute minimal number of BE failures leading to system failure and + // maximal number of BE failures not leading to system failure yet. // TODO: always needed? - preResults.lowerBEBound = storm::dft::utility::FailureBoundFinder::getLeastFailureBound(*dft, useSMT, solverTimeout); - preResults.upperBEBound = storm::dft::utility::FailureBoundFinder::getAlwaysFailedBound(*dft, useSMT, solverTimeout); - STORM_LOG_DEBUG("BE failure bounds" << std::endl << "========================================" << std::endl << - "Lower bound: " << std::to_string(preResults.lowerBEBound) << std::endl << - "Upper bound: " << std::to_string(preResults.upperBEBound)); + auto bounds = storm::api::computeBEFailureBounds(*dft, useSMT, solverTimeout); + STORM_LOG_DEBUG("BE failure bounds: lower bound: " << bounds.first << ", upper bound: " << bounds.second << "."); - // TODO: move into API call? - preResults.fdepConflicts = storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, useSMT, solverTimeout); - - if (preResults.fdepConflicts.empty()) { - STORM_LOG_DEBUG("No FDEP conflicts found"); + // Check which FDEPs actually introduce conflicts which need non-deterministic resolution + bool hasConflicts = storm::api::computeDependencyConflicts(*dft, useSMT, solverTimeout); + if (hasConflicts) { + STORM_LOG_DEBUG("FDEP conflicts found."); } else { - STORM_LOG_DEBUG("========================================" << std::endl << "FDEP CONFLICTS" << std::endl << "========================================"); - } - for (auto pair: preResults.fdepConflicts) { - STORM_LOG_DEBUG("Conflict between " << dft->getElement(pair.first)->name() << " and " << dft->getElement(pair.second)->name()); - } - - // Set the conflict map of the dft - std::set conflict_set; - for (auto conflict : preResults.fdepConflicts) { - conflict_set.insert(size_t(conflict.first)); - conflict_set.insert(size_t(conflict.second)); - } - for (size_t depId : dft->getDependencies()) { - if (!conflict_set.count(depId)) { - dft->setDependencyNotInConflict(depId); - } + STORM_LOG_DEBUG("No FDEP conflicts found."); } #ifdef STORM_HAVE_Z3 if (useSMT) { // Solve with SMT - STORM_LOG_DEBUG("Running DFT analysis with use of SMT"); + STORM_LOG_DEBUG("Running DFT analysis with use of SMT."); // Set dynamic behavior vector storm::api::analyzeDFTSMT(*dft, true); } diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h index bfe90f37a..a14d7d2c7 100644 --- a/src/storm-dft/api/storm-dft.h +++ b/src/storm-dft/api/storm-dft.h @@ -18,12 +18,6 @@ namespace storm { namespace api { - struct PreprocessingResult { - uint64_t lowerBEBound; - uint64_t upperBEBound; - std::vector> fdepConflicts; - }; - /*! * Load DFT from Galileo file. @@ -93,29 +87,36 @@ namespace storm { return transformedDFT; } - template - bool computeDependencyConflicts(storm::storage::DFT const& dft, bool useSMT, double solverTimeout) { - std::vector> fdepConflicts = storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, useSMT, solverTimeout); + template + std::pair computeBEFailureBounds(storm::storage::DFT const& dft, bool useSMT, double solverTimeout) { + uint64_t lowerBEBound = storm::dft::utility::FailureBoundFinder::getLeastFailureBound(dft, useSMT, solverTimeout); + uint64_t upperBEBound = storm::dft::utility::FailureBoundFinder::getAlwaysFailedBound(dft, useSMT, solverTimeout); + return std::make_pair(lowerBEBound, upperBEBound); + } - if (fdepConflicts.empty()) { - return false; - } - for (auto pair: fdepConflicts) { + template + bool computeDependencyConflicts(storm::storage::DFT& dft, bool useSMT, double solverTimeout) { + // Initialize which DFT elements have dynamic behavior + dft.setDynamicBehaviorInfo(); + + std::vector> fdepConflicts = storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(dft, useSMT, solverTimeout); + + for (auto const& pair: fdepConflicts) { STORM_LOG_DEBUG("Conflict between " << dft.getElement(pair.first)->name() << " and " << dft.getElement(pair.second)->name()); } // Set the conflict map of the dft std::set conflict_set; - for (auto conflict : fdepConflicts) { + for (auto const& conflict : fdepConflicts) { conflict_set.insert(size_t(conflict.first)); conflict_set.insert(size_t(conflict.second)); } - for (size_t depId : dft->getDependencies()) { + for (size_t depId : dft.getDependencies()) { if (!conflict_set.count(depId)) { - dft->setDependencyNotInConflict(depId); + dft.setDependencyNotInConflict(depId); } } - return true; + return !fdepConflicts.empty(); } /*! diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index d1c46cbed..956805544 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -34,19 +34,18 @@ namespace storm { } template - ExplicitDFTModelBuilder::ExplicitDFTModelBuilder(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, std::set const& relevantEvents, bool allowDCForRelevantEvents) : + ExplicitDFTModelBuilder::ExplicitDFTModelBuilder(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries) : dft(dft), stateGenerationInfo(std::make_shared(dft.buildStateGenerationInfo(symmetries))), - relevantEvents(relevantEvents), generator(dft, *stateGenerationInfo), matrixBuilder(!generator.isDeterministicModel()), stateStorage(dft.stateBitVectorSize()), explorationQueue(1, 0, 0.9, false) { // Set relevant events - this->dft.setRelevantEvents(this->relevantEvents, allowDCForRelevantEvents); STORM_LOG_DEBUG("Relevant events: " << this->dft.getRelevantEventsString()); - if (this->relevantEvents.empty()) { + if (dft.getRelevantEvents().size() <= 1) { + STORM_LOG_ASSERT(dft.getRelevantEvents()[0] == dft.getTopLevelIndex(), "TLE is not relevant"); // Only interested in top level event -> introduce unique failed state this->uniqueFailedState = true; STORM_LOG_DEBUG("Using unique failed state with id 0."); diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.h b/src/storm-dft/builder/ExplicitDFTModelBuilder.h index a8090a83f..410a1de4d 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.h +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.h @@ -155,10 +155,8 @@ namespace storm { * * @param dft DFT. * @param symmetries Symmetries in the dft. - * @param relevantEvents List with ids of relevant events which should be observed. - * @param allowDCForRelevantEvents If true, Don't Care propagation is allowed even for relevant events. */ - ExplicitDFTModelBuilder(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, std::set const& relevantEvents, bool allowDCForRelevantEvents); + ExplicitDFTModelBuilder(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries); /*! * Build model from DFT. @@ -291,9 +289,6 @@ namespace storm { // TODO: use const reference std::shared_ptr stateGenerationInfo; - // List with ids of relevant events which should be observed. - std::set const& relevantEvents; - // Heuristic used for approximation storm::builder::ApproximationHeuristic usedHeuristic; diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 00907ca7a..fb52401d6 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -207,6 +207,7 @@ namespace storm { STORM_LOG_DEBUG("Building Model via parallel composition..."); explorationTimer.start(); + ft.setRelevantEvents(relevantEvents, allowDCForRelevantEvents); // Find symmetries std::map>> emptySymmetry; storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); @@ -219,7 +220,7 @@ namespace storm { // Build a single CTMC STORM_LOG_DEBUG("Building Model from DFT with top level element " << ft.getElement(ft.getTopLevelIndex())->toString() << " ..."); - storm::builder::ExplicitDFTModelBuilder builder(ft, symmetries, relevantEvents, allowDCForRelevantEvents); + storm::builder::ExplicitDFTModelBuilder builder(ft, symmetries); builder.buildModel(0, 0.0); std::shared_ptr> model = builder.getModel(); explorationTimer.stop(); @@ -267,6 +268,9 @@ namespace storm { } else { // No composition was possible explorationTimer.start(); + + dft.setRelevantEvents(relevantEvents, allowDCForRelevantEvents); + // Find symmetries std::map>> emptySymmetry; storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); @@ -279,8 +283,7 @@ namespace storm { // Build a single CTMC STORM_LOG_DEBUG("Building Model..."); - storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, relevantEvents, - allowDCForRelevantEvents); + storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries); builder.buildModel(0, 0.0); std::shared_ptr> model = builder.getModel(); if (printInfo) { @@ -306,6 +309,8 @@ namespace storm { auto ioSettings = storm::settings::getModule(); auto dftIOSettings = storm::settings::getModule(); + dft.setRelevantEvents(relevantEvents, allowDCForRelevantEvents); + // Find symmetries std::map>> emptySymmetry; storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); @@ -324,8 +329,7 @@ namespace storm { storm::utility::zero()); std::shared_ptr> model; std::vector newResult; - storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, relevantEvents, - allowDCForRelevantEvents); + storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries); // TODO: compute approximation for all properties simultaneously? std::shared_ptr property = properties[0]; @@ -422,8 +426,7 @@ namespace storm { // Build a single Markov Automaton auto ioSettings = storm::settings::getModule(); STORM_LOG_DEBUG("Building Model..."); - storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, relevantEvents, - allowDCForRelevantEvents); + storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries); builder.buildModel(0, 0.0); std::shared_ptr> model = builder.getModel(); if (eliminateChains && model->isOfType(storm::models::ModelType::MarkovAutomaton)) { diff --git a/src/storm-dft/parser/DFTGalileoParser.cpp b/src/storm-dft/parser/DFTGalileoParser.cpp index 9e7e5f146..6fd0ec390 100644 --- a/src/storm-dft/parser/DFTGalileoParser.cpp +++ b/src/storm-dft/parser/DFTGalileoParser.cpp @@ -148,7 +148,7 @@ namespace storm { ValueType probability = valueParser.parseValue(type.substr(5)); success = builder.addDepElement(name, childNames, probability); } else if (type.find("=") != std::string::npos) { - success = parseBasicElement(name, line, lineNo, builder, valueParser); + success = parseBasicElement(tokens[0], line, lineNo, builder, valueParser); } else if (type.find("insp") != std::string::npos) { // Inspection as defined by DFTCalc STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Inspections (defined in line " << lineNo << ") are not supported."); diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index 75d43eb47..570ba9fa5 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -799,6 +799,11 @@ namespace storm { bool sharedSpareMode = false; std::map bijection; + if (getElement(index1)->isRelevant() || getElement(index2)->isRelevant()) { + // Relevant events need to be uniquely identified and cannot be symmetric. + return {}; + } + if (isBasicElement(index1)) { if (!isBasicElement(index2)) { return {}; diff --git a/src/storm-dft/storage/dft/DFTIsomorphism.h b/src/storm-dft/storage/dft/DFTIsomorphism.h index 701082443..8d35f2529 100644 --- a/src/storm-dft/storage/dft/DFTIsomorphism.h +++ b/src/storm-dft/storage/dft/DFTIsomorphism.h @@ -57,16 +57,16 @@ namespace storage { BEColourClass() = default; - BEColourClass(storm::storage::BEType t, ValueType a, ValueType p, size_t h) : type(t), hash(h), aRate(a), pRate(p) { - STORM_LOG_ASSERT(t == storm::storage::BEType::EXPONENTIAL, "Expected type EXPONENTIAL but got type " << t); + BEColourClass(storm::storage::BEType type, ValueType active, ValueType passive, size_t parents) : type(type), nrParents(parents), aRate(active), pRate(passive) { + STORM_LOG_ASSERT(type == storm::storage::BEType::EXPONENTIAL, "Expected type EXPONENTIAL but got type " << type); } - BEColourClass(storm::storage::BEType t, bool fail, size_t h) : type(t), hash(h), failed(fail) { - STORM_LOG_ASSERT(t == storm::storage::BEType::CONSTANT, "Expected type CONSTANT but got type " << t); + BEColourClass(storm::storage::BEType type, bool fail, size_t parents) : type(type), nrParents(parents), failed(fail) { + STORM_LOG_ASSERT(type == storm::storage::BEType::CONSTANT, "Expected type CONSTANT but got type " << type); } storm::storage::BEType type; - size_t hash; + size_t nrParents; ValueType aRate; ValueType pRate; bool failed; @@ -80,9 +80,9 @@ namespace storage { } switch (lhs.type) { case storm::storage::BEType::EXPONENTIAL: - return lhs.hash == rhs.hash && lhs.aRate == rhs.aRate && lhs.pRate == rhs.pRate; + return lhs.nrParents == rhs.nrParents && lhs.aRate == rhs.aRate && lhs.pRate == rhs.pRate; case storm::storage::BEType::CONSTANT: - return lhs.hash == rhs.hash && lhs.failed == rhs.failed; + return lhs.nrParents == rhs.nrParents && lhs.failed == rhs.failed; default: STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "BE of type '" << lhs.type << "' is not known."); break; @@ -491,7 +491,12 @@ namespace storage { // We can skip BEs, as they are identified by they're homomorphic if they are in the same class for(auto const& indexpair : bijection) { // Check type first. Colouring takes care of a lot, but not necesarily everything (e.g. voting thresholds) - equalType(*dft.getElement(indexpair.first), *dft.getElement(indexpair.second)); + if (!equalType(*dft.getElement(indexpair.first), *dft.getElement(indexpair.second))) { + return false; + } + if (dft.getElement(indexpair.first)->isRelevant() || dft.getElement(indexpair.second)->isRelevant()) { + return false; + } if(dft.isGate(indexpair.first)) { STORM_LOG_ASSERT(dft.isGate(indexpair.second), "Element is no gate."); auto const& lGate = dft.getGate(indexpair.first); @@ -699,22 +704,25 @@ namespace std { template struct hash> { size_t operator()(storm::storage::BEColourClass const& bcc) const { - constexpr uint_fast64_t fivebitmask = (1 << 6) - 1; - constexpr uint_fast64_t eightbitmask = (1 << 9) - 1; + constexpr uint_fast64_t fivebitmask = (1ul << 6) - 1ul; + constexpr uint_fast64_t eightbitmask = (1ul << 9) - 1ul; + constexpr uint_fast64_t fortybitmask = (1ul << 41) - 1ul; std::hash hasher; uint_fast64_t groupHash = static_cast(1) << 63; groupHash |= (static_cast(bcc.type) & fivebitmask) << (62 - 5); switch (bcc.type) { case storm::storage::BEType::CONSTANT: - return (bcc.failed << 8); + groupHash |= (static_cast(bcc.failed) & fortybitmask) << 8; + break; case storm::storage::BEType::EXPONENTIAL: - return (hasher(bcc.aRate) ^ hasher(bcc.pRate) << 8); + groupHash |= ((hasher(bcc.aRate) ^ hasher(bcc.pRate)) & fortybitmask) << 8; + break; default: STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "BE of type '" << bcc.type << "' is not known."); break; } - groupHash |= static_cast(bcc.hash) & eightbitmask; + groupHash |= static_cast(bcc.nrParents) & eightbitmask; return groupHash; } }; diff --git a/src/storm-dft/utility/FDEPConflictFinder.cpp b/src/storm-dft/utility/FDEPConflictFinder.cpp index eb4447ffb..3b29c0976 100644 --- a/src/storm-dft/utility/FDEPConflictFinder.cpp +++ b/src/storm-dft/utility/FDEPConflictFinder.cpp @@ -25,29 +25,29 @@ namespace storm { if (dft.getDynamicBehavior()[dep1Index] && dft.getDynamicBehavior()[dep2Index]) { if (useSMT) { // if an SMT solver is to be used if (dft.getDependency(dep1Index)->triggerEvent() == dft.getDependency(dep2Index)->triggerEvent()) { - STORM_LOG_DEBUG("Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name() << ": Same trigger"); + STORM_LOG_TRACE("Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name() << ": Same trigger"); res.emplace_back(std::pair(dep1Index, dep2Index)); } else { switch (smtChecker->checkDependencyConflict(dep1Index, dep2Index, timeout)) { case storm::solver::SmtSolver::CheckResult::Sat: - STORM_LOG_DEBUG("Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); + STORM_LOG_TRACE("Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); res.emplace_back(std::pair(dep1Index, dep2Index)); break; case storm::solver::SmtSolver::CheckResult::Unknown: - STORM_LOG_DEBUG("Unknown: Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); + STORM_LOG_TRACE("Unknown: Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); res.emplace_back(std::pair(dep1Index, dep2Index)); break; default: - STORM_LOG_DEBUG("No conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); + STORM_LOG_TRACE("No conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); break; } } } else { - STORM_LOG_DEBUG("Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); + STORM_LOG_TRACE("Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); res.emplace_back(std::pair(dep1Index, dep2Index)); } } else { - STORM_LOG_DEBUG("Static behavior: No conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); + STORM_LOG_TRACE("Static behavior: No conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); break; } } @@ -70,10 +70,10 @@ namespace storm { for (size_t j = i + 1; j < dft.getDependencies().size(); ++j) { dep2Index = dft.getDependencies().at(j); if (dft.getDynamicBehavior()[dep1Index] && dft.getDynamicBehavior()[dep2Index]) { - STORM_LOG_DEBUG("Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); + STORM_LOG_TRACE("Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); res.emplace_back(std::pair(dep1Index, dep2Index)); } else { - STORM_LOG_DEBUG("Static behavior: No conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); + STORM_LOG_TRACE("Static behavior: No conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); break; } } @@ -88,4 +88,4 @@ namespace storm { class FDEPConflictFinder; } } -} \ No newline at end of file +} diff --git a/src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp b/src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp index 4c77bc3a2..e272d27ec 100644 --- a/src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp +++ b/src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp @@ -88,7 +88,8 @@ namespace storm { if (name.compare("name") == 0) { builder.setGspnName(storm::adapters::XMLtoString(attr->getNodeValue())); } else if (name.compare("show-color-cmd") == 0 || - name.compare("show-fluid-cmd") == 0) { + name.compare("show-fluid-cmd") == 0 || + name.compare("zoom") == 0) { // ignore node } else { // Found node or attribute which is at the moment not handled by this parser. diff --git a/src/test/storm-dft/api/DftModelBuildingTest.cpp b/src/test/storm-dft/api/DftModelBuildingTest.cpp index 51bcec6bc..7837fe793 100644 --- a/src/test/storm-dft/api/DftModelBuildingTest.cpp +++ b/src/test/storm-dft/api/DftModelBuildingTest.cpp @@ -19,17 +19,18 @@ namespace { // Set relevant events (none) std::set relevantEvents; + dft->setRelevantEvents(relevantEvents, false); // Build model - storm::builder::ExplicitDFTModelBuilder builder(*dft, symmetries, relevantEvents, false); + storm::builder::ExplicitDFTModelBuilder builder(*dft, symmetries); builder.buildModel(0, 0.0); std::shared_ptr> model = builder.getModel(); EXPECT_EQ(8ul, model->getNumberOfStates()); EXPECT_EQ(13ul, model->getNumberOfTransitions()); // Set relevant events (all) - relevantEvents = dft->getAllIds(); + dft->setRelevantEvents(dft->getAllIds(), false); // Build model - storm::builder::ExplicitDFTModelBuilder builder2(*dft, symmetries, relevantEvents, false); + storm::builder::ExplicitDFTModelBuilder builder2(*dft, symmetries); builder2.buildModel(0, 0.0); model = builder2.getModel(); EXPECT_EQ(512ul, model->getNumberOfStates()); @@ -38,8 +39,9 @@ namespace { // Set relevant events (H) relevantEvents.clear(); relevantEvents.insert(dft->getIndex("H")); + dft->setRelevantEvents(relevantEvents, false); // Build model - storm::builder::ExplicitDFTModelBuilder builder3(*dft, symmetries, relevantEvents, false); + storm::builder::ExplicitDFTModelBuilder builder3(*dft, symmetries); builder3.buildModel(0, 0.0); model = builder3.getModel(); EXPECT_EQ(12ul, model->getNumberOfStates()); @@ -50,8 +52,9 @@ namespace { relevantEvents.clear(); relevantEvents.insert(dft->getIndex("H")); relevantEvents.insert(dft->getIndex("I")); + dft->setRelevantEvents(relevantEvents, false); // Build model - storm::builder::ExplicitDFTModelBuilder builder4(*dft, symmetries, relevantEvents, false); + storm::builder::ExplicitDFTModelBuilder builder4(*dft, symmetries); builder4.buildModel(0, 0.0); model = builder4.getModel(); EXPECT_EQ(16ul, model->getNumberOfStates()); @@ -59,17 +62,18 @@ namespace { // Set relevant events (none) relevantEvents.clear(); + dft->setRelevantEvents(relevantEvents, true); // Build model - storm::builder::ExplicitDFTModelBuilder builder5(*dft, symmetries, relevantEvents, true); + storm::builder::ExplicitDFTModelBuilder builder5(*dft, symmetries); builder5.buildModel(0, 0.0); model = builder5.getModel(); EXPECT_EQ(8ul, model->getNumberOfStates()); EXPECT_EQ(13ul, model->getNumberOfTransitions()); // Set relevant events (all) - relevantEvents = dft->getAllIds(); + dft->setRelevantEvents(dft->getAllIds(), true); // Build model - storm::builder::ExplicitDFTModelBuilder builder6(*dft, symmetries, relevantEvents, true); + storm::builder::ExplicitDFTModelBuilder builder6(*dft, symmetries); builder6.buildModel(0, 0.0); model = builder6.getModel(); EXPECT_EQ(8ul, model->getNumberOfStates()); @@ -80,13 +84,13 @@ namespace { relevantEvents.clear(); relevantEvents.insert(dft->getIndex("H")); relevantEvents.insert(dft->getIndex("I")); + dft->setRelevantEvents(relevantEvents, true); // Build model - storm::builder::ExplicitDFTModelBuilder builder7(*dft, symmetries, relevantEvents, true); + storm::builder::ExplicitDFTModelBuilder builder7(*dft, symmetries); builder7.buildModel(0, 0.0); model = builder7.getModel(); EXPECT_EQ(8ul, model->getNumberOfStates()); EXPECT_EQ(13ul, model->getNumberOfTransitions()); - } }