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 }} 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 + ``` 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/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/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index 10f01fbe2..6c5ca6c3d 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,10 +220,20 @@ 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(); - 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)); + + 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/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/simulator/DFTTraceSimulator.cpp b/src/storm-dft/simulator/DFTTraceSimulator.cpp index fd0af4b14..9172e76ad 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,18 +34,25 @@ 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 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"); } - 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 @@ -67,58 +74,114 @@ namespace storm { smallestTimebound = timebound; } } - STORM_LOG_TRACE("Let BE " << *nextFail.getFailBE(dft).first << "fail after time " << smallestTimebound); - bool res = step(nextFail); - return res ? smallestTimebound : -1; + STORM_LOG_TRACE("Let BE " << *nextFail.getFailBE(dft).first << " fail after time " << smallestTimebound); + return std::make_tuple(nextFail, smallestTimebound, true); } } + template<> + std::tuple DFTTraceSimulator::randomNextFailure() { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Simulation not support for parametric DFTs."); + } + template - bool DFTTraceSimulator::step(storm::dft::storage::FailableElements::const_iterator nextFailElement) { + 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); + if (time < 0) { + return std::make_pair(SimulationResult::UNSUCCESSFUL, -1); + } else { + // Apply next failure + return std::make_pair(step(nextFailable, successful), time); + } + } + + template + 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); - 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")); - 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<> + SimulationResult 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..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. @@ -52,27 +59,40 @@ namespace storm { * Perform one simulation step by letting the next element fail. * * @param nextFailElement Iterator giving the next element which should fail. - * @return True iff step could be performed successfully. + * @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 Successful if step could be performed, unsuccesful if no element can fail or invalid if the next state is invalid (due to a restrictor). + */ + 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. + * 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. */ - bool step(storm::dft::storage::FailableElements::const_iterator nextFailElement); + std::tuple randomNextFailure(); /*! * 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: @@ -83,7 +103,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; diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index 86a99290c..c309d7439 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 { @@ -1038,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 @@ -1046,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 f089c8ae5..62fb6dd4b 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 { @@ -376,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/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. 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: diff --git a/src/storm-dft/utility/RelevantEvents.h b/src/storm-dft/utility/RelevantEvents.h index f32f348c8..ddca1e1f1 100644 --- a/src/storm-dft/utility/RelevantEvents.h +++ b/src/storm-dft/utility/RelevantEvents.h @@ -19,20 +19,25 @@ 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) { - 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. * @@ -57,8 +62,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."); @@ -73,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 { @@ -85,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; @@ -93,10 +103,6 @@ namespace storm { } } - bool isAllowDC() const { - return this->allowDC; - } - private: /*! @@ -109,13 +115,10 @@ namespace storm { } // Names of relevant events. - std::set names; + std::set names{}; // Whether all elements are relevant. - bool allRelevant; - - // Whether to allow Don't Care propagation for relevant events. - bool allowDC; + bool allRelevant{false}; }; } // namespace utility 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 02de9ad0b..85f26eab0 100644 --- a/src/storm/utility/random.h +++ b/src/storm/utility/random.h @@ -44,6 +44,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/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 9826c8ae3..296a58dc1 100644 --- a/src/test/storm-dft/simulator/DftSimulatorTest.cpp +++ b/src/test/storm-dft/simulator/DftSimulatorTest.cpp @@ -10,16 +10,16 @@ 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))); 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; @@ -27,23 +27,168 @@ 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; i 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) { + double result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/pand.dft", 1, 10000); + EXPECT_NEAR(result, 0.03087312562, 0.01); + } + + TEST(DftSimulatorTest, PorUnreliability) { + double result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/por.dft", 1, 10000); + EXPECT_NEAR(result, 0.2753355179, 0.01); + } + + TEST(DftSimulatorTest, FdepUnreliability) { + double result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/fdep.dft", 1, 10000); + EXPECT_NEAR(result, 0.7768698399, 0.01); + result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/fdep2.dft", 1, 10000); + EXPECT_NEAR(result, 0.3934693403, 0.01); + result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/fdep3.dft", 1, 10000); + EXPECT_NEAR(result, 0.329679954, 0.01); + result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/fdep4.dft", 1, 10000); + EXPECT_NEAR(result, 0.601280086, 0.01); + result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/fdep5.dft", 1, 10000); + EXPECT_NEAR(result, 0.1548181217, 0.01); + result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/fdep6.dft", 1, 10000); + EXPECT_NEAR(result, 0.9985116987, 0.01); + } + + TEST(DftSimulatorTest, PdepUnreliability) { + double result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/pdep.dft", 1, 10000); + EXPECT_NEAR(result, 0.2017690905, 0.01); + result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/pdep2.dft", 1, 10000); + EXPECT_NEAR(result, 0.2401091405, 0.01); + result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/pdep3.dft", 1, 10000); + EXPECT_NEAR(result, 0.2259856274, 0.01); + // Example pdep4 contains non-determinism which is not handled in simulation + //result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/pdep4.dft", 1, 10000); + //EXPECT_NEAR(result, 0.008122157897, 0.01); + } + + TEST(DftSimulatorTest, SpareUnreliability) { + double result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/spare.dft", 1, 10000); + EXPECT_NEAR(result, 0.1118530638, 0.01); + result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/spare2.dft", 1, 10000); + EXPECT_NEAR(result, 0.2905027469, 0.01); + result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/spare3.dft", 1, 10000); + EXPECT_NEAR(result, 0.4660673246, 0.01); + result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/spare4.dft", 1, 10000); + EXPECT_NEAR(result, 0.01273070783, 0.01); + result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/spare5.dft", 1, 10000); + EXPECT_NEAR(result, 0.2017690905, 0.01); + result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/spare6.dft", 1, 10000); + EXPECT_NEAR(result, 0.4693712702, 0.01); + result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/spare7.dft", 1, 10000); + EXPECT_NEAR(result, 0.06108774525, 0.01); + result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/spare8.dft", 1, 10000); + EXPECT_NEAR(result, 0.02686144489, 0.01); + } + + TEST(DftSimulatorTest, SeqUnreliability) { + size_t count; + size_t invalid; + std::tie(count, invalid) = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/seq.dft", 1, 10000); + 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, 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, 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, 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, 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, 0ul); + result = (double) count / 10000; + EXPECT_NEAR(result, 2.499875004e-09, 0.01); + } + + TEST(DftSimulatorTest, MutexUnreliability) { + size_t count; + size_t invalid; + // Invalid states are currently not supported + EXPECT_THROW(simulateDft(STORM_TEST_RESOURCES_DIR "/dft/mutex.dft", 1, 10000), storm::exceptions::NotSupportedException); + //EXPECT_GE(invalid, 0); + //double result = (double) count / (10000 - invalid); + //EXPECT_NEAR(result, 0.8646647168, 0.01); + EXPECT_THROW(simulateDft(STORM_TEST_RESOURCES_DIR "/dft/mutex2.dft", 1, 10000), storm::exceptions::NotSupportedException); + //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, 0ul); + EXPECT_EQ(count, 0ul); + } + + TEST(DftSimulatorTest, SymmetryUnreliability) { + double result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/symmetry6.dft", 1, 10000); + EXPECT_NEAR(result, 0.3421934224, 0.01); + } + + TEST(DftSimulatorTest, HecsUnreliability) { + double result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/hecs_2_2.dft", 1, 10000); + EXPECT_NEAR(result, 0.00021997582, 0.001); + } + } diff --git a/src/test/storm-dft/simulator/DftTraceGeneratorTest.cpp b/src/test/storm-dft/simulator/DftTraceGeneratorTest.cpp index 5bdc5de3a..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; @@ -173,8 +173,11 @@ namespace { auto state = simulator.getCurrentState(); EXPECT_FALSE(state->hasFailed(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);