From cec37005ae946f3f594db6ba46d3c939b0a2506b Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 10 Aug 2020 17:37:14 +0200 Subject: [PATCH] Set relevant DFT elements earlier in code --- .../builder/ExplicitDFTModelBuilder.cpp | 7 +++--- .../builder/ExplicitDFTModelBuilder.h | 7 +----- .../modelchecker/dft/DFTModelChecker.cpp | 17 +++++++------ .../storm-dft/api/DftModelBuildingTest.cpp | 24 +++++++++++-------- 4 files changed, 28 insertions(+), 27 deletions(-) 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/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()); - } }