sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Added const qualifiers

tempestpy_adaptions
Matthias Volk 4 years ago
parent
fe014aaceb
commit
d04268a294
No known key found for this signature in database GPG Key ID: 83A57678F739FCD3
2 changed files with 23 additions and 11 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 21
      src/storm-dft/generator/DftNextStateGenerator.cpp
  2. 13
      src/storm-dft/generator/DftNextStateGenerator.h

21
src/storm-dft/generator/DftNextStateGenerator.cpp
View File

@ -20,9 +20,16 @@ namespace storm {
return deterministicModel; return deterministicModel;
} }
template<typename ValueType, typename StateType>
typename DftNextStateGenerator<ValueType, StateType>::DFTStatePointer DftNextStateGenerator<ValueType, StateType>::createInitialState() const {
return std::make_shared<storm::storage::DFTState<ValueType>>(mDft, mStateGenerationInfo, 0);
}
template<typename ValueType, typename StateType> template<typename ValueType, typename StateType>
std::vector<StateType> DftNextStateGenerator<ValueType, StateType>::getInitialStates(StateToIdCallback const& stateToIdCallback) { std::vector<StateType> DftNextStateGenerator<ValueType, StateType>::getInitialStates(StateToIdCallback const& stateToIdCallback) {
DFTStatePointer initialState = std::make_shared<storm::storage::DFTState<ValueType>>(mDft, mStateGenerationInfo, 0);
DFTStatePointer initialState = createInitialState();
// Check whether constant failed BEs are present
size_t constFailedBeCounter = 0; size_t constFailedBeCounter = 0;
std::shared_ptr<storm::storage::DFTBE<ValueType> const> constFailedBE = nullptr; std::shared_ptr<storm::storage::DFTBE<ValueType> const> constFailedBE = nullptr;
for (auto &be : mDft.getBasicElements()) { for (auto &be : mDft.getBasicElements()) {
@ -214,7 +221,7 @@ namespace storm {
} }
template<typename ValueType, typename StateType> template<typename ValueType, typename StateType>
typename DftNextStateGenerator<ValueType, StateType>::DFTStatePointer DftNextStateGenerator<ValueType, StateType>::createSuccessorState(DFTStatePointer const state, std::shared_ptr<storm::storage::DFTBE<ValueType> const>& failedBE, std::shared_ptr<storm::storage::DFTDependency<ValueType> const>& triggeringDependency) {
typename DftNextStateGenerator<ValueType, StateType>::DFTStatePointer DftNextStateGenerator<ValueType, StateType>::createSuccessorState(DFTStatePointer const state, std::shared_ptr<storm::storage::DFTBE<ValueType> const>& failedBE, std::shared_ptr<storm::storage::DFTDependency<ValueType> const>& triggeringDependency) const {
// Construct new state as copy from original one // Construct new state as copy from original one
DFTStatePointer newState = state->copy(); 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)); 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));
@ -254,9 +261,8 @@ namespace storm {
template<typename ValueType, typename StateType> template<typename ValueType, typename StateType>
void DftNextStateGenerator<ValueType, StateType>::propagateFailure(DFTStatePointer newState,
std::shared_ptr<storm::storage::DFTBE<ValueType> const> &nextBE,
storm::storage::DFTStateSpaceGenerationQueues<ValueType> &queues) {
void DftNextStateGenerator<ValueType, StateType>::propagateFailure(DFTStatePointer newState, std::shared_ptr<storm::storage::DFTBE<ValueType> const> &nextBE,
storm::storage::DFTStateSpaceGenerationQueues<ValueType> &queues) const {
// Propagate failure // Propagate failure
for (DFTGatePointer parent : nextBE->parents()) { for (DFTGatePointer parent : nextBE->parents()) {
if (newState->isOperational(parent->id())) { if (newState->isOperational(parent->id())) {
@ -285,9 +291,8 @@ namespace storm {
} }
template<typename ValueType, typename StateType> template<typename ValueType, typename StateType>
void DftNextStateGenerator<ValueType, StateType>::propagateFailsafe(DFTStatePointer newState,
std::shared_ptr<storm::storage::DFTBE<ValueType> const> &nextBE,
storm::storage::DFTStateSpaceGenerationQueues<ValueType> &queues) {
void DftNextStateGenerator<ValueType, StateType>::propagateFailsafe(DFTStatePointer newState, std::shared_ptr<storm::storage::DFTBE<ValueType> const> &nextBE,
storm::storage::DFTStateSpaceGenerationQueues<ValueType> &queues) const {
// Propagate failsafe // Propagate failsafe
while (!queues.failsafePropagationDone()) { while (!queues.failsafePropagationDone()) {
DFTGatePointer next = queues.nextFailsafePropagation(); DFTGatePointer next = queues.nextFailsafePropagation();

13
src/storm-dft/generator/DftNextStateGenerator.h
View File

@ -48,6 +48,13 @@ namespace storm {
*/ */
StateBehavior<ValueType, StateType> createMergeFailedState(StateToIdCallback const& stateToIdCallback); StateBehavior<ValueType, StateType> 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. * Create successor state from given state by letting the given BE fail next.
* *
@ -57,7 +64,7 @@ namespace storm {
* *
* @return Successor state. * @return Successor state.
*/ */
DFTStatePointer createSuccessorState(DFTStatePointer const state, std::shared_ptr<storm::storage::DFTBE<ValueType> const> &failedBE, std::shared_ptr<storm::storage::DFTDependency<ValueType> const> &triggeringDependency);
DFTStatePointer createSuccessorState(DFTStatePointer const state, std::shared_ptr<storm::storage::DFTBE<ValueType> const> &failedBE, std::shared_ptr<storm::storage::DFTDependency<ValueType> const> &triggeringDependency) const;
/** /**
* Propagate the failures in a given state if the given BE fails * Propagate the failures in a given state if the given BE fails
@ -67,7 +74,7 @@ namespace storm {
*/ */
void void
propagateFailure(DFTStatePointer newState, std::shared_ptr<storm::storage::DFTBE<ValueType> const> &nextBE, propagateFailure(DFTStatePointer newState, std::shared_ptr<storm::storage::DFTBE<ValueType> const> &nextBE,
storm::storage::DFTStateSpaceGenerationQueues<ValueType> &queues);
storm::storage::DFTStateSpaceGenerationQueues<ValueType> &queues) const;
/** /**
* Propagate the failsafe state in a given state if the given BE fails * Propagate the failsafe state in a given state if the given BE fails
@ -77,7 +84,7 @@ namespace storm {
*/ */
void void
propagateFailsafe(DFTStatePointer newState, std::shared_ptr<storm::storage::DFTBE<ValueType> const> &nextBE, propagateFailsafe(DFTStatePointer newState, std::shared_ptr<storm::storage::DFTBE<ValueType> const> &nextBE,
storm::storage::DFTStateSpaceGenerationQueues<ValueType> &queues);
storm::storage::DFTStateSpaceGenerationQueues<ValueType> &queues) const;
private: private:

Write Preview
Loading…
Cancel
Save