Matthias Volk
7 years ago
16 changed files with 1488 additions and 1990 deletions
-
124src/storm-dft-cli/storm-dft.cpp
-
1106src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
-
342src/storm-dft/builder/ExplicitDFTModelBuilder.h
-
841src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
-
362src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h
-
4src/storm-dft/generator/DftNextStateGenerator.cpp
-
32src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
-
51src/storm-dft/settings/DftSettings.cpp
-
11src/storm-dft/settings/DftSettings.h
-
189src/storm-dft/settings/modules/DFTSettings.cpp
-
123src/storm-dft/settings/modules/DftIOSettings.cpp
-
80src/storm-dft/settings/modules/DftIOSettings.h
-
93src/storm-dft/settings/modules/FaultTreeSettings.cpp
-
104src/storm-dft/settings/modules/FaultTreeSettings.h
-
12src/storm/models/sparse/MarkovAutomaton.cpp
-
4src/storm/models/sparse/MarkovAutomaton.h
1106
src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
@ -1,841 +0,0 @@ |
|||
#include "ExplicitDFTModelBuilderApprox.h"
|
|||
|
|||
#include <map>
|
|||
|
|||
#include "storm/models/sparse/MarkovAutomaton.h"
|
|||
#include "storm/models/sparse/Ctmc.h"
|
|||
#include "storm/utility/constants.h"
|
|||
#include "storm/utility/vector.h"
|
|||
#include "storm/utility/bitoperations.h"
|
|||
#include "storm/exceptions/UnexpectedException.h"
|
|||
#include "storm/settings/SettingsManager.h"
|
|||
#include "storm/logic/AtomicLabelFormula.h"
|
|||
#include "storm-dft/settings/modules/DFTSettings.h"
|
|||
|
|||
|
|||
namespace storm { |
|||
namespace builder { |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
ExplicitDFTModelBuilderApprox<ValueType, StateType>::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), markovianStates(), exitRates(), choiceLabeling() { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
ExplicitDFTModelBuilderApprox<ValueType, StateType>::MatrixBuilder::MatrixBuilder(bool canHaveNondeterminism) : mappingOffset(0), stateRemapping(), currentRowGroup(0), currentRow(0), canHaveNondeterminism((canHaveNondeterminism)) { |
|||
// Create matrix builder
|
|||
builder = storm::storage::SparseMatrixBuilder<ValueType>(0, 0, 0, false, canHaveNondeterminism, 0); |
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
ExplicitDFTModelBuilderApprox<ValueType, StateType>::LabelOptions::LabelOptions(std::vector<std::shared_ptr<const storm::logic::Formula>> properties, bool buildAllLabels) : buildFailLabel(true), buildFailSafeLabel(false), buildAllLabels(buildAllLabels) { |
|||
// Get necessary labels from properties
|
|||
std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> atomicLabels; |
|||
for (auto property : properties) { |
|||
property->gatherAtomicLabelFormulas(atomicLabels); |
|||
} |
|||
// Set usage of necessary labels
|
|||
for (auto atomic : atomicLabels) { |
|||
std::string label = atomic->getLabel(); |
|||
std::size_t foundIndex = label.find("_fail"); |
|||
if (foundIndex != std::string::npos) { |
|||
elementLabels.insert(label.substr(0, foundIndex)); |
|||
} else if (label.compare("failed") == 0) { |
|||
buildFailLabel = true; |
|||
} else if (label.compare("failsafe") == 0) { |
|||
buildFailSafeLabel = true; |
|||
} else { |
|||
STORM_LOG_WARN("Label '" << label << "' not known."); |
|||
} |
|||
} |
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
ExplicitDFTModelBuilderApprox<ValueType, StateType>::ExplicitDFTModelBuilderApprox(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) : |
|||
dft(dft), |
|||
stateGenerationInfo(std::make_shared<storm::storage::DFTStateGenerationInfo>(dft.buildStateGenerationInfo(symmetries))), |
|||
enableDC(enableDC), |
|||
usedHeuristic(storm::settings::getModule<storm::settings::modules::DFTSettings>().getApproximationHeuristic()), |
|||
generator(dft, *stateGenerationInfo, enableDC, mergeFailedStates), |
|||
matrixBuilder(!generator.isDeterministicModel()), |
|||
stateStorage(((dft.stateVectorSize() / 64) + 1) * 64), |
|||
// TODO Matthias: make choosable
|
|||
//explorationQueue(dft.nrElements()+1, 0, 1)
|
|||
explorationQueue(200, 0, 0.9) |
|||
{ |
|||
// Intentionally left empty.
|
|||
// TODO Matthias: remove again
|
|||
usedHeuristic = storm::builder::ApproximationHeuristic::DEPTH; |
|||
|
|||
// Compute independent subtrees
|
|||
if (dft.topLevelType() == storm::storage::DFTElementType::OR) { |
|||
// We only support this for approximation with top level element OR
|
|||
for (auto const& child : dft.getGate(dft.getTopLevelIndex())->children()) { |
|||
// Consider all children of the top level gate
|
|||
std::vector<size_t> isubdft; |
|||
if (child->nrParents() > 1 || child->hasOutgoingDependencies()) { |
|||
STORM_LOG_TRACE("child " << child->name() << "does not allow modularisation."); |
|||
isubdft.clear(); |
|||
} else if (dft.isGate(child->id())) { |
|||
isubdft = dft.getGate(child->id())->independentSubDft(false); |
|||
} else { |
|||
STORM_LOG_ASSERT(dft.isBasicElement(child->id()), "Child is no BE."); |
|||
if(dft.getBasicElement(child->id())->hasIngoingDependencies()) { |
|||
STORM_LOG_TRACE("child " << child->name() << "does not allow modularisation."); |
|||
isubdft.clear(); |
|||
} else { |
|||
isubdft = {child->id()}; |
|||
} |
|||
} |
|||
if(isubdft.empty()) { |
|||
subtreeBEs.clear(); |
|||
break; |
|||
} else { |
|||
// Add new independent subtree
|
|||
std::vector<size_t> subtree; |
|||
for (size_t id : isubdft) { |
|||
if (dft.isBasicElement(id)) { |
|||
subtree.push_back(id); |
|||
} |
|||
} |
|||
subtreeBEs.push_back(subtree); |
|||
} |
|||
} |
|||
} |
|||
if (subtreeBEs.empty()) { |
|||
// Consider complete tree
|
|||
std::vector<size_t> subtree; |
|||
for (size_t id = 0; id < dft.nrElements(); ++id) { |
|||
if (dft.isBasicElement(id)) { |
|||
subtree.push_back(id); |
|||
} |
|||
} |
|||
subtreeBEs.push_back(subtree); |
|||
} |
|||
|
|||
for (auto tree : subtreeBEs) { |
|||
std::stringstream stream; |
|||
stream << "Subtree: "; |
|||
for (size_t id : tree) { |
|||
stream << id << ", "; |
|||
} |
|||
STORM_LOG_TRACE(stream.str()); |
|||
} |
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
void ExplicitDFTModelBuilderApprox<ValueType, StateType>::buildModel(LabelOptions const& labelOpts, size_t iteration, double approximationThreshold) { |
|||
STORM_LOG_TRACE("Generating DFT state space"); |
|||
|
|||
if (iteration < 1) { |
|||
// Initialize
|
|||
modelComponents.markovianStates = storm::storage::BitVector(INITIAL_BITVECTOR_SIZE); |
|||
|
|||
if(mergeFailedStates) { |
|||
// Introduce explicit fail state
|
|||
storm::generator::StateBehavior<ValueType, StateType> behavior = generator.createMergeFailedState([this] (DFTStatePointer const& state) { |
|||
this->failedStateId = newIndex++; |
|||
matrixBuilder.stateRemapping.push_back(0); |
|||
return this->failedStateId; |
|||
} ); |
|||
|
|||
matrixBuilder.setRemapping(failedStateId); |
|||
STORM_LOG_ASSERT(!behavior.empty(), "Behavior is empty."); |
|||
matrixBuilder.newRowGroup(); |
|||
setMarkovian(behavior.begin()->isMarkovian()); |
|||
|
|||
// Now add self loop.
|
|||
// TODO Matthias: maybe use general method.
|
|||
STORM_LOG_ASSERT(behavior.getNumberOfChoices() == 1, "Wrong number of choices for failed state."); |
|||
STORM_LOG_ASSERT(behavior.begin()->size() == 1, "Wrong number of transitions for failed state."); |
|||
std::pair<StateType, ValueType> stateProbabilityPair = *(behavior.begin()->begin()); |
|||
STORM_LOG_ASSERT(stateProbabilityPair.first == failedStateId, "No self loop for failed state."); |
|||
STORM_LOG_ASSERT(storm::utility::isOne<ValueType>(stateProbabilityPair.second), "Probability for failed state != 1."); |
|||
matrixBuilder.addTransition(stateProbabilityPair.first, stateProbabilityPair.second); |
|||
matrixBuilder.finishRow(); |
|||
} |
|||
|
|||
// Build initial state
|
|||
this->stateStorage.initialStateIndices = generator.getInitialStates(std::bind(&ExplicitDFTModelBuilderApprox::getOrAddStateIndex, this, std::placeholders::_1)); |
|||
STORM_LOG_ASSERT(stateStorage.initialStateIndices.size() == 1, "Only one initial state assumed."); |
|||
initialStateIndex = stateStorage.initialStateIndices[0]; |
|||
STORM_LOG_TRACE("Initial state: " << initialStateIndex); |
|||
// Initialize heuristic values for inital state
|
|||
STORM_LOG_ASSERT(!statesNotExplored.at(initialStateIndex).second, "Heuristic for initial state is already initialized"); |
|||
ExplorationHeuristicPointer heuristic = std::make_shared<ExplorationHeuristic>(initialStateIndex); |
|||
heuristic->markExpand(); |
|||
statesNotExplored[initialStateIndex].second = heuristic; |
|||
explorationQueue.push(heuristic); |
|||
} else { |
|||
initializeNextIteration(); |
|||
} |
|||
|
|||
if (approximationThreshold > 0) { |
|||
switch (usedHeuristic) { |
|||
case storm::builder::ApproximationHeuristic::NONE: |
|||
// Do not change anything
|
|||
approximationThreshold = dft.nrElements()+10; |
|||
break; |
|||
case storm::builder::ApproximationHeuristic::DEPTH: |
|||
approximationThreshold = iteration + 1; |
|||
break; |
|||
case storm::builder::ApproximationHeuristic::PROBABILITY: |
|||
case storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE: |
|||
approximationThreshold = 10 * std::pow(2, iteration); |
|||
break; |
|||
} |
|||
} |
|||
exploreStateSpace(approximationThreshold); |
|||
|
|||
size_t stateSize = stateStorage.getNumberOfStates() + (mergeFailedStates ? 1 : 0); |
|||
modelComponents.markovianStates.resize(stateSize); |
|||
modelComponents.deterministicModel = generator.isDeterministicModel(); |
|||
|
|||
// Fix the entries in the transition matrix according to the mapping of ids to row group indices
|
|||
STORM_LOG_ASSERT(matrixBuilder.getRemapping(initialStateIndex) == initialStateIndex, "Initial state should not be remapped."); |
|||
// TODO Matthias: do not consider all rows?
|
|||
STORM_LOG_TRACE("Remap matrix: " << matrixBuilder.stateRemapping << ", offset: " << matrixBuilder.mappingOffset); |
|||
matrixBuilder.remap(); |
|||
|
|||
STORM_LOG_TRACE("State remapping: " << matrixBuilder.stateRemapping); |
|||
STORM_LOG_TRACE("Markovian states: " << modelComponents.markovianStates); |
|||
STORM_LOG_DEBUG("Model has " << stateSize << " states"); |
|||
STORM_LOG_DEBUG("Model is " << (generator.isDeterministicModel() ? "deterministic" : "non-deterministic")); |
|||
|
|||
// Build transition matrix
|
|||
modelComponents.transitionMatrix = matrixBuilder.builder.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"); |
|||
} |
|||
|
|||
buildLabeling(labelOpts); |
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
void ExplicitDFTModelBuilderApprox<ValueType, StateType>::initializeNextIteration() { |
|||
STORM_LOG_TRACE("Refining DFT state space"); |
|||
|
|||
// TODO Matthias: should be easier now as skipped states all are at the end of the matrix
|
|||
// Push skipped states to explore queue
|
|||
// TODO Matthias: remove
|
|||
for (auto const& skippedState : skippedStates) { |
|||
statesNotExplored[skippedState.second.first->getId()] = skippedState.second; |
|||
explorationQueue.push(skippedState.second.second); |
|||
} |
|||
|
|||
// Initialize matrix builder again
|
|||
// TODO Matthias: avoid copy
|
|||
std::vector<uint_fast64_t> copyRemapping = matrixBuilder.stateRemapping; |
|||
matrixBuilder = MatrixBuilder(!generator.isDeterministicModel()); |
|||
matrixBuilder.stateRemapping = copyRemapping; |
|||
StateType nrStates = modelComponents.transitionMatrix.getRowGroupCount(); |
|||
STORM_LOG_ASSERT(nrStates == matrixBuilder.stateRemapping.size(), "No. of states does not coincide with mapping size."); |
|||
|
|||
// Start by creating a remapping from the old indices to the new indices
|
|||
std::vector<StateType> indexRemapping = std::vector<StateType>(nrStates, 0); |
|||
auto iterSkipped = skippedStates.begin(); |
|||
size_t skippedBefore = 0; |
|||
for (size_t i = 0; i < indexRemapping.size(); ++i) { |
|||
while (iterSkipped != skippedStates.end() && iterSkipped->first <= i) { |
|||
STORM_LOG_ASSERT(iterSkipped->first < indexRemapping.size(), "Skipped is too high."); |
|||
++skippedBefore; |
|||
++iterSkipped; |
|||
} |
|||
indexRemapping[i] = i - skippedBefore; |
|||
} |
|||
|
|||
// Set remapping
|
|||
size_t nrExpandedStates = nrStates - skippedBefore; |
|||
matrixBuilder.mappingOffset = nrStates; |
|||
STORM_LOG_TRACE("# expanded states: " << nrExpandedStates); |
|||
StateType skippedIndex = nrExpandedStates; |
|||
std::map<StateType, std::pair<DFTStatePointer, ExplorationHeuristicPointer>> skippedStatesNew; |
|||
for (size_t id = 0; id < matrixBuilder.stateRemapping.size(); ++id) { |
|||
StateType index = matrixBuilder.getRemapping(id); |
|||
auto itFind = skippedStates.find(index); |
|||
if (itFind != skippedStates.end()) { |
|||
// Set new mapping for skipped state
|
|||
matrixBuilder.stateRemapping[id] = skippedIndex; |
|||
skippedStatesNew[skippedIndex] = itFind->second; |
|||
indexRemapping[index] = skippedIndex; |
|||
++skippedIndex; |
|||
} else { |
|||
// Set new mapping for expanded state
|
|||
matrixBuilder.stateRemapping[id] = indexRemapping[index]; |
|||
} |
|||
} |
|||
STORM_LOG_TRACE("New state remapping: " << matrixBuilder.stateRemapping); |
|||
std::stringstream ss; |
|||
ss << "Index remapping:" << std::endl; |
|||
for (auto tmp : indexRemapping) { |
|||
ss << tmp << " "; |
|||
} |
|||
STORM_LOG_TRACE(ss.str()); |
|||
|
|||
// Remap markovian states
|
|||
storm::storage::BitVector markovianStatesNew = storm::storage::BitVector(modelComponents.markovianStates.size(), true); |
|||
// Iterate over all not set bits
|
|||
modelComponents.markovianStates.complement(); |
|||
size_t index = modelComponents.markovianStates.getNextSetIndex(0); |
|||
while (index < modelComponents.markovianStates.size()) { |
|||
markovianStatesNew.set(indexRemapping[index], false); |
|||
index = modelComponents.markovianStates.getNextSetIndex(index+1); |
|||
} |
|||
STORM_LOG_ASSERT(modelComponents.markovianStates.size() - modelComponents.markovianStates.getNumberOfSetBits() == markovianStatesNew.getNumberOfSetBits(), "Remapping of markovian states is wrong."); |
|||
STORM_LOG_ASSERT(markovianStatesNew.size() == nrStates, "No. of states does not coincide with markovian size."); |
|||
modelComponents.markovianStates = markovianStatesNew; |
|||
|
|||
// Build submatrix for expanded states
|
|||
// TODO Matthias: only use row groups when necessary
|
|||
for (StateType oldRowGroup = 0; oldRowGroup < modelComponents.transitionMatrix.getRowGroupCount(); ++oldRowGroup) { |
|||
if (indexRemapping[oldRowGroup] < nrExpandedStates) { |
|||
// State is expanded -> copy to new matrix
|
|||
matrixBuilder.newRowGroup(); |
|||
for (StateType oldRow = modelComponents.transitionMatrix.getRowGroupIndices()[oldRowGroup]; oldRow < modelComponents.transitionMatrix.getRowGroupIndices()[oldRowGroup+1]; ++oldRow) { |
|||
for (typename storm::storage::SparseMatrix<ValueType>::const_iterator itEntry = modelComponents.transitionMatrix.begin(oldRow); itEntry != modelComponents.transitionMatrix.end(oldRow); ++itEntry) { |
|||
auto itFind = skippedStates.find(itEntry->getColumn()); |
|||
if (itFind != skippedStates.end()) { |
|||
// Set id for skipped states as we remap it later
|
|||
matrixBuilder.addTransition(matrixBuilder.mappingOffset + itFind->second.first->getId(), itEntry->getValue()); |
|||
} else { |
|||
// Set newly remapped index for expanded states
|
|||
matrixBuilder.addTransition(indexRemapping[itEntry->getColumn()], itEntry->getValue()); |
|||
} |
|||
} |
|||
matrixBuilder.finishRow(); |
|||
} |
|||
} |
|||
} |
|||
|
|||
skippedStates = skippedStatesNew; |
|||
|
|||
STORM_LOG_ASSERT(matrixBuilder.getCurrentRowGroup() == nrExpandedStates, "Row group size does not match."); |
|||
skippedStates.clear(); |
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
void ExplicitDFTModelBuilderApprox<ValueType, StateType>::exploreStateSpace(double approximationThreshold) { |
|||
size_t nrExpandedStates = 0; |
|||
size_t nrSkippedStates = 0; |
|||
// TODO Matthias: do not empty queue every time but break before
|
|||
while (!explorationQueue.empty()) { |
|||
// Get the first state in the queue
|
|||
ExplorationHeuristicPointer currentExplorationHeuristic = explorationQueue.popTop(); |
|||
StateType currentId = currentExplorationHeuristic->getId(); |
|||
auto itFind = statesNotExplored.find(currentId); |
|||
STORM_LOG_ASSERT(itFind != statesNotExplored.end(), "Id " << currentId << " not found"); |
|||
DFTStatePointer currentState = itFind->second.first; |
|||
STORM_LOG_ASSERT(currentExplorationHeuristic == itFind->second.second, "Exploration heuristics do not match"); |
|||
STORM_LOG_ASSERT(currentState->getId() == currentId, "Ids do not match"); |
|||
// Remove it from the list of not explored states
|
|||
statesNotExplored.erase(itFind); |
|||
STORM_LOG_ASSERT(stateStorage.stateToId.contains(currentState->status()), "State is not contained in state storage."); |
|||
STORM_LOG_ASSERT(stateStorage.stateToId.getValue(currentState->status()) == currentId, "Ids of states do not coincide."); |
|||
|
|||
// Get concrete state if necessary
|
|||
if (currentState->isPseudoState()) { |
|||
// Create concrete state from pseudo state
|
|||
currentState->construct(); |
|||
} |
|||
STORM_LOG_ASSERT(!currentState->isPseudoState(), "State is pseudo state."); |
|||
|
|||
// Remember that the current row group was actually filled with the transitions of a different state
|
|||
matrixBuilder.setRemapping(currentId); |
|||
|
|||
matrixBuilder.newRowGroup(); |
|||
|
|||
// Try to explore the next state
|
|||
generator.load(currentState); |
|||
|
|||
//if (approximationThreshold > 0.0 && nrExpandedStates > approximationThreshold && !currentExplorationHeuristic->isExpand()) {
|
|||
if (approximationThreshold > 0.0 && currentExplorationHeuristic->isSkip(approximationThreshold)) { |
|||
// Skip the current state
|
|||
++nrSkippedStates; |
|||
STORM_LOG_TRACE("Skip expansion of state: " << dft.getStateString(currentState)); |
|||
setMarkovian(true); |
|||
// Add transition to target state with temporary value 0
|
|||
// TODO Matthias: what to do when there is no unique target state?
|
|||
matrixBuilder.addTransition(failedStateId, storm::utility::zero<ValueType>()); |
|||
// Remember skipped state
|
|||
skippedStates[matrixBuilder.getCurrentRowGroup() - 1] = std::make_pair(currentState, currentExplorationHeuristic); |
|||
matrixBuilder.finishRow(); |
|||
} else { |
|||
// Explore the current state
|
|||
++nrExpandedStates; |
|||
storm::generator::StateBehavior<ValueType, StateType> behavior = generator.expand(std::bind(&ExplicitDFTModelBuilderApprox::getOrAddStateIndex, this, std::placeholders::_1)); |
|||
STORM_LOG_ASSERT(!behavior.empty(), "Behavior is empty."); |
|||
setMarkovian(behavior.begin()->isMarkovian()); |
|||
|
|||
// Now add all choices.
|
|||
for (auto const& choice : behavior) { |
|||
// Add the probabilistic behavior to the matrix.
|
|||
for (auto const& stateProbabilityPair : choice) { |
|||
STORM_LOG_ASSERT(!storm::utility::isZero(stateProbabilityPair.second), "Probability zero."); |
|||
// Set transition to state id + offset. This helps in only remapping all previously skipped states.
|
|||
matrixBuilder.addTransition(matrixBuilder.mappingOffset + stateProbabilityPair.first, stateProbabilityPair.second); |
|||
// Set heuristic values for reached states
|
|||
auto iter = statesNotExplored.find(stateProbabilityPair.first); |
|||
if (iter != statesNotExplored.end()) { |
|||
// Update heuristic values
|
|||
DFTStatePointer state = iter->second.first; |
|||
if (!iter->second.second) { |
|||
// Initialize heuristic values
|
|||
ExplorationHeuristicPointer heuristic = std::make_shared<ExplorationHeuristic>(stateProbabilityPair.first, *currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass()); |
|||
iter->second.second = heuristic; |
|||
if (state->hasFailed(dft.getTopLevelIndex()) || state->isFailsafe(dft.getTopLevelIndex()) || state->nrFailableDependencies() > 0 || (state->nrFailableDependencies() == 0 && state->nrFailableBEs() == 0)) { |
|||
// Do not skip absorbing state or if reached by dependencies
|
|||
iter->second.second->markExpand(); |
|||
} |
|||
if (usedHeuristic == storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE) { |
|||
// Compute bounds for heuristic now
|
|||
if (state->isPseudoState()) { |
|||
// Create concrete state from pseudo state
|
|||
state->construct(); |
|||
} |
|||
STORM_LOG_ASSERT(!currentState->isPseudoState(), "State is pseudo state."); |
|||
|
|||
// Initialize bounds
|
|||
// TODO Mathias: avoid hack
|
|||
ValueType lowerBound = getLowerBound(state); |
|||
ValueType upperBound = getUpperBound(state); |
|||
heuristic->setBounds(lowerBound, upperBound); |
|||
} |
|||
|
|||
explorationQueue.push(heuristic); |
|||
} else if (!iter->second.second->isExpand()) { |
|||
double oldPriority = iter->second.second->getPriority(); |
|||
if (iter->second.second->updateHeuristicValues(*currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass())) { |
|||
// Update priority queue
|
|||
explorationQueue.update(iter->second.second, oldPriority); |
|||
} |
|||
} |
|||
} |
|||
} |
|||
matrixBuilder.finishRow(); |
|||
} |
|||
} |
|||
} // end exploration
|
|||
|
|||
STORM_LOG_INFO("Expanded " << nrExpandedStates << " states"); |
|||
STORM_LOG_INFO("Skipped " << nrSkippedStates << " states"); |
|||
STORM_LOG_ASSERT(nrSkippedStates == skippedStates.size(), "Nr skipped states is wrong"); |
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
void ExplicitDFTModelBuilderApprox<ValueType, StateType>::buildLabeling(LabelOptions const& labelOpts) { |
|||
// Build state labeling
|
|||
modelComponents.stateLabeling = storm::models::sparse::StateLabeling(modelComponents.transitionMatrix.getRowGroupCount()); |
|||
// Initial state
|
|||
modelComponents.stateLabeling.addLabel("init"); |
|||
STORM_LOG_ASSERT(matrixBuilder.getRemapping(initialStateIndex) == initialStateIndex, "Initial state should not be remapped."); |
|||
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 necessary elements
|
|||
for (size_t id = 0; id < dft.nrElements(); ++id) { |
|||
std::shared_ptr<storage::DFTElement<ValueType> const> element = dft.getElement(id); |
|||
if (labelOpts.buildAllLabels || labelOpts.elementLabels.count(element->name()) > 0) { |
|||
modelComponents.stateLabeling.addLabel(element->name() + "_fail"); |
|||
} |
|||
} |
|||
|
|||
// Set labels to states
|
|||
if (mergeFailedStates) { |
|||
modelComponents.stateLabeling.addLabelToState("failed", failedStateId); |
|||
} |
|||
for (auto const& stateIdPair : stateStorage.stateToId) { |
|||
storm::storage::BitVector state = stateIdPair.first; |
|||
size_t stateId = matrixBuilder.getRemapping(stateIdPair.second); |
|||
if (!mergeFailedStates && labelOpts.buildFailLabel && dft.hasFailed(state, *stateGenerationInfo)) { |
|||
modelComponents.stateLabeling.addLabelToState("failed", stateId); |
|||
} |
|||
if (labelOpts.buildFailSafeLabel && dft.isFailsafe(state, *stateGenerationInfo)) { |
|||
modelComponents.stateLabeling.addLabelToState("failsafe", stateId); |
|||
} |
|||
// Set fail status for each necessary element
|
|||
for (size_t id = 0; id < dft.nrElements(); ++id) { |
|||
std::shared_ptr<storage::DFTElement<ValueType> const> element = dft.getElement(id); |
|||
if ((labelOpts.buildAllLabels || labelOpts.elementLabels.count(element->name()) > 0) && storm::storage::DFTState<ValueType>::hasFailed(state, stateGenerationInfo->getStateIndex(element->id()))) { |
|||
modelComponents.stateLabeling.addLabelToState(element->name() + "_fail", stateId); |
|||
} |
|||
} |
|||
} |
|||
|
|||
STORM_LOG_TRACE(modelComponents.stateLabeling); |
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilderApprox<ValueType, StateType>::getModel() { |
|||
STORM_LOG_ASSERT(skippedStates.size() == 0, "Concrete model has skipped states"); |
|||
return createModel(false); |
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilderApprox<ValueType, StateType>::getModelApproximation(bool lowerBound, bool expectedTime) { |
|||
if (expectedTime) { |
|||
// TODO Matthias: handle case with no skipped states
|
|||
changeMatrixBound(modelComponents.transitionMatrix, lowerBound); |
|||
return createModel(true); |
|||
} else { |
|||
// Change model for probabilities
|
|||
// TODO Matthias: make nicer
|
|||
storm::storage::SparseMatrix<ValueType> matrix = modelComponents.transitionMatrix; |
|||
storm::models::sparse::StateLabeling labeling = modelComponents.stateLabeling; |
|||
if (lowerBound) { |
|||
// Set self loop for lower bound
|
|||
for (auto it = skippedStates.begin(); it != skippedStates.end(); ++it) { |
|||
auto matrixEntry = matrix.getRow(it->first, 0).begin(); |
|||
STORM_LOG_ASSERT(matrixEntry->getColumn() == failedStateId, "Transition has wrong target state."); |
|||
STORM_LOG_ASSERT(!it->second.first->isPseudoState(), "State is still pseudo state."); |
|||
matrixEntry->setValue(storm::utility::one<ValueType>()); |
|||
matrixEntry->setColumn(it->first); |
|||
} |
|||
} else { |
|||
// Make skipped states failed states for upper bound
|
|||
storm::storage::BitVector failedStates = modelComponents.stateLabeling.getStates("failed"); |
|||
for (auto it = skippedStates.begin(); it != skippedStates.end(); ++it) { |
|||
failedStates.set(it->first); |
|||
} |
|||
labeling.setStates("failed", failedStates); |
|||
} |
|||
|
|||
std::shared_ptr<storm::models::sparse::Model<ValueType>> model; |
|||
if (modelComponents.deterministicModel) { |
|||
model = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(std::move(matrix), std::move(labeling)); |
|||
} else { |
|||
// Build MA
|
|||
// Compute exit rates
|
|||
// TODO Matthias: avoid computing multiple times
|
|||
modelComponents.exitRates = std::vector<ValueType>(modelComponents.markovianStates.size()); |
|||
std::vector<typename storm::storage::SparseMatrix<ValueType>::index_type> indices = matrix.getRowGroupIndices(); |
|||
for (StateType stateIndex = 0; stateIndex < modelComponents.markovianStates.size(); ++stateIndex) { |
|||
if (modelComponents.markovianStates[stateIndex]) { |
|||
modelComponents.exitRates[stateIndex] = matrix.getRowSum(indices[stateIndex]); |
|||
} else { |
|||
modelComponents.exitRates[stateIndex] = storm::utility::zero<ValueType>(); |
|||
} |
|||
} |
|||
STORM_LOG_TRACE("Exit rates: " << modelComponents.exitRates); |
|||
|
|||
storm::storage::sparse::ModelComponents<ValueType> maComponents(std::move(matrix), std::move(labeling)); |
|||
maComponents.rateTransitions = true; |
|||
maComponents.markovianStates = modelComponents.markovianStates; |
|||
maComponents.exitRates = modelComponents.exitRates; |
|||
std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(maComponents)); |
|||
if (ma->hasOnlyTrivialNondeterminism()) { |
|||
// Markov automaton can be converted into CTMC
|
|||
// TODO Matthias: change components which were not moved accordingly
|
|||
model = ma->convertToCTMC(); |
|||
} else { |
|||
model = ma; |
|||
} |
|||
|
|||
} |
|||
|
|||
if (model->getNumberOfStates() <= 15) { |
|||
STORM_LOG_TRACE("Transition matrix: " << std::endl << model->getTransitionMatrix()); |
|||
} else { |
|||
STORM_LOG_TRACE("Transition matrix: too big to print"); |
|||
} |
|||
return model; |
|||
} |
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilderApprox<ValueType, StateType>::createModel(bool copy) { |
|||
std::shared_ptr<storm::models::sparse::Model<ValueType>> model; |
|||
|
|||
if (modelComponents.deterministicModel) { |
|||
// Build CTMC
|
|||
if (copy) { |
|||
model = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(modelComponents.transitionMatrix, modelComponents.stateLabeling); |
|||
} else { |
|||
model = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling)); |
|||
} |
|||
} else { |
|||
// Build MA
|
|||
// Compute exit rates
|
|||
// TODO Matthias: avoid computing multiple times
|
|||
modelComponents.exitRates = std::vector<ValueType>(modelComponents.markovianStates.size()); |
|||
std::vector<typename storm::storage::SparseMatrix<ValueType>::index_type> indices = modelComponents.transitionMatrix.getRowGroupIndices(); |
|||
for (StateType stateIndex = 0; stateIndex < modelComponents.markovianStates.size(); ++stateIndex) { |
|||
if (modelComponents.markovianStates[stateIndex]) { |
|||
modelComponents.exitRates[stateIndex] = modelComponents.transitionMatrix.getRowSum(indices[stateIndex]); |
|||
} else { |
|||
modelComponents.exitRates[stateIndex] = storm::utility::zero<ValueType>(); |
|||
} |
|||
} |
|||
STORM_LOG_TRACE("Exit rates: " << modelComponents.exitRates); |
|||
|
|||
std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma; |
|||
if (copy) { |
|||
storm::storage::sparse::ModelComponents<ValueType> maComponents(modelComponents.transitionMatrix, modelComponents.stateLabeling); |
|||
maComponents.rateTransitions = true; |
|||
maComponents.markovianStates = modelComponents.markovianStates; |
|||
maComponents.exitRates = modelComponents.exitRates; |
|||
std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(maComponents)); |
|||
} else { |
|||
storm::storage::sparse::ModelComponents<ValueType> maComponents(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling)); |
|||
maComponents.rateTransitions = true; |
|||
maComponents.markovianStates = std::move(modelComponents.markovianStates); |
|||
maComponents.exitRates = std::move(modelComponents.exitRates); |
|||
std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(maComponents)); |
|||
} |
|||
if (ma->hasOnlyTrivialNondeterminism()) { |
|||
// Markov automaton can be converted into CTMC
|
|||
// TODO Matthias: change components which were not moved accordingly
|
|||
model = ma->convertToCTMC(); |
|||
} else { |
|||
model = ma; |
|||
} |
|||
} |
|||
|
|||
if (model->getNumberOfStates() <= 15) { |
|||
STORM_LOG_TRACE("Transition matrix: " << std::endl << model->getTransitionMatrix()); |
|||
} else { |
|||
STORM_LOG_TRACE("Transition matrix: too big to print"); |
|||
} |
|||
return model; |
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
void ExplicitDFTModelBuilderApprox<ValueType, StateType>::changeMatrixBound(storm::storage::SparseMatrix<ValueType> & matrix, bool lowerBound) const { |
|||
// Set lower bound for skipped states
|
|||
for (auto it = skippedStates.begin(); it != skippedStates.end(); ++it) { |
|||
auto matrixEntry = matrix.getRow(it->first, 0).begin(); |
|||
STORM_LOG_ASSERT(matrixEntry->getColumn() == failedStateId, "Transition has wrong target state."); |
|||
STORM_LOG_ASSERT(!it->second.first->isPseudoState(), "State is still pseudo state."); |
|||
|
|||
ExplorationHeuristicPointer heuristic = it->second.second; |
|||
if (storm::utility::isZero(heuristic->getUpperBound())) { |
|||
// Initialize bounds
|
|||
ValueType lowerBound = getLowerBound(it->second.first); |
|||
ValueType upperBound = getUpperBound(it->second.first); |
|||
heuristic->setBounds(lowerBound, upperBound); |
|||
} |
|||
|
|||
// Change bound
|
|||
if (lowerBound) { |
|||
matrixEntry->setValue(it->second.second->getLowerBound()); |
|||
} else { |
|||
matrixEntry->setValue(it->second.second->getUpperBound()); |
|||
} |
|||
} |
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
ValueType ExplicitDFTModelBuilderApprox<ValueType, StateType>::getLowerBound(DFTStatePointer const& state) const { |
|||
// Get the lower bound by considering the failure of all possible BEs
|
|||
ValueType lowerBound = storm::utility::zero<ValueType>(); |
|||
for (size_t index = 0; index < state->nrFailableBEs(); ++index) { |
|||
lowerBound += state->getFailableBERate(index); |
|||
} |
|||
return lowerBound; |
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
ValueType ExplicitDFTModelBuilderApprox<ValueType, StateType>::getUpperBound(DFTStatePointer const& state) const { |
|||
if (state->hasFailed(dft.getTopLevelIndex())) { |
|||
return storm::utility::zero<ValueType>(); |
|||
} |
|||
|
|||
// Get the upper bound by considering the failure of all BEs
|
|||
ValueType upperBound = storm::utility::one<ValueType>(); |
|||
ValueType rateSum = storm::utility::zero<ValueType>(); |
|||
|
|||
// Compute for each independent subtree
|
|||
for (std::vector<size_t> const& subtree : subtreeBEs) { |
|||
// Get all possible rates
|
|||
std::vector<ValueType> rates; |
|||
storm::storage::BitVector coldBEs(subtree.size(), false); |
|||
for (size_t i = 0; i < subtree.size(); ++i) { |
|||
size_t id = subtree[i]; |
|||
if (state->isOperational(id)) { |
|||
// Get BE rate
|
|||
ValueType rate = state->getBERate(id); |
|||
if (storm::utility::isZero<ValueType>(rate)) { |
|||
// Get active failure rate for cold BE
|
|||
rate = dft.getBasicElement(id)->activeFailureRate(); |
|||
if (storm::utility::isZero<ValueType>(rate)) { |
|||
// Ignore BE which cannot fail
|
|||
continue; |
|||
} |
|||
// Mark BE as cold
|
|||
coldBEs.set(i, true); |
|||
} |
|||
rates.push_back(rate); |
|||
rateSum += rate; |
|||
} |
|||
} |
|||
|
|||
STORM_LOG_ASSERT(rates.size() > 0, "No rates failable"); |
|||
|
|||
// Sort rates
|
|||
std::sort(rates.begin(), rates.end()); |
|||
std::vector<size_t> rateCount(rates.size(), 0); |
|||
size_t lastIndex = 0; |
|||
for (size_t i = 0; i < rates.size(); ++i) { |
|||
if (rates[lastIndex] != rates[i]) { |
|||
lastIndex = i; |
|||
} |
|||
++rateCount[lastIndex]; |
|||
} |
|||
|
|||
for (size_t i = 0; i < rates.size(); ++i) { |
|||
// Cold BEs cannot fail in the first step
|
|||
if (!coldBEs.get(i) && rateCount[i] > 0) { |
|||
std::iter_swap(rates.begin() + i, rates.end() - 1); |
|||
// Compute AND MTTF of subtree without current rate and scale with current rate
|
|||
upperBound += rates.back() * rateCount[i] * computeMTTFAnd(rates, rates.size() - 1); |
|||
// Swap back
|
|||
// TODO try to avoid swapping back
|
|||
std::iter_swap(rates.begin() + i, rates.end() - 1); |
|||
} |
|||
} |
|||
} |
|||
|
|||
STORM_LOG_TRACE("Upper bound is " << (rateSum / upperBound) << " for state " << state->getId()); |
|||
STORM_LOG_ASSERT(!storm::utility::isZero(upperBound), "Upper bound is 0"); |
|||
STORM_LOG_ASSERT(!storm::utility::isZero(rateSum), "State is absorbing"); |
|||
return rateSum / upperBound; |
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
ValueType ExplicitDFTModelBuilderApprox<ValueType, StateType>::computeMTTFAnd(std::vector<ValueType> const& rates, size_t size) const { |
|||
ValueType result = storm::utility::zero<ValueType>(); |
|||
if (size == 0) { |
|||
return result; |
|||
} |
|||
|
|||
// TODO Matthias: works only for <64 BEs!
|
|||
// WARNING: this code produces wrong results for more than 32 BEs
|
|||
/*for (size_t i = 1; i < 4 && i <= rates.size(); ++i) {
|
|||
size_t permutation = smallestIntWithNBitsSet(static_cast<size_t>(i)); |
|||
ValueType sum = storm::utility::zero<ValueType>(); |
|||
do { |
|||
ValueType permResult = storm::utility::zero<ValueType>(); |
|||
for(size_t j = 0; j < rates.size(); ++j) { |
|||
if(permutation & static_cast<size_t>(1 << static_cast<size_t>(j))) { |
|||
// WARNING: if the first bit is set, it also recognizes the 32nd bit as set
|
|||
// TODO: fix
|
|||
permResult += rates[j]; |
|||
} |
|||
} |
|||
permutation = nextBitPermutation(permutation); |
|||
STORM_LOG_ASSERT(!storm::utility::isZero(permResult), "PermResult is 0"); |
|||
sum += storm::utility::one<ValueType>() / permResult; |
|||
} while(permutation < (static_cast<size_t>(1) << rates.size()) && permutation != 0); |
|||
if (i % 2 == 0) { |
|||
result -= sum; |
|||
} else { |
|||
result += sum; |
|||
} |
|||
}*/ |
|||
|
|||
// Compute result with permutations of size <= 3
|
|||
ValueType one = storm::utility::one<ValueType>(); |
|||
for (size_t i1 = 0; i1 < size; ++i1) { |
|||
// + 1/a
|
|||
ValueType sum = rates[i1]; |
|||
result += one / sum; |
|||
for (size_t i2 = 0; i2 < i1; ++i2) { |
|||
// - 1/(a+b)
|
|||
ValueType sum2 = sum + rates[i2]; |
|||
result -= one / sum2; |
|||
for (size_t i3 = 0; i3 < i2; ++i3) { |
|||
// + 1/(a+b+c)
|
|||
result += one / (sum2 + rates[i3]); |
|||
} |
|||
} |
|||
} |
|||
|
|||
STORM_LOG_ASSERT(!storm::utility::isZero(result), "UpperBound is 0"); |
|||
return result; |
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
StateType ExplicitDFTModelBuilderApprox<ValueType, StateType>::getOrAddStateIndex(DFTStatePointer const& state) { |
|||
StateType stateId; |
|||
bool changed = false; |
|||
|
|||
if (stateGenerationInfo->hasSymmetries()) { |
|||
// Order state by symmetry
|
|||
STORM_LOG_TRACE("Check for symmetry: " << dft.getStateString(state)); |
|||
changed = state->orderBySymmetry(); |
|||
STORM_LOG_TRACE("State " << (changed ? "changed to " : "did not change") << (changed ? dft.getStateString(state) : "")); |
|||
} |
|||
|
|||
if (stateStorage.stateToId.contains(state->status())) { |
|||
// State already exists
|
|||
stateId = stateStorage.stateToId.getValue(state->status()); |
|||
STORM_LOG_TRACE("State " << dft.getStateString(state) << " with id " << stateId << " already exists"); |
|||
if (!changed) { |
|||
// Check if state is pseudo state
|
|||
// If state is explored already the possible pseudo state was already constructed
|
|||
auto iter = statesNotExplored.find(stateId); |
|||
if (iter != statesNotExplored.end() && iter->second.first->isPseudoState()) { |
|||
// Create pseudo state now
|
|||
STORM_LOG_ASSERT(iter->second.first->getId() == stateId, "Ids do not match."); |
|||
STORM_LOG_ASSERT(iter->second.first->status() == state->status(), "Pseudo states do not coincide."); |
|||
state->setId(stateId); |
|||
// Update mapping to map to concrete state now
|
|||
// TODO Matthias: just change pointer?
|
|||
statesNotExplored[stateId] = std::make_pair(state, iter->second.second); |
|||
// We do not push the new state on the exploration queue as the pseudo state was already pushed
|
|||
STORM_LOG_TRACE("Created pseudo state " << dft.getStateString(state)); |
|||
} |
|||
} |
|||
} else { |
|||
// State does not exist yet
|
|||
STORM_LOG_ASSERT(state->isPseudoState() == changed, "State type (pseudo/concrete) wrong."); |
|||
// Create new state
|
|||
state->setId(newIndex++); |
|||
stateId = stateStorage.stateToId.findOrAdd(state->status(), state->getId()); |
|||
STORM_LOG_ASSERT(stateId == state->getId(), "Ids do not match."); |
|||
// Insert state as not yet explored
|
|||
ExplorationHeuristicPointer nullHeuristic; |
|||
statesNotExplored[stateId] = std::make_pair(state, nullHeuristic); |
|||
// Reserve one slot for the new state in the remapping
|
|||
matrixBuilder.stateRemapping.push_back(0); |
|||
STORM_LOG_TRACE("New " << (state->isPseudoState() ? "pseudo" : "concrete") << " state: " << dft.getStateString(state)); |
|||
} |
|||
return stateId; |
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
void ExplicitDFTModelBuilderApprox<ValueType, StateType>::setMarkovian(bool markovian) { |
|||
if (matrixBuilder.getCurrentRowGroup() > modelComponents.markovianStates.size()) { |
|||
// Resize BitVector
|
|||
modelComponents.markovianStates.resize(modelComponents.markovianStates.size() + INITIAL_BITVECTOR_SIZE); |
|||
} |
|||
modelComponents.markovianStates.set(matrixBuilder.getCurrentRowGroup() - 1, markovian); |
|||
} |
|||
|
|||
template<typename ValueType, typename StateType> |
|||
void ExplicitDFTModelBuilderApprox<ValueType, StateType>::printNotExplored() const { |
|||
std::cout << "states not explored:" << std::endl; |
|||
for (auto it : statesNotExplored) { |
|||
std::cout << it.first << " -> " << dft.getStateString(it.second.first) << std::endl; |
|||
} |
|||
} |
|||
|
|||
|
|||
// Explicitly instantiate the class.
|
|||
template class ExplicitDFTModelBuilderApprox<double>; |
|||
|
|||
#ifdef STORM_HAVE_CARL
|
|||
template class ExplicitDFTModelBuilderApprox<storm::RationalFunction>; |
|||
#endif
|
|||
|
|||
} // namespace builder
|
|||
} // namespace storm
|
|||
|
|||
|
|||
@ -1,362 +0,0 @@ |
|||
#pragma once |
|||
|
|||
#include <boost/container/flat_set.hpp> |
|||
#include <boost/optional/optional.hpp> |
|||
#include <stack> |
|||
#include <unordered_set> |
|||
#include <limits> |
|||
|
|||
#include "storm/models/sparse/StateLabeling.h" |
|||
#include "storm/models/sparse/ChoiceLabeling.h" |
|||
#include "storm/models/sparse/StandardRewardModel.h" |
|||
#include "storm/models/sparse/Model.h" |
|||
#include "storm/storage/SparseMatrix.h" |
|||
#include "storm/storage/sparse/StateStorage.h" |
|||
|
|||
#include "storm-dft/builder/DftExplorationHeuristic.h" |
|||
#include "storm-dft/generator/DftNextStateGenerator.h" |
|||
#include "storm-dft/storage/dft/DFT.h" |
|||
#include "storm-dft/storage/dft/SymmetricUnits.h" |
|||
#include "storm-dft/storage/BucketPriorityQueue.h" |
|||
|
|||
namespace storm { |
|||
namespace builder { |
|||
|
|||
/*! |
|||
* Build a Markov chain from DFT. |
|||
*/ |
|||
template<typename ValueType, typename StateType = uint32_t> |
|||
class ExplicitDFTModelBuilderApprox { |
|||
|
|||
using DFTStatePointer = std::shared_ptr<storm::storage::DFTState<ValueType>>; |
|||
// TODO Matthias: make choosable |
|||
using ExplorationHeuristic = DFTExplorationHeuristicDepth<ValueType>; |
|||
using ExplorationHeuristicPointer = std::shared_ptr<ExplorationHeuristic>; |
|||
|
|||
|
|||
// A structure holding the individual components of a model. |
|||
struct ModelComponents { |
|||
// Constructor |
|||
ModelComponents(); |
|||
|
|||
// The transition matrix. |
|||
storm::storage::SparseMatrix<ValueType> transitionMatrix; |
|||
|
|||
// The state labeling. |
|||
storm::models::sparse::StateLabeling stateLabeling; |
|||
|
|||
// The Markovian states. |
|||
storm::storage::BitVector markovianStates; |
|||
|
|||
// The exit rates. |
|||
std::vector<ValueType> exitRates; |
|||
|
|||
// A vector that stores a labeling for each choice. |
|||
boost::optional<storm::models::sparse::ChoiceLabeling> choiceLabeling; |
|||
|
|||
// A flag indicating if the model is deterministic. |
|||
bool deterministicModel; |
|||
}; |
|||
|
|||
// A class holding the information for building the transition matrix. |
|||
class MatrixBuilder { |
|||
public: |
|||
// Constructor |
|||
MatrixBuilder(bool canHaveNondeterminism); |
|||
|
|||
/*! |
|||
* Set a mapping from a state id to the index in the matrix. |
|||
* |
|||
* @param id Id of the state. |
|||
*/ |
|||
void setRemapping(StateType id) { |
|||
STORM_LOG_ASSERT(id < stateRemapping.size(), "Invalid index for remapping."); |
|||
stateRemapping[id] = currentRowGroup; |
|||
} |
|||
|
|||
/*! |
|||
* Create a new row group if the model is nondeterministic. |
|||
*/ |
|||
void newRowGroup() { |
|||
if (canHaveNondeterminism) { |
|||
builder.newRowGroup(currentRow); |
|||
} |
|||
++currentRowGroup; |
|||
} |
|||
|
|||
/*! |
|||
* Add a transition from the current row. |
|||
* |
|||
* @param index Target index |
|||
* @param value Value of transition |
|||
*/ |
|||
void addTransition(StateType index, ValueType value) { |
|||
builder.addNextValue(currentRow, index, value); |
|||
} |
|||
|
|||
/*! |
|||
* Finish the current row. |
|||
*/ |
|||
void finishRow() { |
|||
++currentRow; |
|||
} |
|||
|
|||
/*! |
|||
* Remap the columns in the matrix. |
|||
*/ |
|||
void remap() { |
|||
builder.replaceColumns(stateRemapping, mappingOffset); |
|||
} |
|||
|
|||
/*! |
|||
* Get the current row group. |
|||
* |
|||
* @return The current row group. |
|||
*/ |
|||
StateType getCurrentRowGroup() { |
|||
return currentRowGroup; |
|||
} |
|||
|
|||
/*! |
|||
* Get the remapped state for the given id. |
|||
* |
|||
* @param id State. |
|||
* |
|||
* @return Remapped index. |
|||
*/ |
|||
StateType getRemapping(StateType id) { |
|||
STORM_LOG_ASSERT(id < stateRemapping.size(), "Invalid index for remapping."); |
|||
return stateRemapping[id]; |
|||
} |
|||
|
|||
// Matrix builder. |
|||
storm::storage::SparseMatrixBuilder<ValueType> builder; |
|||
|
|||
// Offset to distinguish states which will not be remapped anymore and those which will. |
|||
size_t mappingOffset; |
|||
|
|||
// A mapping from state ids to the row group indices in which they actually reside. |
|||
// TODO Matthias: avoid hack with fixed int type |
|||
std::vector<uint_fast64_t> stateRemapping; |
|||
|
|||
private: |
|||
|
|||
// Index of the current row group. |
|||
StateType currentRowGroup; |
|||
|
|||
// Index of the current row. |
|||
StateType currentRow; |
|||
|
|||
// Flag indicating if row groups are needed. |
|||
bool canHaveNondeterminism; |
|||
}; |
|||
|
|||
public: |
|||
// A structure holding the labeling options. |
|||
struct LabelOptions { |
|||
// Constructor |
|||
LabelOptions(std::vector<std::shared_ptr<storm::logic::Formula const>> properties, bool buildAllLabels = false); |
|||
|
|||
// Flag indicating if the general fail label should be included. |
|||
bool buildFailLabel; |
|||
|
|||
// Flag indicating if the general failsafe label should be included. |
|||
bool buildFailSafeLabel; |
|||
|
|||
// Flag indicating if all possible labels should be included. |
|||
bool buildAllLabels; |
|||
|
|||
// Set of element names whose fail label to include. |
|||
std::set<std::string> elementLabels; |
|||
}; |
|||
|
|||
/*! |
|||
* Constructor. |
|||
* |
|||
* @param dft DFT. |
|||
* @param symmetries Symmetries in the dft. |
|||
* @param enableDC Flag indicating if dont care propagation should be used. |
|||
*/ |
|||
ExplicitDFTModelBuilderApprox(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC); |
|||
|
|||
/*! |
|||
* Build model from DFT. |
|||
* |
|||
* @param labelOpts Options for labeling. |
|||
* @param iteration Current number of iteration. |
|||
* @param approximationThreshold Threshold determining when to skip exploring states. |
|||
*/ |
|||
void buildModel(LabelOptions const& labelOpts, size_t iteration, double approximationThreshold = 0.0); |
|||
|
|||
/*! |
|||
* Get the built model. |
|||
* |
|||
* @return The model built from the DFT. |
|||
*/ |
|||
std::shared_ptr<storm::models::sparse::Model<ValueType>> getModel(); |
|||
|
|||
/*! |
|||
* Get the built approximation model for either the lower or upper bound. |
|||
* |
|||
* @param lowerBound If true, the lower bound model is returned, else the upper bound model |
|||
* @param expectedTime If true, the bounds for expected time are computed, else the bounds for probabilities. |
|||
* |
|||
* @return The model built from the DFT. |
|||
*/ |
|||
std::shared_ptr<storm::models::sparse::Model<ValueType>> getModelApproximation(bool lowerBound, bool expectedTime); |
|||
|
|||
private: |
|||
|
|||
/*! |
|||
* Explore state space of DFT. |
|||
* |
|||
* @param approximationThreshold Threshold to determine when to skip states. |
|||
*/ |
|||
void exploreStateSpace(double approximationThreshold); |
|||
|
|||
/*! |
|||
* Initialize the matrix for a refinement iteration. |
|||
*/ |
|||
void initializeNextIteration(); |
|||
|
|||
/*! |
|||
* Build the labeling. |
|||
* |
|||
* @param labelOpts Options for labeling. |
|||
*/ |
|||
void buildLabeling(LabelOptions const& labelOpts); |
|||
|
|||
/*! |
|||
* 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 state. |
|||
*/ |
|||
StateType getOrAddStateIndex(DFTStatePointer const& state); |
|||
|
|||
/*! |
|||
* Set markovian flag for the current state. |
|||
* |
|||
* @param markovian Flag indicating if the state is markovian. |
|||
*/ |
|||
void setMarkovian(bool markovian); |
|||
|
|||
/** |
|||
* Change matrix to reflect the lower or upper approximation bound. |
|||
* |
|||
* @param matrix Matrix to change. The change are reflected here. |
|||
* @param lowerBound Flag indicating if the lower bound should be used. Otherwise the upper bound is used. |
|||
*/ |
|||
void changeMatrixBound(storm::storage::SparseMatrix<ValueType> & matrix, bool lowerBound) const; |
|||
|
|||
/*! |
|||
* Get lower bound approximation for state. |
|||
* |
|||
* @param state The state. |
|||
* |
|||
* @return Lower bound approximation. |
|||
*/ |
|||
ValueType getLowerBound(DFTStatePointer const& state) const; |
|||
|
|||
/*! |
|||
* Get upper bound approximation for state. |
|||
* |
|||
* @param state The state. |
|||
* |
|||
* @return Upper bound approximation. |
|||
*/ |
|||
ValueType getUpperBound(DFTStatePointer const& state) const; |
|||
|
|||
/*! |
|||
* Compute the MTTF of an AND gate via a closed formula. |
|||
* The used formula is 1/( 1/a + 1/b + 1/c + ... - 1/(a+b) - 1/(a+c) - ... + 1/(a+b+c) + ... - ...) |
|||
* |
|||
* @param rates List of rates of children of AND. |
|||
* @param size Only indices < size are considered in the vector. |
|||
* @return MTTF. |
|||
*/ |
|||
ValueType computeMTTFAnd(std::vector<ValueType> const& rates, size_t size) const; |
|||
|
|||
/*! |
|||
* Compares the priority of two states. |
|||
* |
|||
* @param idA Id of first state |
|||
* @param idB Id of second state |
|||
* |
|||
* @return True if the priority of the first state is greater then the priority of the second one. |
|||
*/ |
|||
bool isPriorityGreater(StateType idA, StateType idB) const; |
|||
|
|||
void printNotExplored() const; |
|||
|
|||
/*! |
|||
* Create the model model from the model components. |
|||
* |
|||
* @param copy If true, all elements of the model component are copied (used for approximation). If false |
|||
* they are moved to reduce the memory overhead. |
|||
* |
|||
* @return The model built from the model components. |
|||
*/ |
|||
std::shared_ptr<storm::models::sparse::Model<ValueType>> createModel(bool copy); |
|||
|
|||
// Initial size of the bitvector. |
|||
const size_t INITIAL_BITVECTOR_SIZE = 20000; |
|||
// Offset used for pseudo states. |
|||
const StateType OFFSET_PSEUDO_STATE = std::numeric_limits<StateType>::max() / 2; |
|||
|
|||
// Dft |
|||
storm::storage::DFT<ValueType> const& dft; |
|||
|
|||
// General information for state generation |
|||
// TODO Matthias: use const reference |
|||
std::shared_ptr<storm::storage::DFTStateGenerationInfo> stateGenerationInfo; |
|||
|
|||
// Flag indication if dont care propagation should be used. |
|||
bool enableDC = true; |
|||
|
|||
//TODO Matthias: make changeable |
|||
const bool mergeFailedStates = true; |
|||
|
|||
// Heuristic used for approximation |
|||
storm::builder::ApproximationHeuristic usedHeuristic; |
|||
|
|||
// Current id for new state |
|||
size_t newIndex = 0; |
|||
|
|||
// Id of failed state |
|||
size_t failedStateId = 0; |
|||
|
|||
// Id of initial state |
|||
size_t initialStateIndex = 0; |
|||
|
|||
// Next state generator for exploring the state space |
|||
storm::generator::DftNextStateGenerator<ValueType, StateType> generator; |
|||
|
|||
// Structure for the components of the model. |
|||
ModelComponents modelComponents; |
|||
|
|||
// Structure for the transition matrix builder. |
|||
MatrixBuilder matrixBuilder; |
|||
|
|||
// Internal information about the states that were explored. |
|||
storm::storage::sparse::StateStorage<StateType> stateStorage; |
|||
|
|||
// A priority queue of states that still need to be explored. |
|||
storm::storage::BucketPriorityQueue<ValueType> explorationQueue; |
|||
|
|||
// A mapping of not yet explored states from the id to the tuple (state object, heuristic values). |
|||
std::map<StateType, std::pair<DFTStatePointer, ExplorationHeuristicPointer>> statesNotExplored; |
|||
|
|||
// Holds all skipped states which were not yet expanded. More concretely it is a mapping from matrix indices |
|||
// to the corresponding skipped states. |
|||
// Notice that we need an ordered map here to easily iterate in increasing order over state ids. |
|||
// TODO remove again |
|||
std::map<StateType, std::pair<DFTStatePointer, ExplorationHeuristicPointer>> skippedStates; |
|||
|
|||
// List of independent subtrees and the BEs contained in them. |
|||
std::vector<std::vector<size_t>> subtreeBEs; |
|||
}; |
|||
|
|||
} |
|||
} |
|||
@ -0,0 +1,51 @@ |
|||
#include "storm-dft/settings/DftSettings.h"
|
|||
|
|||
#include "storm-dft/settings/modules/DftIOSettings.h"
|
|||
#include "storm-dft/settings/modules/FaultTreeSettings.h"
|
|||
|
|||
#include "storm/settings/SettingsManager.h"
|
|||
#include "storm/settings/modules/GeneralSettings.h"
|
|||
#include "storm/settings/modules/CoreSettings.h"
|
|||
#include "storm/settings/modules/IOSettings.h"
|
|||
#include "storm/settings/modules/DebugSettings.h"
|
|||
#include "storm/settings/modules/EigenEquationSolverSettings.h"
|
|||
#include "storm/settings/modules/GmmxxEquationSolverSettings.h"
|
|||
#include "storm/settings/modules/NativeEquationSolverSettings.h"
|
|||
#include "storm/settings/modules/EliminationSettings.h"
|
|||
#include "storm/settings/modules/MinMaxEquationSolverSettings.h"
|
|||
#include "storm/settings/modules/BisimulationSettings.h"
|
|||
#include "storm/settings/modules/ResourceSettings.h"
|
|||
#include "storm/settings/modules/JaniExportSettings.h"
|
|||
#include "storm/settings/modules/GSPNSettings.h"
|
|||
#include "storm/settings/modules/GSPNExportSettings.h"
|
|||
|
|||
|
|||
namespace storm { |
|||
namespace settings { |
|||
void initializeDftSettings(std::string const& name, std::string const& executableName) { |
|||
storm::settings::mutableManager().setName(name, executableName); |
|||
|
|||
// Register relevant settings modules.
|
|||
storm::settings::addModule<storm::settings::modules::GeneralSettings>(); |
|||
storm::settings::addModule<storm::settings::modules::DftIOSettings>(); |
|||
storm::settings::addModule<storm::settings::modules::FaultTreeSettings>(); |
|||
storm::settings::addModule<storm::settings::modules::IOSettings>(); |
|||
storm::settings::addModule<storm::settings::modules::CoreSettings>(); |
|||
|
|||
storm::settings::addModule<storm::settings::modules::DebugSettings>(); |
|||
storm::settings::addModule<storm::settings::modules::NativeEquationSolverSettings>(); |
|||
storm::settings::addModule<storm::settings::modules::GmmxxEquationSolverSettings>(); |
|||
storm::settings::addModule<storm::settings::modules::EigenEquationSolverSettings>(); |
|||
storm::settings::addModule<storm::settings::modules::EliminationSettings>(); |
|||
storm::settings::addModule<storm::settings::modules::MinMaxEquationSolverSettings>(); |
|||
// storm::settings::addModule<storm::settings::modules::BisimulationSettings>();
|
|||
storm::settings::addModule<storm::settings::modules::ResourceSettings>(); |
|||
|
|||
// For translation into JANI via GSPN.
|
|||
storm::settings::addModule<storm::settings::modules::JaniExportSettings>(); |
|||
storm::settings::addModule<storm::settings::modules::GSPNSettings>(); |
|||
storm::settings::addModule<storm::settings::modules::GSPNExportSettings>(); |
|||
} |
|||
|
|||
} |
|||
} |
|||
@ -0,0 +1,11 @@ |
|||
#pragma once |
|||
|
|||
#include <string> |
|||
|
|||
namespace storm { |
|||
namespace settings { |
|||
|
|||
void initializeDftSettings(std::string const& name, std::string const& executableName); |
|||
|
|||
} |
|||
} |
|||
@ -1,189 +0,0 @@ |
|||
#include "DFTSettings.h"
|
|||
|
|||
#include "storm/settings/SettingsManager.h"
|
|||
#include "storm/settings/SettingMemento.h"
|
|||
#include "storm/settings/Option.h"
|
|||
#include "storm/settings/OptionBuilder.h"
|
|||
#include "storm/settings/ArgumentBuilder.h"
|
|||
#include "storm/settings/Argument.h"
|
|||
|
|||
#include "storm/exceptions/InvalidSettingsException.h"
|
|||
#include "storm/exceptions/IllegalArgumentValueException.h"
|
|||
|
|||
namespace storm { |
|||
namespace settings { |
|||
namespace modules { |
|||
|
|||
const std::string DFTSettings::moduleName = "dft"; |
|||
const std::string DFTSettings::dftFileOptionName = "dftfile"; |
|||
const std::string DFTSettings::dftFileOptionShortName = "dft"; |
|||
const std::string DFTSettings::dftJsonFileOptionName = "dftfile-json"; |
|||
const std::string DFTSettings::dftJsonFileOptionShortName = "dftjson"; |
|||
const std::string DFTSettings::symmetryReductionOptionName = "symmetryreduction"; |
|||
const std::string DFTSettings::symmetryReductionOptionShortName = "symred"; |
|||
const std::string DFTSettings::modularisationOptionName = "modularisation"; |
|||
const std::string DFTSettings::disableDCOptionName = "disabledc"; |
|||
const std::string DFTSettings::approximationErrorOptionName = "approximation"; |
|||
const std::string DFTSettings::approximationErrorOptionShortName = "approx"; |
|||
const std::string DFTSettings::approximationHeuristicOptionName = "approximationheuristic"; |
|||
const std::string DFTSettings::propExpectedTimeOptionName = "expectedtime"; |
|||
const std::string DFTSettings::propExpectedTimeOptionShortName = "mttf"; |
|||
const std::string DFTSettings::propProbabilityOptionName = "probability"; |
|||
const std::string DFTSettings::propTimeboundOptionName = "timebound"; |
|||
const std::string DFTSettings::propTimepointsOptionName = "timepoints"; |
|||
const std::string DFTSettings::minValueOptionName = "min"; |
|||
const std::string DFTSettings::maxValueOptionName = "max"; |
|||
const std::string DFTSettings::firstDependencyOptionName = "firstdep"; |
|||
const std::string DFTSettings::transformToGspnOptionName = "gspn"; |
|||
const std::string DFTSettings::exportToJsonOptionName = "export-json"; |
|||
#ifdef STORM_HAVE_Z3
|
|||
const std::string DFTSettings::solveWithSmtOptionName = "smt"; |
|||
#endif
|
|||
|
|||
DFTSettings::DFTSettings() : ModuleSettings(moduleName) { |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, dftFileOptionName, false, "Parses the model given in the Galileo format.").setShortName(dftFileOptionShortName) |
|||
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the DFT model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, dftJsonFileOptionName, false, "Parses the model given in the Cytoscape JSON format.").setShortName(dftJsonFileOptionShortName) |
|||
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file from which to read the DFT model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, symmetryReductionOptionName, false, "Exploit symmetric structure of model.").setShortName(symmetryReductionOptionShortName).build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, modularisationOptionName, false, "Use modularisation (not applicable for expected time).").build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, disableDCOptionName, false, "Disable Dont Care propagation.").build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, firstDependencyOptionName, false, "Avoid non-determinism by always taking the first possible dependency.").build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, approximationErrorOptionName, false, "Approximation error allowed.").setShortName(approximationErrorOptionShortName).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("error", "The relative approximation error to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, approximationHeuristicOptionName, false, "Set the heuristic used for approximation.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("heuristic", "Sets which heuristic is used for approximation. Must be in {depth, probability}. Default is").setDefaultValueString("depth").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator({"depth", "rateratio"})).build()).build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, propExpectedTimeOptionName, false, "Compute expected time of system failure.").setShortName(propExpectedTimeOptionShortName).build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, propProbabilityOptionName, false, "Compute probability of system failure.").build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, propTimeboundOptionName, false, "Compute probability of system failure up to given timebound.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("time", "The timebound to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterValidator(0.0)).build()).build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, propTimepointsOptionName, false, "Compute probability of system failure up to given timebound for a set of given timepoints [starttime, starttime+inc, starttime+2inc, ... ,endtime]").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("starttime", "The timebound to start from.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("endtime", "The timebound to end with.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("inc", "The value to increment with to get the next timepoint.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, minValueOptionName, false, "Compute minimal value in case of non-determinism.").build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, maxValueOptionName, false, "Compute maximal value in case of non-determinism.").build()); |
|||
#ifdef STORM_HAVE_Z3
|
|||
this->addOption(storm::settings::OptionBuilder(moduleName, solveWithSmtOptionName, true, "Solve the DFT with SMT.").build()); |
|||
#endif
|
|||
this->addOption(storm::settings::OptionBuilder(moduleName, transformToGspnOptionName, false, "Transform DFT to GSPN.").build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, exportToJsonOptionName, false, "Export the model to the Cytoscape JSON format.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file to export to.").build()).build()); |
|||
} |
|||
|
|||
bool DFTSettings::isDftFileSet() const { |
|||
return this->getOption(dftFileOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
std::string DFTSettings::getDftFilename() const { |
|||
return this->getOption(dftFileOptionName).getArgumentByName("filename").getValueAsString(); |
|||
} |
|||
|
|||
bool DFTSettings::isDftJsonFileSet() const { |
|||
return this->getOption(dftJsonFileOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
std::string DFTSettings::getDftJsonFilename() const { |
|||
return this->getOption(dftJsonFileOptionName).getArgumentByName("filename").getValueAsString(); |
|||
} |
|||
|
|||
bool DFTSettings::useSymmetryReduction() const { |
|||
return this->getOption(symmetryReductionOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
bool DFTSettings::useModularisation() const { |
|||
return this->getOption(modularisationOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
bool DFTSettings::isDisableDC() const { |
|||
return this->getOption(disableDCOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
bool DFTSettings::isApproximationErrorSet() const { |
|||
return this->getOption(approximationErrorOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
double DFTSettings::getApproximationError() const { |
|||
return this->getOption(approximationErrorOptionName).getArgumentByName("error").getValueAsDouble(); |
|||
} |
|||
|
|||
storm::builder::ApproximationHeuristic DFTSettings::getApproximationHeuristic() const { |
|||
if (!isApproximationErrorSet() || getApproximationError() == 0.0) { |
|||
// No approximation is done
|
|||
return storm::builder::ApproximationHeuristic::NONE; |
|||
} |
|||
std::string heuristicAsString = this->getOption(approximationHeuristicOptionName).getArgumentByName("heuristic").getValueAsString(); |
|||
if (heuristicAsString == "depth") { |
|||
return storm::builder::ApproximationHeuristic::DEPTH; |
|||
} else if (heuristicAsString == "probability") { |
|||
return storm::builder::ApproximationHeuristic::PROBABILITY; |
|||
} |
|||
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal value '" << heuristicAsString << "' set as heuristic for approximation."); |
|||
} |
|||
|
|||
bool DFTSettings::usePropExpectedTime() const { |
|||
return this->getOption(propExpectedTimeOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
bool DFTSettings::usePropProbability() const { |
|||
return this->getOption(propProbabilityOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
bool DFTSettings::usePropTimebound() const { |
|||
return this->getOption(propTimeboundOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
double DFTSettings::getPropTimebound() const { |
|||
return this->getOption(propTimeboundOptionName).getArgumentByName("time").getValueAsDouble(); |
|||
} |
|||
|
|||
bool DFTSettings::usePropTimepoints() const { |
|||
return this->getOption(propTimepointsOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
std::vector<double> DFTSettings::getPropTimepoints() const { |
|||
double starttime = this->getOption(propTimepointsOptionName).getArgumentByName("starttime").getValueAsDouble(); |
|||
double endtime = this->getOption(propTimepointsOptionName).getArgumentByName("endtime").getValueAsDouble(); |
|||
double inc = this->getOption(propTimepointsOptionName).getArgumentByName("inc").getValueAsDouble(); |
|||
std::vector<double> timepoints; |
|||
for (double time = starttime; time <= endtime; time += inc) { |
|||
timepoints.push_back(time); |
|||
} |
|||
return timepoints; |
|||
} |
|||
|
|||
bool DFTSettings::isComputeMinimalValue() const { |
|||
return this->getOption(minValueOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
bool DFTSettings::isComputeMaximalValue() const { |
|||
return this->getOption(maxValueOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
bool DFTSettings::isTakeFirstDependency() const { |
|||
return this->getOption(firstDependencyOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
#ifdef STORM_HAVE_Z3
|
|||
bool DFTSettings::solveWithSMT() const { |
|||
return this->getOption(solveWithSmtOptionName).getHasOptionBeenSet(); |
|||
} |
|||
#endif
|
|||
|
|||
bool DFTSettings::isTransformToGspn() const { |
|||
return this->getOption(transformToGspnOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
bool DFTSettings::isExportToJson() const { |
|||
return this->getOption(exportToJsonOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
std::string DFTSettings::getExportJsonFilename() const { |
|||
return this->getOption(exportToJsonOptionName).getArgumentByName("filename").getValueAsString(); |
|||
} |
|||
|
|||
void DFTSettings::finalize() { |
|||
} |
|||
|
|||
bool DFTSettings::check() const { |
|||
// Ensure that at most one of min or max is set
|
|||
STORM_LOG_THROW(!isComputeMinimalValue() || !isComputeMaximalValue(), storm::exceptions::InvalidSettingsException, "Min and max can not both be set."); |
|||
return true; |
|||
} |
|||
|
|||
} // namespace modules
|
|||
} // namespace settings
|
|||
} // namespace storm
|
|||
@ -0,0 +1,123 @@ |
|||
#include "DftIOSettings.h"
|
|||
|
|||
#include "storm/settings/SettingsManager.h"
|
|||
#include "storm/settings/SettingMemento.h"
|
|||
#include "storm/settings/Option.h"
|
|||
#include "storm/settings/OptionBuilder.h"
|
|||
#include "storm/settings/ArgumentBuilder.h"
|
|||
#include "storm/settings/Argument.h"
|
|||
#include "storm/exceptions/InvalidSettingsException.h"
|
|||
|
|||
namespace storm { |
|||
namespace settings { |
|||
namespace modules { |
|||
|
|||
const std::string DftIOSettings::moduleName = "dftIO"; |
|||
const std::string DftIOSettings::dftFileOptionName = "dftfile"; |
|||
const std::string DftIOSettings::dftFileOptionShortName = "dft"; |
|||
const std::string DftIOSettings::dftJsonFileOptionName = "dftfile-json"; |
|||
const std::string DftIOSettings::dftJsonFileOptionShortName = "dftjson"; |
|||
const std::string DftIOSettings::propExpectedTimeOptionName = "expectedtime"; |
|||
const std::string DftIOSettings::propExpectedTimeOptionShortName = "mttf"; |
|||
const std::string DftIOSettings::propProbabilityOptionName = "probability"; |
|||
const std::string DftIOSettings::propTimeboundOptionName = "timebound"; |
|||
const std::string DftIOSettings::propTimepointsOptionName = "timepoints"; |
|||
const std::string DftIOSettings::minValueOptionName = "min"; |
|||
const std::string DftIOSettings::maxValueOptionName = "max"; |
|||
const std::string DftIOSettings::transformToGspnOptionName = "gspn"; |
|||
const std::string DftIOSettings::exportToJsonOptionName = "export-json"; |
|||
|
|||
DftIOSettings::DftIOSettings() : ModuleSettings(moduleName) { |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, dftFileOptionName, false, "Parses the model given in the Galileo format.").setShortName(dftFileOptionShortName) |
|||
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the DFT model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, dftJsonFileOptionName, false, "Parses the model given in the Cytoscape JSON format.").setShortName(dftJsonFileOptionShortName) |
|||
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file from which to read the DFT model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, propExpectedTimeOptionName, false, "Compute expected time of system failure.").setShortName(propExpectedTimeOptionShortName).build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, propProbabilityOptionName, false, "Compute probability of system failure.").build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, propTimeboundOptionName, false, "Compute probability of system failure up to given timebound.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("time", "The timebound to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterValidator(0.0)).build()).build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, propTimepointsOptionName, false, "Compute probability of system failure up to given timebound for a set of given timepoints [starttime, starttime+inc, starttime+2inc, ... ,endtime]").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("starttime", "The timebound to start from.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("endtime", "The timebound to end with.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("inc", "The value to increment with to get the next timepoint.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, minValueOptionName, false, "Compute minimal value in case of non-determinism.").build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, maxValueOptionName, false, "Compute maximal value in case of non-determinism.").build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, transformToGspnOptionName, false, "Transform DFT to GSPN.").build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, exportToJsonOptionName, false, "Export the model to the Cytoscape JSON format.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file to export to.").build()).build()); |
|||
} |
|||
|
|||
bool DftIOSettings::isDftFileSet() const { |
|||
return this->getOption(dftFileOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
std::string DftIOSettings::getDftFilename() const { |
|||
return this->getOption(dftFileOptionName).getArgumentByName("filename").getValueAsString(); |
|||
} |
|||
|
|||
bool DftIOSettings::isDftJsonFileSet() const { |
|||
return this->getOption(dftJsonFileOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
std::string DftIOSettings::getDftJsonFilename() const { |
|||
return this->getOption(dftJsonFileOptionName).getArgumentByName("filename").getValueAsString(); |
|||
} |
|||
|
|||
bool DftIOSettings::usePropExpectedTime() const { |
|||
return this->getOption(propExpectedTimeOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
bool DftIOSettings::usePropProbability() const { |
|||
return this->getOption(propProbabilityOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
bool DftIOSettings::usePropTimebound() const { |
|||
return this->getOption(propTimeboundOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
double DftIOSettings::getPropTimebound() const { |
|||
return this->getOption(propTimeboundOptionName).getArgumentByName("time").getValueAsDouble(); |
|||
} |
|||
|
|||
bool DftIOSettings::usePropTimepoints() const { |
|||
return this->getOption(propTimepointsOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
std::vector<double> DftIOSettings::getPropTimepoints() const { |
|||
double starttime = this->getOption(propTimepointsOptionName).getArgumentByName("starttime").getValueAsDouble(); |
|||
double endtime = this->getOption(propTimepointsOptionName).getArgumentByName("endtime").getValueAsDouble(); |
|||
double inc = this->getOption(propTimepointsOptionName).getArgumentByName("inc").getValueAsDouble(); |
|||
std::vector<double> timepoints; |
|||
for (double time = starttime; time <= endtime; time += inc) { |
|||
timepoints.push_back(time); |
|||
} |
|||
return timepoints; |
|||
} |
|||
|
|||
bool DftIOSettings::isComputeMinimalValue() const { |
|||
return this->getOption(minValueOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
bool DftIOSettings::isComputeMaximalValue() const { |
|||
return this->getOption(maxValueOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
bool DftIOSettings::isTransformToGspn() const { |
|||
return this->getOption(transformToGspnOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
bool DftIOSettings::isExportToJson() const { |
|||
return this->getOption(exportToJsonOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
std::string DftIOSettings::getExportJsonFilename() const { |
|||
return this->getOption(exportToJsonOptionName).getArgumentByName("filename").getValueAsString(); |
|||
} |
|||
|
|||
void DftIOSettings::finalize() { |
|||
} |
|||
|
|||
bool DftIOSettings::check() const { |
|||
// Ensure that at most one of min or max is set
|
|||
STORM_LOG_THROW(!isComputeMinimalValue() || !isComputeMaximalValue(), storm::exceptions::InvalidSettingsException, "Min and max can not both be set."); |
|||
return true; |
|||
} |
|||
|
|||
} // namespace modules
|
|||
} // namespace settings
|
|||
} // namespace storm
|
|||
@ -0,0 +1,93 @@ |
|||
#include "FaultTreeSettings.h"
|
|||
|
|||
#include "storm/settings/SettingsManager.h"
|
|||
#include "storm/settings/SettingMemento.h"
|
|||
#include "storm/settings/Option.h"
|
|||
#include "storm/settings/OptionBuilder.h"
|
|||
#include "storm/settings/ArgumentBuilder.h"
|
|||
#include "storm/settings/Argument.h"
|
|||
#include "storm/exceptions/IllegalArgumentValueException.h"
|
|||
|
|||
namespace storm { |
|||
namespace settings { |
|||
namespace modules { |
|||
|
|||
const std::string FaultTreeSettings::moduleName = "dft"; |
|||
const std::string FaultTreeSettings::symmetryReductionOptionName = "symmetryreduction"; |
|||
const std::string FaultTreeSettings::symmetryReductionOptionShortName = "symred"; |
|||
const std::string FaultTreeSettings::modularisationOptionName = "modularisation"; |
|||
const std::string FaultTreeSettings::disableDCOptionName = "disabledc"; |
|||
const std::string FaultTreeSettings::approximationErrorOptionName = "approximation"; |
|||
const std::string FaultTreeSettings::approximationErrorOptionShortName = "approx"; |
|||
const std::string FaultTreeSettings::approximationHeuristicOptionName = "approximationheuristic"; |
|||
const std::string FaultTreeSettings::firstDependencyOptionName = "firstdep"; |
|||
#ifdef STORM_HAVE_Z3
|
|||
const std::string FaultTreeSettings::solveWithSmtOptionName = "smt"; |
|||
#endif
|
|||
|
|||
FaultTreeSettings::FaultTreeSettings() : ModuleSettings(moduleName) { |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, symmetryReductionOptionName, false, "Exploit symmetric structure of model.").setShortName(symmetryReductionOptionShortName).build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, modularisationOptionName, false, "Use modularisation (not applicable for expected time).").build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, disableDCOptionName, false, "Disable Dont Care propagation.").build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, firstDependencyOptionName, false, "Avoid non-determinism by always taking the first possible dependency.").build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, approximationErrorOptionName, false, "Approximation error allowed.").setShortName(approximationErrorOptionShortName).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("error", "The relative approximation error to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, approximationHeuristicOptionName, false, "Set the heuristic used for approximation.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("heuristic", "Sets which heuristic is used for approximation. Must be in {depth, probability}. Default is").setDefaultValueString("depth").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator({"depth", "rateratio"})).build()).build()); |
|||
#ifdef STORM_HAVE_Z3
|
|||
this->addOption(storm::settings::OptionBuilder(moduleName, solveWithSmtOptionName, true, "Solve the DFT with SMT.").build()); |
|||
#endif
|
|||
} |
|||
|
|||
bool FaultTreeSettings::useSymmetryReduction() const { |
|||
return this->getOption(symmetryReductionOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
bool FaultTreeSettings::useModularisation() const { |
|||
return this->getOption(modularisationOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
bool FaultTreeSettings::isDisableDC() const { |
|||
return this->getOption(disableDCOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
bool FaultTreeSettings::isApproximationErrorSet() const { |
|||
return this->getOption(approximationErrorOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
double FaultTreeSettings::getApproximationError() const { |
|||
return this->getOption(approximationErrorOptionName).getArgumentByName("error").getValueAsDouble(); |
|||
} |
|||
|
|||
storm::builder::ApproximationHeuristic FaultTreeSettings::getApproximationHeuristic() const { |
|||
if (!isApproximationErrorSet() || getApproximationError() == 0.0) { |
|||
// No approximation is done
|
|||
return storm::builder::ApproximationHeuristic::NONE; |
|||
} |
|||
std::string heuristicAsString = this->getOption(approximationHeuristicOptionName).getArgumentByName("heuristic").getValueAsString(); |
|||
if (heuristicAsString == "depth") { |
|||
return storm::builder::ApproximationHeuristic::DEPTH; |
|||
} else if (heuristicAsString == "probability") { |
|||
return storm::builder::ApproximationHeuristic::PROBABILITY; |
|||
} |
|||
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal value '" << heuristicAsString << "' set as heuristic for approximation."); |
|||
} |
|||
|
|||
bool FaultTreeSettings::isTakeFirstDependency() const { |
|||
return this->getOption(firstDependencyOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
#ifdef STORM_HAVE_Z3
|
|||
bool FaultTreeSettings::solveWithSMT() const { |
|||
return this->getOption(solveWithSmtOptionName).getHasOptionBeenSet(); |
|||
} |
|||
#endif
|
|||
|
|||
void FaultTreeSettings::finalize() { |
|||
} |
|||
|
|||
bool FaultTreeSettings::check() const { |
|||
return true; |
|||
} |
|||
|
|||
} // namespace modules
|
|||
} // namespace settings
|
|||
} // namespace storm
|
|||
@ -0,0 +1,104 @@ |
|||
#pragma once |
|||
|
|||
#include "storm/settings/modules/ModuleSettings.h" |
|||
#include "storm-dft/builder/DftExplorationHeuristic.h" |
|||
#include "storm-config.h" |
|||
|
|||
namespace storm { |
|||
namespace settings { |
|||
namespace modules { |
|||
|
|||
/*! |
|||
* This class represents the settings for DFT model checking. |
|||
*/ |
|||
class FaultTreeSettings : public ModuleSettings { |
|||
public: |
|||
|
|||
/*! |
|||
* Creates a new set of DFT settings. |
|||
*/ |
|||
FaultTreeSettings(); |
|||
|
|||
/*! |
|||
* Retrieves whether the option to use symmetry reduction is set. |
|||
* |
|||
* @return True iff the option was set. |
|||
*/ |
|||
bool useSymmetryReduction() const; |
|||
|
|||
/*! |
|||
* Retrieves whether the option to use modularisation is set. |
|||
* |
|||
* @return True iff the option was set. |
|||
*/ |
|||
bool useModularisation() const; |
|||
|
|||
/*! |
|||
* Retrieves whether the option to disable Dont Care propagation is set. |
|||
* |
|||
* @return True iff the option was set. |
|||
*/ |
|||
bool isDisableDC() const; |
|||
|
|||
/*! |
|||
* Retrieves whether the option to compute an approximation is set. |
|||
* |
|||
* @return True iff the option was set. |
|||
*/ |
|||
bool isApproximationErrorSet() const; |
|||
|
|||
/*! |
|||
* Retrieves the relative error allowed for approximating the model checking result. |
|||
* |
|||
* @return The allowed errorbound. |
|||
*/ |
|||
double getApproximationError() const; |
|||
|
|||
/*! |
|||
* Retrieves the heuristic used for approximation. |
|||
* |
|||
* @return The heuristic to use. |
|||
*/ |
|||
storm::builder::ApproximationHeuristic getApproximationHeuristic() const; |
|||
|
|||
/*! |
|||
* Retrieves whether the non-determinism should be avoided by always taking the first possible dependency. |
|||
* |
|||
* @return True iff the option was set. |
|||
*/ |
|||
bool isTakeFirstDependency() const; |
|||
|
|||
#ifdef STORM_HAVE_Z3 |
|||
/*! |
|||
* Retrieves whether the DFT should be checked via SMT. |
|||
* |
|||
* @return True iff the option was set. |
|||
*/ |
|||
bool solveWithSMT() const; |
|||
#endif |
|||
|
|||
bool check() const override; |
|||
void finalize() override; |
|||
|
|||
// The name of the module. |
|||
static const std::string moduleName; |
|||
|
|||
private: |
|||
// Define the string names of the options as constants. |
|||
static const std::string symmetryReductionOptionName; |
|||
static const std::string symmetryReductionOptionShortName; |
|||
static const std::string modularisationOptionName; |
|||
static const std::string disableDCOptionName; |
|||
static const std::string approximationErrorOptionName; |
|||
static const std::string approximationErrorOptionShortName; |
|||
static const std::string approximationHeuristicOptionName; |
|||
static const std::string firstDependencyOptionName; |
|||
#ifdef STORM_HAVE_Z3 |
|||
static const std::string solveWithSmtOptionName; |
|||
#endif |
|||
|
|||
}; |
|||
|
|||
} // namespace modules |
|||
} // namespace settings |
|||
} // namespace storm |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue