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

Added support for constantly failed BEs in the model generation

main
Alexander Bork 6 years ago
parent
a257071346
commit
2ec921a683
3 changed files with 136 additions and 39 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 20
      src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
  2. 135
      src/storm-dft/generator/DftNextStateGenerator.cpp
  3. 20
      src/storm-dft/generator/DftNextStateGenerator.h

20
src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
View File

@ -167,6 +167,26 @@ namespace storm {
STORM_LOG_ASSERT(stateStorage.initialStateIndices.size() == 1, "Only one initial state assumed.");
initialStateIndex = stateStorage.initialStateIndices[0];
STORM_LOG_TRACE("Initial state: " << initialStateIndex);
// DFT may be instantly failed due to a constant failure
// in this case a model only consisting of the uniqueFailedState suffices
if (initialStateIndex == 0 && this->uniqueFailedState) {
modelComponents.markovianStates.resize(1);
modelComponents.deterministicModel = generator.isDeterministicModel();
STORM_LOG_TRACE("Markovian states: " << modelComponents.markovianStates);
STORM_LOG_DEBUG("Model has 1 state");
STORM_LOG_DEBUG(
"Model is " << (generator.isDeterministicModel() ? "deterministic" : "non-deterministic"));
// Build transition matrix
modelComponents.transitionMatrix = matrixBuilder.builder.build(1, 1);
STORM_LOG_TRACE("Transition matrix: " << std::endl << modelComponents.transitionMatrix);
buildLabeling();
return;
}
// Initialize heuristic values for inital state
STORM_LOG_ASSERT(!statesNotExplored.at(initialStateIndex).second, "Heuristic for initial state is already initialized");
ExplorationHeuristicPointer heuristic;

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

@ -22,11 +22,53 @@ namespace storm {
template<typename ValueType, typename StateType>
std::vector<StateType> DftNextStateGenerator<ValueType, StateType>::getInitialStates(StateToIdCallback const& stateToIdCallback) {
DFTStatePointer initialState = std::make_shared<storm::storage::DFTState<ValueType>>(mDft, mStateGenerationInfo, 0);
size_t constFailedBeCounter = 0;
std::shared_ptr<storm::storage::DFTBE<ValueType> const> constFailedBE = nullptr;
for (auto &be : mDft.getBasicElements()) {
if (be->type() == storm::storage::DFTElementType::BE_CONST) {
auto constBe = std::static_pointer_cast<storm::storage::BEConst<ValueType> const>(be);
if (constBe->failed()) {
constFailedBeCounter++;
STORM_LOG_THROW(constFailedBeCounter < 2, storm::exceptions::NotSupportedException,
"DFTs with more than one constantly failed BE are not supported");
constFailedBE = constBe;
}
}
}
StateType id;
if (constFailedBeCounter == 0) {
// Register initial state
StateType id = stateToIdCallback(initialState);
id = stateToIdCallback(initialState);
} else {
initialState->letNextBEFail(constFailedBE->id(), false);
// Propagate the constant failure to reach the real initial state
storm::storage::DFTStateSpaceGenerationQueues<ValueType> queues;
propagateFailure(initialState, constFailedBE, queues);
if (initialState->hasFailed(mDft.getTopLevelIndex()) && uniqueFailedState) {
propagateFailsafe(initialState, constFailedBE, queues);
// Update failable dependencies
initialState->updateFailableDependencies(constFailedBE->id());
initialState->updateDontCareDependencies(constFailedBE->id());
initialState->updateFailableInRestrictions(constFailedBE->id());
// Unique failed state
id = 0;
} else {
propagateFailsafe(initialState, constFailedBE, queues);
// Update failable dependencies
initialState->updateFailableDependencies(constFailedBE->id());
initialState->updateDontCareDependencies(constFailedBE->id());
initialState->updateFailableInRestrictions(constFailedBE->id());
id = stateToIdCallback(initialState);
}
}
initialState->setId(id);
return {id};
}
@ -90,31 +132,7 @@ namespace storm {
// Propagate
storm::storage::DFTStateSpaceGenerationQueues<ValueType> queues;
// Propagate failure
for (DFTGatePointer parent : nextBE->parents()) {
if (newState->isOperational(parent->id())) {
queues.propagateFailure(parent);
}
}
// Propagate failures
while (!queues.failurePropagationDone()) {
DFTGatePointer next = queues.nextFailurePropagation();
next->checkFails(*newState, queues);
newState->updateFailableDependencies(next->id());
newState->updateFailableInRestrictions(next->id());
}
// Check restrictions
for (DFTRestrictionPointer restr : nextBE->restrictions()) {
queues.checkRestrictionLater(restr);
}
// Check restrictions
while(!queues.restrictionChecksDone()) {
DFTRestrictionPointer next = queues.nextRestrictionCheck();
next->checkFails(*newState, queues);
newState->updateFailableDependencies(next->id());
newState->updateFailableInRestrictions(next->id());
}
propagateFailure(newState, nextBE, queues);
newState->updateRemainingRelevantEvents();
@ -137,18 +155,7 @@ namespace storm {
// Use unique failed state
newStateId = 0;
} else {
// Propagate failsafe
while (!queues.failsafePropagationDone()) {
DFTGatePointer next = queues.nextFailsafePropagation();
next->checkFailsafe(*newState, queues);
}
// Propagate dont cares
// Relevance is considered for each element independently
while (!queues.dontCarePropagationDone()) {
DFTElementPointer next = queues.nextDontCarePropagation();
next->checkDontCareAnymore(*newState, queues);
}
propagateFailsafe(newState, nextBE, queues);
// Update failable dependencies
newState->updateFailableDependencies(nextBE->id());
@ -222,6 +229,56 @@ namespace storm {
return result;
}
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) {
// Propagate failure
for (DFTGatePointer parent : nextBE->parents()) {
if (newState->isOperational(parent->id())) {
queues.propagateFailure(parent);
}
}
// Propagate failures
while (!queues.failurePropagationDone()) {
DFTGatePointer next = queues.nextFailurePropagation();
next->checkFails(*newState, queues);
newState->updateFailableDependencies(next->id());
newState->updateFailableInRestrictions(next->id());
}
// Check restrictions
for (DFTRestrictionPointer restr : nextBE->restrictions()) {
queues.checkRestrictionLater(restr);
}
// Check restrictions
while (!queues.restrictionChecksDone()) {
DFTRestrictionPointer next = queues.nextRestrictionCheck();
next->checkFails(*newState, queues);
newState->updateFailableDependencies(next->id());
newState->updateFailableInRestrictions(next->id());
}
}
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) {
// Propagate failsafe
while (!queues.failsafePropagationDone()) {
DFTGatePointer next = queues.nextFailsafePropagation();
next->checkFailsafe(*newState, queues);
}
// Propagate dont cares
// Relevance is considered for each element independently
while (!queues.dontCarePropagationDone()) {
DFTElementPointer next = queues.nextDontCarePropagation();
next->checkDontCareAnymore(*newState, queues);
}
}
template<typename ValueType, typename StateType>
StateBehavior<ValueType, StateType> DftNextStateGenerator<ValueType, StateType>::createMergeFailedState(StateToIdCallback const& stateToIdCallback) {
this->uniqueFailedState = true;

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

@ -42,6 +42,26 @@ namespace storm {
*/
StateBehavior<ValueType, StateType> createMergeFailedState(StateToIdCallback const& stateToIdCallback);
/**
* Propagate the failures in a given state if the given BE fails
*
* @param newState starting state of the propagation
* @param nextBE BE whose failure is propagated
*/
void
propagateFailure(DFTStatePointer newState, std::shared_ptr<storm::storage::DFTBE<ValueType> const> &nextBE,
storm::storage::DFTStateSpaceGenerationQueues<ValueType> &queues);
/**
* Propagate the failsafe state in a given state if the given BE fails
*
* @param newState starting state of the propagation
* @param nextBE BE whose failure is propagated
*/
void
propagateFailsafe(DFTStatePointer newState, std::shared_ptr<storm::storage::DFTBE<ValueType> const> &nextBE,
storm::storage::DFTStateSpaceGenerationQueues<ValueType> &queues);
private:
StateBehavior<ValueType, StateType> exploreState(StateToIdCallback const& stateToIdCallback, bool exploreDependencies);

Write Preview
Loading…
Cancel
Save