diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp
index f6a7d3863..eb4b1b837 100644
--- a/src/storm-dft-cli/storm-dft.cpp
+++ b/src/storm-dft-cli/storm-dft.cpp
@@ -126,7 +126,7 @@ void processOptions() {
if (faultTreeSettings.isApproximationErrorSet()) {
// Approximate analysis
storm::api::analyzeDFTApprox<ValueType>(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(),
- faultTreeSettings.getApproximationError(), true);
+ faultTreeSettings.getApproximationError(), faultTreeSettings.getApproximationHeuristic(), true);
} else {
storm::api::analyzeDFT<ValueType>(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), true);
}
diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h
index 8b4f0ae9c..e960fb69c 100644
--- a/src/storm-dft/api/storm-dft.h
+++ b/src/storm-dft/api/storm-dft.h
@@ -101,10 +101,9 @@ namespace storm {
template<typename ValueType>
typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results
analyzeDFTApprox(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred,
- bool allowModularisation, bool enableDC, double approximationError, bool printOutput) {
+ bool allowModularisation, bool enableDC, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic, bool printOutput) {
storm::modelchecker::DFTModelChecker<ValueType> modelChecker(printOutput);
- typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC,
- approximationError);
+ typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC, approximationError, approximationHeuristic);
if (printOutput) {
modelChecker.printTimings();
modelChecker.printResults();
diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
index 922f680e9..298936440 100644
--- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
+++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
@@ -56,7 +56,6 @@ namespace storm {
dft(dft),
stateGenerationInfo(std::make_shared<storm::storage::DFTStateGenerationInfo>(dft.buildStateGenerationInfo(symmetries))),
enableDC(enableDC),
- usedHeuristic(storm::settings::getModule<storm::settings::modules::FaultTreeSettings>().getApproximationHeuristic()),
generator(dft, *stateGenerationInfo, enableDC, mergeFailedStates),
matrixBuilder(!generator.isDeterministicModel()),
stateStorage(dft.stateBitVectorSize()),
@@ -120,8 +119,9 @@ namespace storm {
}
template<typename ValueType, typename StateType>
- void ExplicitDFTModelBuilder<ValueType, StateType>::buildModel(LabelOptions const& labelOpts, size_t iteration, double approximationThreshold) {
+ void ExplicitDFTModelBuilder<ValueType, StateType>::buildModel(LabelOptions const& labelOpts, size_t iteration, double approximationThreshold, storm::builder::ApproximationHeuristic approximationHeuristic) {
STORM_LOG_TRACE("Generating DFT state space");
+ usedHeuristic = approximationHeuristic;
if (iteration < 1) {
// Initialize
diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.h b/src/storm-dft/builder/ExplicitDFTModelBuilder.h
index 9858000ec..379918f9b 100644
--- a/src/storm-dft/builder/ExplicitDFTModelBuilder.h
+++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.h
@@ -181,11 +181,12 @@ namespace storm {
/*!
* Build model from DFT.
*
- * @param labelOpts Options for labeling.
- * @param iteration Current number of iteration.
+ * @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);
+ void buildModel(LabelOptions const& labelOpts, size_t iteration, double approximationThreshold = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH);
/*!
* Get the built model.
diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
index d96aacfc4..467125c35 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, bool enableDC, double approximationError) {
+ 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, bool enableDC, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic) {
// Initialize
this->approximationError = approximationError;
totalTimer.start();
@@ -30,21 +30,21 @@ namespace storm {
// Checking DFT
if (properties[0]->isTimeOperatorFormula() && allowModularisation) {
// Use parallel composition as modularisation approach for expected time
- std::shared_ptr<storm::models::sparse::Model<ValueType>> model = buildModelViaComposition(dft, properties, symred, true, enableDC, approximationError);
+ std::shared_ptr<storm::models::sparse::Model<ValueType>> model = buildModelViaComposition(dft, properties, symred, true, enableDC);
// Model checking
std::vector<ValueType> resultsValue = checkModel(model, properties);
for (ValueType result : resultsValue) {
checkResults.push_back(result);
}
} else {
- checkResults = checkHelper(dft, properties, symred, allowModularisation, enableDC, approximationError);
+ checkResults = checkHelper(dft, properties, symred, allowModularisation, enableDC, approximationError, approximationHeuristic);
}
totalTimer.stop();
return checkResults;
}
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, bool enableDC, double approximationError) {
+ typename DFTModelChecker<ValueType>::dft_results DFTModelChecker<ValueType>::checkHelper(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic) {
STORM_LOG_TRACE("Check helper called");
std::vector<storm::storage::DFT<ValueType>> dfts;
bool invResults = false;
@@ -138,12 +138,12 @@ namespace storm {
return results;
} else {
// No modularisation was possible
- return checkDFT(dft, properties, symred, enableDC, approximationError);
+ return checkDFT(dft, properties, symred, enableDC, 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, bool enableDC, double approximationError) {
+ 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, bool enableDC) {
// TODO Matthias: use approximation?
STORM_LOG_TRACE("Build model via composition");
std::vector<storm::storage::DFT<ValueType>> dfts;
@@ -258,7 +258,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, bool enableDC, double approximationError) {
+ typename DFTModelChecker<ValueType>::dft_results DFTModelChecker<ValueType>::checkDFT(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, bool enableDC, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic) {
explorationTimer.start();
// Find symmetries
@@ -297,7 +297,7 @@ namespace storm {
}
STORM_LOG_DEBUG("Building model...");
// TODO Matthias refine model using existing model and MC results
- builder.buildModel(labeloptions, iteration, approximationError);
+ builder.buildModel(labeloptions, iteration, approximationError, approximationHeuristic);
explorationTimer.stop();
buildingTimer.start();
diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.h b/src/storm-dft/modelchecker/dft/DFTModelChecker.h
index cf05cbb8f..56d1b4fad 100644
--- a/src/storm-dft/modelchecker/dft/DFTModelChecker.h
+++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.h
@@ -31,16 +31,17 @@ namespace storm {
/*!
* Main method for checking DFTs.
*
- * @param origDft Original DFT
- * @param properties Properties to check for
- * @param symred Flag indicating if symmetry reduction should be used
- * @param allowModularisation Flag indication if modularisation is allowed
- * @param enableDC Flag indicating if dont care propagation should be used
- * @param approximationError Error allowed for approximation. Value 0 indicates no approximation
+ * @param origDft Original DFT.
+ * @param properties Properties to check for.
+ * @param symred Flag indicating if symmetry reduction should be used.
+ * @param allowModularisation Flag indicating if modularisation is allowed.
+ * @param enableDC Flag indicating if Don't Care propagation should be used.
+ * @param approximationError Error allowed for approximation. Value 0 indicates no approximation.
+ * @param approximationHeuristic Heuristic used for approximation.
*
* @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, bool enableDC = true, double approximationError = 0.0);
+ dft_results check(storm::storage::DFT<ValueType> const& origDft, property_vector const& properties, bool symred = true, bool allowModularisation = true, bool enableDC = true, double approximationError = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH);
/*!
* Print timings of all operations to stream.
@@ -76,43 +77,44 @@ namespace storm {
/*!
* Internal helper for model checking a DFT.
*
- * @param dft DFT
- * @param properties Properties to check for
- * @param symred Flag indicating if symmetry reduction should be used
- * @param allowModularisation Flag indication if modularisation is allowed
- * @param enableDC Flag indicating if dont care propagation should be used
- * @param approximationError Error allowed for approximation. Value 0 indicates no approximation
+ * @param dft DFT.
+ * @param properties Properties to check for.
+ * @param symred Flag indicating if symmetry reduction should be used.
+ * @param allowModularisation Flag indicating if modularisation is allowed.
+ * @param enableDC Flag indicating if Don't Caree propagation should be used.
+ * @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, bool enableDC, double approximationError);
+ dft_results checkHelper(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH);
/*!
* Internal helper for building a CTMC from a DFT via parallel composition.
*
- * @param dft DFT
- * @param properties Properties to check for
- * @param symred Flag indicating if symmetry reduction should be used
- * @param allowModularisation Flag indication if modularisation is allowed
- * @param enableDC Flag indicating if dont care propagation should be used
- * @param approximationError Error allowed for approximation. Value 0 indicates no approximation
+ * @param dft DFT.
+ * @param properties Properties to check for.
+ * @param symred Flag indicating if symmetry reduction should be used.
+ * @param allowModularisation Flag indicating if modularisation is allowed.
+ * @param enableDC Flag indicating if Don't Care propagation should be used.
*
* @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, bool enableDC, double approximationError);
+ std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> buildModelViaComposition(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, bool allowModularisation, bool enableDC);
/*!
* Check model generated from DFT.
*
- * @param dft The DFT
- * @param properties Properties to check for
- * @param symred Flag indicating if symmetry reduction should be used
- * @param enableDC Flag indicating if dont care propagation should be used
- * @param approximationError Error allowed for approximation. Value 0 indicates no approximation
+ * @param dft The DFT.
+ * @param properties Properties to check for.
+ * @param symred Flag indicating if symmetry reduction should be used.
+ * @param enableDC Flag indicating if Don't Care propagation should be used.
+ * @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, bool enableDC, double approximationError = 0.0);
+ dft_results checkDFT(storm::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, bool enableDC, double approximationError = 0.0, storm::builder::ApproximationHeuristic approximationHeuristic = storm::builder::ApproximationHeuristic::DEPTH);
/*!
* Check the given markov model for the given properties.