diff --git a/.github/workflows/buildtest.yml b/.github/workflows/buildtest.yml deleted file mode 100644 index 6f2b5421d..000000000 --- a/.github/workflows/buildtest.yml +++ /dev/null @@ -1,139 +0,0 @@ -name: Build Test -# Builds and tests storm on varius platforms -# also deploys images to dockerhub - -on: - schedule: - # run daily - - cron: '0 6 * * *' - # needed to trigger the workflow manually - workflow_dispatch: - -env: - CARL_BRANCH: "master14" - CARL_GIT_URL: "https://github.com/smtrat/carl.git" - STORM_GIT_URL: "${{ github.server_url }}/${{ github.repository }}.git" - STORM_BRANCH: "master" - # github runners currently have two cores - NR_JOBS: "2" - - # cmake arguments - CMAKE_DEBUG: "-DCMAKE_BUILD_TYPE=Debug -DSTORM_DEVELOPER=ON -DSTORM_PORTABLE=ON" - CMAKE_RELEASE: "-DCMAKE_BUILD_TYPE=Release -DSTORM_DEVELOPER=OFF -DSTORM_PORTABLE=ON" - - CARL_CMAKE_DEBUG: "-DCMAKE_BUILD_TYPE=Debug -DUSE_CLN_NUMBERS=ON -DUSE_GINAC=ON -DTHREAD_SAFE=ON -DBUILD_ADDONS=ON -DBUILD_ADDON_PARSER=ON" - CARL_CMAKE_RELEASE: "-DCMAKE_BUILD_TYPE=Release -DUSE_CLN_NUMBERS=ON -DUSE_GINAC=ON -DTHREAD_SAFE=ON -DBUILD_ADDONS=ON -DBUILD_ADDON_PARSER=ON" - - -jobs: - noDeploy: - runs-on: ubuntu-latest - strategy: - matrix: - distro: ["ubuntu-18.04", "debian-10", "debian-9"] - debugOrRelease: ["debug", "release"] - steps: - - name: Setup cmake arguments - # this is strangely the best way to implement environment variables based on the value of another - # GITHUB_ENV is a magic variable pointing to a file; if a line with format {NAME}={VALUE} - # then the env variable with name NAME will be created/updated with VALUE - run: | - ([[ ${{ matrix.debugOrRelease }} == "debug" ]] && echo "CMAKE_ARGS=${CMAKE_DEBUG}" || echo "CMAKE_ARGS=${CMAKE_RELEASE}") >> $GITHUB_ENV - - - name: Init Docker - run: sudo docker run -d -it --name storm --privileged movesrwth/storm-basesystem:${{ matrix.distro }} - - name: Git clone - run: sudo docker exec storm git clone --depth 1 --branch $STORM_BRANCH $STORM_GIT_URL /opt/storm - - name: Run cmake - run: sudo docker exec storm bash -c "mkdir /opt/storm/build; cd /opt/storm/build; cmake .. ${CMAKE_ARGS}" - - 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 - - name: Check release makeflags - if: matrix.debugOrRelease == 'release' - run: | - sudo docker exec storm bash -c "/opt/storm/build/bin/storm --version | grep 'with flags .* -O3' || (echo \"Error: Missing flag \'-O3\' for release build.\" && false)" - sudo docker exec storm bash -c "/opt/storm/build/bin/storm --version | grep 'with flags .* -DNDEBUG' || (echo \"Error: Missing flag \'-DNDEBUG\' for release build.\" && false)" - - name: Check debug makeflags - if: matrix.debugOrRelease == 'debug' - run: | - sudo docker exec storm bash -c "/opt/storm/build/bin/storm --version | grep 'with flags .* -g' || (echo \"Error: Missing flag \'-g\' for debug build.\" && false)" - - - name: Run unit tests - run: sudo docker exec storm bash -c "cd /opt/storm/build; ctest test --output-on-failure" - - deploy: - runs-on: ubuntu-latest - env: - DISTRO: "ubuntu-20.04" - strategy: - matrix: - debugOrRelease: ["debug", "release"] - steps: - - name: Setup cmake arguments - # this is strangely the best way to implement environment variables based on the value of another - # GITHUB_ENV is a magic variable pointing to a file; if a line with format {NAME}={VALUE} - # then the env variable with name NAME will be created/updated with VALUE - run: | - ([[ ${{ matrix.debugOrRelease }} == "debug" ]] && echo "CMAKE_ARGS=${CMAKE_DEBUG}" || echo "CMAKE_ARGS=${CMAKE_RELEASE}") >> $GITHUB_ENV - ([[ ${{ matrix.debugOrRelease }} == "debug" ]] && echo "CARL_CMAKE_ARGS=${CARL_CMAKE_DEBUG}" || echo "CARL_CMAKE_ARGS=${CARL_CMAKE_RELEASE}") >> $GITHUB_ENV - - - name: Login into docker - run: echo "${{ secrets.DOCKER_PASSWORD }}" | sudo docker login -u "${{ secrets.DOCKER_USERNAME }}" --password-stdin - - name: Init Docker - run: sudo docker run -d -it --name storm --privileged movesrwth/storm-basesystem:${DISTRO} - - ##### - # Build & DEPLOY CARL - ##### - # We should not do partial updates :/ - # but we need to install some dependencies - # Surely we can find a better way to do this at some point - - name: Update base system - run: | - sudo docker exec storm apt-get update - sudo docker exec storm apt-get upgrade -qqy - - name: install dependencies - run: sudo docker exec storm apt-get install -qq -y uuid-dev pkg-config - - name: Git clone carl - run: sudo docker exec storm git clone --depth 1 --branch $CARL_BRANCH $CARL_GIT_URL /opt/carl - - name: Run cmake for carl - run: sudo docker exec storm bash -c "mkdir /opt/carl/build; cd /opt/carl/build; cmake .. ${CARL_CMAKE_ARGS}" - - name: Build carl - run: sudo docker exec storm bash -c "cd /opt/carl/build; make lib_carl -j ${NR_JOBS}" - # dummy step for now - - name: Deploy carl - run: | - sudo docker commit storm movesrwth/carl:ci-${{ matrix.debugOrRelease }} - sudo docker push movesrwth/carl:ci-${{ matrix.debugOrRelease }} - - - ##### - # Build & TEST & DEPLOY STORM - ##### - - name: Git clone - run: sudo docker exec storm git clone --depth 1 --branch $STORM_BRANCH $STORM_GIT_URL /opt/storm - - name: Run cmake - run: sudo docker exec storm bash -c "mkdir /opt/storm/build; cd /opt/storm/build; cmake .. ${CMAKE_ARGS}" - - 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 - - name: Check release makeflags - if: matrix.debugOrRelease == 'release' - run: | - sudo docker exec storm bash -c "/opt/storm/build/bin/storm --version | grep 'with flags .* -O3' || (echo \"Error: Missing flag \'-O3\' for release build.\" && false)" - sudo docker exec storm bash -c "/opt/storm/build/bin/storm --version | grep 'with flags .* -DNDEBUG' || (echo \"Error: Missing flag \'-DNDEBUG\' for release build.\" && false)" - - name: Check debug makeflags - if: matrix.debugOrRelease == 'debug' - run: | - sudo docker exec storm bash -c "/opt/storm/build/bin/storm --version | grep 'with flags .* -g' || (echo \"Error: Missing flag \'-g\' for debug build.\" && false)" - - name: Run unit tests - run: sudo docker exec storm bash -c "cd /opt/storm/build; ctest test --output-on-failure" - - # dummy step for now - - name: Deploy storm - run: | - sudo docker commit storm movesrwth/storm:ci-${{ matrix.debugOrRelease }} - sudo docker push movesrwth/storm:ci-${{ matrix.debugOrRelease }} diff --git a/CHANGELOG.md b/CHANGELOG.md index 3c8aeb2d8..6899f0b90 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -8,22 +8,23 @@ The releases of major and minor versions contain an overview of changes since th Version 1.6.x ------------- ## Version 1.6.4 (20xx/xx) -- Added an export of check results to json. Use `--exportresult` in the command line interface. +- Added an export of check results to json. Use `--exportresult` in the command line interface. - Added computation of steady state probabilities for DTMC/CTMC in the sparse engine. Use `--steadystate` in the command line interface. - Implemented parsing and model building of Stochastic multiplayer games (SMGs) in the PRISM language. No model checking implemented, for now. +- Added support for continuous integration with Github Actions. ## Version 1.6.3 (2020/11) - Added support for multi-objective model checking of long-run average objectives including mixtures with other kinds of objectives. -- Added support for generating optimal schedulers for globally formulae -- Simulator supports exact arithmetic -- Added switch `--no-simplify` to disable simplification of PRISM programs (which sometimes costs a bit of time on extremely large inputs) -- Fixed issues with JANI inputs concerning +- Added support for generating optimal schedulers for globally formulae. +- Simulator supports exact arithmetic. +- Added switch `--no-simplify` to disable simplification of PRISM programs (which sometimes costs a bit of time on extremely large inputs). +- Fixed issues with JANI inputs concerning . - transient variable expressions in properties, - constants in properties, and - integer variables with either only an upper or only a lower bound. -- `storm-pomdp`: States can be labelled with values for observable predicates -- `storm-pomdp`: (Only API) Track state estimates -- `storm-pomdp`: (Only API) Reduce computation of state estimates to computation on unrolled MDP +- `storm-pomdp`: States can be labelled with values for observable predicates. +- `storm-pomdp`: (Only API) Track state estimates. +- `storm-pomdp`: (Only API) Reduce computation of state estimates to computation on unrolled MDP. ## Version 1.6.2 (2020/09) - Prism program simplification improved. diff --git a/README.md b/README.md index 99265f6f0..7fa7dac2d 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,7 @@ Storm - A Modern Probabilistic Model Checker ============================================ -[![Build Status](https://travis-ci.org/moves-rwth/storm.svg?branch=master)](https://travis-ci.org/moves-rwth/storm) + +[![Build Status](https://github.com/moves-rwth/storm/workflows/Build%20Test/badge.svg)](https://github.com/moves-rwth/storm/actions) [![GitHub release](https://img.shields.io/github/release/moves-rwth/storm.svg)](https://github.com/moves-rwth/storm/releases/) [![DOI](https://zenodo.org/badge/DOI/10.5281/zenodo.1181896.svg)](https://doi.org/10.5281/zenodo.1181896) diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index 13628a7ff..3ecc69498 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -743,8 +743,9 @@ namespace storm { ValueType ExplicitDFTModelBuilder::getLowerBound(DFTStatePointer const& state) const { // Get the lower bound by considering the failure of all possible BEs ValueType lowerBound = storm::utility::zero(); - for (state->getFailableElements().init(false); !state->getFailableElements().isEnd(); state->getFailableElements().next()) { - lowerBound += state->getBERate(state->getFailableElements().get()); + STORM_LOG_ASSERT(!state->getFailableElements().hasDependencies(), "Lower bound should only be computed if dependencies were already handled."); + for (auto it = state->getFailableElements().begin(); it != state->getFailableElements().end(); ++it) { + lowerBound += state->getBERate(*it); } STORM_LOG_TRACE("Lower bound is " << lowerBound << " for state " << state->getId()); return lowerBound; diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index ab49cad13..10f01fbe2 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.cpp +++ b/src/storm-dft/generator/DftNextStateGenerator.cpp @@ -20,9 +20,16 @@ namespace storm { return deterministicModel; } + template + typename DftNextStateGenerator::DFTStatePointer DftNextStateGenerator::createInitialState() const { + return std::make_shared>(mDft, mStateGenerationInfo, 0); + } + template std::vector DftNextStateGenerator::getInitialStates(StateToIdCallback const& stateToIdCallback) { - DFTStatePointer initialState = std::make_shared>(mDft, mStateGenerationInfo, 0); + DFTStatePointer initialState = createInitialState(); + + // Check whether constant failed BEs are present size_t constFailedBeCounter = 0; std::shared_ptr const> constFailedBE = nullptr; for (auto &be : mDft.getBasicElements()) { @@ -41,7 +48,7 @@ namespace storm { // Register initial state id = stateToIdCallback(initialState); } else { - initialState->letNextBEFail(constFailedBE->id(), false); + initialState->letBEFail(constFailedBE, nullptr); // Propagate the constant failure to reach the real initial state storm::storage::DFTStateSpaceGenerationQueues queues; propagateFailure(initialState, constFailedBE, queues); @@ -99,14 +106,16 @@ namespace storm { // Prepare the result, in case we return early. StateBehavior result; + STORM_LOG_TRACE("Currently failable: " << state->getFailableElements().getCurrentlyFailableString()); //size_t failableCount = hasDependencies ? state->nrFailableDependencies() : state->nrFailableBEs(); //size_t currentFailable = 0; - state->getFailableElements().init(exploreDependencies); + // TODO remove exploreDependencies + auto iterFailable = state->getFailableElements().begin(!exploreDependencies); // Check for absorbing state: // - either no relevant event remains (i.e., all relevant events have failed already), or // - no BE can fail - if (!state->hasOperationalRelevantEvent() || state->getFailableElements().isEnd()) { + if (!state->hasOperationalRelevantEvent() || iterFailable == state->getFailableElements().end(!exploreDependencies)) { Choice choice(0, true); // Add self loop choice.addProbability(state->getId(), storm::utility::one()); @@ -120,55 +129,29 @@ namespace storm { Choice choice(0, !exploreDependencies); // Let BE fail - bool isFirst = true; - while (!state->getFailableElements().isEnd()) { - //TODO outside - if (takeFirstDependency && exploreDependencies && !isFirst) { - // We discard further exploration as we already chose one dependent event - break; - } - isFirst = false; - - // Construct new state as copy from original one - DFTStatePointer newState = state->copy(); - std::pair const>, bool> nextBEPair = newState->letNextBEFail(state->getFailableElements().get(), exploreDependencies); - std::shared_ptr const>& nextBE = nextBEPair.first; + for (; iterFailable != state->getFailableElements().end(!exploreDependencies); ++iterFailable) { + // Get BE which fails next + std::pair const>, std::shared_ptr const>> nextBEPair = iterFailable.getFailBE(mDft); + std::shared_ptr const> nextBE = nextBEPair.first; + std::shared_ptr const> dependency = nextBEPair.second; STORM_LOG_ASSERT(nextBE, "NextBE is null."); - STORM_LOG_ASSERT(nextBEPair.second == exploreDependencies, "Failure due to dependencies does not match."); - STORM_LOG_TRACE("With the failure of: " << nextBE->name() << " [" << nextBE->id() << "] in " << mDft.getStateString(state)); + STORM_LOG_ASSERT(iterFailable.isFailureDueToDependency() == exploreDependencies, "Failure due to dependencies does not match."); + STORM_LOG_ASSERT((dependency != nullptr) == exploreDependencies, "Failure due to dependencies does not match."); - // Propagate - storm::storage::DFTStateSpaceGenerationQueues queues; + // Obtain successor state by propagating failure + DFTStatePointer newState = createSuccessorState(state, nextBE, dependency); - propagateFailure(newState, nextBE, queues); - - bool transient = false; - // TODO handle for all types of BEs. - if (nextBE->beType() == storm::storage::BEType::EXPONENTIAL) { - auto beExp = std::static_pointer_cast const>(nextBE); - transient = beExp->isTransient(); - } - - if(newState->isInvalid() || (transient && !newState->hasFailed(mDft.getTopLevelIndex()))) { - // Continue with next possible state - state->getFailableElements().next(); + if(newState->isInvalid() || newState->isTransient()) { STORM_LOG_TRACE("State is ignored because " << (newState->isInvalid() ? "it is invalid" : "the transient fault is ignored")); + // Continue with next possible state continue; } - // Get the id of the successor state StateType newStateId; if (newState->hasFailed(mDft.getTopLevelIndex()) && uniqueFailedState) { // Use unique failed state newStateId = 0; } else { - propagateFailsafe(newState, nextBE, queues); - - // Update failable dependencies - newState->updateFailableDependencies(nextBE->id()); - newState->updateDontCareDependencies(nextBE->id()); - newState->updateFailableInRestrictions(nextBE->id()); - // Add new state newStateId = stateToIdCallback(newState); } @@ -176,14 +159,14 @@ namespace storm { // Set transitions if (exploreDependencies) { // Failure is due to dependency -> add non-deterministic choice if necessary - ValueType probability = mDft.getDependency(state->getFailableElements().get())->probability(); + ValueType probability = mDft.getDependency(*iterFailable)->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(state->getFailableElements().get()); + unsuccessfulState->letDependencyBeUnsuccessful(*iterFailable); // Add state StateType unsuccessfulStateId = stateToIdCallback(unsuccessfulState); ValueType remainingProbability = storm::utility::one() - probability; @@ -195,22 +178,23 @@ namespace storm { } else { // Failure is due to "normal" BE failure // Set failure rate according to activation - STORM_LOG_THROW(nextBE->beType() == storm::storage::BEType::EXPONENTIAL, storm::exceptions::NotSupportedException, "BE of type '" << nextBE->type() << "' is not supported."); - auto beExp = std::static_pointer_cast const>(nextBE); - bool isActive = true; - if (mDft.hasRepresentant(beExp->id())) { - // Active must be checked for the state we are coming from as this state is responsible for the rate - isActive = state->isActive(mDft.getRepresentant(beExp->id())); - } - ValueType rate = isActive ? beExp->activeFailureRate() : beExp->passiveFailureRate(); + ValueType rate = state->getBERate(nextBE->id()); STORM_LOG_ASSERT(!storm::utility::isZero(rate), "Rate is 0."); choice.addProbability(newStateId, rate); - STORM_LOG_TRACE("Added transition to " << newStateId << " with " << (isActive ? "active" : "passive") << " failure rate " << rate); + STORM_LOG_TRACE("Added transition to " << newStateId << " with failure rate " << rate); } STORM_LOG_ASSERT(newStateId != state->getId(), "Self loop was added for " << newStateId << " and failure of " << nextBE->name()); - state->getFailableElements().next(); - } // end while failing BE + // Handle premature stop for dependencies + if (iterFailable.isFailureDueToDependency() && !iterFailable.isConflictingDependency()) { + // We only explore the first non-conflicting dependency because we can fix an order. + break; + } + if (takeFirstDependency && exploreDependencies) { + // We discard further exploration as we already chose one dependent event + break; + } + } // end iteration of failing BE if (exploreDependencies) { if (result.empty()) { @@ -237,9 +221,48 @@ namespace storm { } template - void DftNextStateGenerator::propagateFailure(DFTStatePointer newState, - std::shared_ptr const> &nextBE, - storm::storage::DFTStateSpaceGenerationQueues &queues) { + typename DftNextStateGenerator::DFTStatePointer DftNextStateGenerator::createSuccessorState(DFTStatePointer const state, std::shared_ptr const>& failedBE, std::shared_ptr const>& triggeringDependency) 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)); + + newState->letBEFail(failedBE, triggeringDependency); + + // Propagate + storm::storage::DFTStateSpaceGenerationQueues queues; + propagateFailure(newState, failedBE, queues); + + // Check whether transient failure lead to TLE failure + // TODO handle for all types of BEs. + if (failedBE->beType() == storm::storage::BEType::EXPONENTIAL) { + auto beExp = std::static_pointer_cast const>(failedBE); + if (beExp->isTransient() && !newState->hasFailed(mDft.getTopLevelIndex())) { + newState->markAsTransient(); + } + } + + // Check whether fail safe propagation can be discarded + bool discardFailSafe = false; + discardFailSafe |= newState->isInvalid(); + discardFailSafe |= newState->isTransient(); + discardFailSafe |= (newState->hasFailed(mDft.getTopLevelIndex()) && uniqueFailedState); + + // Propagate fail safe (if necessary) + if (!discardFailSafe) { + propagateFailsafe(newState, failedBE, queues); + + // Update failable dependencies + newState->updateFailableDependencies(failedBE->id()); + newState->updateDontCareDependencies(failedBE->id()); + newState->updateFailableInRestrictions(failedBE->id()); + } + return newState; + } + + + template + void DftNextStateGenerator::propagateFailure(DFTStatePointer newState, std::shared_ptr const> &nextBE, + storm::storage::DFTStateSpaceGenerationQueues &queues) const { // Propagate failure for (DFTGatePointer parent : nextBE->parents()) { if (newState->isOperational(parent->id())) { @@ -265,13 +288,11 @@ namespace storm { newState->updateFailableDependencies(next->id()); newState->updateFailableInRestrictions(next->id()); } - } template - void DftNextStateGenerator::propagateFailsafe(DFTStatePointer newState, - std::shared_ptr const> &nextBE, - storm::storage::DFTStateSpaceGenerationQueues &queues) { + void DftNextStateGenerator::propagateFailsafe(DFTStatePointer newState, std::shared_ptr const> &nextBE, + storm::storage::DFTStateSpaceGenerationQueues &queues) const { // Propagate failsafe while (!queues.failsafePropagationDone()) { DFTGatePointer next = queues.nextFailsafePropagation(); diff --git a/src/storm-dft/generator/DftNextStateGenerator.h b/src/storm-dft/generator/DftNextStateGenerator.h index 1e912655f..af13b4750 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.h +++ b/src/storm-dft/generator/DftNextStateGenerator.h @@ -48,6 +48,24 @@ namespace storm { */ StateBehavior createMergeFailedState(StateToIdCallback const& stateToIdCallback); + /*! + * Create initial state. + * + * @return Initial state. + */ + DFTStatePointer createInitialState() const; + + /*! + * Create successor state from given state by letting the given BE fail next. + * + * @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). + * + * @return Successor state. + */ + DFTStatePointer createSuccessorState(DFTStatePointer const state, std::shared_ptr const> &failedBE, std::shared_ptr const> &triggeringDependency) const; + /** * Propagate the failures in a given state if the given BE fails * @@ -56,7 +74,7 @@ namespace storm { */ void propagateFailure(DFTStatePointer newState, std::shared_ptr const> &nextBE, - storm::storage::DFTStateSpaceGenerationQueues &queues); + storm::storage::DFTStateSpaceGenerationQueues &queues) const; /** * Propagate the failsafe state in a given state if the given BE fails @@ -66,7 +84,7 @@ namespace storm { */ void propagateFailsafe(DFTStatePointer newState, std::shared_ptr const> &nextBE, - storm::storage::DFTStateSpaceGenerationQueues &queues); + storm::storage::DFTStateSpaceGenerationQueues &queues) const; private: diff --git a/src/storm-dft/simulator/DFTTraceSimulator.cpp b/src/storm-dft/simulator/DFTTraceSimulator.cpp new file mode 100644 index 000000000..fd0af4b14 --- /dev/null +++ b/src/storm-dft/simulator/DFTTraceSimulator.cpp @@ -0,0 +1,124 @@ +#include "DFTTraceSimulator.h" + +namespace storm { + namespace dft { + namespace simulator { + + template + DFTTraceSimulator::DFTTraceSimulator(storm::storage::DFT const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo, boost::mt19937& randomGenerator) : dft(dft), stateGenerationInfo(stateGenerationInfo), generator(dft, stateGenerationInfo), randomGenerator(randomGenerator) { + // Set initial state + state = generator.createInitialState(); + } + + template + void DFTTraceSimulator::setRandomNumberGenerator(boost::mt19937& randomNumberGenerator) { + this->randomGenerator = randomNumberGenerator; + } + + template + void DFTTraceSimulator::resetToInitial() { + state = generator.createInitialState();; + } + + template + typename DFTTraceSimulator::DFTStatePointer DFTTraceSimulator::getCurrentState() const { + return state; + } + + template + double DFTTraceSimulator::randomStep() { + auto iterFailable = state->getFailableElements().begin(); + + // Check for absorbing state: + // - either no relevant event remains (i.e., all relevant events have failed already), or + // - no BE can fail + if (!state->hasOperationalRelevantEvent() || iterFailable == state->getFailableElements().end()) { + STORM_LOG_TRACE("No sucessor states available for " << state->getId()); + return -1; + } + + // Get all failable elements + if (iterFailable.isFailureDueToDependency()) { + if (iterFailable.isConflictingDependency()) { + // 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; + } else { + // Consider all "normal" BE failures + // Initialize with first BE + storm::dft::storage::FailableElements::const_iterator nextFail = iterFailable; + double rate = state->getBERate(iterFailable.getFailBE(dft).first->id()); + storm::utility::ExponentialDistributionGenerator rateGenerator(rate); + double smallestTimebound = rateGenerator.random(randomGenerator); + ++iterFailable; + + // Consider all other BEs and find the one which fails first + for (; iterFailable != state->getFailableElements().end(); ++iterFailable) { + auto nextBE = iterFailable.getFailBE(dft).first; + rate = state->getBERate(nextBE->id()); + rateGenerator = storm::utility::ExponentialDistributionGenerator(rate); + double timebound = rateGenerator.random(randomGenerator); + if (timebound < smallestTimebound) { + // BE fails earlier -> use as nextFail + nextFail = iterFailable; + smallestTimebound = timebound; + } + } + STORM_LOG_TRACE("Let BE " << *nextFail.getFailBE(dft).first << "fail after time " << smallestTimebound); + bool res = step(nextFail); + return res ? smallestTimebound : -1; + } + } + + template + bool DFTTraceSimulator::step(storm::dft::storage::FailableElements::const_iterator nextFailElement) { + if (nextFailElement == state->getFailableElements().end()) { + return false; + } + + auto nextBEPair = nextFailElement.getFailBE(dft); + auto newState = generator.createSuccessorState(state, nextBEPair.first, nextBEPair.second); + + // TODO handle PDEP + + 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; + } + + state = newState; + return true; + } + + template + bool DFTTraceSimulator::simulateCompleteTrace(double timebound) { + resetToInitial(); + 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 state + double res = randomStep(); + 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; + } + time += res; + } + // Time is up + return false; + } + + template class DFTTraceSimulator; + } + } +} diff --git a/src/storm-dft/simulator/DFTTraceSimulator.h b/src/storm-dft/simulator/DFTTraceSimulator.h new file mode 100644 index 000000000..ac54d87a4 --- /dev/null +++ b/src/storm-dft/simulator/DFTTraceSimulator.h @@ -0,0 +1,97 @@ +#include "storm-dft/generator/DftNextStateGenerator.h" +#include "storm-dft/storage/dft/DFT.h" +#include "storm-dft/storage/dft/DFTState.h" +#include "storm-dft/storage/dft/FailableElements.h" + +#include "storm/utility/random.h" + + +namespace storm { + namespace dft { + namespace simulator { + + /*! + * Simulator for DFTs. + * A step in the simulation corresponds to the failure of one BE (either on its own or triggered by a dependency) + * and the failure propagation through the DFT. + * The simulator also allows to randomly generate a next failure according to the failure rates. + */ + template + class DFTTraceSimulator { + using DFTStatePointer = std::shared_ptr>; + public: + /*! + * Constructor. + * + * @param dft DFT. + * @param stateGenerationInfo Info for state generation. + * @param randomGenerator Random number generator. + */ + DFTTraceSimulator(storm::storage::DFT const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo, boost::mt19937& randomGenerator); + + /*! + * Set the random number generator. + * + * @param randomNumberGenerator Random number generator. + */ + void setRandomNumberGenerator(boost::mt19937& randomNumberGenerator); + + /*! + * Set the current state back to the intial state in order to start a new simulation. + */ + void resetToInitial(); + + /*! + * Get the current DFT state. + * + * @return DFTStatePointer DFT state. + */ + DFTStatePointer getCurrentState() const; + + /*! + * 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. + */ + bool step(storm::dft::storage::FailableElements::const_iterator nextFailElement); + + /*! + * 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. + */ + double 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. + * + * @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. + */ + bool simulateCompleteTrace(double timebound); + + protected: + + // The DFT used for the generation of next states. + storm::storage::DFT const& dft; + + // General information for the state generation. + storm::storage::DFTStateGenerationInfo const& stateGenerationInfo; + + // Generator for creating next state in DFT + storm::generator::DftNextStateGenerator generator; + + // Current state + DFTStatePointer state; + + // Random number generator + boost::mt19937& randomGenerator; + }; + } + } +} + diff --git a/src/storm-dft/storage/BucketPriorityQueue.cpp b/src/storm-dft/storage/BucketPriorityQueue.cpp index ceafc00fb..5e4330e3b 100644 --- a/src/storm-dft/storage/BucketPriorityQueue.cpp +++ b/src/storm-dft/storage/BucketPriorityQueue.cpp @@ -193,7 +193,7 @@ namespace storm { for (size_t bucket = 0; bucket < buckets.size(); ++bucket) { out << buckets[bucket].size() << " "; } - std::cout << std::endl; + out << std::endl; } // Template instantiations diff --git a/src/storm-dft/storage/dft/DFTState.cpp b/src/storm-dft/storage/dft/DFTState.cpp index 4be919435..6c58b0923 100644 --- a/src/storm-dft/storage/dft/DFTState.cpp +++ b/src/storm-dft/storage/dft/DFTState.cpp @@ -51,14 +51,14 @@ namespace storm { if (be->canFail()) { switch (be->beType()) { case storm::storage::BEType::CONSTANT: - failableElements.addBE(index); + failableElements.addBE(be->id()); STORM_LOG_TRACE("Currently failable: " << *be); break; case storm::storage::BEType::EXPONENTIAL: { auto beExp = std::static_pointer_cast const>(be); if (!beExp->isColdBasicElement() || !mDft.hasRepresentant(index) || isActive(mDft.getRepresentant(index))) { - failableElements.addBE(index); + failableElements.addBE(be->id()); STORM_LOG_TRACE("Currently failable: " << *beExp); } break; @@ -327,28 +327,19 @@ namespace storm { } template - std::pair const>, bool> DFTState::letNextBEFail(size_t id, bool dueToDependency) { - STORM_LOG_TRACE("currently failable: " << getCurrentlyFailableString()); - if (dueToDependency) { + void DFTState::letBEFail(std::shared_ptr const> be, std::shared_ptr const> dependency) { + STORM_LOG_ASSERT(!hasFailed(be->id()), "Element " << *be << " has already failed."); + if (dependency != nullptr) { // Consider failure due to dependency - std::shared_ptr const> dependency = mDft.getDependency(id); - STORM_LOG_ASSERT(dependency->dependentEvents().size() == 1, "More than one dependent event"); - std::pair const>,bool> res(mDft.getBasicElement(dependency->dependentEvents()[0]->id()), true); - STORM_LOG_ASSERT(!hasFailed(res.first->id()), "Element " << *(res.first) << " has already failed."); - failableElements.removeDependency(id); - setFailed(res.first->id()); + failableElements.removeDependency(dependency->id()); setDependencySuccessful(dependency->id()); - beNoLongerFailable(res.first->id()); - return res; } else { // Consider "normal" failure - std::pair const>,bool> res(mDft.getBasicElement(id), false); - STORM_LOG_ASSERT(!hasFailed(res.first->id()), "Element " << *(res.first) << " has already failed."); - STORM_LOG_ASSERT(res.first->canFail(), "Element " << *(res.first) << " cannot fail."); - failableElements.removeBE(id); - setFailed(res.first->id()); - return res; + STORM_LOG_ASSERT(be->canFail(), "Element " << *be << " cannot fail."); } + // Set BE as failed + setFailed(be->id()); + failableElements.removeBE(be->id()); } template diff --git a/src/storm-dft/storage/dft/DFTState.h b/src/storm-dft/storage/dft/DFTState.h index 9ebe12dba..72774d166 100644 --- a/src/storm-dft/storage/dft/DFTState.h +++ b/src/storm-dft/storage/dft/DFTState.h @@ -1,11 +1,11 @@ #pragma once -#include #include #include "storm/storage/BitVector.h" #include "storm-dft/storage/dft/DFTElementState.h" +#include "storm-dft/storage/dft/FailableElements.h" #include "storm-dft/builder/DftExplorationHeuristic.h" namespace storm { @@ -16,6 +16,8 @@ namespace storm { template class DFTBE; template + class DFTDependency; + template class DFTElement; class DFTStateGenerationInfo; @@ -23,137 +25,16 @@ namespace storm { class DFTState { friend struct std::hash; - struct FailableElements { - - FailableElements(size_t nrElements) : currentlyFailableBE(nrElements), it(currentlyFailableBE.begin()) { - // Intentionally left empty - } - - void addBE(size_t id) { - currentlyFailableBE.set(id); - } - - void addDependency(size_t id, bool isConflicting) { - if (isConflicting) { - if (std::find(mFailableConflictingDependencies.begin(), mFailableConflictingDependencies.end(), - id) == mFailableConflictingDependencies.end()) { - mFailableConflictingDependencies.push_back(id); - } - } else { - if (std::find(mFailableNonconflictingDependencies.begin(), - mFailableNonconflictingDependencies.end(), id) == - mFailableNonconflictingDependencies.end()) { - mFailableNonconflictingDependencies.push_back(id); - } - } - } - - void removeBE(size_t id) { - currentlyFailableBE.set(id, false); - } - - void removeDependency(size_t id) { - auto it1 = std::find(mFailableConflictingDependencies.begin(), - mFailableConflictingDependencies.end(), id); - if (it1 != mFailableConflictingDependencies.end()) { - mFailableConflictingDependencies.erase(it1); - return; - } - auto it2 = std::find(mFailableNonconflictingDependencies.begin(), - mFailableNonconflictingDependencies.end(), id); - if (it2 != mFailableNonconflictingDependencies.end()) { - mFailableNonconflictingDependencies.erase(it2); - return; - } - } - - void clear() { - currentlyFailableBE.clear(); - mFailableConflictingDependencies.clear(); - mFailableNonconflictingDependencies.clear(); - } - - void init(bool dependency) const { - this->dependency = dependency; - if (this->dependency) { - if (!mFailableNonconflictingDependencies.empty()) { - itDep = mFailableNonconflictingDependencies.begin(); - conflicting = false; - } else { - itDep = mFailableConflictingDependencies.begin(); - conflicting = true; - } - } else { - it = currentlyFailableBE.begin(); - } - } - - /** - * Increment iterator. - */ - void next() const { - if (dependency) { - ++itDep; - } else { - ++it; - } - } - - bool isEnd() const { - if (dependency) { - if (!conflicting) { - // If we are handling the non-conflicting FDEPs, end after the first element - return itDep != mFailableNonconflictingDependencies.begin(); - } else { - return itDep == mFailableConflictingDependencies.end(); - } - } else { - return it == currentlyFailableBE.end(); - } - } - - /** - * Get underlying element of iterator. - * @return Id of element. - */ - size_t get() const { - if (dependency) { - return *itDep; - } else { - return *it; - } - }; - - bool hasDependencies() const { - return !mFailableConflictingDependencies.empty() || !mFailableNonconflictingDependencies.empty(); - } - - bool hasBEs() const { - return !currentlyFailableBE.empty(); - } - - mutable bool dependency; - mutable bool conflicting; - - storm::storage::BitVector currentlyFailableBE; - std::vector mFailableConflictingDependencies; - std::vector mFailableNonconflictingDependencies; - std::set remainingRelevantEvents; - - mutable storm::storage::BitVector::const_iterator it; - mutable std::vector::const_iterator itDep; - }; - - private: // Status is bitvector where each element has two bits with the meaning according to DFTElementState storm::storage::BitVector mStatus; size_t mId; - FailableElements failableElements; + storm::dft::storage::FailableElements failableElements; std::vector mUsedRepresentants; size_t indexRelevant; bool mPseudoState; bool mValid = true; + bool mTransient = false; const DFT& mDft; const DFTStateGenerationInfo& mStateGenerationInfo; @@ -240,6 +121,14 @@ namespace storm { return !mValid; } + void markAsTransient() { + mTransient = true; + } + + bool isTransient() const { + return mTransient; + } + bool isPseudoState() const { return mPseudoState; } @@ -248,7 +137,7 @@ namespace storm { return mStatus; } - FailableElements& getFailableElements() { + storm::dft::storage::FailableElements& getFailableElements() { return failableElements; } @@ -348,12 +237,13 @@ namespace storm { void updateDontCareDependencies(size_t id); /** - * Sets the next BE as failed - * @param index Index in currentlyFailableBE of BE to fail - * @param dueToDependency Whether the failure is due to a dependency. - * @return Pair of BE which fails and flag indicating if the failure was due to functional dependencies + * Sets the next BE as failed. + * Optionally also marks the triggering dependency as successful. + * + * @param be BE to fail. + * @param dependency Dependency which triggered the failure (or nullptr if the BE fails on its own). */ - std::pair const>, bool> letNextBEFail(size_t index, bool dueToDependency); + void letBEFail(std::shared_ptr const> be, std::shared_ptr const> dependency); /** * Sets the dependency as unsuccesful meaning no BE will fail. @@ -386,34 +276,6 @@ namespace storm { * @return True iff one operational relevant event exists. */ bool hasOperationalRelevantEvent(); - - std::string getCurrentlyFailableString() const { - std::stringstream stream; - if (failableElements.hasDependencies()) { - failableElements.init(true); - stream << "{Dependencies: "; - stream << failableElements.get(); - failableElements.next(); - while(!failableElements.isEnd()) { - stream << ", " << failableElements.get(); - failableElements.next(); - } - stream << "} "; - } else { - failableElements.init(false); - stream << "{"; - if (!failableElements.isEnd()) { - stream << failableElements.get(); - failableElements.next(); - while (!failableElements.isEnd()) { - stream << ", " << failableElements.get(); - failableElements.next(); - } - } - stream << "}"; - } - return stream.str(); - } friend bool operator==(DFTState const& a, DFTState const& b) { return a.mStatus == b.mStatus; diff --git a/src/storm-dft/storage/dft/FailableElements.cpp b/src/storm-dft/storage/dft/FailableElements.cpp new file mode 100644 index 000000000..66a268bfc --- /dev/null +++ b/src/storm-dft/storage/dft/FailableElements.cpp @@ -0,0 +1,163 @@ +#include "storm-dft/storage/dft/FailableElements.h" + +#include + +#include "storm-dft/storage/dft/DFT.h" + +namespace storm { + namespace dft { + namespace storage { + + FailableElements::const_iterator::const_iterator(bool dependency, bool conflicting, storm::storage::BitVector::const_iterator const& iterBE, std::list::const_iterator const& iterDependency, std::list::const_iterator nonConflictEnd, std::list::const_iterator conflictBegin) + : dependency(dependency), conflicting(conflicting), itBE(iterBE), itDep(iterDependency), nonConflictEnd(nonConflictEnd), conflictBegin(conflictBegin) { + STORM_LOG_ASSERT(conflicting || itDep != nonConflictEnd, "No non-conflicting dependencies present."); + } + + FailableElements::const_iterator& FailableElements::const_iterator::operator++() { + if (dependency) { + ++itDep; + if (!conflicting && itDep == nonConflictEnd) { + // All non-conflicting dependencies considered -> start with conflicting ones + conflicting = true; + itDep = conflictBegin; + } + } else { + ++itBE; + } + return *this; + } + + uint_fast64_t FailableElements::const_iterator::operator*() const { + if (dependency) { + return *itDep; + } else { + return *itBE; + } + } + + bool FailableElements::const_iterator::operator!=(const_iterator const& other) const { + if (dependency != other.dependency || conflicting != other.conflicting) { + return true; + } + if (dependency) { + return itDep != other.itDep; + } else { + return itBE != other.itBE; + } + } + + bool FailableElements::const_iterator::operator==(const_iterator const& other) const { + if (dependency != other.dependency || conflicting != other.conflicting) { + return false; + } + if (dependency) { + return itDep == other.itDep; + } else { + return itBE == other.itBE; + } + } + + bool FailableElements::const_iterator::isFailureDueToDependency() const { + return dependency; + } + + bool FailableElements::const_iterator::isConflictingDependency() const { + return conflicting; + } + + template + std::pair const>, std::shared_ptr const>> FailableElements::const_iterator::getFailBE(storm::storage::DFT const& dft) const { + size_t nextFailId = **this; + if (isFailureDueToDependency()) { + // Consider failure due to dependency + std::shared_ptr const> dependency = dft.getDependency(nextFailId); + STORM_LOG_ASSERT(dependency->dependentEvents().size() == 1, "More than one dependent event"); + return std::make_pair(dft.getBasicElement(dependency->dependentEvents()[0]->id()), dependency); + } else { + // Consider "normal" failure + return std::make_pair(dft.getBasicElement(nextFailId), nullptr); + } + } + + void FailableElements::addBE(size_t id) { + currentlyFailableBE.set(id); + } + + void FailableElements::addDependency(size_t id, bool isConflicting) { + std::list& failableList = (isConflicting ? failableConflictingDependencies : failableNonconflictingDependencies); + for (auto it = failableList.begin(); it != failableList.end(); ++it) { + if (*it > id) { + failableList.insert(it, id); + return; + } else if (*it == id) { + // Dependency already contained + return; + } + } + failableList.push_back(id); + } + + void FailableElements::removeBE(size_t id) { + currentlyFailableBE.set(id, false); + } + + void FailableElements::removeDependency(size_t id) { + auto iter = std::find(failableConflictingDependencies.begin(), failableConflictingDependencies.end(), id); + if (iter != failableConflictingDependencies.end()) { + failableConflictingDependencies.erase(iter); + return; + } + iter = std::find(failableNonconflictingDependencies.begin(), failableNonconflictingDependencies.end(), id); + if (iter != failableNonconflictingDependencies.end()) { + failableNonconflictingDependencies.erase(iter); + return; + } + } + + void FailableElements::clear() { + currentlyFailableBE.clear(); + failableConflictingDependencies.clear(); + failableNonconflictingDependencies.clear(); + } + + FailableElements::const_iterator FailableElements::begin(bool forceBE) const { + bool dependency = hasDependencies() && !forceBE; + bool conflicting = failableNonconflictingDependencies.empty(); + auto itDep = conflicting ? failableConflictingDependencies.begin() : failableNonconflictingDependencies.begin(); + return FailableElements::const_iterator(dependency, conflicting, currentlyFailableBE.begin(), itDep, failableNonconflictingDependencies.end(), failableConflictingDependencies.begin()); + } + + FailableElements::const_iterator FailableElements::end(bool forceBE) const { + bool dependency = hasDependencies() && !forceBE; + return FailableElements::const_iterator(dependency, true, currentlyFailableBE.end(), failableConflictingDependencies.end(), failableNonconflictingDependencies.end(), failableConflictingDependencies.begin()); + } + + bool FailableElements::hasDependencies() const { + return !failableConflictingDependencies.empty() || !failableNonconflictingDependencies.empty(); + } + + bool FailableElements::hasBEs() const { + return !currentlyFailableBE.empty(); + } + + std::string FailableElements::getCurrentlyFailableString() const { + std::stringstream stream; + stream << "{"; + if (hasDependencies()) { + stream << "Dependencies: "; + } + for (auto it = begin(); it != end(); ++it) { + stream << *it << ", "; + } + stream << "}"; + return stream.str(); + } + + // Explicit instantiations. + template std::pair const>, std::shared_ptr const>> FailableElements::const_iterator::getFailBE(storm::storage::DFT const& dft) const; + + template std::pair const>, std::shared_ptr const>> FailableElements::const_iterator::getFailBE(storm::storage::DFT const& dft) const; + + } // namespace storage + } // namespace dft +} // namespace storm \ No newline at end of file diff --git a/src/storm-dft/storage/dft/FailableElements.h b/src/storm-dft/storage/dft/FailableElements.h new file mode 100644 index 000000000..5e048f6df --- /dev/null +++ b/src/storm-dft/storage/dft/FailableElements.h @@ -0,0 +1,241 @@ +#pragma once + +#include +#include + +#include "storm/storage/BitVector.h" + +namespace storm { + namespace storage { + // Forward declarations + template + class DFT; + template + class DFTBE; + template + class DFTDependency; + } + + namespace dft { + namespace storage { + + /*! + * Handling of currently failable elements (BEs) either due to their own failure or because of dependencies. + * + * We distinguish between failures of BEs and failures of dependencies. + * For dependencies, we further distinguish between non-conflicting and conflicting dependencies. + * Non-conflicting dependencies will lead to spurious non-determinsm. + * + * The class supports iterators for all failable elements (either BE or dependencies). + * + */ + class FailableElements { + + public: + /*! + * Iterator for failable elements. + * + */ + class const_iterator : public std::iterator { + + public: + /*! + * Construct a new iterator. + * We either iterate over all failable BEs or over all dependencies (if dependency is true). + * For dependencies, we start with non-conflicting dependencies before iterating over conflicting ones. + * For dependencies, we start with non-conflicting dependencies if they are present. + * + * @param dependency Whether dependencies should be iterated (or BEs if false). + * @param conflicting Whether conflicting dependencies should be iterated (or non-conflicting if false). + * @param iterBE Iterator for BEs. + * @param iterDependency Iterator for Dependencies. + * @param nonConflictEnd Iterator to end of non-conflicting dependencies. + * @param conflictBegin Iterator to begin of conflicting dependencies. + */ + const_iterator(bool dependency, bool conflicting, storm::storage::BitVector::const_iterator const& iterBE, std::list::const_iterator const& iterDependency, std::list::const_iterator nonConflictEnd, std::list::const_iterator conflictBegin); + + /*! + * Constructs an iterator by copying the given iterator. + * + * @param other The iterator to copy. + */ + const_iterator(const_iterator const& other) = default; + + /*! + * Assigns the contents of the given iterator to the current one via copying the former's contents. + * + * @param other The iterator from which to copy-assign. + */ + const_iterator& operator=(const_iterator const& other) = default; + + /*! + * Increment the iterator. + * + * @return A reference to this iterator. + */ + const_iterator& operator++(); + + /*! + * Returns the id of the current failable element. + * + * @return Element id. + */ + uint_fast64_t operator*() const; + + /*! + * Compares the iterator with another iterator for inequality. + * + * @param other The iterator with respect to which inequality is checked. + * @return True if the two iterators are unequal. + */ + bool operator!=(const_iterator const& other) const; + + /*! + * Compares the iterator with another iterator for equality. + * + * @param other The iterator with respect to which equality is checked. + * @return True if the two iterators are equal. + */ + bool operator==(const_iterator const& other) const; + + /*! + * Return whether the current failure is due to a dependency (or the BE itself). + * + * @return true iff current failure is due to dependency. + */ + bool isFailureDueToDependency() const; + + /*! + * Return whether the current dependency failure is conflicting. + * + * @return true iff current dependency failure is conflicting. + */ + bool isConflictingDependency() const; + + /*! + * Obtain the BE which fails from the current iterator. + * Optionally returns the dependency which triggered the BE failure. + * + * @tparam ValueType Value type. + * @param dft DFT. + * @return Pair of the BE which fails and the dependency which triggered the failure (or nullptr if the BE fails on its own). + */ + template + std::pair const>, std::shared_ptr const>> getFailBE(storm::storage::DFT const& dft) const; + + private: + // Whether dependencies are currently considered. + bool dependency; + // Whether the iterator currently points to a conflicting dependency. + bool conflicting; + // Iterators for underlying data structures + storm::storage::BitVector::const_iterator itBE; + std::list::const_iterator itDep; + + // Pointers marking end of non-conflict list and beginning of conflict list + // Used for sequential iteration over all dependencies + std::list::const_iterator nonConflictEnd; + std::list::const_iterator conflictBegin; + }; + + /*! + * Creator. + * + * @param maxBEId Maximal id of a BE. + */ + FailableElements(size_t maxBEId) : currentlyFailableBE(maxBEId) { + } + + /*! + * Add failable BE. + * Note that this invalidates the iterator. + * + * @param id Id of BE. + */ + void addBE(size_t id); + + /*! + * Add failable dependency. + * Note that this invalidates the iterator. + * + * @param id Id of dependency. + * @param isConflicting Whether the dependency is in conflict to other dependencies. In this case + * the conflict needs to be resolved non-deterministically. + */ + void addDependency(size_t id, bool isConflicting); + + /*! + * Remove BE from list of failable elements. + * Note that this invalidates the iterator. + * + * @param id Id of BE. + */ + void removeBE(size_t id); + + /*! + * Remove dependency from list of failable elements. + * Note that this invalidates the iterator. + * + * @param id Id of dependency. + */ + void removeDependency(size_t id); + + /*! + * Clear list of currently failable elements. + * Note that this invalidates the iterator. + */ + void clear(); + + /*! + * Iterator to first failable element. + * If dependencies are present, the iterator is for dependencies. Otherwise it is for BEs. + * For dependencies, the iterator considers non-conflicting dependencies first. + * + * @param forceBE If true, failable dependencies are ignored and only BEs are considered. + * @return Iterator. + */ + FailableElements::const_iterator begin(bool forceBE = false) const; + + /*! + * Iterator after last failable element. + * + * @param forceBE If true, failable dependencies are ignored and only BEs are considered. + * @return Iterator. + */ + FailableElements::const_iterator end(bool forceBE = false) const; + + /*! + * Whether failable dependencies are present. + * + * @return true iff dependencies can fail. + */ + bool hasDependencies() const; + + /*! + * Whether failable BEs are present. + * + * @return true iff BEs can fail. + */ + bool hasBEs() const; + + /*! + * Get a string representation of the currently failable elements. + * + * @return std::string Enumeration of currently failable elements. + */ + std::string getCurrentlyFailableString() const; + + private: + + // We use a BitVector for BEs but a list for dependencies, because usually only a few dependencies are failable at the same time. + // In contrast, usually most BEs are failable. + // The lists of failable elements are sorted by increasing id. + storm::storage::BitVector currentlyFailableBE; + std::list failableConflictingDependencies; + std::list failableNonconflictingDependencies; + + }; + + } // namespace storage + } // namespace dft +} // namespace storm \ No newline at end of file diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index 7b51a552d..0fb923dc0 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp @@ -140,6 +140,18 @@ namespace storm { gameFormula = (qi::lit("<<") > playerCoalition > qi::lit(">>") > operatorFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createGameFormula, phoenix::ref(*this), qi::_1, qi::_2)]; gameFormula.name("game formula"); + stateFormula = (orStateFormula | multiFormula | quantileFormula | gameFormula); + + coalitionOperator = (qi::lit("<<") + > *( (identifier[phoenix::push_back(qi::_a, qi::_1)] + | qi::int_[phoenix::push_back(qi::_a, qi::_1)]) % ',' + ) + > qi::lit(">>"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createCoalition, phoenix::ref(*this), qi::_a)]; + coalitionOperator.name("coalition operator"); + + gameFormula = (coalitionOperator > operatorFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createGameFormula, phoenix::ref(*this), qi::_1, qi::_2)]; + gameFormula.name("game formula"); + stateFormula = (orStateFormula | multiFormula | quantileFormula | gameFormula); stateFormula.name("state formula"); diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp index 1cd2dd8dd..72399c314 100644 --- a/src/storm-parsers/parser/JaniParser.cpp +++ b/src/storm-parsers/parser/JaniParser.cpp @@ -810,7 +810,7 @@ namespace storm { storm::expressions::Expression functionBody; if (!firstPass) { functionBody = parseExpression(functionDefinitionStructure.at("body"), scope.refine("body of function definition " + functionName), false, parameterNameToVariableMap); - STORM_LOG_WARN_COND(functionBody.getType() == type.expressionType, "Type of body of function " + functionName + "' (scope: " + scope.description + ") has type " << functionBody.getType() << " although the function type is given as " << type.expressionType); + STORM_LOG_WARN_COND(functionBody.getType() == type.expressionType || (functionBody.getType().isIntegerType() && type.expressionType.isRationalType()), "Type of body of function " + functionName + "' (scope: " + scope.description + ") has type " << functionBody.getType() << " although the function type is given as " << type.expressionType); } return storm::jani::FunctionDefinition(functionName, type.expressionType, parameters, functionBody); } @@ -1506,7 +1506,7 @@ namespace storm { std::vector> destinationLocationsAndProbabilities; for(auto const& destEntry : edgeEntry.at("destinations")) { // target location - STORM_LOG_THROW(edgeEntry.count("location") == 1, storm::exceptions::InvalidJaniException, "Each destination in edge from '" << sourceLoc << "' in automaton '" << name << "' must have a target location"); + STORM_LOG_THROW(destEntry.count("location") == 1, storm::exceptions::InvalidJaniException, "Each destination in edge from '" << sourceLoc << "' in automaton '" << name << "' must have a target location"); std::string targetLoc = getString(destEntry.at("location"), "target location for edge from '" + sourceLoc + "' in automaton '" + name + "'"); STORM_LOG_THROW(locIds.count(targetLoc) == 1, storm::exceptions::InvalidJaniException, "Target of edge has unknown location '" << targetLoc << "' in automaton '" << name << "'."); // probability diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index 4710dd432..cfe694c2b 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -415,8 +415,8 @@ namespace storm { } int64_t assignedValue = expressionEvaluator.asInt(assignmentIt->getAssignedExpression()); if (this->options.isExplorationChecksSet()) { - STORM_LOG_THROW(assignedValue >= integerIt->lowerBound, storm::exceptions::WrongFormatException, "The update " << assignmentIt->getExpressionVariable().getName() << " := " << assignmentIt->getAssignedExpression() << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getExpressionVariable().getName() << "'."); - STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << assignmentIt->getExpressionVariable().getName() << " := " << assignmentIt->getAssignedExpression() << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getExpressionVariable().getName() << "'."); + STORM_LOG_THROW(!integerIt->lowerBound || assignedValue >= integerIt->lowerBound.get(), storm::exceptions::WrongFormatException, "The update " << assignmentIt->getExpressionVariable().getName() << " := " << assignmentIt->getAssignedExpression() << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getExpressionVariable().getName() << "'."); + STORM_LOG_THROW(!integerIt->upperBound || assignedValue <= integerIt->upperBound.get(), storm::exceptions::WrongFormatException, "The update " << assignmentIt->getExpressionVariable().getName() << " := " << assignmentIt->getAssignedExpression() << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getExpressionVariable().getName() << "'."); } transientValuation.integerValues.emplace_back(&(*integerIt), assignedValue); } diff --git a/src/storm/logic/CloneVisitor.cpp b/src/storm/logic/CloneVisitor.cpp index 1d751bb2e..103c47fc0 100644 --- a/src/storm/logic/CloneVisitor.cpp +++ b/src/storm/logic/CloneVisitor.cpp @@ -4,30 +4,30 @@ namespace storm { namespace logic { - + std::shared_ptr CloneVisitor::clone(Formula const& f) const { boost::any result = f.accept(*this, boost::any()); return boost::any_cast>(result); } - + boost::any CloneVisitor::visit(AtomicExpressionFormula const& f, boost::any const&) const { return std::static_pointer_cast(std::make_shared(f)); } - + boost::any CloneVisitor::visit(AtomicLabelFormula const& f, boost::any const&) const { return std::static_pointer_cast(std::make_shared(f)); } - + boost::any CloneVisitor::visit(BinaryBooleanStateFormula const& f, boost::any const& data) const { std::shared_ptr left = boost::any_cast>(f.getLeftSubformula().accept(*this, data)); std::shared_ptr right = boost::any_cast>(f.getRightSubformula().accept(*this, data)); return std::static_pointer_cast(std::make_shared(f.getOperator(), left, right)); } - + boost::any CloneVisitor::visit(BooleanLiteralFormula const& f, boost::any const&) const { return std::static_pointer_cast(std::make_shared(f)); } - + boost::any CloneVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { std::vector> lowerBounds, upperBounds; std::vector timeBoundReferences; @@ -57,17 +57,17 @@ namespace storm { return std::static_pointer_cast(std::make_shared(left, right, lowerBounds, upperBounds, timeBoundReferences)); } } - + boost::any CloneVisitor::visit(ConditionalFormula const& f, boost::any const& data) const { std::shared_ptr subformula = boost::any_cast>(f.getSubformula().accept(*this, data)); std::shared_ptr conditionFormula = boost::any_cast>(f.getConditionFormula().accept(*this, data)); return std::static_pointer_cast(std::make_shared(subformula, conditionFormula, f.getContext())); } - + boost::any CloneVisitor::visit(CumulativeRewardFormula const& f, boost::any const&) const { return std::static_pointer_cast(std::make_shared(f)); } - + boost::any CloneVisitor::visit(EventuallyFormula const& f, boost::any const& data) const { std::shared_ptr subformula = boost::any_cast>(f.getSubformula().accept(*this, data)); if (f.hasRewardAccumulation()) { @@ -112,41 +112,41 @@ namespace storm { } return std::static_pointer_cast(std::make_shared(subformulas)); } - + boost::any CloneVisitor::visit(QuantileFormula const& f, boost::any const& data) const { std::shared_ptr subformula = boost::any_cast>(f.getSubformula().accept(*this, data)); return std::static_pointer_cast(std::make_shared(f.getBoundVariables(), subformula)); } - + boost::any CloneVisitor::visit(NextFormula const& f, boost::any const& data) const { std::shared_ptr subformula = boost::any_cast>(f.getSubformula().accept(*this, data)); return std::static_pointer_cast(std::make_shared(subformula)); } - + boost::any CloneVisitor::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const { std::shared_ptr subformula = boost::any_cast>(f.getSubformula().accept(*this, data)); return std::static_pointer_cast(std::make_shared(subformula, f.getOperatorInformation())); } - + boost::any CloneVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const { std::shared_ptr subformula = boost::any_cast>(f.getSubformula().accept(*this, data)); return std::static_pointer_cast(std::make_shared(subformula, f.getOptionalRewardModelName(), f.getOperatorInformation())); } - + boost::any CloneVisitor::visit(TotalRewardFormula const& f, boost::any const&) const { return std::static_pointer_cast(std::make_shared(f)); } - + boost::any CloneVisitor::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const { std::shared_ptr subformula = boost::any_cast>(f.getSubformula().accept(*this, data)); return std::static_pointer_cast(std::make_shared(f.getOperator(), subformula)); } - + boost::any CloneVisitor::visit(UntilFormula const& f, boost::any const& data) const { std::shared_ptr left = boost::any_cast>(f.getLeftSubformula().accept(*this, data)); std::shared_ptr right = boost::any_cast>(f.getRightSubformula().accept(*this, data)); return std::static_pointer_cast(std::make_shared(left, right)); } - + } } diff --git a/src/storm/logic/GameFormula.cpp b/src/storm/logic/GameFormula.cpp index a3e3cc649..8387e38fd 100644 --- a/src/storm/logic/GameFormula.cpp +++ b/src/storm/logic/GameFormula.cpp @@ -24,6 +24,10 @@ namespace storm { return coalition; } + void GameFormula::gatherReferencedRewardModels(std::set& referencedRewardModels) const { + this->getSubformula().gatherReferencedRewardModels(referencedRewardModels); + } + boost::any GameFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { return visitor.visit(*this, data); } diff --git a/src/storm/logic/PlayerCoalition.cpp b/src/storm/logic/PlayerCoalition.cpp index e084ed366..45cc683e9 100644 --- a/src/storm/logic/PlayerCoalition.cpp +++ b/src/storm/logic/PlayerCoalition.cpp @@ -1,5 +1,7 @@ #include "storm/logic/PlayerCoalition.h" +#include + namespace storm { namespace logic { diff --git a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp index d7d305741..34a1a8d93 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp +++ b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp @@ -10,9 +10,6 @@ #include "storm/solver/MinMaxLinearEquationSolver.h" #include "storm/solver/Multiplier.h" -// TODO this should be removed as soon as the other TOOD is fixed -#include "storm/environment/solver/MultiplierEnvironment.h" - #include "storm/utility/solver.h" #include "storm/utility/vector.h" @@ -27,7 +24,7 @@ namespace storm { namespace helper { template - SparseNondeterministicGameInfiniteHorizonHelper::SparseNondeterministicGameInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector statesOfCoalition) : SparseInfiniteHorizonHelper(transitionMatrix), statesOfCoalition(statesOfCoalition) { + SparseNondeterministicGameInfiniteHorizonHelper::SparseNondeterministicGameInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitionMatrix, std::vector> const& player) : SparseInfiniteHorizonHelper(transitionMatrix), player(player) { // Intentionally left empty. } @@ -76,12 +73,6 @@ namespace storm { template std::vector SparseNondeterministicGameInfiniteHorizonHelper::computeLongRunAverageValues(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter) { auto underlyingSolverEnvironment = env; - // TODO needs to be removed: - statesOfCoalition.complement(); - underlyingSolverEnvironment.solver().multiplier().setOptimizationDirectionOverride(statesOfCoalition); - - STORM_LOG_DEBUG(statesOfCoalition); - // should be replaced with passing the bitvector std::vector componentLraValues; createDecomposition(); componentLraValues.reserve(this->_longRunComponentDecomposition->size()); diff --git a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h index 2bda8df78..f6075dc57 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h +++ b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h @@ -28,7 +28,7 @@ namespace storm { /*! * Initializes the helper for a discrete time model with different players (i.e. SMG) */ - SparseNondeterministicGameInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector statesOfCoalition); + SparseNondeterministicGameInfiniteHorizonHelper(storm::storage::SparseMatrix const& transitionMatrix, std::vector> const& player); /*! TODO * Computes the long run average value given the provided state and action based rewards @@ -64,7 +64,7 @@ namespace storm { std::vector buildAndSolveSsp(Environment const& env, std::vector const& mecLraValues); private: - storm::storage::BitVector statesOfCoalition; + std::vector> player; }; diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp index 100cb3844..239817adc 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp +++ b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp @@ -197,7 +197,6 @@ namespace storm { if (storm::utility::resources::isTerminate()) { break; } - // If there will be a next iteration, we have to prepare it. if(!gameNondetTs()) { prepareNextIteration(env); @@ -396,7 +395,6 @@ namespace storm { _TsMultiplier->multiplyAndReduce(env, *dir, xOld(), &_TsChoiceValues, xNew(), &tsChoices); setInputModelChoices(*choices, tsChoices); // no components -> no need for that call? } - //std::cin.get(); } else { _TsMultiplier->multiply(env, xOld(), &_TsChoiceValues, xNew()); } diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index e3f5d46fd..c075ab6af 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -55,6 +55,8 @@ namespace storm { } } + + template std::unique_ptr SparseSmgRpatlModelChecker::checkGameFormula(Environment const& env, CheckTask const& checkTask) { Environment solverEnv = env; @@ -148,9 +150,12 @@ namespace storm { template std::unique_ptr SparseSmgRpatlModelChecker::computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); + STORM_LOG_THROW(checkTask.isPlayerCoalitionSet(), storm::exceptions::InvalidPropertyException, "No player coalition was set."); + auto coalitionStates = this->getModel().computeStatesOfCoalition(checkTask.getPlayerCoalition()); + std::cout << "Found " << coalitionStates.getNumberOfSetBits() << " states in coalition." << std::endl; storm::modelchecker::helper::SparseNondeterministicGameInfiniteHorizonHelper helper(this->getModel().getTransitionMatrix(), statesOfCoalition); storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel()); - auto values = helper.computeLongRunAverageRewards(env, rewardModel.get()); + auto values = helper.computeLongRunAverageRewards(env, rewardModel.get()); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(values))); if (checkTask.isProduceSchedulersSet()) { diff --git a/src/storm/models/sparse/Smg.cpp b/src/storm/models/sparse/Smg.cpp index fc758bcc5..4e52f40bc 100644 --- a/src/storm/models/sparse/Smg.cpp +++ b/src/storm/models/sparse/Smg.cpp @@ -38,7 +38,6 @@ namespace storm { storm::storage::PlayerIndex Smg::getPlayerOfState(uint64_t stateIndex) const { STORM_LOG_ASSERT(stateIndex < this->getNumberOfStates(), "Invalid state index: " << stateIndex << "."); return statePlayerIndications[stateIndex]; - } template storm::storage::PlayerIndex Smg::getPlayerIndex(std::string const& playerName) const { diff --git a/src/storm/solver/GmmxxMultiplier.cpp b/src/storm/solver/GmmxxMultiplier.cpp index 19801a28e..66ae1249a 100644 --- a/src/storm/solver/GmmxxMultiplier.cpp +++ b/src/storm/solver/GmmxxMultiplier.cpp @@ -182,7 +182,7 @@ namespace storm { uint64_t currentRowGroup = backwards ? rowGroupIndices.size() - 2 : 0; auto row_group_it = backwards ? rowGroupIndices.end() - 2 : rowGroupIndices.begin(); auto row_group_ite = backwards ? rowGroupIndices.begin() - 1 : rowGroupIndices.end() - 1; - if(choices) STORM_LOG_DEBUG(" "); + //if(choices) STORM_LOG_DEBUG(" "); while (row_group_it != row_group_ite) { ValueType currentValue = storm::utility::zero(); @@ -218,6 +218,7 @@ namespace storm { uint choiceforprintout = 0; //std::cout << currentRowGroup << ": " << currentValue << ", "; //STORM_LOG_DEBUG(std::setprecision(3) << vect_sp(gmm::linalg_traits::row(itr), x) << " + " << *add_it << "; "); + //STORM_LOG_DEBUG(std::setprecision(3) << vect_sp(gmm::linalg_traits::row(itr), x) << " + " << *add_it << "; "); for (uint64_t i = 1; i < rowGroupSize; ++i) { ValueType newValue = b ? *add_it : storm::utility::zero(); newValue += vect_sp(gmm::linalg_traits::row(itr), x); @@ -269,7 +270,7 @@ namespace storm { ++currentRowGroup; } } - std::cout << std::endl; + //std::cout << std::endl; } template<> diff --git a/src/storm/utility/Engine.cpp b/src/storm/utility/Engine.cpp index 45ba5a3dc..adb9ca6e9 100644 --- a/src/storm/utility/Engine.cpp +++ b/src/storm/utility/Engine.cpp @@ -179,10 +179,10 @@ namespace storm { return storm::modelchecker::SparseDtmcPrctlModelChecker>::canHandleStatic(checkTask); case ModelType::CTMC: return storm::modelchecker::SparseCtmcCslModelChecker>::canHandleStatic(checkTask); + case ModelType::SMG: case ModelType::MDP: case ModelType::MA: case ModelType::POMDP: - case ModelType::SMG: return false; } break; diff --git a/src/storm/utility/random.cpp b/src/storm/utility/random.cpp index 9e2d0ae35..8c576cf95 100644 --- a/src/storm/utility/random.cpp +++ b/src/storm/utility/random.cpp @@ -4,17 +4,12 @@ namespace storm { namespace utility { - RandomProbabilityGenerator::RandomProbabilityGenerator() - : distribution(0.0, 1.0) - { + RandomProbabilityGenerator::RandomProbabilityGenerator() : distribution(0.0, 1.0) { std::random_device rd; engine = std::mt19937(rd()); } - RandomProbabilityGenerator::RandomProbabilityGenerator(uint64_t seed) - : distribution(0.0, 1.0), engine(seed) - { - + RandomProbabilityGenerator::RandomProbabilityGenerator(uint64_t seed) : distribution(0.0, 1.0), engine(seed) { } double RandomProbabilityGenerator::random() { @@ -25,22 +20,16 @@ namespace storm { return std::uniform_int_distribution(min, max)(engine); } - RandomProbabilityGenerator::RandomProbabilityGenerator() - : distribution(0, std::numeric_limits::max()) - { + RandomProbabilityGenerator::RandomProbabilityGenerator() : distribution(0, std::numeric_limits::max()) { std::random_device rd; engine = std::mt19937(rd()); } - RandomProbabilityGenerator::RandomProbabilityGenerator(uint64_t seed) - : distribution(0, std::numeric_limits::max()), engine(seed) - { - + RandomProbabilityGenerator::RandomProbabilityGenerator(uint64_t seed) : distribution(0, std::numeric_limits::max()), engine(seed) { } RationalNumber RandomProbabilityGenerator::random() { return carl::rationalize(distribution(engine)) / carl::rationalize(std::numeric_limits::max()); - } uint64_t RandomProbabilityGenerator::random_uint(uint64_t min, uint64_t max) { @@ -48,5 +37,11 @@ namespace storm { } + ExponentialDistributionGenerator::ExponentialDistributionGenerator(double rate) : distribution(rate) { + } + + double ExponentialDistributionGenerator::random(boost::mt19937& engine) { + return distribution(engine); + } } } diff --git a/src/storm/utility/random.h b/src/storm/utility/random.h index 7e6e015be..80a8d5e61 100644 --- a/src/storm/utility/random.h +++ b/src/storm/utility/random.h @@ -1,4 +1,5 @@ #include +#include #include "storm/adapters/RationalNumberAdapter.h" namespace storm { @@ -41,6 +42,13 @@ namespace storm { }; + class ExponentialDistributionGenerator { + public: + ExponentialDistributionGenerator(double rate); + double random(boost::mt19937& engine); + private: + boost::random::exponential_distribution<> distribution; + }; } } \ No newline at end of file diff --git a/src/test/storm-dft/CMakeLists.txt b/src/test/storm-dft/CMakeLists.txt index a2ef04a4b..c54a09ec4 100644 --- a/src/test/storm-dft/CMakeLists.txt +++ b/src/test/storm-dft/CMakeLists.txt @@ -9,7 +9,7 @@ register_source_groups_from_filestructure("${ALL_FILES}" test) # Note that the tests also need the source files, except for the main file include_directories(${GTEST_INCLUDE_DIR}) -foreach (testsuite api storage) +foreach (testsuite api simulator storage) file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_TESTS_BASE_PATH}/${testsuite}/*.cpp) add_executable (test-dft-${testsuite} ${TEST_${testsuite}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp) diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp index 8c6bab4a8..9eb7145ea 100644 --- a/src/test/storm-dft/api/DftModelCheckerTest.cpp +++ b/src/test/storm-dft/api/DftModelCheckerTest.cpp @@ -72,38 +72,35 @@ namespace { return config; } - double analyzeMTTF(std::string const& file) { + double analyze(std::string const& file, std::string const& property) { + // 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); - std::string property = "Tmin=? [F \"failed\"]"; + + // Create property std::vector> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property)); + // Create relevant names std::vector relevantNames; if (!config.useDC) { relevantNames.push_back("all"); } storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents(*dft, properties, relevantNames, false); + // Perform model checking typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFT(*dft, properties, config.useSR, config.useMod, relevantEvents); return boost::get(results[0]); } + double analyzeMTTF(std::string const& file) { + std::string property = "Tmin=? [F \"failed\"]"; + return analyze(file, property); + } + double analyzeReliability(std::string const &file, double bound) { - 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); std::string property = "Pmin=? [F<=" + std::to_string(bound) + " \"failed\"]"; - std::vector> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property)); - - std::vector relevantNames; - if (!config.useDC) { - relevantNames.push_back("all"); - } - storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents(*dft, properties, relevantNames, false); - - typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFT(*dft, properties, config.useSR, config.useMod, relevantEvents); - return boost::get(results[0]); + return analyze(file, property); } private: diff --git a/src/test/storm-dft/simulator/DftSimulatorTest.cpp b/src/test/storm-dft/simulator/DftSimulatorTest.cpp new file mode 100644 index 000000000..9826c8ae3 --- /dev/null +++ b/src/test/storm-dft/simulator/DftSimulatorTest.cpp @@ -0,0 +1,49 @@ +#include "test/storm_gtest.h" +#include "storm-config.h" + +#include "storm-dft/api/storm-dft.h" +#include "storm-dft/transformations/DftTransformator.h" +#include "storm-dft/generator/DftNextStateGenerator.h" +#include "storm-dft/simulator/DFTTraceSimulator.h" +#include "storm-dft/storage/dft/SymmetricUnits.h" + + +namespace { + + // Helper function + double 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); + + // Find symmetries + std::map>> emptySymmetry; + storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); + storm::storage::DFTStateGenerationInfo stateGenerationInfo(dft->buildStateGenerationInfo(symmetries)); + + // Init random number generator + boost::mt19937 gen(5u); + storm::dft::simulator::DFTTraceSimulator simulator(*dft, stateGenerationInfo, gen); + + size_t count = 0;; + bool res; + for (size_t i=0; i + class DftTraceGeneratorTest : public ::testing::Test { + public: + typedef typename TestType::ValueType ValueType; + + DftTraceGeneratorTest() : config(TestType::createConfig()) { + } + + DftTracesConfig const& getConfig() const { + return config; + } + + std::pair>, storm::storage::DFTStateGenerationInfo> prepareDFT(std::string const& file) { + // 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); + + // Compute relevant events + std::vector relevantNames; + if (!config.useDC) { + relevantNames.push_back("all"); + } + storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents(*dft, {}, relevantNames, false); + dft->setRelevantEvents(relevantEvents); + + // Find symmetries + std::map>> emptySymmetry; + storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); + if (config.useSR) { + auto colouring = dft->colourDFT(); + symmetries = dft->findSymmetries(colouring); + } + EXPECT_EQ(config.useSR && config.useDC, !symmetries.sortedSymmetries.empty()); + storm::storage::DFTStateGenerationInfo stateGenerationInfo(dft->buildStateGenerationInfo(symmetries)); + return std::make_pair(dft, stateGenerationInfo); + } + + private: + DftTracesConfig config; + }; + + typedef ::testing::Types< + NoOptimizationsConfig, + DontCareConfig, + SymmetryReductionConfig, + AllOptimizationsConfig + > TestingTypes; + + TYPED_TEST_SUITE(DftTraceGeneratorTest, TestingTypes,); + + TYPED_TEST(DftTraceGeneratorTest, And) { + auto pair = this->prepareDFT(STORM_TEST_RESOURCES_DIR "/dft/and.dft"); + auto dft = pair.first; + storm::generator::DftNextStateGenerator generator(*dft, pair.second); + + // Start with initial state + auto state = generator.createInitialState(); + EXPECT_FALSE(state->hasFailed(dft->getTopLevelIndex())); + + bool changed = state->orderBySymmetry(); + EXPECT_FALSE(changed); + + // Let C fail + auto iterFailable = state->getFailableElements().begin(); + ASSERT_NE(iterFailable, state->getFailableElements().end()); + ++iterFailable; + ASSERT_NE(iterFailable, state->getFailableElements().end()); + + auto nextBEPair = iterFailable.getFailBE(*dft); + auto nextBE = nextBEPair.first; + auto triggerDep = nextBEPair.second; + ASSERT_TRUE(nextBE); + ASSERT_FALSE(triggerDep); + ASSERT_EQ(nextBE->name(), "C"); + state = generator.createSuccessorState(state, nextBE, triggerDep); + EXPECT_FALSE(state->hasFailed(dft->getTopLevelIndex())); + changed = state->orderBySymmetry(); + EXPECT_EQ(this->getConfig().useSR && this->getConfig().useDC, changed); + if (this->getConfig().useSR && this->getConfig().useDC) { + EXPECT_TRUE(state->hasFailed(0)); + } else { + EXPECT_TRUE(state->hasFailed(1)); + } + + // Let B fail + iterFailable = state->getFailableElements().begin(); + ASSERT_NE(iterFailable, state->getFailableElements().end()); + + nextBEPair = iterFailable.getFailBE(*dft); + nextBE = nextBEPair.first; + triggerDep = nextBEPair.second; + ASSERT_TRUE(nextBE); + ASSERT_FALSE(triggerDep); + if (this->getConfig().useSR && this->getConfig().useDC){ + // TODO: Apply symmetry to failable elements as well + return; + ASSERT_EQ(nextBE->name(), "C"); + } else { + ASSERT_EQ(nextBE->name(), "B"); + } + state = generator.createSuccessorState(state, nextBE, triggerDep); + changed = state->orderBySymmetry(); + EXPECT_FALSE(changed); + EXPECT_TRUE(state->hasFailed(dft->getTopLevelIndex())); + } + + TYPED_TEST(DftTraceGeneratorTest, RandomStepsAnd) { + auto pair = this->prepareDFT(STORM_TEST_RESOURCES_DIR "/dft/and.dft"); + auto dft = pair.first; + + // Init random number generator + boost::mt19937 gen(5u); + storm::dft::simulator::DFTTraceSimulator simulator(*dft, pair.second, gen); + + auto state = simulator.getCurrentState(); + EXPECT_FALSE(state->hasFailed(dft->getTopLevelIndex())); + + // First random step + double timebound = simulator.randomStep(); +#if BOOST_VERSION > 106400 + // Older Boost versions yield different value + EXPECT_FLOAT_EQ(timebound, 0.522079); +#endif + state = simulator.getCurrentState(); + EXPECT_FALSE(state->hasFailed(dft->getTopLevelIndex())); + + timebound = simulator.randomStep(); +#if BOOST_VERSION > 106400 + // Older Boost versions yield different value + EXPECT_FLOAT_EQ(timebound, 0.9497214); +#endif + state = simulator.getCurrentState(); + EXPECT_TRUE(state->hasFailed(dft->getTopLevelIndex())); + } + +} diff --git a/src/test/storm-dft/simulator/SamplingTest.cpp b/src/test/storm-dft/simulator/SamplingTest.cpp new file mode 100644 index 000000000..524947d31 --- /dev/null +++ b/src/test/storm-dft/simulator/SamplingTest.cpp @@ -0,0 +1,25 @@ +#include "test/storm_gtest.h" +#include "storm-config.h" + +#include + +namespace { + + TEST(SamplingTest, SampleExponential) { +#if BOOST_VERSION < 106400 + // Boost changed implementation of exponential distribution + // -> different values are returned + GTEST_SKIP(); + return; +#endif + boost::mt19937 gen(5u); + storm::utility::ExponentialDistributionGenerator dist(5); + + // Ensure that pseudo random numbers are the same on all machines + double reference[] = {0.18241937154, 0.0522078772595, 0.0949721368604, 0.246869315378, 0.765000791199, 0.0177096648877, 0.225167598601, 0.23538530391, 1.01605360643, 0.138846355094}; + for (int i =0; i < 10; ++i) { + EXPECT_FLOAT_EQ(dist.random(gen), reference[i]); + } + } + +}