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

Dft exploration via NextStateGenerator 

Former-commit-id: f81ac4e7fc
tempestpy_adaptions
Mavo 8 years ago
parent
495b42ff4c
commit
fba2071e9f
15 changed files with 561 additions and 664 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. 7
      examples/dft/fdep4.dft
  2. 736
      src/builder/ExplicitDFTModelBuilderApprox.cpp
  3. 111
      src/builder/ExplicitDFTModelBuilderApprox.h
  4. 266
      src/generator/DftNextStateGenerator.cpp
  5. 43
      src/generator/DftNextStateGenerator.h
  6. 3
      src/generator/StateBehavior.cpp
  7. 2
      src/models/sparse/MarkovAutomaton.cpp
  8. 7
      src/models/sparse/MarkovAutomaton.h
  9. 2
      src/models/sparse/StateLabeling.cpp
  10. 2
      src/models/sparse/StateLabeling.h
  11. 5
      src/storage/dft/DFT.cpp
  12. 2
      src/storage/dft/DFT.h
  13. 6
      src/storage/dft/DFTState.cpp
  14. 32
      src/utility/vector.cpp
  15. 1
      src/utility/vector.h

7
examples/dft/fdep4.dft
View File

@ -0,0 +1,7 @@
toplevel "A";
"A" or "F" "B";
"F" fdep "E" "C" "D";
"B" wsp "C" "D";
"C" lambda=1 dorm=0;
"D" lambda=1 dorm=0.5;
"E" lambda=0.5 dorm=0;

736
src/builder/ExplicitDFTModelBuilderApprox.cpp
View File

@ -12,223 +12,167 @@
namespace storm {
namespace builder {
template <typename ValueType>
ExplicitDFTModelBuilderApprox<ValueType>::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), markovianStates(), exitRates(), choiceLabeling() {
template <typename ValueType, typename StateType>
ExplicitDFTModelBuilderApprox<ValueType, StateType>::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), markovianStates(), exitRates(), choiceLabeling() {
// Intentionally left empty.
}
template <typename ValueType>
ExplicitDFTModelBuilderApprox<ValueType>::ExplicitDFTModelBuilderApprox(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) : mDft(dft), enableDC(enableDC), stateStorage(((mDft.stateVectorSize() / 64) + 1) * 64) {
template <typename ValueType, typename StateType>
ExplicitDFTModelBuilderApprox<ValueType, StateType>::ExplicitDFTModelBuilderApprox(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) : dft(dft), enableDC(enableDC), stateStorage(((dft.stateVectorSize() / 64) + 1) * 64) {
// stateVectorSize is bound for size of bitvector
mStateGenerationInfo = std::make_shared<storm::storage::DFTStateGenerationInfo>(mDft.buildStateGenerationInfo(symmetries));
stateGenerationInfo = std::make_shared<storm::storage::DFTStateGenerationInfo>(dft.buildStateGenerationInfo(symmetries));
}
template <typename ValueType, typename StateType>
std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilderApprox<ValueType, StateType>::buildModel(LabelOptions const& labelOpts) {
STORM_LOG_TRACE("Generating DFT state space");
template <typename ValueType>
std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilderApprox<ValueType>::buildModel(LabelOptions const& labelOpts) {
// Initialize
bool deterministicModel = false;
size_t rowOffset = 0;
ModelComponents modelComponents;
std::vector<uint_fast64_t> tmpMarkovianStates;
storm::storage::SparseMatrixBuilder<ValueType> transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0);
StateType currentRowGroup = 0;
StateType currentRow = 0;
modelComponents.markovianStates = storm::storage::BitVector(INITIAL_BITVECTOR_SIZE);
// Create generator
storm::generator::DftNextStateGenerator<ValueType, StateType> generator(dft, *stateGenerationInfo, enableDC, mergeFailedStates);
// Create sparse matrix builder
storm::storage::SparseMatrixBuilder<ValueType> transitionMatrixBuilder(0, 0, 0, false, !generator.isDeterministicModel(), 0);
if(mergeFailedStates) {
// Introduce explicit fail state
failedIndex = newIndex;
newIndex++;
transitionMatrixBuilder.newRowGroup(failedIndex);
transitionMatrixBuilder.addNextValue(failedIndex, failedIndex, storm::utility::one<ValueType>());
STORM_LOG_TRACE("Introduce fail state with id: " << failedIndex);
modelComponents.exitRates.push_back(storm::utility::one<ValueType>());
tmpMarkovianStates.push_back(failedIndex);
}
// Explore state space
DFTStatePointer state = std::make_shared<storm::storage::DFTState<ValueType>>(mDft, *mStateGenerationInfo, newIndex);
auto exploreResult = exploreStates(state, rowOffset, transitionMatrixBuilder, tmpMarkovianStates, modelComponents.exitRates);
initialStateIndex = exploreResult.first;
bool deterministic = exploreResult.second;
// Before ending the exploration check for pseudo states which are not initialized yet
for (auto & pseudoStatePair : mPseudoStatesMapping) {
if (pseudoStatePair.first == 0) {
// Create state from pseudo state and explore
STORM_LOG_ASSERT(stateStorage.stateToId.contains(pseudoStatePair.second), "Pseudo state not contained.");
STORM_LOG_ASSERT(stateStorage.stateToId.getValue(pseudoStatePair.second) >= OFFSET_PSEUDO_STATE, "State is no pseudo state.");
STORM_LOG_TRACE("Create pseudo state from bit vector " << pseudoStatePair.second);
DFTStatePointer pseudoState = std::make_shared<storm::storage::DFTState<ValueType>>(pseudoStatePair.second, mDft, *mStateGenerationInfo, newIndex);
STORM_LOG_ASSERT(pseudoStatePair.second == pseudoState->status(), "Pseudo states do not coincide.");
STORM_LOG_TRACE("Explore pseudo state " << mDft.getStateString(pseudoState) << " with id " << pseudoState->getId());
auto exploreResult = exploreStates(pseudoState, rowOffset, transitionMatrixBuilder, tmpMarkovianStates, modelComponents.exitRates);
deterministic &= exploreResult.second;
STORM_LOG_ASSERT(pseudoStatePair.first == pseudoState->getId(), "Pseudo state ids do not coincide");
STORM_LOG_ASSERT(pseudoState->getId() == exploreResult.first, "Pseudo state ids do not coincide.");
}
}
// Replace pseudo states in matrix
std::vector<uint_fast64_t> pseudoStatesVector;
for (auto const& pseudoStatePair : mPseudoStatesMapping) {
pseudoStatesVector.push_back(pseudoStatePair.first);
}
STORM_LOG_ASSERT(std::find(pseudoStatesVector.begin(), pseudoStatesVector.end(), 0) == pseudoStatesVector.end(), "Unexplored pseudo state still contained.");
transitionMatrixBuilder.replaceColumns(pseudoStatesVector, OFFSET_PSEUDO_STATE);
STORM_LOG_DEBUG("Generated " << stateStorage.getNumberOfStates() + (mergeFailedStates ? 1 : 0) << " states");
STORM_LOG_DEBUG("Model is " << (deterministic ? "deterministic" : "non-deterministic"));
storm::generator::StateBehavior<ValueType, StateType> behavior = generator.createMergeFailedState([this] (DFTStatePointer const& state) {
this->failedStateId = newIndex++;
stateRemapping.push_back(0);
return this->failedStateId;
} );
size_t stateSize = stateStorage.getNumberOfStates() + (mergeFailedStates ? 1 : 0);
// Build Markov Automaton
modelComponents.markovianStates = storm::storage::BitVector(stateSize, tmpMarkovianStates);
// Build transition matrix
modelComponents.transitionMatrix = transitionMatrixBuilder.build(stateSize, stateSize);
if (stateSize <= 15) {
STORM_LOG_TRACE("Transition matrix: " << std::endl << modelComponents.transitionMatrix);
} else {
STORM_LOG_TRACE("Transition matrix: too big to print");
}
STORM_LOG_TRACE("Exit rates: " << modelComponents.exitRates);
STORM_LOG_TRACE("Markovian states: " << modelComponents.markovianStates);
// Build state labeling
modelComponents.stateLabeling = storm::models::sparse::StateLabeling(stateStorage.getNumberOfStates() + (mergeFailedStates ? 1 : 0));
// Initial state is always first state without any failure
modelComponents.stateLabeling.addLabel("init");
modelComponents.stateLabeling.addLabelToState("init", initialStateIndex);
// Label all states corresponding to their status (failed, failsafe, failed BE)
if(labelOpts.buildFailLabel) {
modelComponents.stateLabeling.addLabel("failed");
}
if(labelOpts.buildFailSafeLabel) {
modelComponents.stateLabeling.addLabel("failsafe");
}
// Collect labels for all BE
std::vector<std::shared_ptr<storage::DFTBE<ValueType>>> basicElements = mDft.getBasicElements();
for (std::shared_ptr<storage::DFTBE<ValueType>> elem : basicElements) {
if(labelOpts.beLabels.count(elem->name()) > 0) {
modelComponents.stateLabeling.addLabel(elem->name() + "_fail");
setRemapping(failedStateId, currentRowGroup);
STORM_LOG_ASSERT(!behavior.empty(), "Behavior is empty.");
setMarkovian(currentRowGroup, behavior.begin()->isMarkovian());
// If the model is nondeterministic, we need to open a row group.
if (!generator.isDeterministicModel()) {
transitionMatrixBuilder.newRowGroup(currentRow);
}
}
if(mergeFailedStates) {
modelComponents.stateLabeling.addLabelToState("failed", failedIndex);
// Now add self loop.
// TODO Matthias: maybe use general method.
STORM_LOG_ASSERT(behavior.getNumberOfChoices() == 1, "Wrong number of choices for failed state.");
STORM_LOG_ASSERT(behavior.begin()->size() == 1, "Wrong number of transitions for failed state.");
std::pair<StateType, ValueType> stateProbabilityPair = *(behavior.begin()->begin());
STORM_LOG_ASSERT(stateProbabilityPair.first == failedStateId, "No self loop for failed state.");
STORM_LOG_ASSERT(storm::utility::isOne<ValueType>(stateProbabilityPair.second), "Probability for failed state != 1.");
transitionMatrixBuilder.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second);
++currentRow;
++currentRowGroup;
}
for (auto const& stateIdPair : stateStorage.stateToId) {
storm::storage::BitVector state = stateIdPair.first;
size_t stateId = stateIdPair.second;
if (!mergeFailedStates && labelOpts.buildFailLabel && mDft.hasFailed(state, *mStateGenerationInfo)) {
modelComponents.stateLabeling.addLabelToState("failed", stateId);
}
if (labelOpts.buildFailSafeLabel && mDft.isFailsafe(state, *mStateGenerationInfo)) {
modelComponents.stateLabeling.addLabelToState("failsafe", stateId);
};
// Set fail status for each BE
for (std::shared_ptr<storage::DFTBE<ValueType>> elem : basicElements) {
if (labelOpts.beLabels.count(elem->name()) > 0 && storm::storage::DFTState<ValueType>::hasFailed(state, mStateGenerationInfo->getStateIndex(elem->id())) ) {
modelComponents.stateLabeling.addLabelToState(elem->name() + "_fail", stateId);
}
// Create a callback for the next-state generator to enable it to add states
std::function<StateType (DFTStatePointer const&)> stateToIdCallback = std::bind(&ExplicitDFTModelBuilderApprox::getOrAddStateIndex, this, std::placeholders::_1);
// Build initial states
this->stateStorage.initialStateIndices = generator.getInitialStates(stateToIdCallback);
STORM_LOG_ASSERT(stateStorage.initialStateIndices.size() == 1, "Only one initial state assumed.");
StateType initialStateIndex = stateStorage.initialStateIndices[0];
STORM_LOG_TRACE("Initial state: " << initialStateIndex);
// Explore state space
bool explorationFinished = false;
while (!explorationFinished) {
// Get the first state in the queue
DFTStatePointer currentState = statesToExplore.front();
STORM_LOG_ASSERT(stateStorage.stateToId.getValue(currentState->status()) == currentState->getId(), "Ids of states do not coincide.");
statesToExplore.pop_front();
// Remember that this row group was actually filled with the transitions of a different state
setRemapping(currentState->getId(), currentRowGroup);
// Explore state
generator.load(currentState);
storm::generator::StateBehavior<ValueType, StateType> behavior = generator.expand(stateToIdCallback);
STORM_LOG_ASSERT(!behavior.empty(), "Behavior is empty.");
setMarkovian(currentRowGroup, behavior.begin()->isMarkovian());
// If the model is nondeterministic, we need to open a row group.
if (!generator.isDeterministicModel()) {
transitionMatrixBuilder.newRowGroup(currentRow);
}
}
std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
if (deterministic) {
// Turn the probabilities into rates by multiplying each row with the exit rate of the state.
// TODO Matthias: avoid transforming back and forth
storm::storage::SparseMatrix<ValueType> rateMatrix(modelComponents.transitionMatrix);
for (uint_fast64_t row = 0; row < rateMatrix.getRowCount(); ++row) {
STORM_LOG_ASSERT(row < modelComponents.markovianStates.size(), "Row exceeds no. of markovian states.");
if (modelComponents.markovianStates.get(row)) {
for (auto& entry : rateMatrix.getRow(row)) {
entry.setValue(entry.getValue() * modelComponents.exitRates[row]);
// Now add all choices.
for (auto const& choice : behavior) {
// Add the probabilistic behavior to the matrix.
for (auto const& stateProbabilityPair : choice) {
// Check that pseudo state and its instantiation do not appear together
// TODO Matthias: prove that this is not possible and remove
if (stateProbabilityPair.first >= OFFSET_PSEUDO_STATE) {
StateType newId = stateProbabilityPair.first - OFFSET_PSEUDO_STATE;
STORM_LOG_ASSERT(newId < mPseudoStatesMapping.size(), "Id is not valid.");
if (mPseudoStatesMapping[newId].first > 0) {
// State exists already
newId = mPseudoStatesMapping[newId].first;
for (auto itFind = choice.begin(); itFind != choice.end(); ++itFind) {
STORM_LOG_ASSERT(itFind->first != newId, "Pseudo state and instantiation occur together in a distribution.");
}
}
}
transitionMatrixBuilder.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second);
}
++currentRow;
}
model = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(std::move(rateMatrix), std::move(modelComponents.exitRates), std::move(modelComponents.stateLabeling));
} else {
std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.markovianStates), std::move(modelComponents.exitRates), true);
if (ma->hasOnlyTrivialNondeterminism()) {
// Markov automaton can be converted into CTMC
model = ma->convertToCTMC();
} else {
model = ma;
}
}
return model;
}
template <typename ValueType>
std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilderApprox<ValueType>::buildModelApprox(LabelOptions const& labelOpts) {
// Initialize
bool deterministicModel = false;
size_t rowOffset = 0;
ModelComponents modelComponents;
std::vector<uint_fast64_t> tmpMarkovianStates;
storm::storage::SparseMatrixBuilder<ValueType> transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0);
if(mergeFailedStates) {
// Introduce explicit fail state
failedIndex = newIndex;
newIndex++;
transitionMatrixBuilder.newRowGroup(failedIndex);
transitionMatrixBuilder.addNextValue(failedIndex, failedIndex, storm::utility::one<ValueType>());
STORM_LOG_TRACE("Introduce fail state with id: " << failedIndex);
modelComponents.exitRates.push_back(storm::utility::one<ValueType>());
tmpMarkovianStates.push_back(failedIndex);
}
// Initialize generator
storm::generator::DftNextStateGenerator<ValueType, uint_fast64_t> generator(mDft, *mStateGenerationInfo);
// Explore state space
typename storm::generator::DftNextStateGenerator<ValueType, uint_fast64_t>::StateToIdCallback stateToIdCallback = [this] (DFTStatePointer const& state) -> uint_fast64_t {
uint_fast64_t id = newIndex++;
std::cout << "Added state " << id << std::endl;
return id;
};
uint_fast64_t id = generator.getInitialStates(stateToIdCallback)[0];
std::cout << "Initial state " << id << std::endl;
DFTStatePointer state = std::make_shared<storm::storage::DFTState<ValueType>>(mDft, *mStateGenerationInfo, newIndex);
auto exploreResult = exploreStates(state, rowOffset, transitionMatrixBuilder, tmpMarkovianStates, modelComponents.exitRates);
initialStateIndex = exploreResult.first;
bool deterministic = exploreResult.second;
// Before ending the exploration check for pseudo states which are not initialized yet
for (auto & pseudoStatePair : mPseudoStatesMapping) {
if (pseudoStatePair.first == 0) {
// Create state from pseudo state and explore
STORM_LOG_ASSERT(stateStorage.stateToId.contains(pseudoStatePair.second), "Pseudo state not contained.");
STORM_LOG_ASSERT(stateStorage.stateToId.getValue(pseudoStatePair.second) >= OFFSET_PSEUDO_STATE, "State is no pseudo state.");
STORM_LOG_TRACE("Create pseudo state from bit vector " << pseudoStatePair.second);
DFTStatePointer pseudoState = std::make_shared<storm::storage::DFTState<ValueType>>(pseudoStatePair.second, mDft, *mStateGenerationInfo, newIndex);
STORM_LOG_ASSERT(pseudoStatePair.second == pseudoState->status(), "Pseudo states do not coincide.");
STORM_LOG_TRACE("Explore pseudo state " << mDft.getStateString(pseudoState) << " with id " << pseudoState->getId());
auto exploreResult = exploreStates(pseudoState, rowOffset, transitionMatrixBuilder, tmpMarkovianStates, modelComponents.exitRates);
deterministic &= exploreResult.second;
STORM_LOG_ASSERT(pseudoStatePair.first == pseudoState->getId(), "Pseudo state ids do not coincide");
STORM_LOG_ASSERT(pseudoState->getId() == exploreResult.first, "Pseudo state ids do not coincide.");
++currentRowGroup;
if (statesToExplore.empty()) {
explorationFinished = true;
// Before ending the exploration check for pseudo states which are not initialized yet
for ( ; pseudoStatesToCheck < mPseudoStatesMapping.size(); ++pseudoStatesToCheck) {
std::pair<StateType, storm::storage::BitVector> pseudoStatePair = mPseudoStatesMapping[pseudoStatesToCheck];
if (pseudoStatePair.first == 0) {
// Create state from pseudo state and explore
STORM_LOG_ASSERT(stateStorage.stateToId.contains(pseudoStatePair.second), "Pseudo state not contained.");
STORM_LOG_ASSERT(stateStorage.stateToId.getValue(pseudoStatePair.second) >= OFFSET_PSEUDO_STATE, "State is no pseudo state.");
STORM_LOG_TRACE("Create pseudo state from bit vector " << pseudoStatePair.second);
DFTStatePointer pseudoState = std::make_shared<storm::storage::DFTState<ValueType>>(pseudoStatePair.second, dft, *stateGenerationInfo, newIndex);
STORM_LOG_ASSERT(pseudoStatePair.second == pseudoState->status(), "Pseudo states do not coincide.");
STORM_LOG_TRACE("Explore pseudo state " << dft.getStateString(pseudoState) << " with id " << pseudoState->getId());
getOrAddStateIndex(pseudoState);
explorationFinished = false;
break;
}
}
}
}
} // end exploration
size_t stateSize = stateStorage.getNumberOfStates() + (mergeFailedStates ? 1 : 0);
modelComponents.markovianStates.resize(stateSize);
// Replace pseudo states in matrix
// TODO Matthias: avoid hack with fixed int type
std::vector<uint_fast64_t> pseudoStatesVector;
for (auto const& pseudoStatePair : mPseudoStatesMapping) {
pseudoStatesVector.push_back(pseudoStatePair.first);
}
STORM_LOG_ASSERT(std::find(pseudoStatesVector.begin(), pseudoStatesVector.end(), 0) == pseudoStatesVector.end(), "Unexplored pseudo state still contained.");
transitionMatrixBuilder.replaceColumns(pseudoStatesVector, OFFSET_PSEUDO_STATE);
STORM_LOG_DEBUG("Generated " << stateStorage.getNumberOfStates() + (mergeFailedStates ? 1 : 0) << " states");
STORM_LOG_DEBUG("Model is " << (deterministic ? "deterministic" : "non-deterministic"));
size_t stateSize = stateStorage.getNumberOfStates() + (mergeFailedStates ? 1 : 0);
// Build Markov Automaton
modelComponents.markovianStates = storm::storage::BitVector(stateSize, tmpMarkovianStates);
// Fix the entries in the matrix according to the (reversed) mapping of row groups to indices
STORM_LOG_ASSERT(stateRemapping[initialStateIndex] == initialStateIndex, "Initial state should not be remapped.");
// Fix the transition matrix
transitionMatrixBuilder.replaceColumns(stateRemapping, 0);
// Fix the hash map storing the mapping states -> ids
this->stateStorage.stateToId.remap([this] (StateType const& state) { return this->stateRemapping[state]; } );
STORM_LOG_TRACE("State remapping: " << stateRemapping);
STORM_LOG_TRACE("Markovian states: " << modelComponents.markovianStates);
STORM_LOG_DEBUG("Generated " << stateSize << " states");
STORM_LOG_DEBUG("Model is " << (generator.isDeterministicModel() ? "deterministic" : "non-deterministic"));
// Build transition matrix
modelComponents.transitionMatrix = transitionMatrixBuilder.build(stateSize, stateSize);
if (stateSize <= 15) {
@ -236,11 +180,9 @@ namespace storm {
} else {
STORM_LOG_TRACE("Transition matrix: too big to print");
}
STORM_LOG_TRACE("Exit rates: " << modelComponents.exitRates);
STORM_LOG_TRACE("Markovian states: " << modelComponents.markovianStates);
// Build state labeling
modelComponents.stateLabeling = storm::models::sparse::StateLabeling(stateStorage.getNumberOfStates() + (mergeFailedStates ? 1 : 0));
modelComponents.stateLabeling = storm::models::sparse::StateLabeling(stateSize);
// Initial state is always first state without any failure
modelComponents.stateLabeling.addLabel("init");
modelComponents.stateLabeling.addLabelToState("init", initialStateIndex);
@ -251,52 +193,56 @@ namespace storm {
if(labelOpts.buildFailSafeLabel) {
modelComponents.stateLabeling.addLabel("failsafe");
}
// Collect labels for all BE
std::vector<std::shared_ptr<storage::DFTBE<ValueType>>> basicElements = mDft.getBasicElements();
std::vector<std::shared_ptr<storage::DFTBE<ValueType>>> basicElements = dft.getBasicElements();
for (std::shared_ptr<storage::DFTBE<ValueType>> elem : basicElements) {
if(labelOpts.beLabels.count(elem->name()) > 0) {
modelComponents.stateLabeling.addLabel(elem->name() + "_fail");
}
}
// Set labels to states
if(mergeFailedStates) {
modelComponents.stateLabeling.addLabelToState("failed", failedIndex);
modelComponents.stateLabeling.addLabelToState("failed", failedStateId);
}
for (auto const& stateIdPair : stateStorage.stateToId) {
storm::storage::BitVector state = stateIdPair.first;
size_t stateId = stateIdPair.second;
if (!mergeFailedStates && labelOpts.buildFailLabel && mDft.hasFailed(state, *mStateGenerationInfo)) {
if (!mergeFailedStates && labelOpts.buildFailLabel && dft.hasFailed(state, *stateGenerationInfo)) {
modelComponents.stateLabeling.addLabelToState("failed", stateId);
}
if (labelOpts.buildFailSafeLabel && mDft.isFailsafe(state, *mStateGenerationInfo)) {
if (labelOpts.buildFailSafeLabel && dft.isFailsafe(state, *stateGenerationInfo)) {
modelComponents.stateLabeling.addLabelToState("failsafe", stateId);
};
// Set fail status for each BE
for (std::shared_ptr<storage::DFTBE<ValueType>> elem : basicElements) {
if (labelOpts.beLabels.count(elem->name()) > 0 && storm::storage::DFTState<ValueType>::hasFailed(state, mStateGenerationInfo->getStateIndex(elem->id())) ) {
if (labelOpts.beLabels.count(elem->name()) > 0 && storm::storage::DFTState<ValueType>::hasFailed(state, stateGenerationInfo->getStateIndex(elem->id())) ) {
modelComponents.stateLabeling.addLabelToState(elem->name() + "_fail", stateId);
}
}
}
std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
if (deterministic) {
// Turn the probabilities into rates by multiplying each row with the exit rate of the state.
// TODO Matthias: avoid transforming back and forth
storm::storage::SparseMatrix<ValueType> rateMatrix(modelComponents.transitionMatrix);
for (uint_fast64_t row = 0; row < rateMatrix.getRowCount(); ++row) {
STORM_LOG_ASSERT(row < modelComponents.markovianStates.size(), "Row exceeds no. of markovian states.");
if (modelComponents.markovianStates.get(row)) {
for (auto& entry : rateMatrix.getRow(row)) {
entry.setValue(entry.getValue() * modelComponents.exitRates[row]);
}
if (generator.isDeterministicModel()) {
// Build CTMC
model = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling));
} else {
// Build MA
// Compute exit rates
modelComponents.exitRates = std::vector<ValueType>(stateSize);
std::vector<typename storm::storage::SparseMatrix<ValueType>::index_type> indices = modelComponents.transitionMatrix.getRowGroupIndices();
for (StateType stateIndex = 0; stateIndex < stateSize; ++stateIndex) {
if (modelComponents.markovianStates[stateIndex]) {
modelComponents.exitRates[stateIndex] = modelComponents.transitionMatrix.getRowSum(indices[stateIndex]);
} else {
modelComponents.exitRates[stateIndex] = storm::utility::zero<ValueType>();
}
}
model = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(std::move(rateMatrix), std::move(modelComponents.exitRates), std::move(modelComponents.stateLabeling));
} else {
std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.markovianStates), std::move(modelComponents.exitRates), true);
STORM_LOG_TRACE("Exit rates: " << modelComponents.exitRates);
std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.markovianStates), std::move(modelComponents.exitRates));
if (ma->hasOnlyTrivialNondeterminism()) {
// Markov automaton can be converted into CTMC
model = ma->convertToCTMC();
@ -325,331 +271,77 @@ namespace storm {
return eval < threshold;
}
template <typename ValueType>
std::pair<uint_fast64_t, bool> ExplicitDFTModelBuilderApprox<ValueType>::exploreStates(DFTStatePointer const& state, size_t& rowOffset, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<uint_fast64_t>& markovianStates, std::vector<ValueType>& exitRates) {
STORM_LOG_TRACE("Explore state: " << mDft.getStateString(state));
auto explorePair = checkForExploration(state);
if (!explorePair.first) {
// State does not need any exploration
return std::make_pair(explorePair.second, true);
}
// Initialization
// TODO Matthias: set Markovian states directly as bitvector?
std::map<uint_fast64_t, ValueType> outgoingRates;
std::vector<std::map<uint_fast64_t, ValueType>> outgoingProbabilities;
bool hasDependencies = state->nrFailableDependencies() > 0;
size_t failableCount = hasDependencies ? state->nrFailableDependencies() : state->nrFailableBEs();
size_t smallest = 0;
ValueType exitRate = storm::utility::zero<ValueType>();
bool deterministic = !hasDependencies;
// Absorbing state
if (mDft.hasFailed(state) || mDft.isFailsafe(state) || state->nrFailableBEs() == 0) {
uint_fast64_t stateId = addState(state);
STORM_LOG_ASSERT(stateId == state->getId(), "Ids do not coincide.");
// Add self loop
transitionMatrixBuilder.newRowGroup(stateId + rowOffset);
transitionMatrixBuilder.addNextValue(stateId + rowOffset, stateId, storm::utility::one<ValueType>());
STORM_LOG_TRACE("Added self loop for " << stateId);
exitRates.push_back(storm::utility::one<ValueType>());
STORM_LOG_ASSERT(exitRates.size()-1 == stateId, "No. of considered states does not match state id.");
markovianStates.push_back(stateId);
// No further exploration required
return std::make_pair(stateId, true);
}
// Let BE fail
while (smallest < failableCount) {
STORM_LOG_ASSERT(!mDft.hasFailed(state), "Dft has failed.");
// Construct new state as copy from original one
DFTStatePointer newState = std::make_shared<storm::storage::DFTState<ValueType>>(*state);
std::pair<std::shared_ptr<storm::storage::DFTBE<ValueType> const>, bool> nextBEPair = newState->letNextBEFail(smallest++);
std::shared_ptr<storm::storage::DFTBE<ValueType> const>& nextBE = nextBEPair.first;
STORM_LOG_ASSERT(nextBE, "NextBE is null.");
STORM_LOG_ASSERT(nextBEPair.second == hasDependencies, "Failure due to dependencies does not match.");
STORM_LOG_TRACE("With the failure of: " << nextBE->name() << " [" << nextBE->id() << "] in " << mDft.getStateString(state));
if (storm::settings::getModule<storm::settings::modules::DFTSettings>().computeApproximation()) {
if (!storm::utility::isZero(exitRate)) {
ValueType rate = nextBE->activeFailureRate();
ValueType div = rate / exitRate;
if (!storm::utility::isZero(exitRate) && belowThreshold(div)) {
// Set transition directly to failed state
auto resultFind = outgoingRates.find(failedIndex);
if (resultFind != outgoingRates.end()) {
// Add to existing transition
resultFind->second += rate;
STORM_LOG_TRACE("Updated transition to " << resultFind->first << " with rate " << rate << " to new rate " << resultFind->second);
} else {
// Insert new transition
outgoingRates.insert(std::make_pair(failedIndex, rate));
STORM_LOG_TRACE("Added transition to " << failedIndex << " with rate " << rate);
}
exitRate += rate;
std::cout << "IGNORE: " << nextBE->name() << " [" << nextBE->id() << "] with rate " << rate << std::endl;
//STORM_LOG_TRACE("Ignore: " << nextBE->name() << " [" << nextBE->id() << "] with rate " << rate);
continue;
}
}
}
// Propagate failures
storm::storage::DFTStateSpaceGenerationQueues<ValueType> queues;
for (DFTGatePointer parent : nextBE->parents()) {
if (newState->isOperational(parent->id())) {
queues.propagateFailure(parent);
}
}
for (DFTRestrictionPointer restr : nextBE->restrictions()) {
queues.checkRestrictionLater(restr);
}
while (!queues.failurePropagationDone()) {
DFTGatePointer next = queues.nextFailurePropagation();
next->checkFails(*newState, queues);
newState->updateFailableDependencies(next->id());
}
while(!queues.restrictionChecksDone()) {
DFTRestrictionPointer next = queues.nextRestrictionCheck();
next->checkFails(*newState, queues);
newState->updateFailableDependencies(next->id());
}
if(newState->isInvalid()) {
continue;
}
bool dftFailed = newState->hasFailed(mDft.getTopLevelIndex());
while (!dftFailed && !queues.failsafePropagationDone()) {
DFTGatePointer next = queues.nextFailsafePropagation();
next->checkFailsafe(*newState, queues);
}
while (!dftFailed && enableDC && !queues.dontCarePropagationDone()) {
DFTElementPointer next = queues.nextDontCarePropagation();
next->checkDontCareAnymore(*newState, queues);
}
// Update failable dependencies
if (!dftFailed) {
newState->updateFailableDependencies(nextBE->id());
newState->updateDontCareDependencies(nextBE->id());
}
uint_fast64_t newStateId;
if(dftFailed && mergeFailedStates) {
newStateId = failedIndex;
} else {
// Explore new state recursively
auto explorePair = exploreStates(newState, rowOffset, transitionMatrixBuilder, markovianStates, exitRates);
newStateId = explorePair.first;
deterministic &= explorePair.second;
}
// Set transitions
if (hasDependencies) {
// Failure is due to dependency -> add non-deterministic choice
std::map<uint_fast64_t, ValueType> choiceProbabilities;
std::shared_ptr<storm::storage::DFTDependency<ValueType> const> dependency = mDft.getDependency(state->getDependencyId(smallest-1));
choiceProbabilities.insert(std::make_pair(newStateId, dependency->probability()));
STORM_LOG_TRACE("Added transition to " << newStateId << " with probability " << dependency->probability());
if (!storm::utility::isOne(dependency->probability())) {
// Add transition to state where dependency was unsuccessful
DFTStatePointer unsuccessfulState = std::make_shared<storm::storage::DFTState<ValueType>>(*state);
unsuccessfulState->letDependencyBeUnsuccessful(smallest-1);
auto explorePair = exploreStates(unsuccessfulState, rowOffset, transitionMatrixBuilder, markovianStates, exitRates);
uint_fast64_t unsuccessfulStateId = explorePair.first;
deterministic &= explorePair.second;
ValueType remainingProbability = storm::utility::one<ValueType>() - dependency->probability();
choiceProbabilities.insert(std::make_pair(unsuccessfulStateId, remainingProbability));
STORM_LOG_TRACE("Added transition to " << unsuccessfulStateId << " with remaining probability " << remainingProbability);
}
outgoingProbabilities.push_back(choiceProbabilities);
} else {
// Set failure rate according to activation
bool isActive = true;
if (mDft.hasRepresentant(nextBE->id())) {
// Active must be checked for the state we are coming from as this state is responsible for the
// rate and not the new state we are going to
isActive = state->isActive(mDft.getRepresentant(nextBE->id())->id());
}
ValueType rate = isActive ? nextBE->activeFailureRate() : nextBE->passiveFailureRate();
STORM_LOG_ASSERT(!storm::utility::isZero(rate), "Rate is 0.");
auto resultFind = outgoingRates.find(newStateId);
if (resultFind != outgoingRates.end()) {
// Add to existing transition
resultFind->second += rate;
STORM_LOG_TRACE("Updated transition to " << resultFind->first << " with " << (isActive ? "active" : "passive") << " rate " << rate << " to new rate " << resultFind->second);
} else {
// Insert new transition
outgoingRates.insert(std::make_pair(newStateId, rate));
STORM_LOG_TRACE("Added transition to " << newStateId << " with " << (isActive ? "active" : "passive") << " rate " << rate);
}
exitRate += rate;
}
} // end while failing BE
// Add state
uint_fast64_t stateId = addState(state);
STORM_LOG_ASSERT(stateId == state->getId(), "Ids do not match.");
STORM_LOG_ASSERT(stateId == newIndex-1, "Id does not match no. of states.");
if (hasDependencies) {
// Add all probability transitions
STORM_LOG_ASSERT(outgoingRates.empty(), "Outgoing transitions not empty.");
transitionMatrixBuilder.newRowGroup(stateId + rowOffset);
for (size_t i = 0; i < outgoingProbabilities.size(); ++i, ++rowOffset) {
STORM_LOG_ASSERT(outgoingProbabilities[i].size() == 1 || outgoingProbabilities[i].size() == 2, "No. of outgoing transitions is not valid.");
for (auto it = outgoingProbabilities[i].begin(); it != outgoingProbabilities[i].end(); ++it)
{
STORM_LOG_TRACE("Set transition from " << stateId << " to " << it->first << " with probability " << it->second);
transitionMatrixBuilder.addNextValue(stateId + rowOffset, it->first, it->second);
}
}
rowOffset--; // One increment too many
} else {
// Try to merge pseudo states with their instantiation
// TODO Matthias: improve?
for (auto it = outgoingRates.begin(); it != outgoingRates.end(); ) {
if (it->first >= OFFSET_PSEUDO_STATE) {
uint_fast64_t newId = it->first - OFFSET_PSEUDO_STATE;
STORM_LOG_ASSERT(newId < mPseudoStatesMapping.size(), "Id is not valid.");
if (mPseudoStatesMapping[newId].first > 0) {
// State exists already
newId = mPseudoStatesMapping[newId].first;
auto itFind = outgoingRates.find(newId);
if (itFind != outgoingRates.end()) {
// Add probability from pseudo state to instantiation
itFind->second += it->second;
STORM_LOG_TRACE("Merged pseudo state " << newId << " adding rate " << it->second << " to total rate of " << itFind->second);
} else {
// Only change id
outgoingRates.emplace(newId, it->second);
STORM_LOG_TRACE("Instantiated pseudo state " << newId << " with rate " << it->second);
}
// Remove pseudo state
it = outgoingRates.erase(it);
} else {
++it;
}
} else {
++it;
}
}
// Add all rate transitions
STORM_LOG_ASSERT(outgoingProbabilities.empty(), "Outgoing probabilities not empty.");
transitionMatrixBuilder.newRowGroup(state->getId() + rowOffset);
STORM_LOG_TRACE("Exit rate for " << state->getId() << ": " << exitRate);
for (auto it = outgoingRates.begin(); it != outgoingRates.end(); ++it)
{
ValueType probability = it->second / exitRate; // Transform rate to probability
STORM_LOG_TRACE("Set transition from " << state->getId() << " to " << it->first << " with rate " << it->second);
transitionMatrixBuilder.addNextValue(state->getId() + rowOffset, it->first, probability);
}
markovianStates.push_back(state->getId());
}
STORM_LOG_TRACE("Finished exploring state: " << mDft.getStateString(state));
exitRates.push_back(exitRate);
STORM_LOG_ASSERT(exitRates.size()-1 == state->getId(), "Id does not match no. of states.");
return std::make_pair(state->getId(), deterministic);
}
template <typename ValueType>
std::pair<bool, uint_fast64_t> ExplicitDFTModelBuilderApprox<ValueType>::checkForExploration(DFTStatePointer const& state) {
template <typename ValueType, typename StateType>
StateType ExplicitDFTModelBuilderApprox<ValueType, StateType>::getOrAddStateIndex(DFTStatePointer const& state) {
StateType stateId;
bool changed = false;
if (mStateGenerationInfo->hasSymmetries()) {
if (stateGenerationInfo->hasSymmetries()) {
// Order state by symmetry
STORM_LOG_TRACE("Check for symmetry: " << mDft.getStateString(state));
STORM_LOG_TRACE("Check for symmetry: " << dft.getStateString(state));
changed = state->orderBySymmetry();
STORM_LOG_TRACE("State " << (changed ? "changed to " : "did not change") << (changed ? mDft.getStateString(state) : ""));
STORM_LOG_TRACE("State " << (changed ? "changed to " : "did not change") << (changed ? dft.getStateString(state) : ""));
}
if (stateStorage.stateToId.contains(state->status())) {
// State already exists
uint_fast64_t stateId = stateStorage.stateToId.getValue(state->status());
STORM_LOG_TRACE("State " << mDft.getStateString(state) << " with id " << stateId << " already exists");
if (changed || stateId < OFFSET_PSEUDO_STATE) {
// State is changed or an explored "normal" state
return std::make_pair(false, stateId);
}
stateId -= OFFSET_PSEUDO_STATE;
STORM_LOG_ASSERT(stateId < mPseudoStatesMapping.size(), "Id not valid.");
if (mPseudoStatesMapping[stateId].first > 0) {
// Pseudo state already explored
return std::make_pair(false, mPseudoStatesMapping[stateId].first);
stateId = stateStorage.stateToId.getValue(state->status());
STORM_LOG_TRACE("State " << dft.getStateString(state) << " with id " << stateId << " already exists");
if (!changed && stateId >= OFFSET_PSEUDO_STATE) {
// Pseudo state can be created now
STORM_LOG_ASSERT(stateId >= OFFSET_PSEUDO_STATE, "State is no pseudo state.");
stateId -= OFFSET_PSEUDO_STATE;
STORM_LOG_ASSERT(stateId < mPseudoStatesMapping.size(), "Pseudo state not known.");
STORM_LOG_ASSERT(mPseudoStatesMapping[stateId].first == 0, "Pseudo state already created.");
// Create pseudo state now
STORM_LOG_ASSERT(mPseudoStatesMapping[stateId].second == state->status(), "Pseudo states do not coincide.");
state->setId(newIndex++);
mPseudoStatesMapping[stateId].first = state->getId();
stateId = state->getId();
stateStorage.stateToId.setOrAdd(state->status(), stateId);
STORM_LOG_TRACE("Now create state " << dft.getStateString(state) << " with id " << stateId);
statesToExplore.push_front(state);
}
STORM_LOG_ASSERT(mPseudoStatesMapping[stateId].second == state->status(), "States do not coincide.");
STORM_LOG_TRACE("Pseudo state " << mDft.getStateString(state) << " can be explored now");
return std::make_pair(true, stateId);
} else {
// State does not exists
// State does not exist yet
if (changed) {
// Remember state for later creation
state->setId(mPseudoStatesMapping.size() + OFFSET_PSEUDO_STATE);
mPseudoStatesMapping.push_back(std::make_pair(0, state->status()));
stateStorage.stateToId.findOrAdd(state->status(), state->getId());
STORM_LOG_TRACE("Remember state for later creation: " << mDft.getStateString(state));
return std::make_pair(false, state->getId());
stateId = stateStorage.stateToId.findOrAdd(state->status(), state->getId());
STORM_LOG_ASSERT(stateId == state->getId(), "Ids do not match.");
STORM_LOG_TRACE("Remember state for later creation: " << dft.getStateString(state));
// Reserve one slot for the coming state in the remapping
stateRemapping.push_back(0);
} else {
// State needs exploration
return std::make_pair(true, 0);
// Create new state
state->setId(newIndex++);
stateId = stateStorage.stateToId.findOrAdd(state->status(), state->getId());
STORM_LOG_ASSERT(stateId == state->getId(), "Ids do not match.");
STORM_LOG_TRACE("New state: " << dft.getStateString(state));
statesToExplore.push_front(state);
// Reserve one slot for the new state in the remapping
stateRemapping.push_back(0);
}
}
return stateId;
}
template <typename ValueType>
uint_fast64_t ExplicitDFTModelBuilderApprox<ValueType>::addState(DFTStatePointer const& state) {
uint_fast64_t stateId;
// TODO remove
bool changed = state->orderBySymmetry();
STORM_LOG_ASSERT(!changed, "State to add has changed by applying symmetry.");
// Check if state already exists
if (stateStorage.stateToId.contains(state->status())) {
// State already exists
stateId = stateStorage.stateToId.getValue(state->status());
STORM_LOG_TRACE("State " << mDft.getStateString(state) << " with id " << stateId << " already exists");
// Check if possible pseudo state can be created now
STORM_LOG_ASSERT(stateId >= OFFSET_PSEUDO_STATE, "State is no pseudo state.");
stateId -= OFFSET_PSEUDO_STATE;
STORM_LOG_ASSERT(stateId < mPseudoStatesMapping.size(), "Pseudo state not known.");
if (mPseudoStatesMapping[stateId].first == 0) {
// Create pseudo state now
STORM_LOG_ASSERT(mPseudoStatesMapping[stateId].second == state->status(), "Pseudo states do not coincide.");
state->setId(newIndex++);
mPseudoStatesMapping[stateId].first = state->getId();
stateId = state->getId();
stateStorage.stateToId.setOrAdd(state->status(), stateId);
STORM_LOG_TRACE("Now create state " << mDft.getStateString(state) << " with id " << stateId);
return stateId;
} else {
STORM_LOG_ASSERT(false, "Pseudo state already created.");
return 0;
}
} else {
// Create new state
state->setId(newIndex++);
stateId = stateStorage.stateToId.findOrAdd(state->status(), state->getId());
STORM_LOG_TRACE("New state: " << mDft.getStateString(state));
return stateId;
template <typename ValueType, typename StateType>
void ExplicitDFTModelBuilderApprox<ValueType, StateType>::setMarkovian(StateType id, bool markovian) {
if (id >= modelComponents.markovianStates.size()) {
// Resize BitVector
modelComponents.markovianStates.resize(modelComponents.markovianStates.size() + INITIAL_BITVECTOR_SIZE);
}
modelComponents.markovianStates.set(id, markovian);
}
template <typename ValueType, typename StateType>
void ExplicitDFTModelBuilderApprox<ValueType, StateType>::setRemapping(StateType id, StateType mappedId) {
STORM_LOG_ASSERT(id < stateRemapping.size(), "Invalid index for remapping.");
stateRemapping[id] = mappedId;
}

111
src/builder/ExplicitDFTModelBuilderApprox.h
View File

@ -12,11 +12,15 @@
#include <boost/optional/optional.hpp>
#include <stack>
#include <unordered_set>
#include <limits>
namespace storm {
namespace builder {
template<typename ValueType>
/*!
* Build a Markov chain from DFT.
*/
template<typename ValueType, typename StateType = uint32_t>
class ExplicitDFTModelBuilderApprox {
using DFTElementPointer = std::shared_ptr<storm::storage::DFTElement<ValueType>>;
@ -43,57 +47,100 @@ namespace storm {
std::vector<ValueType> exitRates;
// A vector that stores a labeling for each choice.
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> choiceLabeling;
boost::optional<std::vector<boost::container::flat_set<StateType>>> choiceLabeling;
};
const uint_fast64_t OFFSET_PSEUDO_STATE = UINT_FAST64_MAX / 2;
storm::storage::DFT<ValueType> const& mDft;
std::shared_ptr<storm::storage::DFTStateGenerationInfo> mStateGenerationInfo;
//TODO Matthias: remove when everything works
std::vector<std::pair<uint_fast64_t, storm::storage::BitVector>> mPseudoStatesMapping; // vector of (id to concrete state, bitvector)
size_t newIndex = 0;
bool mergeFailedStates = true;
bool enableDC = true;
size_t failedIndex = 0;
size_t initialStateIndex = 0;
// Internal information about the states that were explored.
storm::storage::sparse::StateStorage<uint_fast64_t> stateStorage;
public:
// A structure holding the labeling options.
struct LabelOptions {
bool buildFailLabel = true;
bool buildFailSafeLabel = false;
std::set<std::string> beLabels = {};
};
/*!
* Constructor.
*
* @param dft DFT.
* @param symmetries Symmetries in the dft.
* @param enableDC Flag indicating if dont care propagation should be used.
*/
ExplicitDFTModelBuilderApprox(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC);
/*!
* Build model from Dft.
*
* @param labelOpts Options for labeling.
*
* @return Built model (either MA or CTMC).
*/
std::shared_ptr<storm::models::sparse::Model<ValueType>> buildModel(LabelOptions const& labelOpts);
// TODO Matthias: only temporary used for avoiding crashing everything
std::shared_ptr<storm::models::sparse::Model<ValueType>> buildModelApprox(LabelOptions const& labelOpts);
private:
std::pair<uint_fast64_t, bool> exploreStates(DFTStatePointer const& state, size_t& rowOffset, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<uint_fast64_t>& markovianStates, std::vector<ValueType>& exitRates);
/*!
* Adds a state to the explored states and handles pseudo states.
* Add a state to the explored states (if not already there). It also handles pseudo states.
*
* @param state The state to add.
* @return Id of added state.
*
* @return Id of state.
*/
StateType getOrAddStateIndex(DFTStatePointer const& state);
/*!
* Set if the given state is markovian.
*
* @param id Id of the state.
* @param markovian Flag indicating if the state is markovian.
*/
uint_fast64_t addState(DFTStatePointer const& state);
void setMarkovian(StateType id, bool markovian);
/*!
* Check if state needs an exploration and remember pseudo states for later creation.
* Set a mapping from a state id to its new id.
*
* @param state State which might need exploration.
* @return Pair of flag indicating whether the state needs exploration now and the state id if the state already
* exists.
* @param id Id of the state.
* @param mappedId New id to use.
*/
std::pair<bool, uint_fast64_t> checkForExploration(DFTStatePointer const& state);
void setRemapping(StateType id, StateType mappedId);
// Initial size of the bitvector.
const size_t INITIAL_BITVECTOR_SIZE = 20000;
// Offset used for pseudo states.
const StateType OFFSET_PSEUDO_STATE = std::numeric_limits<StateType>::max() / 2;
// Dft
storm::storage::DFT<ValueType> const& dft;
// General information for state generation
// TODO Matthias: use const reference
std::shared_ptr<storm::storage::DFTStateGenerationInfo> stateGenerationInfo;
// Current id for new state
size_t newIndex = 0;
//TODO Matthias: remove when everything works
std::vector<std::pair<StateType, storm::storage::BitVector>> mPseudoStatesMapping; // vector of (id to concrete state, bitvector)
//TODO Matthias: make changeable
const bool mergeFailedStates = true;
size_t failedStateId = 0;
size_t initialStateIndex = 0;
size_t pseudoStatesToCheck = 0;
// Flag indication if dont care propagation should be used.
bool enableDC = true;
// Structure for the components of the model.
ModelComponents modelComponents;
// Internal information about the states that were explored.
storm::storage::sparse::StateStorage<StateType> stateStorage;
// A set of states that still need to be explored.
std::deque<DFTStatePointer> statesToExplore;
// A mapping from state indices to the row groups in which they actually reside
// TODO Matthias: avoid hack with fixed int type
std::vector<uint_fast64_t> stateRemapping;
};

266
src/generator/DftNextStateGenerator.cpp
View File

@ -8,13 +8,13 @@ namespace storm {
namespace generator {
template<typename ValueType, typename StateType>
DftNextStateGenerator<ValueType, StateType>::DftNextStateGenerator(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo) : mDft(dft), mStateGenerationInfo(stateGenerationInfo), state(nullptr), comparator() {
// Intentionally left empty.
DftNextStateGenerator<ValueType, StateType>::DftNextStateGenerator(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo, bool enableDC, bool mergeFailedStates) : mDft(dft), mStateGenerationInfo(stateGenerationInfo), state(nullptr), enableDC(enableDC), mergeFailedStates(mergeFailedStates), comparator() {
deterministicModel = !mDft.canHaveNondeterminism();
}
template<typename ValueType, typename StateType>
bool DftNextStateGenerator<ValueType, StateType>::isDeterministicModel() const {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented.");
return deterministicModel;
}
template<typename ValueType, typename StateType>
@ -29,117 +29,201 @@ namespace storm {
}
template<typename ValueType, typename StateType>
void DftNextStateGenerator<ValueType, StateType>::load(std::shared_ptr<storm::storage::DFTState<ValueType>> const& state) {
/*// Since almost all subsequent operations are based on the evaluator, we load the state into it now.
unpackStateIntoEvaluator(state, variableInformation, evaluator);
// Also, we need to store a pointer to the state itself, because we need to be able to access it when expanding it.
this->state = &state;*/
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented.");
void DftNextStateGenerator<ValueType, StateType>::load(DFTStatePointer const& state) {
// TODO Matthias load state from bitvector
// Store a pointer to the state itself, because we need to be able to access it when expanding it.
this->state = &state;
}
template<typename ValueType, typename StateType>
bool DftNextStateGenerator<ValueType, StateType>::satisfies(storm::expressions::Expression const& expression) const {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented.");
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The method 'satisfies' is not yet implemented.");
}
template<typename ValueType, typename StateType>
StateBehavior<ValueType, StateType> DftNextStateGenerator<ValueType, StateType>::expand(StateToIdCallback const& stateToIdCallback) {
/*// Prepare the result, in case we return early.
DFTStatePointer currentState = *state;
STORM_LOG_TRACE("Explore state: " << mDft.getStateString(currentState));
// Prepare the result, in case we return early.
StateBehavior<ValueType, StateType> result;
// First, construct the state rewards, as we may return early if there are no choices later and we already
// need the state rewards then.
for (auto const& rewardModel : selectedRewardModels) {
ValueType stateRewardValue = storm::utility::zero<ValueType>();
if (rewardModel.get().hasStateRewards()) {
for (auto const& stateReward : rewardModel.get().getStateRewards()) {
if (evaluator.asBool(stateReward.getStatePredicateExpression())) {
stateRewardValue += ValueType(evaluator.asRational(stateReward.getRewardValueExpression()));
}
}
}
result.addStateReward(stateRewardValue);
}
// If a terminal expression was set and we must not expand this state, return now.
if (terminalExpression && evaluator.asBool(terminalExpression.get())) {
return result;
}
// Get all choices for the state.
std::vector<Choice<ValueType>> allChoices = getUnlabeledChoices(*this->state, stateToIdCallback);
std::vector<Choice<ValueType>> allLabeledChoices = getLabeledChoices(*this->state, stateToIdCallback);
for (auto& choice : allLabeledChoices) {
allChoices.push_back(std::move(choice));
}
std::size_t totalNumberOfChoices = allChoices.size();
// If there is not a single choice, we return immediately, because the state has no behavior (other than
// the state reward).
if (totalNumberOfChoices == 0) {
// Initialization
bool hasDependencies = currentState->nrFailableDependencies() > 0;
size_t failableCount = hasDependencies ? currentState->nrFailableDependencies() : currentState->nrFailableBEs();
size_t currentFailable = 0;
Choice<ValueType, StateType> choice(0, !hasDependencies);
// Check for absorbing state
if (mDft.hasFailed(currentState) || mDft.isFailsafe(currentState) || currentState->nrFailableBEs() == 0) {
// Add self loop
choice.addProbability(currentState->getId(), storm::utility::one<ValueType>());
STORM_LOG_TRACE("Added self loop for " << currentState->getId());
// No further exploration required
result.addChoice(std::move(choice));
result.setExpanded();
return result;
}
// If the model is a deterministic model, we need to fuse the choices into one.
if (program.isDeterministicModel() && totalNumberOfChoices > 1) {
Choice<ValueType> globalChoice;
// For CTMCs, we need to keep track of the total exit rate to scale the action rewards later. For DTMCs
// this is equal to the number of choices, which is why we initialize it like this here.
ValueType totalExitRate = program.isDiscreteTimeModel() ? static_cast<ValueType>(totalNumberOfChoices) : storm::utility::zero<ValueType>();
// Iterate over all choices and combine the probabilities/rates into one choice.
for (auto const& choice : allChoices) {
for (auto const& stateProbabilityPair : choice) {
if (program.isDiscreteTimeModel()) {
globalChoice.addProbability(stateProbabilityPair.first, stateProbabilityPair.second / totalNumberOfChoices);
} else {
globalChoice.addProbability(stateProbabilityPair.first, stateProbabilityPair.second);
// Let BE fail
while (currentFailable < failableCount) {
STORM_LOG_ASSERT(!mDft.hasFailed(currentState), "Dft has failed.");
// Construct new state as copy from original one
DFTStatePointer newState = std::make_shared<storm::storage::DFTState<ValueType>>(*currentState);
std::pair<std::shared_ptr<storm::storage::DFTBE<ValueType> const>, bool> nextBEPair = newState->letNextBEFail(currentFailable);
std::shared_ptr<storm::storage::DFTBE<ValueType> const>& nextBE = nextBEPair.first;
STORM_LOG_ASSERT(nextBE, "NextBE is null.");
STORM_LOG_ASSERT(nextBEPair.second == hasDependencies, "Failure due to dependencies does not match.");
STORM_LOG_TRACE("With the failure of: " << nextBE->name() << " [" << nextBE->id() << "] in " << mDft.getStateString(currentState));
/*if (storm::settings::getModule<storm::settings::modules::DFTSettings>().computeApproximation()) {
if (!storm::utility::isZero(exitRate)) {
ValueType rate = nextBE->activeFailureRate();
ValueType div = rate / exitRate;
if (!storm::utility::isZero(exitRate) && belowThreshold(div)) {
// Set transition directly to failed state
auto resultFind = outgoingRates.find(failedIndex);
if (resultFind != outgoingRates.end()) {
// Add to existing transition
resultFind->second += rate;
STORM_LOG_TRACE("Updated transition to " << resultFind->first << " with rate " << rate << " to new rate " << resultFind->second);
} else {
// Insert new transition
outgoingRates.insert(std::make_pair(failedIndex, rate));
STORM_LOG_TRACE("Added transition to " << failedIndex << " with rate " << rate);
}
exitRate += rate;
std::cout << "IGNORE: " << nextBE->name() << " [" << nextBE->id() << "] with rate " << rate << std::endl;
//STORM_LOG_TRACE("Ignore: " << nextBE->name() << " [" << nextBE->id() << "] with rate " << rate);
continue;
}
}
if (hasStateActionRewards && !program.isDiscreteTimeModel()) {
totalExitRate += choice.getTotalMass();
}*/
// 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());
}
// 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());
}
if(newState->isInvalid()) {
// Continue with next possible state
++currentFailable;
continue;
}
StateType newStateId;
if (newState->hasFailed(mDft.getTopLevelIndex()) && mergeFailedStates) {
// Use unique failed state
newStateId = mergeFailedStateId;
} else {
// Propagate failsafe
while (!queues.failsafePropagationDone()) {
DFTGatePointer next = queues.nextFailsafePropagation();
next->checkFailsafe(*newState, queues);
}
if (buildChoiceLabeling) {
globalChoice.addChoiceLabels(choice.getChoiceLabels());
// Propagate dont cares
while (enableDC && !queues.dontCarePropagationDone()) {
DFTElementPointer next = queues.nextDontCarePropagation();
next->checkDontCareAnymore(*newState, queues);
}
// Update failable dependencies
newState->updateFailableDependencies(nextBE->id());
newState->updateDontCareDependencies(nextBE->id());
// Add new state
newStateId = stateToIdCallback(newState);
}
// Now construct the state-action reward for all selected reward models.
for (auto const& rewardModel : selectedRewardModels) {
ValueType stateActionRewardValue = storm::utility::zero<ValueType>();
if (rewardModel.get().hasStateActionRewards()) {
for (auto const& stateActionReward : rewardModel.get().getStateActionRewards()) {
for (auto const& choice : allChoices) {
if (stateActionReward.getActionIndex() == choice.getActionIndex() && evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
stateActionRewardValue += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass() / totalExitRate;
}
}
}
// Set transitions
if (hasDependencies) {
// Failure is due to dependency -> add non-deterministic choice
std::shared_ptr<storm::storage::DFTDependency<ValueType> const> dependency = mDft.getDependency(currentState->getDependencyId(currentFailable));
choice.addProbability(newStateId, dependency->probability());
STORM_LOG_TRACE("Added transition to " << newStateId << " with probability " << dependency->probability());
if (!storm::utility::isOne(dependency->probability())) {
// Add transition to state where dependency was unsuccessful
DFTStatePointer unsuccessfulState = std::make_shared<storm::storage::DFTState<ValueType>>(*currentState);
unsuccessfulState->letDependencyBeUnsuccessful(currentFailable);
// Add state
StateType unsuccessfulStateId = stateToIdCallback(unsuccessfulState);
ValueType remainingProbability = storm::utility::one<ValueType>() - dependency->probability();
choice.addProbability(unsuccessfulStateId, remainingProbability);
STORM_LOG_TRACE("Added transition to " << unsuccessfulStateId << " with remaining probability " << remainingProbability);
}
globalChoice.addChoiceReward(stateActionRewardValue);
result.addChoice(std::move(choice));
} else {
// Failure is due to "normal" BE failure
// Set failure rate according to activation
bool isActive = true;
if (mDft.hasRepresentant(nextBE->id())) {
// Active must be checked for the state we are coming from as this state is responsible for the
// rate and not the new state we are going to
isActive = currentState->isActive(mDft.getRepresentant(nextBE->id())->id());
}
ValueType rate = isActive ? nextBE->activeFailureRate() : nextBE->passiveFailureRate();
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") << " rate " << rate);
}
// Move the newly fused choice in place.
allChoices.clear();
allChoices.push_back(std::move(globalChoice));
}
++currentFailable;
} // end while failing BE
// Move all remaining choices in place.
for (auto& choice : allChoices) {
if (!hasDependencies) {
// Add all rates as one choice
result.addChoice(std::move(choice));
}
STORM_LOG_TRACE("Finished exploring state: " << mDft.getStateString(currentState));
result.setExpanded();
return result;*/
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented.");
return result;
}
template<typename ValueType, typename StateType>
StateBehavior<ValueType, StateType> DftNextStateGenerator<ValueType, StateType>::createMergeFailedState(StateToIdCallback const& stateToIdCallback) {
STORM_LOG_ASSERT(mergeFailedStates, "No unique failed state used.");
// Introduce explicit fail state
DFTStatePointer failedState = std::make_shared<storm::storage::DFTState<ValueType>>(mDft, mStateGenerationInfo, 0);
mergeFailedStateId = stateToIdCallback(failedState);
STORM_LOG_TRACE("Introduce fail state with id: " << mergeFailedStateId);
// Add self loop
Choice<ValueType, StateType> choice(0, true);
choice.addProbability(mergeFailedStateId, storm::utility::one<ValueType>());
// No further exploration required
StateBehavior<ValueType, StateType> result;
result.addChoice(std::move(choice));
result.setExpanded();
return result;
}
template class DftNextStateGenerator<double>;
template class DftNextStateGenerator<storm::RationalFunction>;

43
src/generator/DftNextStateGenerator.h
View File

@ -9,15 +9,21 @@
namespace storm {
namespace generator {
template<typename ValueType, typename StateType = uint_fast64_t>
/*!
* Next state generator for DFTs.
*/
template<typename ValueType, typename StateType = uint32_t>
class DftNextStateGenerator : public NextStateGenerator<ValueType, std::shared_ptr<storm::storage::DFTState<ValueType>>, StateType> {
using DFTStatePointer = std::shared_ptr<storm::storage::DFTState<ValueType>>;
using DFTElementPointer = std::shared_ptr<storm::storage::DFTElement<ValueType>>;
using DFTGatePointer = std::shared_ptr<storm::storage::DFTGate<ValueType>>;
using DFTRestrictionPointer = std::shared_ptr<storm::storage::DFTRestriction<ValueType>>;
public:
typedef typename NextStateGenerator<ValueType, DFTStatePointer, StateType>::StateToIdCallback StateToIdCallback;
DftNextStateGenerator(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo);
DftNextStateGenerator(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo, bool enableDC, bool mergeFailedStates);
virtual bool isDeterministicModel() const override;
virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) override;
@ -26,15 +32,38 @@ namespace storm {
virtual StateBehavior<ValueType, StateType> expand(StateToIdCallback const& stateToIdCallback) override;
virtual bool satisfies(storm::expressions::Expression const& expression) const override;
/*!
* Create unique failed state.
*
* @param stateToIdCallback Callback for state. The callback should just return the id and not use the state.
*
* @return Behavior of state.
*/
StateBehavior<ValueType, StateType> createMergeFailedState(StateToIdCallback const& stateToIdCallback);
private:
// The program used for the generation of next states.
// The dft used for the generation of next states.
storm::storage::DFT<ValueType> const& mDft;
// General information for the state generation.
storm::storage::DFTStateGenerationInfo const& mStateGenerationInfo;
DFTStatePointer const state;
// Current state
DFTStatePointer const* state;
// Flag indicating if dont care propagation is enabled.
bool enableDC;
// Flag indication if all failed states should be merged into one.
bool mergeFailedStates = true;
// Id of the merged failed state
StateType mergeFailedStateId = 0;
// Flag indicating if the model is deterministic.
bool deterministicModel = true;
// A comparator used to compare constants.
storm::utility::ConstantsComparator<ValueType> comparator;
};

3
src/generator/StateBehavior.cpp
View File

@ -56,7 +56,10 @@ namespace storm {
}
template class StateBehavior<double>;
#ifdef STORM_HAVE_CARL
template class StateBehavior<storm::RationalFunction>;
#endif
}
}

2
src/models/sparse/MarkovAutomaton.cpp
View File

@ -265,7 +265,7 @@ namespace storm {
}
template <typename ValueType, typename RewardModelType>
std::shared_ptr<storm::models::sparse::Ctmc<ValueType, RewardModelType>> MarkovAutomaton<ValueType, RewardModelType>::convertToCTMC() {
std::shared_ptr<storm::models::sparse::Ctmc<ValueType, RewardModelType>> MarkovAutomaton<ValueType, RewardModelType>::convertToCTMC() const {
STORM_LOG_TRACE("MA matrix:" << std::endl << this->getTransitionMatrix());
STORM_LOG_TRACE("Markovian states: " << getMarkovianStates());

7
src/models/sparse/MarkovAutomaton.h
View File

@ -150,7 +150,12 @@ namespace storm {
bool hasOnlyTrivialNondeterminism() const;
std::shared_ptr<storm::models::sparse::Ctmc<ValueType, RewardModelType>> convertToCTMC();
/*!
* Convert the MA into a MA by eliminating all states with probabilistic choices.
*
* @return Ctmc.
*/
std::shared_ptr<storm::models::sparse::Ctmc<ValueType, RewardModelType>> convertToCTMC() const;
virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector<ValueType> const* firstValue = nullptr, std::vector<ValueType> const* secondValue = nullptr, std::vector<uint_fast64_t> const* stateColoring = nullptr, std::vector<std::string> const* colors = nullptr, std::vector<uint_fast64_t>* scheduler = nullptr, bool finalizeOutput = true) const;

2
src/models/sparse/StateLabeling.cpp
View File

@ -29,7 +29,7 @@ namespace storm {
return true;
}
StateLabeling StateLabeling::getSubLabeling(storm::storage::BitVector const& states) {
StateLabeling StateLabeling::getSubLabeling(storm::storage::BitVector const& states) const {
StateLabeling result(states.getNumberOfSetBits());
for (auto const& labelIndexPair : nameToLabelingIndexMap) {
result.addLabel(labelIndexPair.first, labelings[labelIndexPair.second] % states);

2
src/models/sparse/StateLabeling.h
View File

@ -49,7 +49,7 @@ namespace storm {
*
* @param states The selected set of states.
*/
StateLabeling getSubLabeling(storm::storage::BitVector const& states);
StateLabeling getSubLabeling(storm::storage::BitVector const& states) const;
/*!
* Adds a new label to the labelings. Initially, no state is labeled with this label.

5
src/storage/dft/DFT.cpp
View File

@ -528,6 +528,11 @@ namespace storm {
}
}
template<typename ValueType>
bool DFT<ValueType>::canHaveNondeterminism() const {
return !getDependencies().empty();
}
template<typename ValueType>
DFTColouring<ValueType> DFT<ValueType>::colourDFT() const {
return DFTColouring<ValueType>(*this);

2
src/storage/dft/DFT.h
View File

@ -198,6 +198,8 @@ namespace storm {
}
return elements;
}
bool canHaveNondeterminism() const;
std::vector<DFT<ValueType>> topModularisation() const;

6
src/storage/dft/DFTState.cpp
View File

@ -9,11 +9,11 @@ namespace storm {
DFTState<ValueType>::DFTState(DFT<ValueType> const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(dft.stateVectorSize()), mId(id), mDft(dft), mStateGenerationInfo(stateGenerationInfo) {
// Initialize uses
for(size_t id : mDft.getSpareIndices()) {
std::shared_ptr<DFTGate<ValueType> const> elem = mDft.getGate(id);
for(size_t spareId : mDft.getSpareIndices()) {
std::shared_ptr<DFTGate<ValueType> const> elem = mDft.getGate(spareId);
STORM_LOG_ASSERT(elem->isSpareGate(), "Element is no spare gate.");
STORM_LOG_ASSERT(elem->nrChildren() > 0, "Element has no child.");
this->setUses(id, elem->children()[0]->id());
this->setUses(spareId, elem->children()[0]->id());
}
// Initialize activation

32
src/utility/vector.cpp
View File

@ -1,8 +1,9 @@
#include "src/utility/vector.h"
//template<typename ValueType>
//std::ostream& operator<<(std::ostream& out, std::vector<ValueType> const& vector) {
std::ostream& operator<<(std::ostream& out, std::vector<double> const& vector) {
// Template was causing problems as Carl has the same function
/*
template<typename ValueType>
std::ostream& operator<<(std::ostream& out, std::vector<ValueType> const& vector) {
out << "vector (" << vector.size() << ") [ ";
for (uint_fast64_t i = 0; i < vector.size() - 1; ++i) {
out << vector[i] << ", ";
@ -13,5 +14,26 @@ std::ostream& operator<<(std::ostream& out, std::vector<double> const& vector) {
}
// Explicitly instantiate functions.
//template std::ostream& operator<<(std::ostream& out, std::vector<double> const& vector);
//template std::ostream& operator<<(std::ostream& out, std::vector<uint_fast64_t> const& vector);
template std::ostream& operator<<(std::ostream& out, std::vector<double> const& vector);
template std::ostream& operator<<(std::ostream& out, std::vector<uint_fast64_t> const& vector);
*/
std::ostream& operator<<(std::ostream& out, std::vector<double> const& vector) {
out << "vector (" << vector.size() << ") [ ";
for (uint_fast64_t i = 0; i < vector.size() - 1; ++i) {
out << vector[i] << ", ";
}
out << vector.back();
out << " ]";
return out;
}
std::ostream& operator<<(std::ostream& out, std::vector<uint_fast64_t> const& vector) {
out << "vector (" << vector.size() << ") [ ";
for (uint_fast64_t i = 0; i < vector.size() - 1; ++i) {
out << vector[i] << ", ";
}
out << vector.back();
out << " ]";
return out;
}

1
src/utility/vector.h
View File

@ -19,6 +19,7 @@
//template<typename ValueType>
//std::ostream& operator<<(std::ostream& out, std::vector<ValueType> const& vector);
std::ostream& operator<<(std::ostream& out, std::vector<double> const& vector);
std::ostream& operator<<(std::ostream& out, std::vector<uint_fast64_t> const& vector);
namespace storm {
namespace utility {

Write Preview
Loading…
Cancel
Save