diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp
index 1c036a33d..0db58195b 100644
--- a/src/storm-dft-cli/storm-dft.cpp
+++ b/src/storm-dft-cli/storm-dft.cpp
@@ -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);
}
}
diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h
index f801b0eda..754bdfc91 100644
--- a/src/storm-dft/api/storm-dft.h
+++ b/src/storm-dft/api/storm-dft.h
@@ -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);
diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
index da2100537..9fc882e27 100644
--- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
+++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
@@ -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;
diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.h b/src/storm-dft/builder/ExplicitDFTModelBuilder.h
index 5598ac6ef..46ac973b8 100644
--- a/src/storm-dft/builder/ExplicitDFTModelBuilder.h
+++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.h
@@ -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;
diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp
index eb1795448..4dd2e8402 100644
--- a/src/storm-dft/generator/DftNextStateGenerator.cpp
+++ b/src/storm-dft/generator/DftNextStateGenerator.cpp
@@ -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;
diff --git a/src/storm-dft/generator/DftNextStateGenerator.h b/src/storm-dft/generator/DftNextStateGenerator.h
index b77751521..9fab2ee1f 100644
--- a/src/storm-dft/generator/DftNextStateGenerator.h
+++ b/src/storm-dft/generator/DftNextStateGenerator.h
@@ -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;
diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
index 19a091a50..eed303311 100644
--- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
@@ -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();
diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.h b/src/storm-dft/modelchecker/dft/DFTModelChecker.h
index 34568d2f4..4b4cd4d3d 100644
--- a/src/storm-dft/modelchecker/dft/DFTModelChecker.h
+++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.h
@@ -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.
diff --git a/src/storm-dft/settings/modules/FaultTreeSettings.cpp b/src/storm-dft/settings/modules/FaultTreeSettings.cpp
index fd365a1ea..140b0f175 100644
--- a/src/storm-dft/settings/modules/FaultTreeSettings.cpp
+++ b/src/storm-dft/settings/modules/FaultTreeSettings.cpp
@@ -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() != "");
}
diff --git a/src/storm-dft/settings/modules/FaultTreeSettings.h b/src/storm-dft/settings/modules/FaultTreeSettings.h
index 1e88b48e4..16a726e04 100644
--- a/src/storm-dft/settings/modules/FaultTreeSettings.h
+++ b/src/storm-dft/settings/modules/FaultTreeSettings.h
@@ -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;
diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp
index 7538c4abc..21251f044 100644
--- a/src/storm-dft/storage/dft/DFT.cpp
+++ b/src/storm-dft/storage/dft/DFT.cpp
@@ -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);
}
}
}
diff --git a/src/storm-dft/storage/dft/DFT.h b/src/storm-dft/storage/dft/DFT.h
index 2b8795a82..27079a6ba 100644
--- a/src/storm-dft/storage/dft/DFT.h
+++ b/src/storm-dft/storage/dft/DFT.h
@@ -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;
diff --git a/src/storm-dft/storage/dft/elements/DFTElement.cpp b/src/storm-dft/storage/dft/elements/DFTElement.cpp
index d9bba261a..57c3b1ee0 100644
--- a/src/storm-dft/storage/dft/elements/DFTElement.cpp
+++ b/src/storm-dft/storage/dft/elements/DFTElement.cpp
@@ -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;
}
diff --git a/src/storm-dft/storage/dft/elements/DFTElement.h b/src/storm-dft/storage/dft/elements/DFTElement.h
index f89f69c7a..27784dae0 100644
--- a/src/storm-dft/storage/dft/elements/DFTElement.h
+++ b/src/storm-dft/storage/dft/elements/DFTElement.h
@@ -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
};
diff --git a/src/test/storm-dft/api/DftApproximationTest.cpp b/src/test/storm-dft/api/DftApproximationTest.cpp
index 7718d9218..e17fa200c 100644
--- a/src/test/storm-dft/api/DftApproximationTest.cpp
+++ b/src/test/storm-dft/api/DftApproximationTest.cpp
@@ -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]);
}
diff --git a/src/test/storm-dft/api/DftModelBuildingTest.cpp b/src/test/storm-dft/api/DftModelBuildingTest.cpp
index cbaa53e82..cd71be290 100644
--- a/src/test/storm-dft/api/DftModelBuildingTest.cpp
+++ b/src/test/storm-dft/api/DftModelBuildingTest.cpp
@@ -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());
diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp
index baf30dc02..f49639ba3 100644
--- a/src/test/storm-dft/api/DftModelCheckerTest.cpp
+++ b/src/test/storm-dft/api/DftModelCheckerTest.cpp
@@ -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]);
}