33 changed files with 1123 additions and 462 deletions
-
139.github/workflows/buildtest.yml
-
17CHANGELOG.md
-
3README.md
-
5src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
-
143src/storm-dft/generator/DftNextStateGenerator.cpp
-
22src/storm-dft/generator/DftNextStateGenerator.h
-
124src/storm-dft/simulator/DFTTraceSimulator.cpp
-
97src/storm-dft/simulator/DFTTraceSimulator.h
-
2src/storm-dft/storage/BucketPriorityQueue.cpp
-
29src/storm-dft/storage/dft/DFTState.cpp
-
178src/storm-dft/storage/dft/DFTState.h
-
163src/storm-dft/storage/dft/FailableElements.cpp
-
241src/storm-dft/storage/dft/FailableElements.h
-
12src/storm-parsers/parser/FormulaParserGrammar.cpp
-
4src/storm-parsers/parser/JaniParser.cpp
-
4src/storm/generator/JaniNextStateGenerator.cpp
-
34src/storm/logic/CloneVisitor.cpp
-
4src/storm/logic/GameFormula.cpp
-
2src/storm/logic/PlayerCoalition.cpp
-
11src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp
-
4src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h
-
2src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp
-
7src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
-
1src/storm/models/sparse/Smg.cpp
-
5src/storm/solver/GmmxxMultiplier.cpp
-
2src/storm/utility/Engine.cpp
-
25src/storm/utility/random.cpp
-
8src/storm/utility/random.h
-
2src/test/storm-dft/CMakeLists.txt
-
27src/test/storm-dft/api/DftModelCheckerTest.cpp
-
49src/test/storm-dft/simulator/DftSimulatorTest.cpp
-
194src/test/storm-dft/simulator/DftTraceGeneratorTest.cpp
-
25src/test/storm-dft/simulator/SamplingTest.cpp
@ -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 }} |
|||
@ -0,0 +1,124 @@ |
|||
#include "DFTTraceSimulator.h"
|
|||
|
|||
namespace storm { |
|||
namespace dft { |
|||
namespace simulator { |
|||
|
|||
template<typename ValueType> |
|||
DFTTraceSimulator<ValueType>::DFTTraceSimulator(storm::storage::DFT<ValueType> 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<typename ValueType> |
|||
void DFTTraceSimulator<ValueType>::setRandomNumberGenerator(boost::mt19937& randomNumberGenerator) { |
|||
this->randomGenerator = randomNumberGenerator; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
void DFTTraceSimulator<ValueType>::resetToInitial() { |
|||
state = generator.createInitialState();; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
typename DFTTraceSimulator<ValueType>::DFTStatePointer DFTTraceSimulator<ValueType>::getCurrentState() const { |
|||
return state; |
|||
} |
|||
|
|||
template<typename ValueType> |
|||
double DFTTraceSimulator<ValueType>::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<typename ValueType> |
|||
bool DFTTraceSimulator<ValueType>::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<typename ValueType> |
|||
bool DFTTraceSimulator<ValueType>::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<double>; |
|||
} |
|||
} |
|||
} |
|||
@ -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<typename ValueType> |
|||
class DFTTraceSimulator { |
|||
using DFTStatePointer = std::shared_ptr<storm::storage::DFTState<ValueType>>; |
|||
public: |
|||
/*! |
|||
* Constructor. |
|||
* |
|||
* @param dft DFT. |
|||
* @param stateGenerationInfo Info for state generation. |
|||
* @param randomGenerator Random number generator. |
|||
*/ |
|||
DFTTraceSimulator(storm::storage::DFT<ValueType> 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<ValueType> const& dft; |
|||
|
|||
// General information for the state generation. |
|||
storm::storage::DFTStateGenerationInfo const& stateGenerationInfo; |
|||
|
|||
// Generator for creating next state in DFT |
|||
storm::generator::DftNextStateGenerator<double> generator; |
|||
|
|||
// Current state |
|||
DFTStatePointer state; |
|||
|
|||
// Random number generator |
|||
boost::mt19937& randomGenerator; |
|||
}; |
|||
} |
|||
} |
|||
} |
|||
|
|||
@ -0,0 +1,163 @@ |
|||
#include "storm-dft/storage/dft/FailableElements.h"
|
|||
|
|||
#include <sstream>
|
|||
|
|||
#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<size_t>::const_iterator const& iterDependency, std::list<size_t>::const_iterator nonConflictEnd, std::list<size_t>::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<typename ValueType> |
|||
std::pair<std::shared_ptr<storm::storage::DFTBE<ValueType> const>, std::shared_ptr<storm::storage::DFTDependency<ValueType> const>> FailableElements::const_iterator::getFailBE(storm::storage::DFT<ValueType> const& dft) const { |
|||
size_t nextFailId = **this; |
|||
if (isFailureDueToDependency()) { |
|||
// Consider failure due to dependency
|
|||
std::shared_ptr<storm::storage::DFTDependency<ValueType> 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<size_t>& 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<std::shared_ptr<storm::storage::DFTBE<double> const>, std::shared_ptr<storm::storage::DFTDependency<double> const>> FailableElements::const_iterator::getFailBE(storm::storage::DFT<double> const& dft) const; |
|||
|
|||
template std::pair<std::shared_ptr<storm::storage::DFTBE<storm::RationalFunction> const>, std::shared_ptr<storm::storage::DFTDependency<storm::RationalFunction> const>> FailableElements::const_iterator::getFailBE(storm::storage::DFT<storm::RationalFunction> const& dft) const; |
|||
|
|||
} // namespace storage
|
|||
} // namespace dft
|
|||
} // namespace storm
|
|||
@ -0,0 +1,241 @@ |
|||
#pragma once |
|||
|
|||
#include <list> |
|||
#include <memory> |
|||
|
|||
#include "storm/storage/BitVector.h" |
|||
|
|||
namespace storm { |
|||
namespace storage { |
|||
// Forward declarations |
|||
template<typename ValueType> |
|||
class DFT; |
|||
template<typename ValueType> |
|||
class DFTBE; |
|||
template<typename ValueType> |
|||
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<std::input_iterator_tag, size_t> { |
|||
|
|||
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<size_t>::const_iterator const& iterDependency, std::list<size_t>::const_iterator nonConflictEnd, std::list<size_t>::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<typename ValueType> |
|||
std::pair<std::shared_ptr<storm::storage::DFTBE<ValueType> const>, std::shared_ptr<storm::storage::DFTDependency<ValueType> const>> getFailBE(storm::storage::DFT<ValueType> 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<size_t>::const_iterator itDep; |
|||
|
|||
// Pointers marking end of non-conflict list and beginning of conflict list |
|||
// Used for sequential iteration over all dependencies |
|||
std::list<size_t>::const_iterator nonConflictEnd; |
|||
std::list<size_t>::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<size_t> failableConflictingDependencies; |
|||
std::list<size_t> failableNonconflictingDependencies; |
|||
|
|||
}; |
|||
|
|||
} // namespace storage |
|||
} // namespace dft |
|||
} // namespace storm |
|||
@ -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<double> dftTransformator = storm::transformations::dft::DftTransformator<double>(); |
|||
std::shared_ptr<storm::storage::DFT<double>> dft = dftTransformator.transformBinaryFDEPs(*(storm::api::loadDFTGalileoFile<double>(file))); |
|||
EXPECT_TRUE(storm::api::isWellFormed(*dft).first); |
|||
|
|||
// Set relevant events
|
|||
storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents<double>(*dft, {}, {}, false); |
|||
dft->setRelevantEvents(relevantEvents); |
|||
|
|||
// Find symmetries
|
|||
std::map<size_t, std::vector<std::vector<size_t>>> 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<double> simulator(*dft, stateGenerationInfo, gen); |
|||
|
|||
size_t count = 0;; |
|||
bool res; |
|||
for (size_t i=0; i<noRuns; ++i) { |
|||
res = simulator.simulateCompleteTrace(timebound); |
|||
if (res) { |
|||
++count; |
|||
} |
|||
} |
|||
return (double) count / noRuns; |
|||
} |
|||
|
|||
TEST(DftSimulatorTest, And) { |
|||
double result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/and.dft", 2, 10000); |
|||
EXPECT_NEAR(result, 0.3995764009, 0.01); |
|||
} |
|||
|
|||
} |
|||
@ -0,0 +1,194 @@ |
|||
#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"
|
|||
#include "storm-dft/storage/dft/DFTIsomorphism.h"
|
|||
|
|||
#include "storm-parsers/api/storm-parsers.h"
|
|||
|
|||
namespace { |
|||
|
|||
// Configurations for DFT traces
|
|||
struct DftTracesConfig { |
|||
bool useDC; |
|||
bool useSR; |
|||
}; |
|||
|
|||
class NoOptimizationsConfig { |
|||
public: |
|||
typedef double ValueType; |
|||
|
|||
static DftTracesConfig createConfig() { |
|||
return DftTracesConfig{false, false}; |
|||
} |
|||
}; |
|||
|
|||
class DontCareConfig { |
|||
public: |
|||
typedef double ValueType; |
|||
|
|||
static DftTracesConfig createConfig() { |
|||
return DftTracesConfig{true, false}; |
|||
} |
|||
}; |
|||
|
|||
class SymmetryReductionConfig { |
|||
public: |
|||
typedef double ValueType; |
|||
|
|||
static DftTracesConfig createConfig() { |
|||
return DftTracesConfig{false, true}; |
|||
} |
|||
}; |
|||
|
|||
class AllOptimizationsConfig { |
|||
public: |
|||
typedef double ValueType; |
|||
|
|||
static DftTracesConfig createConfig() { |
|||
return DftTracesConfig{true, true}; |
|||
} |
|||
}; |
|||
|
|||
// General base class for testing of generating DFT traces.
|
|||
template<typename TestType> |
|||
class DftTraceGeneratorTest : public ::testing::Test { |
|||
public: |
|||
typedef typename TestType::ValueType ValueType; |
|||
|
|||
DftTraceGeneratorTest() : config(TestType::createConfig()) { |
|||
} |
|||
|
|||
DftTracesConfig const& getConfig() const { |
|||
return config; |
|||
} |
|||
|
|||
std::pair<std::shared_ptr<storm::storage::DFT<double>>, storm::storage::DFTStateGenerationInfo> prepareDFT(std::string const& file) { |
|||
// Load, build and prepare DFT
|
|||
storm::transformations::dft::DftTransformator<double> dftTransformator = storm::transformations::dft::DftTransformator<double>(); |
|||
std::shared_ptr<storm::storage::DFT<double>> dft = dftTransformator.transformBinaryFDEPs(*(storm::api::loadDFTGalileoFile<double>(file))); |
|||
EXPECT_TRUE(storm::api::isWellFormed(*dft).first); |
|||
|
|||
// Compute relevant events
|
|||
std::vector<std::string> relevantNames; |
|||
if (!config.useDC) { |
|||
relevantNames.push_back("all"); |
|||
} |
|||
storm::utility::RelevantEvents relevantEvents = storm::api::computeRelevantEvents<double>(*dft, {}, relevantNames, false); |
|||
dft->setRelevantEvents(relevantEvents); |
|||
|
|||
// Find symmetries
|
|||
std::map<size_t, std::vector<std::vector<size_t>>> 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<double> 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<double> 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())); |
|||
} |
|||
|
|||
} |
|||
@ -0,0 +1,25 @@ |
|||
#include "test/storm_gtest.h"
|
|||
#include "storm-config.h"
|
|||
|
|||
#include <storm/utility/random.h>
|
|||
|
|||
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]); |
|||
} |
|||
} |
|||
|
|||
} |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue