diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index 0a2d172d8..98ddf3b50 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -171,7 +171,7 @@ void processOptions() { // All events are relevant additionalRelevantEventNames = {"all"}; } - storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents(*dft, props, additionalRelevantEventNames, faultTreeSettings.isAllowDCForRelevantEvents()); + storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents(*dft, props, additionalRelevantEventNames); // Analyze DFT @@ -183,7 +183,7 @@ void processOptions() { if (faultTreeSettings.isApproximationErrorSet()) { approximationError = faultTreeSettings.getApproximationError(); } - storm::api::analyzeDFT(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), relevantEvents, approximationError, faultTreeSettings.getApproximationHeuristic(), transformationSettings.isChainEliminationSet(), transformationSettings.getLabelBehavior(), true); + storm::api::analyzeDFT(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), relevantEvents, faultTreeSettings.isAllowDCForRelevantEvents(), approximationError, faultTreeSettings.getApproximationHeuristic(), transformationSettings.isChainEliminationSet(), transformationSettings.getLabelBehavior(), true); } } diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h index 0535cf280..09188848b 100644 --- a/src/storm-dft/api/storm-dft.h +++ b/src/storm-dft/api/storm-dft.h @@ -125,12 +125,11 @@ namespace storm { * @param dft DFT. * @param properties List of properties. All events occurring in a property are relevant. * @param additionalRelevantEventNames List of names of additional relevant events. - * @param allowDCForRelevant Whether to allow Don't Care propagation for relevant events. * @return Relevant events. */ template - storm::utility::RelevantEvents computeRelevantEvents(storm::storage::DFT const& dft, std::vector> const& properties, std::vector const& additionalRelevantEventNames, bool allowDCForRelevant) { - storm::utility::RelevantEvents events(additionalRelevantEventNames, allowDCForRelevant); + storm::utility::RelevantEvents computeRelevantEvents(storm::storage::DFT const& dft, std::vector> const& properties, std::vector const& additionalRelevantEventNames) { + storm::utility::RelevantEvents events(additionalRelevantEventNames); events.addNamesFromProperty(properties); return events; } @@ -144,6 +143,7 @@ namespace storm { * @param symred Flag whether symmetry reduction should be used. * @param allowModularisation Flag whether modularisation should be applied if possible. * @param relevantEvents Relevant events which should be observed. + * @param allowDCForRelevant Whether to allow Don't Care propagation for relevant events * @param approximationError Allowed approximation error. Value 0 indicates no approximation. * @param approximationHeuristic Heuristic used for state space exploration. * @param eliminateChains If true, chains of non-Markovian states are eliminated from the resulting MA. @@ -153,11 +153,11 @@ namespace storm { */ template typename storm::modelchecker::DFTModelChecker::dft_results - analyzeDFT(storm::storage::DFT const& dft, std::vector> const& properties, bool symred = true, bool allowModularisation = true, storm::utility::RelevantEvents const& relevantEvents = storm::utility::RelevantEvents(), + analyzeDFT(storm::storage::DFT const& dft, std::vector> const& properties, bool symred = true, bool allowModularisation = true, storm::utility::RelevantEvents const& relevantEvents = storm::utility::RelevantEvents(), bool allowDCForRelevant = false, double approximationError = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH, bool eliminateChains = false, storm::transformer::EliminationLabelBehavior labelBehavior = storm::transformer::EliminationLabelBehavior::KeepLabels, bool printOutput = false) { storm::modelchecker::DFTModelChecker modelChecker(printOutput); - typename storm::modelchecker::DFTModelChecker::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, relevantEvents, approximationError, approximationHeuristic, eliminateChains, labelBehavior); + typename storm::modelchecker::DFTModelChecker::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, relevantEvents, allowDCForRelevant, approximationError, approximationHeuristic, eliminateChains, labelBehavior); if (printOutput) { modelChecker.printTimings(); modelChecker.printResults(results); diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index a200563b1..096fa4fed 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -22,7 +22,7 @@ namespace storm { template typename DFTModelChecker::dft_results DFTModelChecker::check(storm::storage::DFT const& origDft, std::vector> const& properties, - bool symred, bool allowModularisation, storm::utility::RelevantEvents const& relevantEvents, + bool symred, bool allowModularisation, storm::utility::RelevantEvents const& relevantEvents, bool allowDCForRelevant, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic, bool eliminateChains, storm::transformer::EliminationLabelBehavior labelBehavior) { totalTimer.start(); @@ -44,14 +44,14 @@ namespace storm { // TODO: distinguish for all properties, not only for first one if (properties[0]->isTimeOperatorFormula() && allowModularisation) { // Use parallel composition as modularisation approach for expected time - std::shared_ptr> model = buildModelViaComposition(dft, properties, symred, true, relevantEvents); + std::shared_ptr> model = buildModelViaComposition(dft, properties, symred, true, relevantEvents, allowDCForRelevant); // Model checking std::vector resultsValue = checkModel(model, properties); for (ValueType result : resultsValue) { results.push_back(result); } } else { - results = checkHelper(dft, properties, symred, allowModularisation, relevantEvents, approximationError, approximationHeuristic, eliminateChains, labelBehavior); + results = checkHelper(dft, properties, symred, allowModularisation, relevantEvents, allowDCForRelevant, approximationError, approximationHeuristic, eliminateChains, labelBehavior); } totalTimer.stop(); return results; @@ -59,7 +59,7 @@ namespace storm { template typename DFTModelChecker::dft_results DFTModelChecker::checkHelper(storm::storage::DFT const& dft, property_vector const& properties, - bool symred, bool allowModularisation, storm::utility::RelevantEvents const& relevantEvents, + bool symred, bool allowModularisation, storm::utility::RelevantEvents const& relevantEvents, bool allowDCForRelevant, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic, bool eliminateChains, storm::transformer::EliminationLabelBehavior labelBehavior) { STORM_LOG_TRACE("Check helper called"); @@ -114,7 +114,7 @@ namespace storm { std::vector res; for (auto const ft : dfts) { // TODO: allow approximation in modularisation - dft_results ftResults = checkHelper(ft, {property}, symred, true, relevantEvents, 0.0); + dft_results ftResults = checkHelper(ft, {property}, symred, true, relevantEvents, allowDCForRelevant, 0.0); STORM_LOG_ASSERT(ftResults.size() == 1, "Wrong number of results"); res.push_back(boost::get(ftResults[0])); } @@ -152,13 +152,13 @@ namespace storm { return results; } else { // No modularisation was possible - return checkDFT(dft, properties, symred, relevantEvents, approximationError, approximationHeuristic, eliminateChains, labelBehavior); + return checkDFT(dft, properties, symred, relevantEvents, allowDCForRelevant, approximationError, approximationHeuristic, eliminateChains, labelBehavior); } } template std::shared_ptr> - DFTModelChecker::buildModelViaComposition(storm::storage::DFT const &dft, property_vector const &properties, bool symred, bool allowModularisation, storm::utility::RelevantEvents const& relevantEvents) { + DFTModelChecker::buildModelViaComposition(storm::storage::DFT const &dft, property_vector const &properties, bool symred, bool allowModularisation, storm::utility::RelevantEvents const& relevantEvents, bool allowDCForRelevant) { // TODO: use approximation? STORM_LOG_TRACE("Build model via composition"); std::vector> dfts; @@ -197,7 +197,7 @@ namespace storm { STORM_LOG_DEBUG("Building Model via parallel composition..."); explorationTimer.start(); - ft.setRelevantEvents(relevantEvents); + ft.setRelevantEvents(relevantEvents, allowDCForRelevant); // Find symmetries std::map>> emptySymmetry; storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); @@ -259,7 +259,7 @@ namespace storm { // No composition was possible explorationTimer.start(); - dft.setRelevantEvents(relevantEvents); + dft.setRelevantEvents(relevantEvents, allowDCForRelevant); // Find symmetries std::map>> emptySymmetry; @@ -289,13 +289,13 @@ namespace storm { template typename DFTModelChecker::dft_results - DFTModelChecker::checkDFT(storm::storage::DFT const &dft, property_vector const &properties, bool symred, storm::utility::RelevantEvents const& relevantEvents, + DFTModelChecker::checkDFT(storm::storage::DFT const &dft, property_vector const &properties, bool symred, storm::utility::RelevantEvents const& relevantEvents, bool allowDCForRelevant, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic, bool eliminateChains, storm::transformer::EliminationLabelBehavior labelBehavior) { explorationTimer.start(); auto ioSettings = storm::settings::getModule(); auto dftIOSettings = storm::settings::getModule(); - dft.setRelevantEvents(relevantEvents); + dft.setRelevantEvents(relevantEvents, allowDCForRelevant); // Find symmetries std::map>> emptySymmetry; diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.h b/src/storm-dft/modelchecker/dft/DFTModelChecker.h index 4c61655fa..71a5c8fdf 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.h @@ -48,13 +48,15 @@ namespace storm { * @param symred Flag whether symmetry reduction should be used. * @param allowModularisation Flag indicating if modularisation is allowed. * @param relevantEvents Relevant events which should be observed. + * @param allowDCForRelevant Whether to allow Don't Care propagation for relevant events * @param approximationError Error allowed for approximation. Value 0 indicates no approximation. * @param approximationHeuristic Heuristic used for state space exploration. * @param eliminateChains If true, chains of non-Markovian states are elimianted from the resulting MA * @param labelBehavior Behavior of labels of eliminated states * @return Model checking results for the given properties.. */ - dft_results check(storm::storage::DFT const& origDft, property_vector const& properties, bool symred = true, bool allowModularisation = true, storm::utility::RelevantEvents const& relevantEvents = storm::utility::RelevantEvents(), + dft_results check(storm::storage::DFT const& origDft, property_vector const& properties, bool symred = true, bool allowModularisation = true, + storm::utility::RelevantEvents const& relevantEvents = storm::utility::RelevantEvents(), bool allowDCForRelevant = false, double approximationError = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH, bool eliminateChains = false, storm::transformer::EliminationLabelBehavior labelBehavior = storm::transformer::EliminationLabelBehavior::KeepLabels); @@ -92,13 +94,15 @@ namespace storm { * @param symred Flag indicating if symmetry reduction should be used. * @param allowModularisation Flag indicating if modularisation is allowed. * @param relevantEvents Relevant events which should be observed. + * @param allowDCForRelevant Whether to allow Don't Care propagation for relevant events * @param approximationError Error allowed for approximation. Value 0 indicates no approximation. * @param approximationHeuristic Heuristic used for approximation. * @param eliminateChains If true, chains of non-Markovian states are elimianted from the resulting MA * @param labelBehavior Behavior of labels of eliminated states * @return Model checking results (or in case of approximation two results for lower and upper bound) */ - dft_results checkHelper(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, storm::utility::RelevantEvents const& relevantEvents, + dft_results checkHelper(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, + storm::utility::RelevantEvents const& relevantEvents, bool allowDCForRelevant = false, double approximationError = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH, bool eliminateChains = false, storm::transformer::EliminationLabelBehavior labelBehavior = storm::transformer::EliminationLabelBehavior::KeepLabels); @@ -109,10 +113,16 @@ namespace storm { * @param properties Properties to check for. * @param symred Flag indicating if symmetry reduction should be used. * @param allowModularisation Flag indicating if modularisation is allowed. - * @param relevantEvents List with ids of relevant events which should be observed. + * @param relevantEvents Relevant events which should be observed. + * @param allowDCForRelevant Whether to allow Don't Care propagation for relevant events * @return CTMC representing the DFT */ - std::shared_ptr> buildModelViaComposition(storm::storage::DFT const& dft, property_vector const& properties, bool symred, bool allowModularisation, storm::utility::RelevantEvents const& relevantEvents); + std::shared_ptr> buildModelViaComposition(storm::storage::DFT const& dft, + property_vector const& properties, + bool symred, + bool allowModularisation, + storm::utility::RelevantEvents const& relevantEvents, + bool allowDCForRelevant); /*! * Check model generated from DFT. @@ -120,7 +130,8 @@ namespace storm { * @param dft The DFT. * @param properties Properties to check for. * @param symred Flag indicating if symmetry reduction should be used. - * @param relevantEvents List with ids of relevant events which should be observed. + * @param relevantEvents Relevant events which should be observed. + * @param allowDCForRelevant Whether to allow Don't Care propagation for relevant events * @param approximationError Error allowed for approximation. Value 0 indicates no approximation. * @param approximationHeuristic Heuristic used for approximation. * @param eliminateChains If true, chains of non-Markovian states are elimianted from the resulting MA @@ -128,7 +139,7 @@ namespace storm { * * @return Model checking result */ - dft_results checkDFT(storm::storage::DFT const& dft, property_vector const& properties, bool symred, storm::utility::RelevantEvents const& relevantEvents, + dft_results checkDFT(storm::storage::DFT const& dft, property_vector const& properties, bool symred, storm::utility::RelevantEvents const& relevantEvents, bool allowDCForRelevant, double approximationError = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH, bool eliminateChains = false, storm::transformer::EliminationLabelBehavior labelBehavior = storm::transformer::EliminationLabelBehavior::KeepLabels); diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index 5496e5476..c309d7439 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -1039,7 +1039,7 @@ namespace storm { } template - void DFT::setRelevantEvents(storm::utility::RelevantEvents const& relevantEvents) const { + void DFT::setRelevantEvents(storm::utility::RelevantEvents const& relevantEvents, bool const allowDCForRelevant) const { mRelevantEvents.clear(); STORM_LOG_THROW(relevantEvents.checkRelevantNames(*this), storm::exceptions::InvalidArgumentException, "One of the relevant elements does not exist."); // Top level element is first element @@ -1047,7 +1047,7 @@ namespace storm { for (auto& elem : mElements) { if (relevantEvents.isRelevant(elem->name()) || elem->id() == this->getTopLevelIndex()) { elem->setRelevance(true); - elem->setAllowDC(relevantEvents.isAllowDC()); + elem->setAllowDC(allowDCForRelevant); if (elem->id() != this->getTopLevelIndex()) { // Top level element was already added mRelevantEvents.push_back(elem->id()); diff --git a/src/storm-dft/storage/dft/DFT.h b/src/storm-dft/storage/dft/DFT.h index db0704ee9..62fb6dd4b 100644 --- a/src/storm-dft/storage/dft/DFT.h +++ b/src/storm-dft/storage/dft/DFT.h @@ -378,8 +378,9 @@ namespace storm { /*! * Set the relevance flag for all elements according to the given relevant events. * @param relevantEvents All elements which should be to relevant. All elements not occurring are set to irrelevant. + * @param allowDCForRelevant Whether to allow Don't Care propagation for relevant events */ - void setRelevantEvents(storm::utility::RelevantEvents const& relevantEvents) const; + void setRelevantEvents(storm::utility::RelevantEvents const& relevantEvents, bool const allowDCForRelevant) const; /*! * Get a string containing the list of all relevant events. diff --git a/src/storm-dft/utility/RelevantEvents.h b/src/storm-dft/utility/RelevantEvents.h index 4e07d4e26..40627dbc1 100644 --- a/src/storm-dft/utility/RelevantEvents.h +++ b/src/storm-dft/utility/RelevantEvents.h @@ -19,9 +19,8 @@ namespace storm { * If name 'all' occurs, all elements are stored as relevant. * * @param relevantEvents List of relevant event names. - * @param allowDCForRelevant Whether to allow Don't Care propagation for relevant events. */ - RelevantEvents(std::vector const& relevantEvents = {}, bool allowDCForRelevant = false) : names(), allRelevant(false), allowDC(allowDCForRelevant) { + RelevantEvents(std::vector const& relevantEvents = {}) : names(), allRelevant(false) { for (auto const& name: relevantEvents) { if (name == "all") { this->allRelevant = true; @@ -95,10 +94,6 @@ namespace storm { } } - bool isAllowDC() const { - return this->allowDC; - } - private: /*! @@ -115,9 +110,6 @@ namespace storm { // Whether all elements are relevant. bool allRelevant; - - // Whether to allow Don't Care propagation for relevant events. - bool allowDC; }; } // namespace utility diff --git a/src/test/storm-dft/api/DftApproximationTest.cpp b/src/test/storm-dft/api/DftApproximationTest.cpp index 70778c653..e7377c33d 100644 --- a/src/test/storm-dft/api/DftApproximationTest.cpp +++ b/src/test/storm-dft/api/DftApproximationTest.cpp @@ -57,7 +57,7 @@ namespace { EXPECT_TRUE(storm::api::isWellFormed(*dft).first); std::string property = "T=? [F \"failed\"]"; std::vector> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property)); - typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFT(*dft, properties, config.useSR, false, storm::utility::RelevantEvents(), errorBound, config.heuristic, false); + typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFT(*dft, properties, config.useSR, false, storm::utility::RelevantEvents(), false, errorBound, config.heuristic, false); return boost::get::approximation_result>(results[0]); } @@ -67,7 +67,7 @@ namespace { std::stringstream propertyStream; propertyStream << "P=? [F<=" << timeBound << " \"failed\"]"; std::vector > properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(propertyStream.str())); - typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFT(*dft, properties, config.useSR, false, storm::utility::RelevantEvents(), errorBound, config.heuristic, false); + typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFT(*dft, properties, config.useSR, false, storm::utility::RelevantEvents(), false, errorBound, config.heuristic, false); return boost::get::approximation_result>(results[0]); } diff --git a/src/test/storm-dft/api/DftModelBuildingTest.cpp b/src/test/storm-dft/api/DftModelBuildingTest.cpp index 71c6351e1..96c5e9f93 100644 --- a/src/test/storm-dft/api/DftModelBuildingTest.cpp +++ b/src/test/storm-dft/api/DftModelBuildingTest.cpp @@ -18,8 +18,8 @@ namespace { storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); // Set relevant events (none) - storm::utility::RelevantEvents relevantEvents({}, false); - dft->setRelevantEvents(relevantEvents); + storm::utility::RelevantEvents relevantEvents{}; + dft->setRelevantEvents(relevantEvents, false); // Build model storm::builder::ExplicitDFTModelBuilder builder(*dft, symmetries); builder.buildModel(0, 0.0); @@ -28,8 +28,8 @@ namespace { EXPECT_EQ(13ul, model->getNumberOfTransitions()); // Set relevant events (all) - relevantEvents = storm::utility::RelevantEvents({"all"}, false); - dft->setRelevantEvents(relevantEvents); + relevantEvents = storm::utility::RelevantEvents({"all"}); + dft->setRelevantEvents(relevantEvents, false); // Build model storm::builder::ExplicitDFTModelBuilder builder2(*dft, symmetries); builder2.buildModel(0, 0.0); @@ -38,8 +38,8 @@ namespace { EXPECT_EQ(2305ul, model->getNumberOfTransitions()); // Set relevant events (H) - relevantEvents = storm::utility::RelevantEvents({"H"}, false); - dft->setRelevantEvents(relevantEvents); + relevantEvents = storm::utility::RelevantEvents({"H"}); + dft->setRelevantEvents(relevantEvents, false); // Build model storm::builder::ExplicitDFTModelBuilder builder3(*dft, symmetries); builder3.buildModel(0, 0.0); @@ -49,8 +49,8 @@ namespace { // Set relevant events (H, I) - relevantEvents = storm::utility::RelevantEvents({"H", "I"}, false); - dft->setRelevantEvents(relevantEvents); + relevantEvents = storm::utility::RelevantEvents({"H", "I"}); + dft->setRelevantEvents(relevantEvents, false); // Build model storm::builder::ExplicitDFTModelBuilder builder4(*dft, symmetries); builder4.buildModel(0, 0.0); @@ -59,8 +59,8 @@ namespace { EXPECT_EQ(33ul, model->getNumberOfTransitions()); // Set relevant events (none) - relevantEvents = storm::utility::RelevantEvents({}, true); - dft->setRelevantEvents(relevantEvents); + relevantEvents = storm::utility::RelevantEvents{}; + dft->setRelevantEvents(relevantEvents, true); // Build model storm::builder::ExplicitDFTModelBuilder builder5(*dft, symmetries); builder5.buildModel(0, 0.0); @@ -69,8 +69,8 @@ namespace { EXPECT_EQ(13ul, model->getNumberOfTransitions()); // Set relevant events (all) - relevantEvents = storm::utility::RelevantEvents({"all"}, true); - dft->setRelevantEvents(relevantEvents); + relevantEvents = storm::utility::RelevantEvents({"all"}); + dft->setRelevantEvents(relevantEvents, true); // Build model storm::builder::ExplicitDFTModelBuilder builder6(*dft, symmetries); builder6.buildModel(0, 0.0); @@ -80,8 +80,8 @@ namespace { // Set relevant events (H, I) - relevantEvents = storm::utility::RelevantEvents({"H", "I"}, true); - dft->setRelevantEvents(relevantEvents); + relevantEvents = storm::utility::RelevantEvents({"H", "I"}); + dft->setRelevantEvents(relevantEvents, true); // Build model storm::builder::ExplicitDFTModelBuilder builder7(*dft, symmetries); builder7.buildModel(0, 0.0); diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp index 9eb7145ea..bb2d45d72 100644 --- a/src/test/storm-dft/api/DftModelCheckerTest.cpp +++ b/src/test/storm-dft/api/DftModelCheckerTest.cpp @@ -86,10 +86,10 @@ namespace { if (!config.useDC) { relevantNames.push_back("all"); } - storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents(*dft, properties, relevantNames, false); + storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents(*dft, properties, relevantNames); // Perform model checking - typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFT(*dft, properties, config.useSR, config.useMod, relevantEvents); + typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFT(*dft, properties, config.useSR, config.useMod, relevantEvents, false); return boost::get(results[0]); } diff --git a/src/test/storm-dft/simulator/DftSimulatorTest.cpp b/src/test/storm-dft/simulator/DftSimulatorTest.cpp index 1932f292e..296a58dc1 100644 --- a/src/test/storm-dft/simulator/DftSimulatorTest.cpp +++ b/src/test/storm-dft/simulator/DftSimulatorTest.cpp @@ -18,8 +18,8 @@ namespace { EXPECT_TRUE(storm::api::isWellFormed(*dft).first); // Set relevant events - storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents(*dft, {}, {}, false); - dft->setRelevantEvents(relevantEvents); + storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents(*dft, {}, {}); + dft->setRelevantEvents(relevantEvents, false); // Find symmetries std::map>> emptySymmetry; diff --git a/src/test/storm-dft/simulator/DftTraceGeneratorTest.cpp b/src/test/storm-dft/simulator/DftTraceGeneratorTest.cpp index 7ace25f11..d695b83c8 100644 --- a/src/test/storm-dft/simulator/DftTraceGeneratorTest.cpp +++ b/src/test/storm-dft/simulator/DftTraceGeneratorTest.cpp @@ -78,8 +78,8 @@ namespace { if (!config.useDC) { relevantNames.push_back("all"); } - storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents(*dft, {}, relevantNames, false); - dft->setRelevantEvents(relevantEvents); + storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents(*dft, {}, relevantNames); + dft->setRelevantEvents(relevantEvents, false); // Find symmetries std::map>> emptySymmetry;