Sebastian Junges
7 years ago
24 changed files with 1540 additions and 2016 deletions
-
1CHANGELOG.md
-
6resources/3rdparty/sylvan/src/lace.c
-
2src/storm-cli-utilities/cli.cpp
-
5src/storm-cli-utilities/cli.h
-
4src/storm-dft-cli/CMakeLists.txt
-
177src/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
-
2src/storm-pars-cli/CMakeLists.txt
-
3src/storm-pars-cli/storm-pars.cpp
-
12src/storm/models/sparse/MarkovAutomaton.cpp
-
4src/storm/models/sparse/MarkovAutomaton.h
-
2src/storm/parser/ExpressionParser.cpp
@ -1,9 +1,9 @@ |
|||||
# Create storm-dft. |
# Create storm-dft. |
||||
add_executable(storm-dft-cli ${PROJECT_SOURCE_DIR}/src/storm-dft-cli/storm-dyftee.cpp) |
|
||||
|
add_executable(storm-dft-cli ${PROJECT_SOURCE_DIR}/src/storm-dft-cli/storm-dft.cpp) |
||||
target_link_libraries(storm-dft-cli storm-dft storm-cli-utilities) # Adding headers for xcode |
target_link_libraries(storm-dft-cli storm-dft storm-cli-utilities) # Adding headers for xcode |
||||
set_target_properties(storm-dft-cli PROPERTIES OUTPUT_NAME "storm-dft") |
set_target_properties(storm-dft-cli PROPERTIES OUTPUT_NAME "storm-dft") |
||||
|
|
||||
add_dependencies(binaries storm-dft-cli) |
add_dependencies(binaries storm-dft-cli) |
||||
|
|
||||
# installation |
# installation |
||||
install(TARGETS storm-dft-cli RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) |
|
||||
|
install(TARGETS storm-dft-cli RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) |
||||
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