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

Set labels, dont care propagation and unique failed state according to relevant events

tempestpy_adaptions
Matthias Volk 6 years ago
parent
4b1af3c51e
commit
5952aa8a6f
17 changed files with 162 additions and 152 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 16
      src/storm-dft-cli/storm-dft.cpp
  2. 8
      src/storm-dft/api/storm-dft.h
  3. 109
      src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
  4. 36
      src/storm-dft/builder/ExplicitDFTModelBuilder.h
  5. 17
      src/storm-dft/generator/DftNextStateGenerator.cpp
  6. 9
      src/storm-dft/generator/DftNextStateGenerator.h
  7. 34
      src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
  8. 20
      src/storm-dft/modelchecker/dft/DFTModelChecker.h
  9. 10
      src/storm-dft/settings/modules/FaultTreeSettings.cpp
  10. 8
      src/storm-dft/settings/modules/FaultTreeSettings.h
  11. 4
      src/storm-dft/storage/dft/DFT.cpp
  12. 3
      src/storm-dft/storage/dft/DFT.h
  13. 3
      src/storm-dft/storage/dft/elements/DFTElement.cpp
  14. 11
      src/storm-dft/storage/dft/elements/DFTElement.h
  15. 6
      src/test/storm-dft/api/DftApproximationTest.cpp
  16. 18
      src/test/storm-dft/api/DftModelBuildingTest.cpp
  17. 2
      src/test/storm-dft/api/DftModelCheckerTest.cpp

16
src/storm-dft-cli/storm-dft.cpp
View File

@ -138,11 +138,15 @@ void processOptions() {
// Events from properties are relevant as well
for (auto atomic : atomicLabels) {
std::string label = atomic->getLabel();
std::size_t foundIndex = label.find("_fail");
if (foundIndex != std::string::npos) {
relevantEventNames.push_back(label.substr(0, foundIndex));
if (label == "failed") {
// Ignore as this label will always be added
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Label '" << label << "' not known.");
std::size_t foundIndex = label.find("_fail");
if (foundIndex != std::string::npos) {
relevantEventNames.push_back(label.substr(0, foundIndex));
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Label '" << label << "' not known.");
}
}
}
@ -178,8 +182,8 @@ void processOptions() {
if (faultTreeSettings.isApproximationErrorSet()) {
approximationError = faultTreeSettings.getApproximationError();
}
storm::api::analyzeDFT<ValueType>(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), relevantEvents, approximationError,
faultTreeSettings.getApproximationHeuristic(), true);
storm::api::analyzeDFT<ValueType>(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), relevantEvents,
faultTreeSettings.isAllowDCForRelevantEvents(), approximationError, faultTreeSettings.getApproximationHeuristic(), true);
}
}

8
src/storm-dft/api/storm-dft.h
View File

@ -70,6 +70,7 @@ namespace storm {
* @param symred Flag whether symmetry reduction should be used.
* @param allowModularisation Flag whether modularisation should be applied if possible.
* @param relevantEvents List of relevant events which should be observed.
* @param allowDCForRelevantEvents If true, Don't Care propagation is allowed even for relevant events.
* @param approximationError Allowed approximation error. Value 0 indicates no approximation.
* @param approximationHeuristic Heuristic used for state space exploration.
* @param printOutput If true, model information, timings, results, etc. are printed.
@ -78,11 +79,12 @@ namespace storm {
template<typename ValueType>
typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results
analyzeDFT(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred = true,
bool allowModularisation = true, std::set<size_t> const& relevantEvents = {}, double approximationError = 0.0,
storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH, bool printOutput = false) {
bool allowModularisation = true, std::set<size_t> const& relevantEvents = {}, bool allowDCForRelevantEvents = true, double approximationError = 0.0,
storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH, bool printOutput = false) {
storm::modelchecker::DFTModelChecker<ValueType> modelChecker(printOutput);
typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, relevantEvents,
approximationError, approximationHeuristic);
allowDCForRelevantEvents, approximationError,
approximationHeuristic);
if (printOutput) {
modelChecker.printTimings();
modelChecker.printResults(results);

109
src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
View File

@ -31,43 +31,24 @@ namespace storm {
}
template<typename ValueType, typename StateType>
ExplicitDFTModelBuilder<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>
ExplicitDFTModelBuilder<ValueType, StateType>::ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, std::set<size_t> const& relevantEvents) :
ExplicitDFTModelBuilder<ValueType, StateType>::ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, std::set<size_t> const& relevantEvents, bool allowDCForRelevantEvents) :
dft(dft),
stateGenerationInfo(std::make_shared<storm::storage::DFTStateGenerationInfo>(dft.buildStateGenerationInfo(symmetries))),
relevantEvents(relevantEvents),
generator(dft, *stateGenerationInfo, mergeFailedStates),
generator(dft, *stateGenerationInfo),
matrixBuilder(!generator.isDeterministicModel()),
stateStorage(dft.stateBitVectorSize()),
explorationQueue(1, 0, 0.9, false)
{
// Set relevant events
this->dft.setRelevantEvents(this->relevantEvents);
this->dft.setRelevantEvents(this->relevantEvents, allowDCForRelevantEvents);
// Mark top level element as relevant
this->dft.getElement(this->dft.getTopLevelIndex())->setRelevance(true);
if (this->relevantEvents.empty()) {
// Only interested in top level event -> introduce unique failed state
this->uniqueFailedState = true;
STORM_LOG_DEBUG("Using unique failed state with id 0.");
}
// Compute independent subtrees
if (dft.topLevelType() == storm::storage::DFTElementType::OR) {
@ -126,10 +107,17 @@ namespace storm {
}
template<typename ValueType, typename StateType>
void ExplicitDFTModelBuilder<ValueType, StateType>::buildModel(LabelOptions const& labelOpts, size_t iteration, double approximationThreshold, storm::builder::ApproximationHeuristic approximationHeuristic) {
void ExplicitDFTModelBuilder<ValueType, StateType>::buildModel(size_t iteration, double approximationThreshold, storm::builder::ApproximationHeuristic approximationHeuristic) {
STORM_LOG_TRACE("Generating DFT state space");
usedHeuristic = approximationHeuristic;
if (approximationThreshold > 0 && !this->uniqueFailedState) {
// Approximation requires unique failed states
// TODO lift this restriction
STORM_LOG_WARN("Approximation requires unique failed state. Forcing use of unique failed state.");
this->uniqueFailedState = true;
}
if (iteration < 1) {
// Initialize
switch (usedHeuristic) {
@ -147,15 +135,16 @@ namespace storm {
}
modelComponents.markovianStates = storm::storage::BitVector(INITIAL_BITVECTOR_SIZE);
if(mergeFailedStates) {
if (this->uniqueFailedState) {
// Introduce explicit fail state
storm::generator::StateBehavior<ValueType, StateType> behavior = generator.createMergeFailedState([this] (DFTStatePointer const& state) {
this->failedStateId = newIndex++;
size_t failedStateId = newIndex++;
STORM_LOG_ASSERT(failedStateId == 0, "Unique failed id is not 0.");
matrixBuilder.stateRemapping.push_back(0);
return this->failedStateId;
return failedStateId;
} );
matrixBuilder.setRemapping(failedStateId);
matrixBuilder.setRemapping(0);
STORM_LOG_ASSERT(!behavior.empty(), "Behavior is empty.");
matrixBuilder.newRowGroup();
setMarkovian(behavior.begin()->isMarkovian());
@ -165,7 +154,7 @@ namespace storm {
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(stateProbabilityPair.first == 0, "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();
@ -214,7 +203,7 @@ namespace storm {
}
exploreStateSpace(approximationThreshold);
size_t stateSize = stateStorage.getNumberOfStates() + (mergeFailedStates ? 1 : 0);
size_t stateSize = stateStorage.getNumberOfStates() + (this->uniqueFailedState ? 1 : 0);
modelComponents.markovianStates.resize(stateSize);
modelComponents.deterministicModel = generator.isDeterministicModel();
@ -237,7 +226,7 @@ namespace storm {
STORM_LOG_TRACE("Transition matrix: too big to print");
}
buildLabeling(labelOpts);
buildLabeling();
}
template<typename ValueType, typename StateType>
@ -386,7 +375,8 @@ namespace storm {
setMarkovian(true);
// Add transition to target state with temporary value 0
// TODO: what to do when there is no unique target state?
matrixBuilder.addTransition(failedStateId, storm::utility::zero<ValueType>());
STORM_LOG_ASSERT(this->uniqueFailedState, "Approximation only works with unique failed state");
matrixBuilder.addTransition(0, storm::utility::zero<ValueType>());
// Remember skipped state
skippedStates[matrixBuilder.getCurrentRowGroup() - 1] = std::make_pair(currentState, currentExplorationHeuristic);
matrixBuilder.finishRow();
@ -471,47 +461,54 @@ namespace storm {
}
template<typename ValueType, typename StateType>
void ExplicitDFTModelBuilder<ValueType, StateType>::buildLabeling(LabelOptions const& labelOpts) {
void ExplicitDFTModelBuilder<ValueType, StateType>::buildLabeling() {
// 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");
}
// Label all states corresponding to their status (failed, failed/dont care BE)
modelComponents.stateLabeling.addLabel("failed");
// 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) {
if (element->isRelevant()) {
modelComponents.stateLabeling.addLabel(element->name() + "_fail");
modelComponents.stateLabeling.addLabel(element->name() + "_dc");
}
}
// Set labels to states
if (mergeFailedStates) {
modelComponents.stateLabeling.addLabelToState("failed", failedStateId);
if (this->uniqueFailedState) {
modelComponents.stateLabeling.addLabelToState("failed", 0);
}
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)) {
if (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
// Set fail/dont care 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);
if (element->isRelevant()){
storm::storage::DFTElementState elementState = storm::storage::DFTState<ValueType>::getElementState(state, *stateGenerationInfo, element->id());
switch (elementState) {
case storm::storage::DFTElementState::Failed:
modelComponents.stateLabeling.addLabelToState(element->name() + "_fail", stateId);
break;
case storm::storage::DFTElementState::DontCare:
modelComponents.stateLabeling.addLabelToState(element->name() + "_dc", stateId);
break;
case storm::storage::DFTElementState::Operational:
case storm::storage::DFTElementState::Failsafe:
// do nothing
break;
default:
STORM_LOG_ASSERT(false, "Unknown element state " << elementState);
}
}
}
}
@ -540,7 +537,7 @@ namespace storm {
// 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(matrixEntry->getColumn() == 0, "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);
@ -658,7 +655,7 @@ namespace storm {
// 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(matrixEntry->getColumn() == 0, "Transition has wrong target state.");
STORM_LOG_ASSERT(!it->second.first->isPseudoState(), "State is still pseudo state.");
ExplorationHeuristicPointer heuristic = it->second.second;

36
src/storm-dft/builder/ExplicitDFTModelBuilder.h
View File

@ -151,42 +151,24 @@ namespace storm {
};
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 relevantEvents List with ids of relevant events which should be observed.
* @param allowDCForRelevantEvents If true, Don't Care propagation is allowed even for relevant events.
*/
ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, std::set<size_t> const& relevantEvents);
ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, std::set<size_t> const& relevantEvents, bool allowDCForRelevantEvents);
/*!
* Build model from DFT.
*
* @param labelOpts Options for labeling.
* @param iteration Current number of iteration.
* @param approximationThreshold Threshold determining when to skip exploring states.
* @param approximationHeuristic Heuristic used for exploring states.
*/
void buildModel(LabelOptions const& labelOpts, size_t iteration, double approximationThreshold = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH);
void buildModel(size_t iteration, double approximationThreshold = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH);
/*!
* Get the built model.
@ -221,10 +203,8 @@ namespace storm {
/*!
* Build the labeling.
*
* @param labelOpts Options for labeling.
*/
void buildLabeling(LabelOptions const& labelOpts);
void buildLabeling();
/*!
* Add a state to the explored states (if not already there). It also handles pseudo states.
@ -315,17 +295,15 @@ namespace storm {
// List with ids of relevant events which should be observed.
std::set<size_t> const& relevantEvents;
//TODO: merge depending on relevant events
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;
// Whether to use a unique state for all failed states
// If used, the unique failed state has the id 0
bool uniqueFailedState = false;
// Id of initial state
size_t initialStateIndex = 0;

17
src/storm-dft/generator/DftNextStateGenerator.cpp
View File

@ -10,7 +10,7 @@ namespace storm {
namespace generator {
template<typename ValueType, typename StateType>
DftNextStateGenerator<ValueType, StateType>::DftNextStateGenerator(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo, bool mergeFailedStates) : mDft(dft), mStateGenerationInfo(stateGenerationInfo), state(nullptr), mergeFailedStates(mergeFailedStates) {
DftNextStateGenerator<ValueType, StateType>::DftNextStateGenerator(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo) : mDft(dft), mStateGenerationInfo(stateGenerationInfo), state(nullptr), uniqueFailedState(false) {
deterministicModel = !mDft.canHaveNondeterminism();
}
@ -135,9 +135,9 @@ namespace storm {
// Get the id of the successor state
StateType newStateId;
if (newState->hasFailed(mDft.getTopLevelIndex()) && mergeFailedStates) {
if (newState->hasFailed(mDft.getTopLevelIndex()) && uniqueFailedState) {
// Use unique failed state
newStateId = mergeFailedStateId;
newStateId = 0;
} else {
// Propagate failsafe
while (!queues.failsafePropagationDone()) {
@ -226,15 +226,16 @@ namespace storm {
template<typename ValueType, typename StateType>
StateBehavior<ValueType, StateType> DftNextStateGenerator<ValueType, StateType>::createMergeFailedState(StateToIdCallback const& stateToIdCallback) {
STORM_LOG_ASSERT(mergeFailedStates, "No unique failed state used.");
// Introduce explicit fail state
this->uniqueFailedState = true;
// Introduce explicit fail state with id 0
DFTStatePointer failedState = std::make_shared<storm::storage::DFTState<ValueType>>(mDft, mStateGenerationInfo, 0);
mergeFailedStateId = stateToIdCallback(failedState);
STORM_LOG_TRACE("Introduce fail state with id: " << mergeFailedStateId);
size_t failedStateId = stateToIdCallback(failedState);
STORM_LOG_ASSERT(failedStateId == 0, "Unique failed state has not id 0.");
STORM_LOG_TRACE("Introduce fail state with id 0.");
// Add self loop
Choice<ValueType, StateType> choice(0, true);
choice.addProbability(mergeFailedStateId, storm::utility::one<ValueType>());
choice.addProbability(0, storm::utility::one<ValueType>());
// No further exploration required
StateBehavior<ValueType, StateType> result;

9
src/storm-dft/generator/DftNextStateGenerator.h
View File

@ -24,7 +24,7 @@ namespace storm {
public:
typedef std::function<StateType (DFTStatePointer const&)> StateToIdCallback;
DftNextStateGenerator(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo, bool mergeFailedStates);
DftNextStateGenerator(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo);
bool isDeterministicModel() const;
std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback);
@ -55,11 +55,8 @@ namespace storm {
// Current state
DFTStatePointer state;
// Flag indication if all failed states should be merged into one.
bool mergeFailedStates = true;
// Id of the merged failed state
StateType mergeFailedStateId = 0;
// Flag indication if all failed states should be merged into one unique failed state.
bool uniqueFailedState;
// Flag indicating if the model is deterministic.
bool deterministicModel = false;

34
src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
View File

@ -17,7 +17,7 @@ namespace storm {
namespace modelchecker {
template<typename ValueType>
typename DFTModelChecker<ValueType>::dft_results DFTModelChecker<ValueType>::check(storm::storage::DFT<ValueType> const& origDft, std::vector<std::shared_ptr<const storm::logic::Formula>> const& properties, bool symred, bool allowModularisation, std::set<size_t> const& relevantEvents, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic) {
typename DFTModelChecker<ValueType>::dft_results DFTModelChecker<ValueType>::check(storm::storage::DFT<ValueType> const& origDft, std::vector<std::shared_ptr<const storm::logic::Formula>> const& properties, bool symred, bool allowModularisation, std::set<size_t> const& relevantEvents, bool allowDCForRelevantEvents, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic) {
totalTimer.start();
dft_results results;
@ -37,14 +37,14 @@ namespace storm {
results.push_back(result);
}
} else {
results = checkHelper(dft, properties, symred, allowModularisation, relevantEvents, approximationError, approximationHeuristic);
results = checkHelper(dft, properties, symred, allowModularisation, relevantEvents, allowDCForRelevantEvents, approximationError, approximationHeuristic);
}
totalTimer.stop();
return results;
}
template<typename ValueType>
typename DFTModelChecker<ValueType>::dft_results DFTModelChecker<ValueType>::checkHelper(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, bool allowModularisation, std::set<size_t> const& relevantEvents, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic) {
typename DFTModelChecker<ValueType>::dft_results DFTModelChecker<ValueType>::checkHelper(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, bool allowModularisation, std::set<size_t> const& relevantEvents, bool allowDCForRelevantEvents, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic) {
STORM_LOG_TRACE("Check helper called");
std::vector<storm::storage::DFT<ValueType>> dfts;
bool invResults = false;
@ -99,7 +99,7 @@ namespace storm {
std::vector<ValueType> res;
for(auto const ft : dfts) {
// TODO: allow approximation in modularisation
dft_results ftResults = checkHelper(ft, {property}, symred, true, relevantEvents, 0.0);
dft_results ftResults = checkHelper(ft, {property}, symred, true, relevantEvents, allowDCForRelevantEvents, 0.0);
STORM_LOG_ASSERT(ftResults.size() == 1, "Wrong number of results");
res.push_back(boost::get<ValueType>(ftResults[0]));
}
@ -138,12 +138,12 @@ namespace storm {
return results;
} else {
// No modularisation was possible
return checkDFT(dft, properties, symred, relevantEvents, approximationError, approximationHeuristic);
return checkDFT(dft, properties, symred, relevantEvents, allowDCForRelevantEvents, approximationError, approximationHeuristic);
}
}
template<typename ValueType>
std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> DFTModelChecker<ValueType>::buildModelViaComposition(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, bool allowModularisation, std::set<size_t> const& relevantEvents) {
std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> DFTModelChecker<ValueType>::buildModelViaComposition(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, bool allowModularisation, std::set<size_t> const& relevantEvents, bool allowDCForRelevantEvents) {
// TODO: use approximation?
STORM_LOG_TRACE("Build model via composition");
std::vector<storm::storage::DFT<ValueType>> dfts;
@ -194,9 +194,8 @@ namespace storm {
// Build a single CTMC
STORM_LOG_DEBUG("Building Model...");
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(ft, symmetries, relevantEvents);
typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties);
builder.buildModel(labeloptions, 0, 0.0);
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(ft, symmetries, relevantEvents, allowDCForRelevantEvents);
builder.buildModel(0, 0.0);
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
explorationTimer.stop();
@ -246,9 +245,8 @@ namespace storm {
// Build a single CTMC
STORM_LOG_DEBUG("Building Model...");
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, relevantEvents);
typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties);
builder.buildModel(labeloptions, 0, 0.0);
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, relevantEvents, allowDCForRelevantEvents);
builder.buildModel(0, 0.0);
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
//model->printModelInformationToStream(std::cout);
explorationTimer.stop();
@ -258,7 +256,7 @@ namespace storm {
}
template<typename ValueType>
typename DFTModelChecker<ValueType>::dft_results DFTModelChecker<ValueType>::checkDFT(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, std::set<size_t> const& relevantEvents, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic) {
typename DFTModelChecker<ValueType>::dft_results DFTModelChecker<ValueType>::checkDFT(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, std::set<size_t> const& relevantEvents, bool allowDCForRelevantEvents, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic) {
explorationTimer.start();
// Find symmetries
@ -278,8 +276,7 @@ namespace storm {
approximation_result approxResult = std::make_pair(storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>());
std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
std::vector<ValueType> newResult;
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, relevantEvents);
typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties);
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, relevantEvents, allowDCForRelevantEvents);
// TODO: compute approximation for all properties simultaneously?
std::shared_ptr<const storm::logic::Formula> property = properties[0];
@ -297,7 +294,7 @@ namespace storm {
}
STORM_LOG_DEBUG("Building model...");
// TODO refine model using existing model and MC results
builder.buildModel(labeloptions, iteration, approximationError, approximationHeuristic);
builder.buildModel(iteration, approximationError, approximationHeuristic);
explorationTimer.stop();
buildingTimer.start();
@ -344,9 +341,8 @@ namespace storm {
// Build a single Markov Automaton
auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
STORM_LOG_DEBUG("Building Model...");
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, relevantEvents);
typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties, ioSettings.isExportExplicitSet() || ioSettings.isExportDotSet());
builder.buildModel(labeloptions, 0, 0.0);
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, relevantEvents, allowDCForRelevantEvents);
builder.buildModel(0, 0.0);
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
explorationTimer.stop();

20
src/storm-dft/modelchecker/dft/DFTModelChecker.h
View File

@ -52,11 +52,14 @@ namespace storm {
* @param symred Flag whether symmetry reduction should be used.
* @param allowModularisation Flag indicating if modularisation is allowed.
* @param relevantEvents List with ids of relevant events which should be observed.
* @param allowDCForRelevantEvents If true, Don't Care propagation is allowed even for relevant events.
* @param approximationError Error allowed for approximation. Value 0 indicates no approximation.
* @param approximationHeuristic Heuristic used for state space exploration.
* @return Model checking results for the given properties..
*/
dft_results check(storm::storage::DFT<ValueType> const& origDft, property_vector const& properties, bool symred = true, bool allowModularisation = true, std::set<size_t> const& relevantEvents = {}, double approximationError = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH);
dft_results check(storm::storage::DFT<ValueType> const& origDft, property_vector const& properties, bool symred = true, bool allowModularisation = true,
std::set<size_t> const& relevantEvents = {}, bool allowDCForRelevantEvents = true, double approximationError = 0.0,
storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH);
/*!
* Print timings of all operations to stream.
@ -92,11 +95,14 @@ namespace storm {
* @param symred Flag indicating if symmetry reduction should be used.
* @param allowModularisation Flag indicating if modularisation is allowed.
* @param relevantEvents List with ids of relevant events which should be observed.
* @param allowDCForRelevantEvents If true, Don't Care propagation is allowed even for relevant events.
* @param approximationError Error allowed for approximation. Value 0 indicates no approximation.
* @param approximationHeuristic Heuristic used for approximation.
* @return Model checking results (or in case of approximation two results for lower and upper bound)
*/
dft_results checkHelper(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, bool allowModularisation, std::set<size_t> const& relevantEvents, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH);
dft_results checkHelper(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, bool allowModularisation,
std::set<size_t> const& relevantEvents, bool allowDCForRelevantEvents = true, double approximationError = 0.0,
storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH);
/*!
* Internal helper for building a CTMC from a DFT via parallel composition.
@ -106,9 +112,12 @@ namespace storm {
* @param symred Flag indicating if symmetry reduction should be used.
* @param allowModularisation Flag indicating if modularisation is allowed.
* @param relevantEvents List with ids of relevant events which should be observed.
* @param allowDCForRelevantEvents If true, Don't Care propagation is allowed even for relevant events.
* @return CTMC representing the DFT
*/
std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> buildModelViaComposition(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, bool allowModularisation, std::set<size_t> const& relevantEvents);
std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> buildModelViaComposition(storm::storage::DFT<ValueType> const& dft, property_vector const& properties,
bool symred, bool allowModularisation, std::set<size_t> const& relevantEvents,
bool allowDCForRelevantEvents = true);
/*!
* Check model generated from DFT.
@ -117,12 +126,15 @@ namespace storm {
* @param properties Properties to check for.
* @param symred Flag indicating if symmetry reduction should be used.
* @param relevantEvents List with ids of relevant events which should be observed.
* @param allowDCForRelevantEvents If true, Don't Care propagation is allowed even for relevant events.
* @param approximationError Error allowed for approximation. Value 0 indicates no approximation.
* @param approximationHeuristic Heuristic used for approximation.
*
* @return Model checking result
*/
dft_results checkDFT(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, std::set<size_t> const& relevantEvents = {}, double approximationError = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH);
dft_results checkDFT(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, std::set<size_t> const& relevantEvents = {},
bool allowDCForRelevantEvents = true, double approximationError = 0.0,
storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH);
/*!
* Check the given markov model for the given properties.

10
src/storm-dft/settings/modules/FaultTreeSettings.cpp
View File

@ -19,6 +19,7 @@ namespace storm {
const std::string FaultTreeSettings::symmetryReductionOptionShortName = "symred";
const std::string FaultTreeSettings::modularisationOptionName = "modularisation";
const std::string FaultTreeSettings::disableDCOptionName = "disabledc";
const std::string FaultTreeSettings::allowDCRelevantOptionName = "allowdcrelevant";
const std::string FaultTreeSettings::relevantEventsOptionName = "relevantevents";
const std::string FaultTreeSettings::approximationErrorOptionName = "approximation";
const std::string FaultTreeSettings::approximationErrorOptionShortName = "approx";
@ -31,10 +32,11 @@ namespace storm {
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, disableDCOptionName, false, "Disable Don't 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, relevantEventsOptionName, false, "Specifies the relevant events from the DFT.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of relevant events. 'all' marks all events as relevant, The default '' or 'none' mark only the top level event as relevant.").setDefaultValueString("").build()).build());
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of names of relevant events. 'all' marks all events as relevant, The default '' or 'none' marks only the top level event as relevant.").setDefaultValueString("").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, allowDCRelevantOptionName, false, "Allow Don't Care propagation for relevant events.").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", "The name of the heuristic used for approximation.")
@ -57,6 +59,10 @@ namespace storm {
return this->getOption(disableDCOptionName).getHasOptionBeenSet();
}
bool FaultTreeSettings::isAllowDCForRelevantEvents() const {
return this->getOption(allowDCRelevantOptionName).getHasOptionBeenSet();
}
bool FaultTreeSettings::areRelevantEventsSet() const {
return this->getOption(relevantEventsOptionName).getHasOptionBeenSet() && (this->getOption(relevantEventsOptionName).getArgumentByName("values").getValueAsString() != "");
}

8
src/storm-dft/settings/modules/FaultTreeSettings.h
View File

@ -40,6 +40,13 @@ namespace storm {
*/
bool isDisableDC() const;
/*!
* Retrieves whether the option to allow Dont Care propagation for relevant events is set.
*
* @return True iff the option was set.
*/
bool isAllowDCForRelevantEvents() const;
/*!
* Retrieves whether the option to give relevant events is set.
*
@ -106,6 +113,7 @@ namespace storm {
static const std::string symmetryReductionOptionShortName;
static const std::string modularisationOptionName;
static const std::string disableDCOptionName;
static const std::string allowDCRelevantOptionName;
static const std::string relevantEventsOptionName;
static const std::string approximationErrorOptionName;
static const std::string approximationErrorOptionShortName;

4
src/storm-dft/storage/dft/DFT.cpp
View File

@ -862,12 +862,14 @@ namespace storm {
}
template<typename ValueType>
void DFT<ValueType>::setRelevantEvents(std::set<size_t> const& relevantEvents) const {
void DFT<ValueType>::setRelevantEvents(std::set<size_t> const& relevantEvents, bool allowDCForRelevantEvents) const {
for (auto const& elem : mElements) {
if (relevantEvents.find(elem->id()) != relevantEvents.end()) {
elem->setRelevance(true);
elem->setAllowDC(allowDCForRelevantEvents);
} else {
elem->setRelevance(false);
elem->setAllowDC(true);
}
}
}

3
src/storm-dft/storage/dft/DFT.h
View File

@ -321,8 +321,9 @@ namespace storm {
/*!
* Set the relevance flag for all elements according to the given relevant events.
* @param relevantEvents All elements which should be to relevant. All elements not occuring are set to irrelevant.
* @param allowDCForRelevantEvents Flag whether Don't Care propagation is allowed even for relevant events.
*/
void setRelevantEvents(std::set<size_t> const& relevantEvents) const;
void setRelevantEvents(std::set<size_t> const& relevantEvents, bool allowDCForRelevantEvents) const;
private:
std::tuple<std::vector<size_t>, std::vector<size_t>, std::vector<size_t>> getSortedParentAndDependencyIds(size_t index) const;

3
src/storm-dft/storage/dft/elements/DFTElement.cpp
View File

@ -9,8 +9,7 @@ namespace storm {
template<typename ValueType>
bool DFTElement<ValueType>::checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
if (this->isRelevant()) {
// Relevant events are ignored for Don't Care propagation
if (!this->mAllowDC) {
return false;
}

11
src/storm-dft/storage/dft/elements/DFTElement.h
View File

@ -51,7 +51,7 @@ namespace storm {
* @param id Id.
* @param name Name.
*/
DFTElement(size_t id, std::string const& name) : mId(id), mName(name), mRank(-1), mRelevant(false) {
DFTElement(size_t id, std::string const& name) : mId(id), mName(name), mRank(-1), mRelevant(false), mAllowDC(true) {
// Intentionally left empty.
}
@ -134,6 +134,14 @@ namespace storm {
this->mRelevant = relevant;
}
/*!
* Set whether Don't Care propagation is allowed for this element.
* @param allowDC If true, the element is allowed to be set to Don't Care.
*/
virtual void setAllowDC(bool allowDC) const {
this->mAllowDC = allowDC;
}
/*!
* Checks whether the element is a basic element.
* @return True iff element is a BE.
@ -438,6 +446,7 @@ namespace storm {
DFTDependencyVector mOutgoingDependencies;
DFTRestrictionVector mRestrictions;
mutable bool mRelevant; // Must be mutable to allow changes later on. TODO: avoid mutable
mutable bool mAllowDC; // Must be mutable to allow changes later on. TODO: avoid mutable
};

6
src/test/storm-dft/api/DftApproximationTest.cpp
View File

@ -57,7 +57,7 @@ namespace {
EXPECT_TRUE(storm::api::isWellFormed(*dft));
std::string property = "T=? [F \"failed\"]";
std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(*dft, properties, config.useSR, false, {}, errorBound,
typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(*dft, properties, config.useSR, false, {}, true, errorBound,
config.heuristic, false);
return boost::get<storm::modelchecker::DFTModelChecker<double>::approximation_result>(results[0]);
}
@ -67,8 +67,8 @@ namespace {
EXPECT_TRUE(storm::api::isWellFormed(*dft));
std::stringstream propertyStream;
propertyStream << "P=? [F<=" << timeBound << " \"failed\"]";
std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(propertyStream.str()));
typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(*dft, properties, config.useSR, false, {}, errorBound,
std::vector <std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(propertyStream.str()));
typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(*dft, properties, config.useSR, false, {}, true, errorBound,
config.heuristic, false);
return boost::get<storm::modelchecker::DFTModelChecker<double>::approximation_result>(results[0]);
}

18
src/test/storm-dft/api/DftModelBuildingTest.cpp
View File

@ -16,14 +16,12 @@ namespace {
std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
std::map<size_t, std::vector<std::vector<size_t>>> emptySymmetry;
storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry);
typename storm::builder::ExplicitDFTModelBuilder<double>::LabelOptions labeloptions(properties, false);
// Set relevant events (none)
std::set<size_t> relevantEvents;
// Build model
storm::builder::ExplicitDFTModelBuilder<double> builder(*dft, symmetries, relevantEvents);
builder.buildModel(labeloptions, 0, 0.0);
storm::builder::ExplicitDFTModelBuilder<double> builder(*dft, symmetries, relevantEvents, false);
builder.buildModel(0, 0.0);
std::shared_ptr<storm::models::sparse::Model<double>> model = builder.getModel();
EXPECT_EQ(8ul, model->getNumberOfStates());
EXPECT_EQ(13ul, model->getNumberOfTransitions());
@ -31,8 +29,8 @@ namespace {
// Set relevant events (all)
relevantEvents = dft->getAllIds();
// Build model
storm::builder::ExplicitDFTModelBuilder<double> builder2(*dft, symmetries, relevantEvents);
builder2.buildModel(labeloptions, 0, 0.0);
storm::builder::ExplicitDFTModelBuilder<double> builder2(*dft, symmetries, relevantEvents, false);
builder2.buildModel(0, 0.0);
model = builder2.getModel();
EXPECT_EQ(170ul, model->getNumberOfStates());
EXPECT_EQ(688ul, model->getNumberOfTransitions());
@ -42,8 +40,8 @@ namespace {
relevantEvents.clear();
relevantEvents.insert(dft->getIndex("H"));
// Build model
storm::builder::ExplicitDFTModelBuilder<double> builder3(*dft, symmetries, relevantEvents);
builder3.buildModel(labeloptions, 0, 0.0);
storm::builder::ExplicitDFTModelBuilder<double> builder3(*dft, symmetries, relevantEvents, false);
builder3.buildModel(0, 0.0);
model = builder3.getModel();
EXPECT_EQ(11ul, model->getNumberOfStates());
EXPECT_EQ(23ul, model->getNumberOfTransitions());
@ -54,8 +52,8 @@ namespace {
relevantEvents.insert(dft->getIndex("H"));
relevantEvents.insert(dft->getIndex("I"));
// Build model
storm::builder::ExplicitDFTModelBuilder<double> builder4(*dft, symmetries, relevantEvents);
builder4.buildModel(labeloptions, 0, 0.0);
storm::builder::ExplicitDFTModelBuilder<double> builder4(*dft, symmetries, relevantEvents, false);
builder4.buildModel(0, 0.0);
model = builder4.getModel();
EXPECT_EQ(14ul, model->getNumberOfStates());
EXPECT_EQ(30ul, model->getNumberOfTransitions());

2
src/test/storm-dft/api/DftModelCheckerTest.cpp
View File

@ -81,7 +81,7 @@ namespace {
relevantEvents = dft->getAllIds();
}
typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(*dft, properties, config.useSR, config.useMod,
relevantEvents);
relevantEvents, true);
return boost::get<double>(results[0]);
}

Write Preview
Loading…
Cancel
Save