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

renamed elimination settings 

Former-commit-id: 5155d0a465
tempestpy_adaptions
dehnert 9 years ago
parent
8ce9e56af8
commit
35bb3a3c26
7 changed files with 60 additions and 60 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. 24
      src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
  2. 4
      src/settings/SettingsManager.cpp
  3. 22
      src/settings/modules/EliminationSettings.cpp
  4. 14
      src/settings/modules/EliminationSettings.h
  5. 4
      src/storm-dyftee.cpp
  6. 40
      src/utility/stateelimination.cpp
  7. 12
      src/utility/stateelimination.h

24
src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
View File

@ -6,7 +6,7 @@
#include "src/adapters/CarlAdapter.h"
#include "src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h"
#include "src/settings/modules/EliminationSettings.h"
#include "src/settings/modules/MarkovChainSettings.h"
#include "src/settings/SettingsManager.h"
@ -193,7 +193,7 @@ namespace storm {
std::chrono::high_resolution_clock::time_point modelCheckingStart = std::chrono::high_resolution_clock::now();
storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder order = storm::settings::getModule<storm::settings::modules::SparseDtmcEliminationModelCheckerSettings>().getEliminationOrder();
storm::settings::modules::EliminationSettings::EliminationOrder order = storm::settings::getModule<storm::settings::modules::EliminationSettings>().getEliminationOrder();
boost::optional<std::vector<uint_fast64_t>> distanceBasedPriorities;
if (eliminationOrderNeedsDistances(order)) {
distanceBasedPriorities = getDistanceBasedPriorities(transitionMatrix, backwardTransitions, initialStates, stateValues,
@ -607,7 +607,7 @@ namespace storm {
storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true);
// Do some sanity checks to establish some required properties.
// STORM_LOG_WARN_COND(storm::settings::getModule<storm::settings::modules::SparseDtmcEliminationModelCheckerSettings>().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::State, "The chosen elimination method is not available for computing conditional probabilities. Falling back to regular state elimination.");
// STORM_LOG_WARN_COND(storm::settings::getModule<storm::settings::modules::EliminationSettings>().getEliminationMethod() == storm::settings::modules::EliminationSettings::EliminationMethod::State, "The chosen elimination method is not available for computing conditional probabilities. Falling back to regular state elimination.");
STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state.");
STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::IllegalArgumentException, "Cannot compute conditional probabilities for all states.");
storm::storage::sparse::state_type initialState = *this->getModel().getInitialStates().begin();
@ -668,7 +668,7 @@ namespace storm {
// Before starting the model checking process, we assign priorities to states so we can use them to
// impose ordering constraints later.
boost::optional<std::vector<uint_fast64_t>> distanceBasedPriorities;
storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder order = storm::settings::getModule<storm::settings::modules::SparseDtmcEliminationModelCheckerSettings>().getEliminationOrder();
storm::settings::modules::EliminationSettings::EliminationOrder order = storm::settings::getModule<storm::settings::modules::EliminationSettings>().getEliminationOrder();
if (eliminationOrderNeedsDistances(order)) {
distanceBasedPriorities = getDistanceBasedPriorities(submatrix, submatrixTransposed, newInitialStates, oneStepProbabilities,
eliminationOrderNeedsForwardDistances(order),
@ -836,10 +836,10 @@ namespace storm {
// When using the hybrid technique, we recursively treat the SCCs up to some size.
std::vector<storm::storage::sparse::state_type> entryStateQueue;
STORM_LOG_DEBUG("Eliminating " << subsystem.size() << " states using the hybrid elimination technique." << std::endl);
uint_fast64_t maximalDepth = treatScc(transitionMatrix, values, initialStates, subsystem, initialStates, forwardTransitions, backwardTransitions, false, 0, storm::settings::getModule<storm::settings::modules::SparseDtmcEliminationModelCheckerSettings>().getMaximalSccSize(), entryStateQueue, computeResultsForInitialStatesOnly, distanceBasedPriorities);
uint_fast64_t maximalDepth = treatScc(transitionMatrix, values, initialStates, subsystem, initialStates, forwardTransitions, backwardTransitions, false, 0, storm::settings::getModule<storm::settings::modules::EliminationSettings>().getMaximalSccSize(), entryStateQueue, computeResultsForInitialStatesOnly, distanceBasedPriorities);
// If the entry states were to be eliminated last, we need to do so now.
if (storm::settings::getModule<storm::settings::modules::SparseDtmcEliminationModelCheckerSettings>().isEliminateEntryStatesLastSet()) {
if (storm::settings::getModule<storm::settings::modules::EliminationSettings>().isEliminateEntryStatesLastSet()) {
STORM_LOG_DEBUG("Eliminating " << entryStateQueue.size() << " entry states as a last step.");
std::vector<storm::storage::sparse::state_type> sortedStates(entryStateQueue.begin(), entryStateQueue.end());
std::shared_ptr<StatePriorityQueue> queuePriorities = std::make_shared<StaticStatePriorityQueue>(sortedStates);
@ -855,7 +855,7 @@ namespace storm {
storm::storage::FlexibleSparseMatrix<ValueType> flexibleMatrix(transitionMatrix);
storm::storage::FlexibleSparseMatrix<ValueType> flexibleBackwardTransitions(backwardTransitions);
storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder order = storm::settings::getModule<storm::settings::modules::SparseDtmcEliminationModelCheckerSettings>().getEliminationOrder();
storm::settings::modules::EliminationSettings::EliminationOrder order = storm::settings::getModule<storm::settings::modules::EliminationSettings>().getEliminationOrder();
boost::optional<std::vector<uint_fast64_t>> distanceBasedPriorities;
if (eliminationOrderNeedsDistances(order)) {
distanceBasedPriorities = getDistanceBasedPriorities(transitionMatrix, backwardTransitions, initialStates, oneStepProbabilitiesToTarget,
@ -866,9 +866,9 @@ namespace storm {
storm::storage::BitVector subsystem = storm::storage::BitVector(transitionMatrix.getRowCount(), true);
uint_fast64_t maximalDepth = 0;
if (storm::settings::getModule<storm::settings::modules::SparseDtmcEliminationModelCheckerSettings>().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::State) {
if (storm::settings::getModule<storm::settings::modules::EliminationSettings>().getEliminationMethod() == storm::settings::modules::EliminationSettings::EliminationMethod::State) {
performOrdinaryStateElimination(flexibleMatrix, flexibleBackwardTransitions, subsystem, initialStates, computeResultsForInitialStatesOnly, values, distanceBasedPriorities);
} else if (storm::settings::getModule<storm::settings::modules::SparseDtmcEliminationModelCheckerSettings>().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::Hybrid) {
} else if (storm::settings::getModule<storm::settings::modules::EliminationSettings>().getEliminationMethod() == storm::settings::modules::EliminationSettings::EliminationMethod::Hybrid) {
maximalDepth = performHybridStateElimination(transitionMatrix, flexibleMatrix, flexibleBackwardTransitions, subsystem, initialStates, computeResultsForInitialStatesOnly, values, distanceBasedPriorities);
}
@ -934,7 +934,7 @@ namespace storm {
}
// Recursively descend in SCC-hierarchy.
uint_fast64_t depth = treatScc(matrix, values, entryStates, newSccAsBitVector, initialStates, forwardTransitions, backwardTransitions, eliminateEntryStates || !storm::settings::getModule<storm::settings::modules::SparseDtmcEliminationModelCheckerSettings>().isEliminateEntryStatesLastSet(), level + 1, maximalSccSize, entryStateQueue, computeResultsForInitialStatesOnly, distanceBasedPriorities);
uint_fast64_t depth = treatScc(matrix, values, entryStates, newSccAsBitVector, initialStates, forwardTransitions, backwardTransitions, eliminateEntryStates || !storm::settings::getModule<storm::settings::modules::EliminationSettings>().isEliminateEntryStatesLastSet(), level + 1, maximalSccSize, entryStateQueue, computeResultsForInitialStatesOnly, distanceBasedPriorities);
maximalDepth = std::max(maximalDepth, depth);
}
} else {
@ -970,8 +970,8 @@ namespace storm {
}
std::vector<std::size_t> distances = getStateDistances(transitionMatrix, transitionMatrixTransposed, initialStates, oneStepProbabilities,
storm::settings::getModule<storm::settings::modules::SparseDtmcEliminationModelCheckerSettings>().getEliminationOrder() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Forward ||
storm::settings::getModule<storm::settings::modules::SparseDtmcEliminationModelCheckerSettings>().getEliminationOrder() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::ForwardReversed);
storm::settings::getModule<storm::settings::modules::EliminationSettings>().getEliminationOrder() == storm::settings::modules::EliminationSettings::EliminationOrder::Forward ||
storm::settings::getModule<storm::settings::modules::EliminationSettings>().getEliminationOrder() == storm::settings::modules::EliminationSettings::EliminationOrder::ForwardReversed);
// In case of the forward or backward ordering, we can sort the states according to the distances.
if (forward ^ reverse) {

4
src/settings/SettingsManager.cpp
View File

@ -27,7 +27,7 @@
#include "src/settings/modules/GlpkSettings.h"
#include "src/settings/modules/GurobiSettings.h"
#include "src/settings/modules/ParametricSettings.h"
#include "src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h"
#include "src/settings/modules/EliminationSettings.h"
#include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h"
#include "src/settings/modules/ExplorationSettings.h"
#include "src/utility/macros.h"
@ -516,7 +516,7 @@ namespace storm {
storm::settings::addModule<storm::settings::modules::GurobiSettings>();
storm::settings::addModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>();
storm::settings::addModule<storm::settings::modules::ParametricSettings>();
storm::settings::addModule<storm::settings::modules::SparseDtmcEliminationModelCheckerSettings>();
storm::settings::addModule<storm::settings::modules::EliminationSettings>();
storm::settings::addModule<storm::settings::modules::ExplorationSettings>();
}

22
src/settings/modules/SparseDtmcEliminationModelCheckerSettings.cpp → src/settings/modules/EliminationSettings.cpp
View File

@ -1,4 +1,4 @@
#include "src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h"
#include "src/settings/modules/EliminationSettings.h"
#include "src/settings/Option.h"
#include "src/settings/OptionBuilder.h"
@ -10,13 +10,13 @@ namespace storm {
namespace settings {
namespace modules {
const std::string SparseDtmcEliminationModelCheckerSettings::moduleName = "sparseelim";
const std::string SparseDtmcEliminationModelCheckerSettings::eliminationMethodOptionName = "method";
const std::string SparseDtmcEliminationModelCheckerSettings::eliminationOrderOptionName = "order";
const std::string SparseDtmcEliminationModelCheckerSettings::entryStatesLastOptionName = "entrylast";
const std::string SparseDtmcEliminationModelCheckerSettings::maximalSccSizeOptionName = "sccsize";
const std::string EliminationSettings::moduleName = "sparseelim";
const std::string EliminationSettings::eliminationMethodOptionName = "method";
const std::string EliminationSettings::eliminationOrderOptionName = "order";
const std::string EliminationSettings::entryStatesLastOptionName = "entrylast";
const std::string EliminationSettings::maximalSccSizeOptionName = "sccsize";
SparseDtmcEliminationModelCheckerSettings::SparseDtmcEliminationModelCheckerSettings() : ModuleSettings(moduleName) {
EliminationSettings::EliminationSettings() : ModuleSettings(moduleName) {
std::vector<std::string> orders = {"fw", "fwrev", "bw", "bwrev", "rand", "spen", "dpen", "regex"};
this->addOption(storm::settings::OptionBuilder(moduleName, eliminationOrderOptionName, true, "The order that is to be used for the elimination techniques. Available are {fw, fwrev, bw, bwrev, rand, spen, dpen}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the order in which states are chosen for elimination.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(orders)).setDefaultValueString("fwrev").build()).build());
@ -28,7 +28,7 @@ namespace storm {
.addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("maxsize", "The maximal size of an SCC on which state elimination is applied.").setDefaultValueUnsignedInteger(20).setIsOptional(true).build()).build());
}
SparseDtmcEliminationModelCheckerSettings::EliminationMethod SparseDtmcEliminationModelCheckerSettings::getEliminationMethod() const {
EliminationSettings::EliminationMethod EliminationSettings::getEliminationMethod() const {
std::string eliminationMethodAsString = this->getOption(eliminationMethodOptionName).getArgumentByName("name").getValueAsString();
if (eliminationMethodAsString == "state") {
return EliminationMethod::State;
@ -39,7 +39,7 @@ namespace storm {
}
}
SparseDtmcEliminationModelCheckerSettings::EliminationOrder SparseDtmcEliminationModelCheckerSettings::getEliminationOrder() const {
EliminationSettings::EliminationOrder EliminationSettings::getEliminationOrder() const {
std::string eliminationOrderAsString = this->getOption(eliminationOrderOptionName).getArgumentByName("name").getValueAsString();
if (eliminationOrderAsString == "fw") {
return EliminationOrder::Forward;
@ -62,11 +62,11 @@ namespace storm {
}
}
bool SparseDtmcEliminationModelCheckerSettings::isEliminateEntryStatesLastSet() const {
bool EliminationSettings::isEliminateEntryStatesLastSet() const {
return this->getOption(entryStatesLastOptionName).getHasOptionBeenSet();
}
uint_fast64_t SparseDtmcEliminationModelCheckerSettings::getMaximalSccSize() const {
uint_fast64_t EliminationSettings::getMaximalSccSize() const {
return this->getOption(maximalSccSizeOptionName).getArgumentByName("maxsize").getValueAsUnsignedInteger();
}
} // namespace modules

14
src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h → src/settings/modules/EliminationSettings.h
View File

@ -1,5 +1,5 @@
#ifndef STORM_SETTINGS_MODULES_SPARSEDTMCELIMINATIONMODELCHECKERSETTINGS_H_
#define STORM_SETTINGS_MODULES_SPARSEDTMCELIMINATIONMODELCHECKERSETTINGS_H_
#ifndef STORM_SETTINGS_MODULES_ELIMINATIONSETTINGS_H_
#define STORM_SETTINGS_MODULES_ELIMINATIONSETTINGS_H_
#include "src/settings/modules/ModuleSettings.h"
@ -8,9 +8,9 @@ namespace storm {
namespace modules {
/*!
* This class represents the settings for the elimination-based DTMC model checker.
* This class represents the settings for the elimination-based procedures.
*/
class SparseDtmcEliminationModelCheckerSettings : public ModuleSettings {
class EliminationSettings : public ModuleSettings {
public:
/*!
* An enum that contains all available state elimination orders.
@ -18,14 +18,14 @@ namespace storm {
enum class EliminationOrder { Forward, ForwardReversed, Backward, BackwardReversed, Random, StaticPenalty, DynamicPenalty, RegularExpression };
/*!
* An enum that contains all available techniques to solve parametric systems.
* An enum that contains all available elimination methods.
*/
enum class EliminationMethod { State, Scc, Hybrid};
/*!
* Creates a new set of parametric model checking settings.
*/
SparseDtmcEliminationModelCheckerSettings();
EliminationSettings();
/*!
* Retrieves the selected elimination method.
@ -68,4 +68,4 @@ namespace storm {
} // namespace settings
} // namespace storm
#endif /* STORM_SETTINGS_MODULES_SPARSEDTMCELIMINATIONMODELCHECKERSETTINGS_H_ */
#endif /* STORM_SETTINGS_MODULES_ELIMINATIONSETTINGS_H_ */

4
src/storm-dyftee.cpp
View File

@ -21,7 +21,7 @@
//#include "src/settings/modules/GurobiSettings.h"
//#include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h"
//#include "src/settings/modules/ParametricSettings.h"
#include "src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h"
#include "src/settings/modules/EliminationSettings.h"
/*!
* Load DFT from filename, build corresponding Model and check against given property.
@ -65,7 +65,7 @@ void initializeSettings() {
//storm::settings::addModule<storm::settings::modules::GurobiSettings>();
//storm::settings::addModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>();
//storm::settings::addModule<storm::settings::modules::ParametricSettings>();
storm::settings::addModule<storm::settings::modules::SparseDtmcEliminationModelCheckerSettings>();
storm::settings::addModule<storm::settings::modules::EliminationSettings>();
}
/*!

40
src/utility/stateelimination.cpp
View File

@ -20,31 +20,31 @@ namespace storm {
namespace utility {
namespace stateelimination {
bool eliminationOrderNeedsDistances(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder const& order) {
return order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Forward ||
order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::ForwardReversed ||
order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Backward ||
order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::BackwardReversed;
bool eliminationOrderNeedsDistances(storm::settings::modules::EliminationSettings::EliminationOrder const& order) {
return order == storm::settings::modules::EliminationSettings::EliminationOrder::Forward ||
order == storm::settings::modules::EliminationSettings::EliminationOrder::ForwardReversed ||
order == storm::settings::modules::EliminationSettings::EliminationOrder::Backward ||
order == storm::settings::modules::EliminationSettings::EliminationOrder::BackwardReversed;
}
bool eliminationOrderNeedsForwardDistances(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder const& order) {
return order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Forward ||
order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::ForwardReversed;
bool eliminationOrderNeedsForwardDistances(storm::settings::modules::EliminationSettings::EliminationOrder const& order) {
return order == storm::settings::modules::EliminationSettings::EliminationOrder::Forward ||
order == storm::settings::modules::EliminationSettings::EliminationOrder::ForwardReversed;
}
bool eliminationOrderNeedsReversedDistances(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder const& order) {
return order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::ForwardReversed ||
order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::BackwardReversed;
bool eliminationOrderNeedsReversedDistances(storm::settings::modules::EliminationSettings::EliminationOrder const& order) {
return order == storm::settings::modules::EliminationSettings::EliminationOrder::ForwardReversed ||
order == storm::settings::modules::EliminationSettings::EliminationOrder::BackwardReversed;
}
bool eliminationOrderIsPenaltyBased(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder const& order) {
return order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::StaticPenalty ||
order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::DynamicPenalty ||
order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::RegularExpression;
bool eliminationOrderIsPenaltyBased(storm::settings::modules::EliminationSettings::EliminationOrder const& order) {
return order == storm::settings::modules::EliminationSettings::EliminationOrder::StaticPenalty ||
order == storm::settings::modules::EliminationSettings::EliminationOrder::DynamicPenalty ||
order == storm::settings::modules::EliminationSettings::EliminationOrder::RegularExpression;
}
bool eliminationOrderIsStatic(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder const& order) {
return eliminationOrderNeedsDistances(order) || order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::StaticPenalty;
bool eliminationOrderIsStatic(storm::settings::modules::EliminationSettings::EliminationOrder const& order) {
return eliminationOrderNeedsDistances(order) || order == storm::settings::modules::EliminationSettings::EliminationOrder::StaticPenalty;
}
template<typename ValueType>
@ -100,11 +100,11 @@ namespace storm {
STORM_LOG_TRACE("Creating state priority queue for states " << states);
// Get the settings to customize the priority queue.
storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder order = storm::settings::getModule<storm::settings::modules::SparseDtmcEliminationModelCheckerSettings>().getEliminationOrder();
storm::settings::modules::EliminationSettings::EliminationOrder order = storm::settings::getModule<storm::settings::modules::EliminationSettings>().getEliminationOrder();
std::vector<storm::storage::sparse::state_type> sortedStates(states.begin(), states.end());
if (order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Random) {
if (order == storm::settings::modules::EliminationSettings::EliminationOrder::Random) {
std::random_device randomDevice;
std::mt19937 generator(randomDevice());
std::shuffle(sortedStates.begin(), sortedStates.end(), generator);
@ -116,7 +116,7 @@ namespace storm {
return std::make_unique<StaticStatePriorityQueue>(sortedStates);
} else if (eliminationOrderIsPenaltyBased(order)) {
std::vector<std::pair<storm::storage::sparse::state_type, uint_fast64_t>> statePenalties(sortedStates.size());
typename DynamicStatePriorityQueue<ValueType>::PenaltyFunctionType penaltyFunction = order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::RegularExpression ? computeStatePenaltyRegularExpression<ValueType> : computeStatePenalty<ValueType>;
typename DynamicStatePriorityQueue<ValueType>::PenaltyFunctionType penaltyFunction = order == storm::settings::modules::EliminationSettings::EliminationOrder::RegularExpression ? computeStatePenaltyRegularExpression<ValueType> : computeStatePenalty<ValueType>;
for (uint_fast64_t index = 0; index < sortedStates.size(); ++index) {
statePenalties[index] = std::make_pair(sortedStates[index], penaltyFunction(sortedStates[index], transitionMatrix, backwardTransitions, oneStepProbabilities));
}

12
src/utility/stateelimination.h
View File

@ -9,7 +9,7 @@
#include "src/adapters/CarlAdapter.h"
#include "src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h"
#include "src/settings/modules/EliminationSettings.h"
namespace storm {
namespace solver {
@ -30,11 +30,11 @@ namespace storm {
using namespace storm::solver::stateelimination;
bool eliminationOrderNeedsDistances(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder const& order);
bool eliminationOrderNeedsForwardDistances(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder const& order);
bool eliminationOrderNeedsReversedDistances(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder const& order);
bool eliminationOrderIsPenaltyBased(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder const& order);
bool eliminationOrderIsStatic(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder const& order);
bool eliminationOrderNeedsDistances(storm::settings::modules::EliminationSettings::EliminationOrder const& order);
bool eliminationOrderNeedsForwardDistances(storm::settings::modules::EliminationSettings::EliminationOrder const& order);
bool eliminationOrderNeedsReversedDistances(storm::settings::modules::EliminationSettings::EliminationOrder const& order);
bool eliminationOrderIsPenaltyBased(storm::settings::modules::EliminationSettings::EliminationOrder const& order);
bool eliminationOrderIsStatic(storm::settings::modules::EliminationSettings::EliminationOrder const& order);
template<typename ValueType>
uint_fast64_t estimateComplexity(ValueType const& value);

Write Preview
Loading…
Cancel
Save