diff --git a/examples/dft/fdep4.dft b/examples/dft/fdep4.dft new file mode 100644 index 000000000..7e3c5642a --- /dev/null +++ b/examples/dft/fdep4.dft @@ -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; diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp index 285301807..9ff34b734 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp @@ -12,223 +12,167 @@ namespace storm { namespace builder { - template - ExplicitDFTModelBuilderApprox::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), markovianStates(), exitRates(), choiceLabeling() { + template + ExplicitDFTModelBuilderApprox::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), markovianStates(), exitRates(), choiceLabeling() { // Intentionally left empty. } - - template - ExplicitDFTModelBuilderApprox::ExplicitDFTModelBuilderApprox(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) : mDft(dft), enableDC(enableDC), stateStorage(((mDft.stateVectorSize() / 64) + 1) * 64) { + + template + ExplicitDFTModelBuilderApprox::ExplicitDFTModelBuilderApprox(storm::storage::DFT 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(mDft.buildStateGenerationInfo(symmetries)); + stateGenerationInfo = std::make_shared(dft.buildStateGenerationInfo(symmetries)); } + template + std::shared_ptr> ExplicitDFTModelBuilderApprox::buildModel(LabelOptions const& labelOpts) { + STORM_LOG_TRACE("Generating DFT state space"); - template - std::shared_ptr> ExplicitDFTModelBuilderApprox::buildModel(LabelOptions const& labelOpts) { // Initialize - bool deterministicModel = false; - size_t rowOffset = 0; - ModelComponents modelComponents; - std::vector tmpMarkovianStates; - storm::storage::SparseMatrixBuilder 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 generator(dft, *stateGenerationInfo, enableDC, mergeFailedStates); + // Create sparse matrix builder + storm::storage::SparseMatrixBuilder 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()); - STORM_LOG_TRACE("Introduce fail state with id: " << failedIndex); - modelComponents.exitRates.push_back(storm::utility::one()); - tmpMarkovianStates.push_back(failedIndex); - } - - // Explore state space - DFTStatePointer state = std::make_shared>(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>(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 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 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>> basicElements = mDft.getBasicElements(); - for (std::shared_ptr> 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 stateProbabilityPair = *(behavior.begin()->begin()); + STORM_LOG_ASSERT(stateProbabilityPair.first == failedStateId, "No self loop for failed state."); + STORM_LOG_ASSERT(storm::utility::isOne(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> elem : basicElements) { - if (labelOpts.beLabels.count(elem->name()) > 0 && storm::storage::DFTState::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 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 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> 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 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>(std::move(rateMatrix), std::move(modelComponents.exitRates), std::move(modelComponents.stateLabeling)); - } else { - std::shared_ptr> ma = std::make_shared>(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 - std::shared_ptr> ExplicitDFTModelBuilderApprox::buildModelApprox(LabelOptions const& labelOpts) { - // Initialize - bool deterministicModel = false; - size_t rowOffset = 0; - ModelComponents modelComponents; - std::vector tmpMarkovianStates; - storm::storage::SparseMatrixBuilder 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()); - STORM_LOG_TRACE("Introduce fail state with id: " << failedIndex); - modelComponents.exitRates.push_back(storm::utility::one()); - tmpMarkovianStates.push_back(failedIndex); - } - - // Initialize generator - storm::generator::DftNextStateGenerator generator(mDft, *mStateGenerationInfo); - - // Explore state space - typename storm::generator::DftNextStateGenerator::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>(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>(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 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>(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 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>> basicElements = mDft.getBasicElements(); + std::vector>> basicElements = dft.getBasicElements(); for (std::shared_ptr> 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> elem : basicElements) { - if (labelOpts.beLabels.count(elem->name()) > 0 && storm::storage::DFTState::hasFailed(state, mStateGenerationInfo->getStateIndex(elem->id())) ) { + if (labelOpts.beLabels.count(elem->name()) > 0 && storm::storage::DFTState::hasFailed(state, stateGenerationInfo->getStateIndex(elem->id())) ) { modelComponents.stateLabeling.addLabelToState(elem->name() + "_fail", stateId); } } } - + std::shared_ptr> 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 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>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling)); + } else { + // Build MA + // Compute exit rates + modelComponents.exitRates = std::vector(stateSize); + std::vector::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(); } } - model = std::make_shared>(std::move(rateMatrix), std::move(modelComponents.exitRates), std::move(modelComponents.stateLabeling)); - } else { - std::shared_ptr> ma = std::make_shared>(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> ma = std::make_shared>(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 - std::pair ExplicitDFTModelBuilderApprox::exploreStates(DFTStatePointer const& state, size_t& rowOffset, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector& markovianStates, std::vector& 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 outgoingRates; - std::vector> outgoingProbabilities; - bool hasDependencies = state->nrFailableDependencies() > 0; - size_t failableCount = hasDependencies ? state->nrFailableDependencies() : state->nrFailableBEs(); - size_t smallest = 0; - ValueType exitRate = storm::utility::zero(); - 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()); - STORM_LOG_TRACE("Added self loop for " << stateId); - exitRates.push_back(storm::utility::one()); - 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>(*state); - std::pair const>, bool> nextBEPair = newState->letNextBEFail(smallest++); - std::shared_ptr 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().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 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 choiceProbabilities; - std::shared_ptr 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>(*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() - 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 - std::pair ExplicitDFTModelBuilderApprox::checkForExploration(DFTStatePointer const& state) { + template + StateType ExplicitDFTModelBuilderApprox::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 - uint_fast64_t ExplicitDFTModelBuilderApprox::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 + void ExplicitDFTModelBuilderApprox::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 + void ExplicitDFTModelBuilderApprox::setRemapping(StateType id, StateType mappedId) { + STORM_LOG_ASSERT(id < stateRemapping.size(), "Invalid index for remapping."); + stateRemapping[id] = mappedId; } diff --git a/src/builder/ExplicitDFTModelBuilderApprox.h b/src/builder/ExplicitDFTModelBuilderApprox.h index d03681cbe..247b66ca1 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.h +++ b/src/builder/ExplicitDFTModelBuilderApprox.h @@ -12,11 +12,15 @@ #include #include #include +#include namespace storm { namespace builder { - template + /*! + * Build a Markov chain from DFT. + */ + template class ExplicitDFTModelBuilderApprox { using DFTElementPointer = std::shared_ptr>; @@ -43,57 +47,100 @@ namespace storm { std::vector exitRates; // A vector that stores a labeling for each choice. - boost::optional>> choiceLabeling; + boost::optional>> choiceLabeling; }; - - const uint_fast64_t OFFSET_PSEUDO_STATE = UINT_FAST64_MAX / 2; - - storm::storage::DFT const& mDft; - std::shared_ptr mStateGenerationInfo; - //TODO Matthias: remove when everything works - std::vector> 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 stateStorage; public: + // A structure holding the labeling options. struct LabelOptions { bool buildFailLabel = true; bool buildFailSafeLabel = false; std::set 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 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> buildModel(LabelOptions const& labelOpts); - // TODO Matthias: only temporary used for avoiding crashing everything - std::shared_ptr> buildModelApprox(LabelOptions const& labelOpts); - private: - std::pair exploreStates(DFTStatePointer const& state, size_t& rowOffset, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector& markovianStates, std::vector& 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 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::max() / 2; + + // Dft + storm::storage::DFT const& dft; + + // General information for state generation + // TODO Matthias: use const reference + std::shared_ptr stateGenerationInfo; + + // Current id for new state + size_t newIndex = 0; + + //TODO Matthias: remove when everything works + std::vector> 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 stateStorage; + + // A set of states that still need to be explored. + std::deque 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 stateRemapping; }; diff --git a/src/generator/DftNextStateGenerator.cpp b/src/generator/DftNextStateGenerator.cpp index 3138fef6a..953a36db4 100644 --- a/src/generator/DftNextStateGenerator.cpp +++ b/src/generator/DftNextStateGenerator.cpp @@ -8,13 +8,13 @@ namespace storm { namespace generator { template - DftNextStateGenerator::DftNextStateGenerator(storm::storage::DFT const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo) : mDft(dft), mStateGenerationInfo(stateGenerationInfo), state(nullptr), comparator() { - // Intentionally left empty. + DftNextStateGenerator::DftNextStateGenerator(storm::storage::DFT 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 bool DftNextStateGenerator::isDeterministicModel() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented."); + return deterministicModel; } template @@ -29,117 +29,201 @@ namespace storm { } template - void DftNextStateGenerator::load(std::shared_ptr> 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::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 bool DftNextStateGenerator::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 StateBehavior DftNextStateGenerator::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 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(); - 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> allChoices = getUnlabeledChoices(*this->state, stateToIdCallback); - std::vector> 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 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()); + 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 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(totalNumberOfChoices) : storm::utility::zero(); - - // 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>(*currentState); + std::pair const>, bool> nextBEPair = newState->letNextBEFail(currentFailable); + std::shared_ptr 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().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 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(); - 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 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>(*currentState); + unsuccessfulState->letDependencyBeUnsuccessful(currentFailable); + // Add state + StateType unsuccessfulStateId = stateToIdCallback(unsuccessfulState); + ValueType remainingProbability = storm::utility::one() - 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 + StateBehavior DftNextStateGenerator::createMergeFailedState(StateToIdCallback const& stateToIdCallback) { + STORM_LOG_ASSERT(mergeFailedStates, "No unique failed state used."); + // Introduce explicit fail state + DFTStatePointer failedState = std::make_shared>(mDft, mStateGenerationInfo, 0); + mergeFailedStateId = stateToIdCallback(failedState); + STORM_LOG_TRACE("Introduce fail state with id: " << mergeFailedStateId); + + // Add self loop + Choice choice(0, true); + choice.addProbability(mergeFailedStateId, storm::utility::one()); + + // No further exploration required + StateBehavior result; + result.addChoice(std::move(choice)); + result.setExpanded(); + return result; } - template class DftNextStateGenerator; template class DftNextStateGenerator; diff --git a/src/generator/DftNextStateGenerator.h b/src/generator/DftNextStateGenerator.h index 17a7dd25a..f7c4945c7 100644 --- a/src/generator/DftNextStateGenerator.h +++ b/src/generator/DftNextStateGenerator.h @@ -9,15 +9,21 @@ namespace storm { namespace generator { - template + /*! + * Next state generator for DFTs. + */ + template class DftNextStateGenerator : public NextStateGenerator>, StateType> { using DFTStatePointer = std::shared_ptr>; + using DFTElementPointer = std::shared_ptr>; + using DFTGatePointer = std::shared_ptr>; + using DFTRestrictionPointer = std::shared_ptr>; public: typedef typename NextStateGenerator::StateToIdCallback StateToIdCallback; - DftNextStateGenerator(storm::storage::DFT const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo); + DftNextStateGenerator(storm::storage::DFT const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo, bool enableDC, bool mergeFailedStates); virtual bool isDeterministicModel() const override; virtual std::vector getInitialStates(StateToIdCallback const& stateToIdCallback) override; @@ -26,15 +32,38 @@ namespace storm { virtual StateBehavior 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 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 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 comparator; }; diff --git a/src/generator/StateBehavior.cpp b/src/generator/StateBehavior.cpp index 6ae1f6de0..ccbdd5166 100644 --- a/src/generator/StateBehavior.cpp +++ b/src/generator/StateBehavior.cpp @@ -56,7 +56,10 @@ namespace storm { } template class StateBehavior; + +#ifdef STORM_HAVE_CARL template class StateBehavior; +#endif } } \ No newline at end of file diff --git a/src/models/sparse/MarkovAutomaton.cpp b/src/models/sparse/MarkovAutomaton.cpp index 7b997293f..f8c40ad2f 100644 --- a/src/models/sparse/MarkovAutomaton.cpp +++ b/src/models/sparse/MarkovAutomaton.cpp @@ -265,7 +265,7 @@ namespace storm { } template - std::shared_ptr> MarkovAutomaton::convertToCTMC() { + std::shared_ptr> MarkovAutomaton::convertToCTMC() const { STORM_LOG_TRACE("MA matrix:" << std::endl << this->getTransitionMatrix()); STORM_LOG_TRACE("Markovian states: " << getMarkovianStates()); diff --git a/src/models/sparse/MarkovAutomaton.h b/src/models/sparse/MarkovAutomaton.h index 9864f4f85..bb7272f6d 100644 --- a/src/models/sparse/MarkovAutomaton.h +++ b/src/models/sparse/MarkovAutomaton.h @@ -150,7 +150,12 @@ namespace storm { bool hasOnlyTrivialNondeterminism() const; - std::shared_ptr> convertToCTMC(); + /*! + * Convert the MA into a MA by eliminating all states with probabilistic choices. + * + * @return Ctmc. + */ + std::shared_ptr> convertToCTMC() const; virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const; diff --git a/src/models/sparse/StateLabeling.cpp b/src/models/sparse/StateLabeling.cpp index 7957e6a99..70561c8cb 100644 --- a/src/models/sparse/StateLabeling.cpp +++ b/src/models/sparse/StateLabeling.cpp @@ -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); diff --git a/src/models/sparse/StateLabeling.h b/src/models/sparse/StateLabeling.h index c7b3411a7..ac8ac730a 100644 --- a/src/models/sparse/StateLabeling.h +++ b/src/models/sparse/StateLabeling.h @@ -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. diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index 5fdf44ab3..87ee74cdd 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -528,6 +528,11 @@ namespace storm { } } + template + bool DFT::canHaveNondeterminism() const { + return !getDependencies().empty(); + } + template DFTColouring DFT::colourDFT() const { return DFTColouring(*this); diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h index 7b0177d07..c12204e06 100644 --- a/src/storage/dft/DFT.h +++ b/src/storage/dft/DFT.h @@ -198,6 +198,8 @@ namespace storm { } return elements; } + + bool canHaveNondeterminism() const; std::vector> topModularisation() const; diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index 9a0a16dba..156f99d14 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -9,11 +9,11 @@ namespace storm { DFTState::DFTState(DFT 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 const> elem = mDft.getGate(id); + for(size_t spareId : mDft.getSpareIndices()) { + std::shared_ptr 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 diff --git a/src/utility/vector.cpp b/src/utility/vector.cpp index 20af3c628..44e480029 100644 --- a/src/utility/vector.cpp +++ b/src/utility/vector.cpp @@ -1,8 +1,9 @@ #include "src/utility/vector.h" -//template -//std::ostream& operator<<(std::ostream& out, std::vector const& vector) { -std::ostream& operator<<(std::ostream& out, std::vector const& vector) { +// Template was causing problems as Carl has the same function +/* +template +std::ostream& operator<<(std::ostream& out, std::vector 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 const& vector) { } // Explicitly instantiate functions. -//template std::ostream& operator<<(std::ostream& out, std::vector const& vector); -//template std::ostream& operator<<(std::ostream& out, std::vector const& vector); \ No newline at end of file +template std::ostream& operator<<(std::ostream& out, std::vector const& vector); +template std::ostream& operator<<(std::ostream& out, std::vector const& vector); +*/ + +std::ostream& operator<<(std::ostream& out, std::vector 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 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; +} \ No newline at end of file diff --git a/src/utility/vector.h b/src/utility/vector.h index 0a4da1e03..a767f5fcc 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -19,6 +19,7 @@ //template //std::ostream& operator<<(std::ostream& out, std::vector const& vector); std::ostream& operator<<(std::ostream& out, std::vector const& vector); +std::ostream& operator<<(std::ostream& out, std::vector const& vector); namespace storm { namespace utility {