diff --git a/examples/dft/mas.dft b/examples/dft/mas.dft new file mode 100644 index 000000000..bed57d59c --- /dev/null +++ b/examples/dft/mas.dft @@ -0,0 +1,58 @@ +toplevel "MAS"; +"MAS" or "CPU" "DB" "MB" "VMB" "MEM" "VMS"; +"CPU" or "CW" "SO1" "SO2" "PG" "SM"; +"CW" and "CWA" "CWB"; +"SO1" and "SO1A" "SO1B"; +"SO2" and "SO2A" "SO2B"; +"PG" and "PGA" "PGB"; +"SM" and "SMA" "SMB"; +"CWA" csp "CWAev" "S1" "S2"; +"CWB" csp "CWBev" "S1" "S2"; +"SO1A" csp "SO1Aev" "S1" "S2"; +"SO1B" csp "SO1Bev" "S1" "S2"; +"SO2A" csp "SO2Aev" "S1" "S2"; +"SO2B" csp "SO2Bev" "S1" "S2"; +"PGA" csp "PGAev" "S1" "S2"; +"PGB" csp "PGBev" "S1" "S2"; +"SMA" csp "SMAev" "S1" "S2"; +"SMB" csp "SMBev" "S1" "S2"; +"CWAev" lambda=1.0e-6 dorm=0; +"CWBev" lambda=1.0e-6 dorm=0; +"SO1Aev" lambda=1.0e-6 dorm=0; +"SO1Bev" lambda=1.0e-6 dorm=0; +"SO2Aev" lambda=1.0e-6 dorm=0; +"SO2Bev" lambda=1.0e-6 dorm=0; +"PGAev" lambda=1.0e-6 dorm=0; +"PGBev" lambda=1.0e-6 dorm=0; +"SMAev" lambda=1.0e-6 dorm=0; +"SMBev" lambda=1.0e-6 dorm=0; +"S1" lambda=1.0e-6 dorm=0; +"S2" lambda=1.0e-6 dorm=0; +"DB" and "DB1" "DB2" "DB3"; +"DB1" lambda=5.0e-6 dorm=0; +"DB2" lambda=5.0e-6 dorm=0; +"DB3" lambda=5.0e-6 dorm=0; +"MB" and "MB1" "MB2" "MB3"; +"MB1" lambda=5.0e-6 dorm=0; +"MB2" lambda=5.0e-6 dorm=0; +"MB3" lambda=5.0e-6 dorm=0; +"VMB" and "VMB1" "VMB2"; +"VMB1" lambda=5.0e-6 dorm=0; +"VMB2" lambda=5.0e-6 dorm=0; +"MEM" and "MEM1" "MEM2"; +"MEM1" lambda=1.0e-5 dorm=0; +"MEM2" lambda=1.0e-5 dorm=0; +"VMS" or "VM1" "VM2"; +"VM1" and "VM1A" "VM1B"; +"VM2" and "VM2A" "VM2B"; +"VM1A" csp "VM1Aev" "VMS1" "VMS2"; +"VM1B" csp "VM1Bev" "VMS1" "VMS2"; +"VM2A" csp "VM2Aev" "VMS1" "VMS2"; +"VM2B" csp "VM2Bev" "VMS1" "VMS2"; +"VM1Aev" lambda=1.0e-6 dorm=0; +"VM1Bev" lambda=1.0e-6 dorm=0; +"VM2Aev" lambda=1.0e-6 dorm=0; +"VM2Bev" lambda=1.0e-6 dorm=0; +"VMS1" lambda=1.0e-6 dorm=0; +"VMS2" lambda=1.0e-6 dorm=0; + diff --git a/examples/dft/nonmonoton_param.dft b/examples/dft/nonmonoton_param.dft index e83f3b012..fab011e64 100644 --- a/examples/dft/nonmonoton_param.dft +++ b/examples/dft/nonmonoton_param.dft @@ -2,7 +2,7 @@ param x; param y; toplevel "A"; "A" or "B" "Z"; -"B" pand "D" "S"; -"Z" lambda=y dorm=0; -"D" lambda=100 dorm=0; -"S" lambda=100*x dorm=0; +"Z" pand "C" "D"; +"B" lambda=y dorm=0; +"C" lambda=100 dorm=0; +"D" lambda=100*x dorm=0; diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index 4d794cb2f..46797aa23 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -160,23 +160,6 @@ namespace storm { return model; } - template<> - bool belowThreshold(double const& number) { - return number < 0.1; - } - - template<> - bool belowThreshold(storm::RationalFunction const& number) { - storm::RationalFunction threshold = storm::utility::one() / 10; - std::cout << number << " < " << threshold << ": " << (number < threshold) << std::endl; - std::map mapping; - - storm::RationalFunction eval(number.evaluate(mapping)); - std::cout << "Evaluated: " << eval << std::endl; - return eval < threshold; - } - - template std::pair ExplicitDFTModelBuilder::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)); @@ -225,29 +208,6 @@ namespace storm { 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; diff --git a/src/builder/ExplicitDFTModelBuilder.h b/src/builder/ExplicitDFTModelBuilder.h index eae19cb61..b9c54d2b6 100644 --- a/src/builder/ExplicitDFTModelBuilder.h +++ b/src/builder/ExplicitDFTModelBuilder.h @@ -91,9 +91,6 @@ namespace storm { std::pair checkForExploration(DFTStatePointer const& state); }; - - template - bool belowThreshold(ValueType const& number); } } diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp new file mode 100644 index 000000000..285301807 --- /dev/null +++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp @@ -0,0 +1,666 @@ +#include "src/builder/ExplicitDFTModelBuilderApprox.h" +#include +#include +#include +#include +#include +#include "src/settings/modules/DFTSettings.h" +#include "src/settings/SettingsManager.h" +#include "src/generator/DftNextStateGenerator.h" +#include + +namespace storm { + namespace builder { + + 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) { + // stateVectorSize is bound for size of bitvector + + mStateGenerationInfo = std::make_shared(mDft.buildStateGenerationInfo(symmetries)); + } + + + 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); + + 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")); + + 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"); + } + } + + if(mergeFailedStates) { + modelComponents.stateLabeling.addLabelToState("failed", failedIndex); + } + 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); + } + } + } + + 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]); + } + } + } + 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."); + } + } + + // 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")); + + 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"); + } + } + + if(mergeFailedStates) { + modelComponents.stateLabeling.addLabelToState("failed", failedIndex); + } + 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); + } + } + } + + 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]); + } + } + } + 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<> + bool belowThreshold(double const& number) { + return number < 0.1; + } + + template<> + bool belowThreshold(storm::RationalFunction const& number) { + storm::RationalFunction threshold = storm::utility::one() / 10; + std::cout << number << " < " << threshold << ": " << (number < threshold) << std::endl; + std::map mapping; + + storm::RationalFunction eval(number.evaluate(mapping)); + std::cout << "Evaluated: " << eval << std::endl; + 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) { + bool changed = false; + if (mStateGenerationInfo->hasSymmetries()) { + // Order state by symmetry + STORM_LOG_TRACE("Check for symmetry: " << mDft.getStateString(state)); + changed = state->orderBySymmetry(); + STORM_LOG_TRACE("State " << (changed ? "changed to " : "did not change") << (changed ? mDft.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); + } + + 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 + 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()); + } else { + // State needs exploration + return std::make_pair(true, 0); + } + } + } + + 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; + } + } + + + // Explicitly instantiate the class. + template class ExplicitDFTModelBuilderApprox; + +#ifdef STORM_HAVE_CARL + template class ExplicitDFTModelBuilderApprox; +#endif + + } // namespace builder +} // namespace storm + + diff --git a/src/builder/ExplicitDFTModelBuilderApprox.h b/src/builder/ExplicitDFTModelBuilderApprox.h new file mode 100644 index 000000000..d03681cbe --- /dev/null +++ b/src/builder/ExplicitDFTModelBuilderApprox.h @@ -0,0 +1,105 @@ +#ifndef EXPLICITDFTMODELBUILDERAPPROX_H +#define EXPLICITDFTMODELBUILDERAPPROX_H + +#include +#include +#include +#include +#include "src/storage/sparse/StateStorage.h" +#include +#include +#include +#include +#include +#include + +namespace storm { + namespace builder { + + template + class ExplicitDFTModelBuilderApprox { + + using DFTElementPointer = std::shared_ptr>; + using DFTElementCPointer = std::shared_ptr const>; + using DFTGatePointer = std::shared_ptr>; + using DFTStatePointer = std::shared_ptr>; + using DFTRestrictionPointer = std::shared_ptr>; + + + // A structure holding the individual components of a model. + struct ModelComponents { + ModelComponents(); + + // The transition matrix. + storm::storage::SparseMatrix transitionMatrix; + + // The state labeling. + storm::models::sparse::StateLabeling stateLabeling; + + // The Markovian states. + storm::storage::BitVector markovianStates; + + // The exit rates. + std::vector exitRates; + + // A vector that stores a labeling for each choice. + 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: + struct LabelOptions { + bool buildFailLabel = true; + bool buildFailSafeLabel = false; + std::set beLabels = {}; + }; + + ExplicitDFTModelBuilderApprox(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC); + + 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. + * + * @param state The state to add. + * @return Id of added state. + */ + uint_fast64_t addState(DFTStatePointer const& state); + + /*! + * Check if state needs an exploration and remember pseudo states for later creation. + * + * @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. + */ + std::pair checkForExploration(DFTStatePointer const& state); + + }; + + template + bool belowThreshold(ValueType const& number); + } +} + +#endif /* EXPLICITDFTMODELBUILDERAPPROX_H */ diff --git a/src/generator/DftNextStateGenerator.cpp b/src/generator/DftNextStateGenerator.cpp index b56f8a358..3138fef6a 100644 --- a/src/generator/DftNextStateGenerator.cpp +++ b/src/generator/DftNextStateGenerator.cpp @@ -2,38 +2,30 @@ #include "src/utility/constants.h" #include "src/utility/macros.h" -#include "src/exceptions/WrongFormatException.h" +#include "src/exceptions/NotImplementedException.h" namespace storm { namespace generator { template - DftNextStateGenerator::DftNextStateGenerator(storm::storage::DFT const& dft) : mDft(dft), state(nullptr), comparator() { + DftNextStateGenerator::DftNextStateGenerator(storm::storage::DFT const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo) : mDft(dft), mStateGenerationInfo(stateGenerationInfo), state(nullptr), comparator() { // Intentionally left empty. } template bool DftNextStateGenerator::isDeterministicModel() const { - assert(false); - return true; + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented."); } template std::vector DftNextStateGenerator::getInitialStates(StateToIdCallback const& stateToIdCallback) { - // FIXME: This only works for models with exactly one initial state. We should make this more general. - /*CompressedState initialState(variableInformation.getTotalBitOffset()); - - // We need to initialize the values of the variables to their initial value. - for (auto const& booleanVariable : variableInformation.booleanVariables) { - initialState.set(booleanVariable.bitOffset, booleanVariable.initialValue); - } - for (auto const& integerVariable : variableInformation.integerVariables) { - initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast(integerVariable.initialValue - integerVariable.lowerBound)); - } + DFTStatePointer initialState = std::make_shared>(mDft, mStateGenerationInfo, 0); - // Register initial state and return it. + // Register initial state StateType id = stateToIdCallback(initialState); - return {id};*/ + + initialState->setId(id); + return {id}; } template @@ -43,14 +35,12 @@ namespace storm { // 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."); } template bool DftNextStateGenerator::satisfies(storm::expressions::Expression const& expression) const { - /* if (expression.isTrue()) { - return true; - } - return evaluator.asBool(expression);*/ + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented."); } template @@ -147,6 +137,7 @@ namespace storm { result.setExpanded(); return result;*/ + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented."); } diff --git a/src/generator/DftNextStateGenerator.h b/src/generator/DftNextStateGenerator.h index 6c8e5538d..17a7dd25a 100644 --- a/src/generator/DftNextStateGenerator.h +++ b/src/generator/DftNextStateGenerator.h @@ -9,17 +9,20 @@ namespace storm { namespace generator { - template + template class DftNextStateGenerator : public NextStateGenerator>, StateType> { + + using DFTStatePointer = std::shared_ptr>; + public: - typedef typename NextStateGenerator>, StateType>::StateToIdCallback StateToIdCallback; + typedef typename NextStateGenerator::StateToIdCallback StateToIdCallback; - DftNextStateGenerator(storm::storage::DFT const& dft); + DftNextStateGenerator(storm::storage::DFT const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo); virtual bool isDeterministicModel() const override; virtual std::vector getInitialStates(StateToIdCallback const& stateToIdCallback) override; - virtual void load(std::shared_ptr> const& state) override; + virtual void load(DFTStatePointer const& state) override; virtual StateBehavior expand(StateToIdCallback const& stateToIdCallback) override; virtual bool satisfies(storm::expressions::Expression const& expression) const override; @@ -28,7 +31,9 @@ namespace storm { // The program used for the generation of next states. storm::storage::DFT const& mDft; - CompressedState const* state; + storm::storage::DFTStateGenerationInfo const& mStateGenerationInfo; + + DFTStatePointer const state; // A comparator used to compare constants. storm::utility::ConstantsComparator comparator; diff --git a/src/modelchecker/DFTAnalyser.h b/src/modelchecker/DFTAnalyser.h index 24c1068ba..cc1e34696 100644 --- a/src/modelchecker/DFTAnalyser.h +++ b/src/modelchecker/DFTAnalyser.h @@ -1,12 +1,14 @@ #pragma once -#include "logic/Formula.h" -#include "parser/DFTGalileoParser.h" -#include "builder/ExplicitDFTModelBuilder.h" -#include "modelchecker/results/CheckResult.h" -#include "utility/storm.h" -#include "storage/dft/DFTIsomorphism.h" -#include "utility/bitoperations.h" +#include "src/logic/Formula.h" +#include "src/parser/DFTGalileoParser.h" +#include "src/builder/ExplicitDFTModelBuilder.h" +#include "src/builder/ExplicitDFTModelBuilderApprox.h" +#include "src/modelchecker/results/CheckResult.h" +#include "src/utility/storm.h" +#include "src/storage/dft/DFTIsomorphism.h" +#include "src/settings/modules/DFTSettings.h" +#include "src/utility/bitoperations.h" #include @@ -149,9 +151,17 @@ private: // Building Markov Automaton STORM_LOG_INFO("Building Model..."); - storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, enableDC); - typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions; // TODO initialize this with the formula - std::shared_ptr> model = builder.buildModel(labeloptions); + std::shared_ptr> model; + // TODO Matthias: use only one builder if everything works again + if (storm::settings::getModule().computeApproximation()) { + storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, enableDC); + typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions; // TODO initialize this with the formula + model = builder.buildModel(labeloptions); + } else { + storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, enableDC); + typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions; // TODO initialize this with the formula + model = builder.buildModel(labeloptions); + } //model->printModelInformationToStream(std::cout); STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates()); STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions()); diff --git a/src/storage/sparse/StateStorage.cpp b/src/storage/sparse/StateStorage.cpp index 60af49179..15789c355 100644 --- a/src/storage/sparse/StateStorage.cpp +++ b/src/storage/sparse/StateStorage.cpp @@ -15,6 +15,7 @@ namespace storm { } template class StateStorage; + template class StateStorage; } } } \ No newline at end of file