From fb2f55d8049e38f8bcfb764ca99493963d2c3f9f Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 25 Jan 2021 20:14:42 +0100 Subject: [PATCH 01/13] Fixed bug where POR was changed to PAND during transformation to binary FDEPs --- src/storm-dft/transformations/DftTransformator.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm-dft/transformations/DftTransformator.cpp b/src/storm-dft/transformations/DftTransformator.cpp index ea62a686c..3cd52c11a 100644 --- a/src/storm-dft/transformations/DftTransformator.cpp +++ b/src/storm-dft/transformations/DftTransformator.cpp @@ -150,7 +150,7 @@ namespace storm { } case storm::storage::DFTElementType::POR: { auto por = std::static_pointer_cast const>(element); - builder.addPandElement(por->name(), getChildrenVector(por), por->isInclusive()); + builder.addPorElement(por->name(), getChildrenVector(por), por->isInclusive()); break; } case storm::storage::DFTElementType::SPARE: From 344ba353e05c22737ce651576f2c516064b050f6 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 25 Jan 2021 20:50:48 +0100 Subject: [PATCH 02/13] Use template for DFTTraceSimulator --- src/storm-dft/simulator/DFTTraceSimulator.cpp | 14 +++++++++++++- src/storm-dft/simulator/DFTTraceSimulator.h | 2 +- 2 files changed, 14 insertions(+), 2 deletions(-) diff --git a/src/storm-dft/simulator/DFTTraceSimulator.cpp b/src/storm-dft/simulator/DFTTraceSimulator.cpp index fd0af4b14..eae3a004c 100644 --- a/src/storm-dft/simulator/DFTTraceSimulator.cpp +++ b/src/storm-dft/simulator/DFTTraceSimulator.cpp @@ -67,12 +67,18 @@ namespace storm { smallestTimebound = timebound; } } - STORM_LOG_TRACE("Let BE " << *nextFail.getFailBE(dft).first << "fail after time " << smallestTimebound); + STORM_LOG_TRACE("Let BE " << *nextFail.getFailBE(dft).first << " fail after time " << smallestTimebound); bool res = step(nextFail); return res ? smallestTimebound : -1; } } + template<> + double DFTTraceSimulator::randomStep() { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Simulation not support for parametric DFTs."); + } + + template bool DFTTraceSimulator::step(storm::dft::storage::FailableElements::const_iterator nextFailElement) { if (nextFailElement == state->getFailableElements().end()) { @@ -116,9 +122,15 @@ namespace storm { } // Time is up return false; + } + + template<> + bool DFTTraceSimulator::simulateCompleteTrace(double timebound) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Simulation not support for parametric DFTs."); } template class DFTTraceSimulator; + template class DFTTraceSimulator; } } } diff --git a/src/storm-dft/simulator/DFTTraceSimulator.h b/src/storm-dft/simulator/DFTTraceSimulator.h index ac54d87a4..7f9203207 100644 --- a/src/storm-dft/simulator/DFTTraceSimulator.h +++ b/src/storm-dft/simulator/DFTTraceSimulator.h @@ -83,7 +83,7 @@ namespace storm { storm::storage::DFTStateGenerationInfo const& stateGenerationInfo; // Generator for creating next state in DFT - storm::generator::DftNextStateGenerator generator; + storm::generator::DftNextStateGenerator generator; // Current state DFTStatePointer state; From 6c025f13d2e2ff096d728a628bce49f7e8b2c805 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 25 Jan 2021 20:55:57 +0100 Subject: [PATCH 03/13] Added more tests for DFT simulation --- resources/examples/testfiles/dft/fdep6.dft | 11 +++ .../storm-dft/simulator/DftSimulatorTest.cpp | 72 ++++++++++++++++++- 2 files changed, 82 insertions(+), 1 deletion(-) create mode 100644 resources/examples/testfiles/dft/fdep6.dft diff --git a/resources/examples/testfiles/dft/fdep6.dft b/resources/examples/testfiles/dft/fdep6.dft new file mode 100644 index 000000000..033b73198 --- /dev/null +++ b/resources/examples/testfiles/dft/fdep6.dft @@ -0,0 +1,11 @@ +toplevel "A"; +"A" and "B" "C"; +"B" lambda=1; +"C" lambda=1; +"F1" fdep "O" "B"; +"F2" fdep "O" "C"; +"O" or "S" "T"; +"S" or "T" "D"; +"T" or "E"; +"D" lambda=2; +"E" lambda=4; diff --git a/src/test/storm-dft/simulator/DftSimulatorTest.cpp b/src/test/storm-dft/simulator/DftSimulatorTest.cpp index 9826c8ae3..3bc92bb7f 100644 --- a/src/test/storm-dft/simulator/DftSimulatorTest.cpp +++ b/src/test/storm-dft/simulator/DftSimulatorTest.cpp @@ -41,9 +41,79 @@ namespace { return (double) count / noRuns; } - TEST(DftSimulatorTest, And) { + TEST(DftSimulatorTest, AndUnreliability) { double result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/and.dft", 2, 10000); EXPECT_NEAR(result, 0.3995764009, 0.01); } + TEST(DftSimulatorTest, OrUnreliability) { + double result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/or.dft", 1, 10000); + EXPECT_NEAR(result, 0.6321205588, 0.01); + } + + TEST(DftSimulatorTest, VotingUnreliability) { + double result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/voting.dft", 1, 10000); + EXPECT_NEAR(result, 0.4511883639, 0.01); + result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/voting2.dft", 1, 10000); + EXPECT_NEAR(result, 0.8173164759, 0.01); + result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/voting3.dft", 1, 10000); + EXPECT_NEAR(result, 0.3496529873, 0.01); + result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/voting4.dft", 1, 10000); + EXPECT_NEAR(result, 0.693568287, 0.01); + } + + TEST(DftSimulatorTest, PandUnreliability) { + double result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/pand.dft", 1, 10000); + EXPECT_NEAR(result, 0.03087312562, 0.01); + } + + TEST(DftSimulatorTest, PorUnreliability) { + double result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/por.dft", 1, 10000); + EXPECT_NEAR(result, 0.2753355179, 0.01); + } + + TEST(DftSimulatorTest, FdepUnreliability) { + double result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/fdep.dft", 1, 10000); + EXPECT_NEAR(result, 0.7768698399, 0.01); + result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/fdep2.dft", 1, 10000); + EXPECT_NEAR(result, 0.3934693403, 0.01); + result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/fdep3.dft", 1, 10000); + EXPECT_NEAR(result, 0.329679954, 0.01); + result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/fdep4.dft", 1, 10000); + EXPECT_NEAR(result, 0.601280086, 0.01); + result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/fdep5.dft", 1, 10000); + EXPECT_NEAR(result, 0.1548181217, 0.01); + result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/fdep6.dft", 1, 10000); + EXPECT_NEAR(result, 0.9985116987, 0.01); + } + + TEST(DftSimulatorTest, SpareUnreliability) { + double result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/spare.dft", 1, 10000); + EXPECT_NEAR(result, 0.1118530638, 0.01); + result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/spare2.dft", 1, 10000); + EXPECT_NEAR(result, 0.2905027469, 0.01); + result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/spare3.dft", 1, 10000); + EXPECT_NEAR(result, 0.4660673246, 0.01); + result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/spare4.dft", 1, 10000); + EXPECT_NEAR(result, 0.01273070783, 0.01); + result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/spare5.dft", 1, 10000); + EXPECT_NEAR(result, 0.2017690905, 0.01); + result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/spare6.dft", 1, 10000); + EXPECT_NEAR(result, 0.4693712702, 0.01); + result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/spare7.dft", 1, 10000); + EXPECT_NEAR(result, 0.06108774525, 0.01); + result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/spare8.dft", 1, 10000); + EXPECT_NEAR(result, 0.02686144489, 0.01); + } + + TEST(DftSimulatorTest, SymmetryUnreliability) { + double result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/symmetry6.dft", 1, 10000); + EXPECT_NEAR(result, 0.3421934224, 0.01); + } + + TEST(DftSimulatorTest, HecsUnreliability) { + double result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/hecs_2_2.dft", 1, 10000); + EXPECT_NEAR(result, 0.00021997582, 0.001); + } + } From 9e3e2c02fe80421bc03151e2afc8881bc1993d30 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 8 Feb 2021 12:28:20 +0100 Subject: [PATCH 04/13] Handle PDEP in createSuccessorState as well --- .../generator/DftNextStateGenerator.cpp | 17 +++++++++++++---- src/storm-dft/generator/DftNextStateGenerator.h | 4 +++- src/storm-dft/storage/dft/DFTState.cpp | 6 +++--- src/storm-dft/storage/dft/DFTState.h | 4 ++-- 4 files changed, 21 insertions(+), 10 deletions(-) diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index 10f01fbe2..e0dd7c4ea 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.cpp +++ b/src/storm-dft/generator/DftNextStateGenerator.cpp @@ -159,14 +159,13 @@ namespace storm { // Set transitions if (exploreDependencies) { // Failure is due to dependency -> add non-deterministic choice if necessary - ValueType probability = mDft.getDependency(*iterFailable)->probability(); + ValueType probability = dependency->probability(); choice.addProbability(newStateId, probability); STORM_LOG_TRACE("Added transition to " << newStateId << " with probability " << probability); if (!storm::utility::isOne(probability)) { // Add transition to state where dependency was unsuccessful - DFTStatePointer unsuccessfulState = state->copy(); - unsuccessfulState->letDependencyBeUnsuccessful(*iterFailable); + DFTStatePointer unsuccessfulState = createSuccessorState(state, nextBE, dependency, false); // Add state StateType unsuccessfulStateId = stateToIdCallback(unsuccessfulState); ValueType remainingProbability = storm::utility::one() - probability; @@ -221,9 +220,19 @@ namespace storm { } template - typename DftNextStateGenerator::DFTStatePointer DftNextStateGenerator::createSuccessorState(DFTStatePointer const state, std::shared_ptr const>& failedBE, std::shared_ptr const>& triggeringDependency) const { + typename DftNextStateGenerator::DFTStatePointer DftNextStateGenerator::createSuccessorState(DFTStatePointer const state, std::shared_ptr const>& failedBE, std::shared_ptr const>& triggeringDependency, bool dependencySuccessful) const { // Construct new state as copy from original one DFTStatePointer newState = state->copy(); + + if (!dependencySuccessful) { + // Dependency was unsuccessful -> no BE fails + STORM_LOG_ASSERT(triggeringDependency != nullptr, "Dependency is not given"); + STORM_LOG_TRACE("With the unsuccessful triggering of PDEP: " << triggeringDependency->name() << " [" << triggeringDependency->id() << "]" << " in " << mDft.getStateString(state)); + newState->letDependencyBeUnsuccessful(triggeringDependency); + return newState; + } + + STORM_LOG_TRACE("With the failure of: " << failedBE->name() << " [" << failedBE->id() << "]" << (triggeringDependency != nullptr ? " (through dependency " + triggeringDependency->name() + " [" + std::to_string(triggeringDependency->id()) + ")]" : "") << " in " << mDft.getStateString(state)); newState->letBEFail(failedBE, triggeringDependency); diff --git a/src/storm-dft/generator/DftNextStateGenerator.h b/src/storm-dft/generator/DftNextStateGenerator.h index af13b4750..c62ff9fa7 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.h +++ b/src/storm-dft/generator/DftNextStateGenerator.h @@ -61,10 +61,12 @@ namespace storm { * @param state Current state. * @param failedBE BE which fails next. * @param triggeringDependency Dependency which triggered the failure (or nullptr if BE failed on its own). + * @param dependencySuccessful Whether the triggering dependency was successful. + * If the dependency is unsuccessful, failedBE does not fail and only the depedendy is marked as failed. * * @return Successor state. */ - DFTStatePointer createSuccessorState(DFTStatePointer const state, std::shared_ptr const> &failedBE, std::shared_ptr const> &triggeringDependency) const; + DFTStatePointer createSuccessorState(DFTStatePointer const state, std::shared_ptr const> &failedBE, std::shared_ptr const> &triggeringDependency, bool dependencySuccessful = true) const; /** * Propagate the failures in a given state if the given BE fails diff --git a/src/storm-dft/storage/dft/DFTState.cpp b/src/storm-dft/storage/dft/DFTState.cpp index abfcdad58..fb320a88a 100644 --- a/src/storm-dft/storage/dft/DFTState.cpp +++ b/src/storm-dft/storage/dft/DFTState.cpp @@ -343,10 +343,10 @@ namespace storm { } template - void DFTState::letDependencyBeUnsuccessful(size_t id) { + void DFTState::letDependencyBeUnsuccessful(std::shared_ptr const> dependency) { STORM_LOG_ASSERT(failableElements.hasDependencies(), "Index invalid."); - std::shared_ptr const> dependency = mDft.getDependency(id); - failableElements.removeDependency(id); + STORM_LOG_ASSERT(!dependency->isFDEP(), "Dependency is not a PDEP."); + failableElements.removeDependency(dependency->id()); setDependencyUnsuccessful(dependency->id()); } diff --git a/src/storm-dft/storage/dft/DFTState.h b/src/storm-dft/storage/dft/DFTState.h index 72774d166..34fa16ddf 100644 --- a/src/storm-dft/storage/dft/DFTState.h +++ b/src/storm-dft/storage/dft/DFTState.h @@ -247,9 +247,9 @@ namespace storm { /** * Sets the dependency as unsuccesful meaning no BE will fail. - * @param index Index of dependency to fail. + * @param dependency Dependency. */ - void letDependencyBeUnsuccessful(size_t index = 0); + void letDependencyBeUnsuccessful(std::shared_ptr const> dependency); /** * Order the state in decreasing order using the symmetries. From 7111674ec81822b684b53513dfa20b50fb2d5356 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 8 Feb 2021 12:31:56 +0100 Subject: [PATCH 05/13] Support for simulation of PDEP --- src/storm-dft/simulator/DFTTraceSimulator.cpp | 43 +++++++++++++------ src/storm-dft/simulator/DFTTraceSimulator.h | 13 +++++- src/storm/utility/random.cpp | 7 +++ src/storm/utility/random.h | 8 ++++ .../storm-dft/simulator/DftSimulatorTest.cpp | 12 ++++++ 5 files changed, 70 insertions(+), 13 deletions(-) diff --git a/src/storm-dft/simulator/DFTTraceSimulator.cpp b/src/storm-dft/simulator/DFTTraceSimulator.cpp index eae3a004c..4baba8e07 100644 --- a/src/storm-dft/simulator/DFTTraceSimulator.cpp +++ b/src/storm-dft/simulator/DFTTraceSimulator.cpp @@ -26,7 +26,7 @@ namespace storm { } template - double DFTTraceSimulator::randomStep() { + std::tuple DFTTraceSimulator::randomNextFailure() { auto iterFailable = state->getFailableElements().begin(); // Check for absorbing state: @@ -34,7 +34,7 @@ namespace storm { // - no BE can fail if (!state->hasOperationalRelevantEvent() || iterFailable == state->getFailableElements().end()) { STORM_LOG_TRACE("No sucessor states available for " << state->getId()); - return -1; + return std::make_tuple(iterFailable, -1, true); } // Get all failable elements @@ -43,9 +43,16 @@ namespace storm { // We take the first dependeny to resolve the non-determinism STORM_LOG_WARN("Non-determinism present! We take the dependency with the lowest id"); } - STORM_LOG_TRACE("Let dependency " << *iterFailable.getFailBE(dft).second << " fail"); - bool res = step(iterFailable); - return res ? 0 : -1; + + auto dependency = iterFailable.getFailBE(dft).second; + if (!dependency->isFDEP()) { + // Flip a coin whether the PDEP is successful + storm::utility::BernoulliDistributionGenerator probGenerator(dependency->probability()); + bool successful = probGenerator.random(randomGenerator); + return std::make_tuple(iterFailable, 0, successful); + } + STORM_LOG_TRACE("Let dependency " << *dependency << " fail"); + return std::make_tuple(iterFailable, 0, true); } else { // Consider all "normal" BE failures // Initialize with first BE @@ -68,27 +75,39 @@ namespace storm { } } STORM_LOG_TRACE("Let BE " << *nextFail.getFailBE(dft).first << " fail after time " << smallestTimebound); - bool res = step(nextFail); - return res ? smallestTimebound : -1; + return std::make_tuple(nextFail, smallestTimebound, true); } } template<> - double DFTTraceSimulator::randomStep() { + std::tuple DFTTraceSimulator::randomNextFailure() { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Simulation not support for parametric DFTs."); } + template + double DFTTraceSimulator::randomStep() { + auto retTuple = this->randomNextFailure(); + storm::dft::storage::FailableElements::const_iterator nextFailable = std::get<0>(retTuple); + double time = std::get<1>(retTuple); + bool successful = std::get<2>(retTuple); + //double time = pairNextFailure.second; + if (time < 0) { + return -1; + } else { + // Apply next failure + bool res = step(nextFailable, successful); + return res ? time : -1; + } + } template - bool DFTTraceSimulator::step(storm::dft::storage::FailableElements::const_iterator nextFailElement) { + bool DFTTraceSimulator::step(storm::dft::storage::FailableElements::const_iterator nextFailElement, bool dependencySuccessful) { if (nextFailElement == state->getFailableElements().end()) { return false; } auto nextBEPair = nextFailElement.getFailBE(dft); - auto newState = generator.createSuccessorState(state, nextBEPair.first, nextBEPair.second); - - // TODO handle PDEP + auto newState = generator.createSuccessorState(state, nextBEPair.first, nextBEPair.second, dependencySuccessful); if(newState->isInvalid() || newState->isTransient()) { STORM_LOG_TRACE("Step is invalid because new state " << (newState->isInvalid() ? "it is invalid" : "the transient fault is ignored")); diff --git a/src/storm-dft/simulator/DFTTraceSimulator.h b/src/storm-dft/simulator/DFTTraceSimulator.h index 7f9203207..6ef4e1ea0 100644 --- a/src/storm-dft/simulator/DFTTraceSimulator.h +++ b/src/storm-dft/simulator/DFTTraceSimulator.h @@ -52,9 +52,20 @@ namespace storm { * Perform one simulation step by letting the next element fail. * * @param nextFailElement Iterator giving the next element which should fail. + * @param dependencySuccessful Whether the triggering dependency was successful. + * If the dependency is unsuccessful, no BE fails and only the depedendy is marked as failed. * @return True iff step could be performed successfully. */ - bool step(storm::dft::storage::FailableElements::const_iterator nextFailElement); + bool step(storm::dft::storage::FailableElements::const_iterator nextFailElement, bool dependencySuccessful = true); + + /*! + * Randomly pick an element which fails next (either a BE or a dependency which triggers a BE) and the time after which it fails. + * The time is 0 for a dependency and -1 if no failure can take place. + * In the latter case, the next failable element is not defined. + * + * @return Tuple of next failable element, time after which is fails and whether a possible failure through the dependency is successful. + */ + std::tuple randomNextFailure(); /*! * Perform a random step by using the random number generator. diff --git a/src/storm/utility/random.cpp b/src/storm/utility/random.cpp index 8c576cf95..ddeb4038f 100644 --- a/src/storm/utility/random.cpp +++ b/src/storm/utility/random.cpp @@ -37,6 +37,13 @@ namespace storm { } + BernoulliDistributionGenerator::BernoulliDistributionGenerator(double prob) : distribution(prob) { + } + + bool BernoulliDistributionGenerator::random(boost::mt19937& engine) { + return distribution(engine); + } + ExponentialDistributionGenerator::ExponentialDistributionGenerator(double rate) : distribution(rate) { } diff --git a/src/storm/utility/random.h b/src/storm/utility/random.h index 80a8d5e61..d99f81f53 100644 --- a/src/storm/utility/random.h +++ b/src/storm/utility/random.h @@ -42,6 +42,14 @@ namespace storm { }; + class BernoulliDistributionGenerator { + public: + BernoulliDistributionGenerator(double prob); + bool random(boost::mt19937& engine); + private: + boost::random::bernoulli_distribution<> distribution; + }; + class ExponentialDistributionGenerator { public: ExponentialDistributionGenerator(double rate); diff --git a/src/test/storm-dft/simulator/DftSimulatorTest.cpp b/src/test/storm-dft/simulator/DftSimulatorTest.cpp index 3bc92bb7f..bfb07e3fa 100644 --- a/src/test/storm-dft/simulator/DftSimulatorTest.cpp +++ b/src/test/storm-dft/simulator/DftSimulatorTest.cpp @@ -87,6 +87,18 @@ namespace { EXPECT_NEAR(result, 0.9985116987, 0.01); } + TEST(DftSimulatorTest, PdepUnreliability) { + double result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/pdep.dft", 1, 10000); + EXPECT_NEAR(result, 0.2017690905, 0.01); + result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/pdep2.dft", 1, 10000); + EXPECT_NEAR(result, 0.2401091405, 0.01); + result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/pdep3.dft", 1, 10000); + EXPECT_NEAR(result, 0.2259856274, 0.01); + // Examle pdep4 contains non-determinism which is not handled in simulation + //result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/pdep4.dft", 1, 10000); + //EXPECT_NEAR(result, 0.008122157897, 0.01); + } + TEST(DftSimulatorTest, SpareUnreliability) { double result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/spare.dft", 1, 10000); EXPECT_NEAR(result, 0.1118530638, 0.01); From 6eec25de6c0fdc6cacc04b6c530a71131667621b Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 8 Feb 2021 20:35:04 +0100 Subject: [PATCH 06/13] Typos --- src/storm-dft/generator/DftNextStateGenerator.cpp | 4 ++-- src/storm-dft/simulator/DFTTraceSimulator.cpp | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index e0dd7c4ea..6c5ca6c3d 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.cpp +++ b/src/storm-dft/generator/DftNextStateGenerator.cpp @@ -227,13 +227,13 @@ namespace storm { if (!dependencySuccessful) { // Dependency was unsuccessful -> no BE fails STORM_LOG_ASSERT(triggeringDependency != nullptr, "Dependency is not given"); - STORM_LOG_TRACE("With the unsuccessful triggering of PDEP: " << triggeringDependency->name() << " [" << triggeringDependency->id() << "]" << " in " << mDft.getStateString(state)); + STORM_LOG_TRACE("With the unsuccessful triggering of PDEP " << triggeringDependency->name() << " [" << triggeringDependency->id() << "]" << " in " << mDft.getStateString(state)); newState->letDependencyBeUnsuccessful(triggeringDependency); return newState; } - STORM_LOG_TRACE("With the failure of: " << failedBE->name() << " [" << failedBE->id() << "]" << (triggeringDependency != nullptr ? " (through dependency " + triggeringDependency->name() + " [" + std::to_string(triggeringDependency->id()) + ")]" : "") << " in " << mDft.getStateString(state)); + STORM_LOG_TRACE("With the failure of " << failedBE->name() << " [" << failedBE->id() << "]" << (triggeringDependency != nullptr ? " (through dependency " + triggeringDependency->name() + " [" + std::to_string(triggeringDependency->id()) + ")]" : "") << " in " << mDft.getStateString(state)); newState->letBEFail(failedBE, triggeringDependency); diff --git a/src/storm-dft/simulator/DFTTraceSimulator.cpp b/src/storm-dft/simulator/DFTTraceSimulator.cpp index 4baba8e07..11f49c588 100644 --- a/src/storm-dft/simulator/DFTTraceSimulator.cpp +++ b/src/storm-dft/simulator/DFTTraceSimulator.cpp @@ -40,7 +40,7 @@ namespace storm { // Get all failable elements if (iterFailable.isFailureDueToDependency()) { if (iterFailable.isConflictingDependency()) { - // We take the first dependeny to resolve the non-determinism + // We take the first dependency to resolve the non-determinism STORM_LOG_WARN("Non-determinism present! We take the dependency with the lowest id"); } From 76afd5e3de2dc5af368a923538947f07df4f8b03 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 8 Feb 2021 20:37:41 +0100 Subject: [PATCH 07/13] Implemented basis for handling invalid traces during simulation --- src/storm-dft/simulator/DFTTraceSimulator.cpp | 80 +++++++---- src/storm-dft/simulator/DFTTraceSimulator.h | 23 +++- .../storm-dft/simulator/DftSimulatorTest.cpp | 126 +++++++++++++----- .../simulator/DftTraceGeneratorTest.cpp | 8 +- 4 files changed, 170 insertions(+), 67 deletions(-) diff --git a/src/storm-dft/simulator/DFTTraceSimulator.cpp b/src/storm-dft/simulator/DFTTraceSimulator.cpp index 11f49c588..9172e76ad 100644 --- a/src/storm-dft/simulator/DFTTraceSimulator.cpp +++ b/src/storm-dft/simulator/DFTTraceSimulator.cpp @@ -85,25 +85,24 @@ namespace storm { } template - double DFTTraceSimulator::randomStep() { + std::pair DFTTraceSimulator::randomStep() { auto retTuple = this->randomNextFailure(); storm::dft::storage::FailableElements::const_iterator nextFailable = std::get<0>(retTuple); double time = std::get<1>(retTuple); bool successful = std::get<2>(retTuple); - //double time = pairNextFailure.second; if (time < 0) { - return -1; + return std::make_pair(SimulationResult::UNSUCCESSFUL, -1); } else { // Apply next failure - bool res = step(nextFailable, successful); - return res ? time : -1; + return std::make_pair(step(nextFailable, successful), time); } } template - bool DFTTraceSimulator::step(storm::dft::storage::FailableElements::const_iterator nextFailElement, bool dependencySuccessful) { + SimulationResult DFTTraceSimulator::step(storm::dft::storage::FailableElements::const_iterator nextFailElement, bool dependencySuccessful) { if (nextFailElement == state->getFailableElements().end()) { - return false; + // No next failure possible + return SimulationResult::UNSUCCESSFUL; } auto nextBEPair = nextFailElement.getFailBE(dft); @@ -111,40 +110,73 @@ namespace storm { if(newState->isInvalid() || newState->isTransient()) { STORM_LOG_TRACE("Step is invalid because new state " << (newState->isInvalid() ? "it is invalid" : "the transient fault is ignored")); - return false; + return SimulationResult::INVALID; } state = newState; - return true; + return SimulationResult::SUCCESSFUL; } template - bool DFTTraceSimulator::simulateCompleteTrace(double timebound) { + SimulationResult DFTTraceSimulator::simulateCompleteTrace(double timebound) { resetToInitial(); + + // Check whether DFT is initially already failed. + if (state->hasFailed(dft.getTopLevelIndex())) { + STORM_LOG_TRACE("DFT is initially failed"); + return SimulationResult::SUCCESSFUL; + } + double time = 0; while (time <= timebound) { - // Check whether DFT failed within timebound - if (state->hasFailed(dft.getTopLevelIndex())) { - STORM_LOG_TRACE("DFT has failed after " << time); - return true; + // Generate next failure + auto retTuple = randomNextFailure(); + storm::dft::storage::FailableElements::const_iterator nextFailable = std::get<0>(retTuple); + double addTime = std::get<1>(retTuple); + bool successfulDependency = std::get<2>(retTuple); + if (addTime < 0) { + // No next state can be reached, because no element can fail anymore. + STORM_LOG_TRACE("No next state possible in state " << dft.getStateString(state) << " because no element can fail anymore"); + return SimulationResult::UNSUCCESSFUL; } - // Generate next state - double res = randomStep(); + // TODO: exit if time would be up after this failure + // This is only correct if no invalid states are possible! (no restrictors and no transient failures) + + // Apply next failure + auto stepResult = step(nextFailable, successfulDependency); STORM_LOG_TRACE("Current state: " << dft.getStateString(state)); - if (res < 0) { - // No next state can be reached - STORM_LOG_TRACE("No next state possible in state " << dft.getStateString(state)); - return false; + + // Check whether state is invalid + if (stepResult != SimulationResult::SUCCESSFUL) { + STORM_LOG_ASSERT(stepResult == SimulationResult::INVALID, "Result of simulation step should be invalid."); + // No next state can be reached, because the state is invalid. + STORM_LOG_TRACE("No next state possible in state " << dft.getStateString(state) << " because simulation was invalid"); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Handling of invalid states is not supported for simulation"); + return SimulationResult::INVALID; + } + + // Check whether time is up + // Checking whether the time is up must be performed after checking if a state is invalid. + // Otherwise we would erroneously mark invalid traces as unsucessful. + time += addTime; + if (time > timebound) { + STORM_LOG_TRACE("Time limit" << timebound << " exceeded: " << time); + return SimulationResult::UNSUCCESSFUL; + } + + // Check whether DFT is failed + if (state->hasFailed(dft.getTopLevelIndex())) { + STORM_LOG_TRACE("DFT has failed after " << time); + return SimulationResult::SUCCESSFUL; } - time += res; } - // Time is up - return false; + STORM_LOG_ASSERT(false, "Should not be reachable"); + return SimulationResult::UNSUCCESSFUL; } template<> - bool DFTTraceSimulator::simulateCompleteTrace(double timebound) { + SimulationResult DFTTraceSimulator::simulateCompleteTrace(double timebound) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Simulation not support for parametric DFTs."); } diff --git a/src/storm-dft/simulator/DFTTraceSimulator.h b/src/storm-dft/simulator/DFTTraceSimulator.h index 6ef4e1ea0..92eecbf5d 100644 --- a/src/storm-dft/simulator/DFTTraceSimulator.h +++ b/src/storm-dft/simulator/DFTTraceSimulator.h @@ -10,6 +10,12 @@ namespace storm { namespace dft { namespace simulator { + /*! + * Simulation result. + * + */ + enum class SimulationResult { SUCCESSFUL, UNSUCCESSFUL, INVALID }; + /*! * Simulator for DFTs. * A step in the simulation corresponds to the failure of one BE (either on its own or triggered by a dependency) @@ -19,6 +25,7 @@ namespace storm { template class DFTTraceSimulator { using DFTStatePointer = std::shared_ptr>; + public: /*! * Constructor. @@ -54,9 +61,9 @@ namespace storm { * @param nextFailElement Iterator giving the next element which should fail. * @param dependencySuccessful Whether the triggering dependency was successful. * If the dependency is unsuccessful, no BE fails and only the depedendy is marked as failed. - * @return True iff step could be performed successfully. + * @return Successful if step could be performed, unsuccesful if no element can fail or invalid if the next state is invalid (due to a restrictor). */ - bool step(storm::dft::storage::FailableElements::const_iterator nextFailElement, bool dependencySuccessful = true); + SimulationResult step(storm::dft::storage::FailableElements::const_iterator nextFailElement, bool dependencySuccessful = true); /*! * Randomly pick an element which fails next (either a BE or a dependency which triggers a BE) and the time after which it fails. @@ -70,20 +77,22 @@ namespace storm { /*! * Perform a random step by using the random number generator. * - * @return double The time which progessed between the last step and this step. - * Returns -1 if no next step could be created. + * @return Pair of the simulation result (successful, unsuccesful, invalid) and the time which progessed between the last step and this step. */ - double randomStep(); + std::pair randomStep(); /*! * Perform a complete simulation of a failure trace by using the random number generator. * The simulation starts in the initial state and tries to reach a state where the top-level event of the DFT has failed. * If this target state can be reached within the given timebound, the simulation was successful. + * If an invalid state (due to a restrictor) was reached, the simulated trace is invalid. * * @param timebound Time bound in which the system failure should occur. - * @return True iff a system failure occurred for the generated trace within the time bound. + * @return Simulation result is (1) successful if a system failure occurred for the generated trace within the time bound, + * (2) unsuccesfull, if no system failure occurred within the time bound, or + * (3) invalid, if an invalid state (due to a restrictor) was reached during the trace generation. */ - bool simulateCompleteTrace(double timebound); + SimulationResult simulateCompleteTrace(double timebound); protected: diff --git a/src/test/storm-dft/simulator/DftSimulatorTest.cpp b/src/test/storm-dft/simulator/DftSimulatorTest.cpp index bfb07e3fa..ff34b2880 100644 --- a/src/test/storm-dft/simulator/DftSimulatorTest.cpp +++ b/src/test/storm-dft/simulator/DftSimulatorTest.cpp @@ -10,8 +10,8 @@ namespace { - // Helper function - double simulateDft(std::string const& file, double timebound, size_t noRuns) { + // Helper functions + std::pair simulateDft(std::string const& file, double timebound, size_t noRuns) { // Load, build and prepare DFT storm::transformations::dft::DftTransformator dftTransformator = storm::transformations::dft::DftTransformator(); std::shared_ptr> dft = dftTransformator.transformBinaryFDEPs(*(storm::api::loadDFTGalileoFile(file))); @@ -27,104 +27,162 @@ namespace { storm::storage::DFTStateGenerationInfo stateGenerationInfo(dft->buildStateGenerationInfo(symmetries)); // Init random number generator + //storm::utility::setLogLevel(l3pp::LogLevel::TRACE); boost::mt19937 gen(5u); storm::dft::simulator::DFTTraceSimulator simulator(*dft, stateGenerationInfo, gen); - size_t count = 0;; - bool res; + size_t count = 0; + size_t invalid = 0; + storm::dft::simulator::SimulationResult res; for (size_t i=0; ihasFailed(dft->getTopLevelIndex())); + storm::dft::simulator::SimulationResult res; + double timebound; // First random step - double timebound = simulator.randomStep(); + std::tie(res, timebound) = simulator.randomStep(); + EXPECT_EQ(res, storm::dft::simulator::SimulationResult::SUCCESSFUL); #if BOOST_VERSION > 106400 // Older Boost versions yield different value EXPECT_FLOAT_EQ(timebound, 0.522079); @@ -182,7 +185,8 @@ namespace { state = simulator.getCurrentState(); EXPECT_FALSE(state->hasFailed(dft->getTopLevelIndex())); - timebound = simulator.randomStep(); + std::tie(res, timebound) = simulator.randomStep(); + EXPECT_EQ(res, storm::dft::simulator::SimulationResult::SUCCESSFUL); #if BOOST_VERSION > 106400 // Older Boost versions yield different value EXPECT_FLOAT_EQ(timebound, 0.9497214); From 7fc4046fbc47a352679c81b7e2af35f232a82dd2 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 23 Feb 2021 19:36:13 +0100 Subject: [PATCH 08/13] Fix DftSimulatorTest for older Boost versions --- .../storm-dft/simulator/DftSimulatorTest.cpp | 23 +++++++++++-------- 1 file changed, 14 insertions(+), 9 deletions(-) diff --git a/src/test/storm-dft/simulator/DftSimulatorTest.cpp b/src/test/storm-dft/simulator/DftSimulatorTest.cpp index ff34b2880..1932f292e 100644 --- a/src/test/storm-dft/simulator/DftSimulatorTest.cpp +++ b/src/test/storm-dft/simulator/DftSimulatorTest.cpp @@ -50,7 +50,7 @@ namespace { size_t count; size_t invalid; std::tie(count, invalid) = simulateDft(file, timebound, noRuns); - EXPECT_EQ(invalid, 0); + EXPECT_EQ(invalid, 0ul); return (double) count / noRuns; } @@ -72,7 +72,12 @@ namespace { result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/voting3.dft", 1, 10000); EXPECT_NEAR(result, 0.3496529873, 0.01); result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/voting4.dft", 1, 10000); +#if BOOST_VERSION > 106400 EXPECT_NEAR(result, 0.693568287, 0.01); +#else + // Older Boost versions yield different value + EXPECT_NEAR(result, 0.693568287, 0.015); +#endif } TEST(DftSimulatorTest, PandUnreliability) { @@ -135,27 +140,27 @@ namespace { size_t count; size_t invalid; std::tie(count, invalid) = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/seq.dft", 1, 10000); - EXPECT_EQ(invalid, 0); + EXPECT_EQ(invalid, 0ul); double result = (double) count / 10000; EXPECT_NEAR(result, 0.09020401043, 0.01); std::tie(count, invalid) = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/seq2.dft", 1, 10000); - EXPECT_EQ(invalid, 0); + EXPECT_EQ(invalid, 0ul); result = (double) count / 10000; EXPECT_NEAR(result, 0.01438767797, 0.01); std::tie(count, invalid) = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/seq3.dft", 1, 10000); - EXPECT_EQ(invalid, 0); + EXPECT_EQ(invalid, 0ul); result = (double) count / 10000; EXPECT_NEAR(result, 0.01438767797, 0.01); std::tie(count, invalid) = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/seq4.dft", 1, 10000); - EXPECT_EQ(invalid, 0); + EXPECT_EQ(invalid, 0ul); result = (double) count / 10000; EXPECT_NEAR(result, 0.01438767797, 0.01); std::tie(count, invalid) = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/seq5.dft", 1, 10000); - EXPECT_EQ(invalid, 0); + EXPECT_EQ(invalid, 0ul); result = (double) count / 10000; EXPECT_FLOAT_EQ(result, 0); std::tie(count, invalid) = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/seq6.dft", 1, 10000); - EXPECT_EQ(invalid, 0); + EXPECT_EQ(invalid, 0ul); result = (double) count / 10000; EXPECT_NEAR(result, 2.499875004e-09, 0.01); } @@ -172,8 +177,8 @@ namespace { //EXPECT_EQ(invalid, 10000); //EXPECT_EQ(count, 0); std::tie(count, invalid) = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/mutex3.dft", 1, 10000); - EXPECT_EQ(invalid, 0); - EXPECT_EQ(count, 0); + EXPECT_EQ(invalid, 0ul); + EXPECT_EQ(count, 0ul); } TEST(DftSimulatorTest, SymmetryUnreliability) { From 972ef8b14cf72c9883deffe54a4f7038b391a505 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Basg=C3=B6ze?= Date: Thu, 25 Feb 2021 15:08:14 +0100 Subject: [PATCH 09/13] Break inclusion loop in DFT.h and comment magic numbers in RelevantEvents.h --- src/storm-dft/storage/dft/DFT.cpp | 1 + src/storm-dft/storage/dft/DFT.h | 6 ++++-- src/storm-dft/utility/RelevantEvents.h | 2 ++ 3 files changed, 7 insertions(+), 2 deletions(-) diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index 86a99290c..5496e5476 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -10,6 +10,7 @@ #include "storm-dft/builder/DFTBuilder.h" #include "storm-dft/storage/dft/DFTIsomorphism.h" +#include "storm-dft/utility/RelevantEvents.h" namespace storm { diff --git a/src/storm-dft/storage/dft/DFT.h b/src/storm-dft/storage/dft/DFT.h index f089c8ae5..db0704ee9 100644 --- a/src/storm-dft/storage/dft/DFT.h +++ b/src/storm-dft/storage/dft/DFT.h @@ -17,13 +17,15 @@ #include "storm-dft/storage/dft/SymmetricUnits.h" #include "storm-dft/storage/dft/DFTStateGenerationInfo.h" #include "storm-dft/storage/dft/DFTLayoutInfo.h" -#include "storm-dft/utility/RelevantEvents.h" namespace storm { + // Forward declarations namespace builder { - // Forward declaration template class DFTBuilder; } + namespace utility { + class RelevantEvents; + } namespace storage { diff --git a/src/storm-dft/utility/RelevantEvents.h b/src/storm-dft/utility/RelevantEvents.h index f32f348c8..4e07d4e26 100644 --- a/src/storm-dft/utility/RelevantEvents.h +++ b/src/storm-dft/utility/RelevantEvents.h @@ -57,8 +57,10 @@ namespace storm { } else { // Get name of event if (boost::ends_with(label, "_failed")) { + // length of "_failed" = 7 this->addEvent(label.substr(0, label.size() - 7)); } else if (boost::ends_with(label, "_dc")) { + // length of "_dc" = 3 this->addEvent(label.substr(0, label.size() - 3)); } else if (label.find("_claimed_") != std::string::npos) { STORM_LOG_THROW(storm::settings::getModule().isAddLabelsClaiming(), storm::exceptions::InvalidArgumentException, "Claiming labels will not be exported but are required for label '" << label << "'. Try setting --labels-claiming."); From 7a2b060afc4505703e120b002102464050836137 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Basg=C3=B6ze?= Date: Thu, 25 Feb 2021 15:27:24 +0100 Subject: [PATCH 10/13] Remove allowDCForRelevant from RelevantEvents --- src/storm-dft-cli/storm-dft.cpp | 4 +-- src/storm-dft/api/storm-dft.h | 10 +++---- .../modelchecker/dft/DFTModelChecker.cpp | 22 +++++++-------- .../modelchecker/dft/DFTModelChecker.h | 23 +++++++++++---- src/storm-dft/storage/dft/DFT.cpp | 4 +-- src/storm-dft/storage/dft/DFT.h | 3 +- src/storm-dft/utility/RelevantEvents.h | 10 +------ .../storm-dft/api/DftApproximationTest.cpp | 4 +-- .../storm-dft/api/DftModelBuildingTest.cpp | 28 +++++++++---------- .../storm-dft/api/DftModelCheckerTest.cpp | 4 +-- .../storm-dft/simulator/DftSimulatorTest.cpp | 4 +-- .../simulator/DftTraceGeneratorTest.cpp | 4 +-- 12 files changed, 62 insertions(+), 58 deletions(-) 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; From 0ed64b62579de01f9d04c75c07d5e595283c57c4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Basg=C3=B6ze?= Date: Thu, 25 Feb 2021 15:33:09 +0100 Subject: [PATCH 11/13] Add == and != ops to RelevantEvents and simplify constructor of RelevantEvents --- src/storm-dft/utility/RelevantEvents.h | 33 ++++++++++++++++---------- 1 file changed, 21 insertions(+), 12 deletions(-) diff --git a/src/storm-dft/utility/RelevantEvents.h b/src/storm-dft/utility/RelevantEvents.h index 40627dbc1..ddca1e1f1 100644 --- a/src/storm-dft/utility/RelevantEvents.h +++ b/src/storm-dft/utility/RelevantEvents.h @@ -20,18 +20,24 @@ namespace storm { * * @param relevantEvents List of relevant event names. */ - RelevantEvents(std::vector const& relevantEvents = {}) : names(), allRelevant(false) { - for (auto const& name: relevantEvents) { - if (name == "all") { - this->allRelevant = true; - this->names.clear(); - break; - } else { - this->addEvent(name); - } + RelevantEvents(std::vector const& relevantEvents = {}) { + // check if the name "all" occurs + if (std::any_of(relevantEvents.begin(), relevantEvents.end(), + [](auto const& name) { return name == "all"; })) { + this->allRelevant = true; + } else { + this->names.insert(relevantEvents.begin(), relevantEvents.end()); } } + bool operator==(RelevantEvents const& rhs) { + return this->allRelevant == rhs.allRelevant || this->names == rhs.names; + } + + bool operator!=(RelevantEvents const& rhs) { + return !(*this == rhs); + } + /*! * Add relevant event names required by the labels in properties. * @@ -74,7 +80,7 @@ namespace storm { * Check that the relevant names correspond to existing elements in the DFT. * * @param dft DFT. - * @return True iff relevant names are consistent with DFT elements. + * @return True iff the relevant names are consistent with the given DFT. */ template bool checkRelevantNames(storm::storage::DFT const& dft) const { @@ -86,6 +92,9 @@ namespace storm { return true; } + /*! + * @return True iff the given name is the name of a relevant Event + */ bool isRelevant(std::string const& name) const { if (this->allRelevant) { return true; @@ -106,10 +115,10 @@ namespace storm { } // Names of relevant events. - std::set names; + std::set names{}; // Whether all elements are relevant. - bool allRelevant; + bool allRelevant{false}; }; } // namespace utility From 3f9616d3e069778a84c5badb636ae8d6b4e94084 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 1 Mar 2021 18:10:26 +0100 Subject: [PATCH 12/13] Added documentation about integrating Github pull requests --- doc/merge_pull_requests.md | 39 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) create mode 100644 doc/merge_pull_requests.md diff --git a/doc/merge_pull_requests.md b/doc/merge_pull_requests.md new file mode 100644 index 000000000..77fed308a --- /dev/null +++ b/doc/merge_pull_requests.md @@ -0,0 +1,39 @@ +The following steps should be performed to integrate pull requests from Github. + +0. After a pull request is opened, some automatic build checks should be performed by Github Actions. + Failures of these checks should be fixed. + +1. Manually review the pull request on Github and suggest improvements if necessary. + In particular make sure: + * No unnecessary files were committed (for example build artefacts, etc.) + * No remains from the development are present (for example debug output, hackish workarounds, etc.) + * ... + +2. Integrate the pull request via Github, preferably by *rebase and merge*. + +3. Optional (if not done already): add the Github repository as another remote for your local copy of the internal repository: + ```console + git remote add github https://github.com/moves-rwth/storm.git + ``` + +4. Fetch the current Github master: + ```console + git fetch github + ``` + +5. Make sure to be on the (internal) master: + ```console + git checkout master + ``` + +6. Rebase the changes of Github onto the (internal) master: + ```console + git rebase github/master + ``` + +7. Check that Storm builds successfully and everything works as expected. + +8. Push the changes into the internal repository: + ```console + git push origin + ``` From d25cd1d6367ca5a47679d70309020c79f8cd2314 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 2 Mar 2021 11:43:49 +0100 Subject: [PATCH 13/13] Enable Github Actions for pull requests (without deployment) --- .github/workflows/buildtest.yml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/.github/workflows/buildtest.yml b/.github/workflows/buildtest.yml index ba0bdbf79..bc34b202d 100644 --- a/.github/workflows/buildtest.yml +++ b/.github/workflows/buildtest.yml @@ -1,6 +1,6 @@ name: Build Test -# Builds and tests storm on varius platforms -# also deploys images to dockerhub +# Builds and tests storm on various platforms +# also deploys images to Dockerhub on: schedule: @@ -8,6 +8,7 @@ on: - cron: '0 6 * * *' # needed to trigger the workflow manually workflow_dispatch: + pull_request: env: CARL_BRANCH: "master14" @@ -120,7 +121,7 @@ jobs: - name: Build storm run: sudo docker exec storm bash -c "cd /opt/storm/build; make -j ${NR_JOBS}" - # A bit hacky... but its usefullnes has been proven in production + # A bit hacky... but its usefulness has been proven in production - name: Check release makeflags if: matrix.debugOrRelease == 'release' run: | @@ -134,6 +135,8 @@ jobs: run: sudo docker exec storm bash -c "cd /opt/storm/build; ctest test --output-on-failure" - name: Deploy storm + # Only deploy if using master (and not for pull requests) + if: github.ref == 'refs/heads/master' run: | sudo docker commit storm movesrwth/storm:ci-${{ matrix.debugOrRelease }} sudo docker push movesrwth/storm:ci-${{ matrix.debugOrRelease }}