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

Heuristic is argument for functions in approximation algorithm

main
Matthias Volk 7 years ago
parent
7b4a51effe
commit
a410b6d7bc
6 changed files with 46 additions and 44 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      src/storm-dft-cli/storm-dft.cpp
  2. 5
      src/storm-dft/api/storm-dft.h
  3. 4
      src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
  4. 3
      src/storm-dft/builder/ExplicitDFTModelBuilder.h
  5. 16
      src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
  6. 56
      src/storm-dft/modelchecker/dft/DFTModelChecker.h

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

@ -126,7 +126,7 @@ void processOptions() {
if (faultTreeSettings.isApproximationErrorSet()) { if (faultTreeSettings.isApproximationErrorSet()) {
// Approximate analysis // Approximate analysis
storm::api::analyzeDFTApprox<ValueType>(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), storm::api::analyzeDFTApprox<ValueType>(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(),
faultTreeSettings.getApproximationError(), true);
faultTreeSettings.getApproximationError(), faultTreeSettings.getApproximationHeuristic(), true);
} else { } else {
storm::api::analyzeDFT<ValueType>(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), true); storm::api::analyzeDFT<ValueType>(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), true);
} }

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

@ -101,10 +101,9 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results 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, 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); 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) { if (printOutput) {
modelChecker.printTimings(); modelChecker.printTimings();
modelChecker.printResults(); modelChecker.printResults();

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

@ -56,7 +56,6 @@ namespace storm {
dft(dft), dft(dft),
stateGenerationInfo(std::make_shared<storm::storage::DFTStateGenerationInfo>(dft.buildStateGenerationInfo(symmetries))), stateGenerationInfo(std::make_shared<storm::storage::DFTStateGenerationInfo>(dft.buildStateGenerationInfo(symmetries))),
enableDC(enableDC), enableDC(enableDC),
usedHeuristic(storm::settings::getModule<storm::settings::modules::FaultTreeSettings>().getApproximationHeuristic()),
generator(dft, *stateGenerationInfo, enableDC, mergeFailedStates), generator(dft, *stateGenerationInfo, enableDC, mergeFailedStates),
matrixBuilder(!generator.isDeterministicModel()), matrixBuilder(!generator.isDeterministicModel()),
stateStorage(dft.stateBitVectorSize()), stateStorage(dft.stateBitVectorSize()),
@ -120,8 +119,9 @@ namespace storm {
} }
template<typename ValueType, typename StateType> 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"); STORM_LOG_TRACE("Generating DFT state space");
usedHeuristic = approximationHeuristic;
if (iteration < 1) { if (iteration < 1) {
// Initialize // Initialize

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

@ -184,8 +184,9 @@ namespace storm {
* @param labelOpts Options for labeling. * @param labelOpts Options for labeling.
* @param iteration Current number of iteration. * @param iteration Current number of iteration.
* @param approximationThreshold Threshold determining when to skip exploring states. * @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. * Get the built model.

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

@ -17,7 +17,7 @@ namespace storm {
namespace modelchecker { namespace modelchecker {
template<typename ValueType> 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 // Initialize
this->approximationError = approximationError; this->approximationError = approximationError;
totalTimer.start(); totalTimer.start();
@ -30,21 +30,21 @@ namespace storm {
// Checking DFT // Checking DFT
if (properties[0]->isTimeOperatorFormula() && allowModularisation) { if (properties[0]->isTimeOperatorFormula() && allowModularisation) {
// Use parallel composition as modularisation approach for expected time // 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 // Model checking
std::vector<ValueType> resultsValue = checkModel(model, properties); std::vector<ValueType> resultsValue = checkModel(model, properties);
for (ValueType result : resultsValue) { for (ValueType result : resultsValue) {
checkResults.push_back(result); checkResults.push_back(result);
} }
} else { } else {
checkResults = checkHelper(dft, properties, symred, allowModularisation, enableDC, approximationError);
checkResults = checkHelper(dft, properties, symred, allowModularisation, enableDC, approximationError, approximationHeuristic);
} }
totalTimer.stop(); totalTimer.stop();
return checkResults; return checkResults;
} }
template<typename ValueType> 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"); STORM_LOG_TRACE("Check helper called");
std::vector<storm::storage::DFT<ValueType>> dfts; std::vector<storm::storage::DFT<ValueType>> dfts;
bool invResults = false; bool invResults = false;
@ -138,12 +138,12 @@ namespace storm {
return results; return results;
} else { } else {
// No modularisation was possible // No modularisation was possible
return checkDFT(dft, properties, symred, enableDC, approximationError);
return checkDFT(dft, properties, symred, enableDC, approximationError, approximationHeuristic);
} }
} }
template<typename ValueType> 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? // TODO Matthias: use approximation?
STORM_LOG_TRACE("Build model via composition"); STORM_LOG_TRACE("Build model via composition");
std::vector<storm::storage::DFT<ValueType>> dfts; std::vector<storm::storage::DFT<ValueType>> dfts;
@ -258,7 +258,7 @@ namespace storm {
} }
template<typename ValueType> 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(); explorationTimer.start();
// Find symmetries // Find symmetries
@ -297,7 +297,7 @@ namespace storm {
} }
STORM_LOG_DEBUG("Building model..."); STORM_LOG_DEBUG("Building model...");
// TODO Matthias refine model using existing model and MC results // TODO Matthias refine model using existing model and MC results
builder.buildModel(labeloptions, iteration, approximationError);
builder.buildModel(labeloptions, iteration, approximationError, approximationHeuristic);
explorationTimer.stop(); explorationTimer.stop();
buildingTimer.start(); buildingTimer.start();

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

@ -31,16 +31,17 @@ namespace storm {
/*! /*!
* Main method for checking DFTs. * 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. * @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. * Print timings of all operations to stream.
@ -76,43 +77,44 @@ namespace storm {
/*! /*!
* Internal helper for model checking a DFT. * 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) * @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. * 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 * @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. * 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 * @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. * Check the given markov model for the given properties.

Write Preview
Loading…
Cancel
Save