diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index d2a58b68c..f6cb7e9c4 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -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().getEliminationOrder(); + storm::settings::modules::EliminationSettings::EliminationOrder order = storm::settings::getModule().getEliminationOrder(); boost::optional> 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().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().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> distanceBasedPriorities; - storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder order = storm::settings::getModule().getEliminationOrder(); + storm::settings::modules::EliminationSettings::EliminationOrder order = storm::settings::getModule().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 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().getMaximalSccSize(), entryStateQueue, computeResultsForInitialStatesOnly, distanceBasedPriorities); + uint_fast64_t maximalDepth = treatScc(transitionMatrix, values, initialStates, subsystem, initialStates, forwardTransitions, backwardTransitions, false, 0, storm::settings::getModule().getMaximalSccSize(), entryStateQueue, computeResultsForInitialStatesOnly, distanceBasedPriorities); // If the entry states were to be eliminated last, we need to do so now. - if (storm::settings::getModule().isEliminateEntryStatesLastSet()) { + if (storm::settings::getModule().isEliminateEntryStatesLastSet()) { STORM_LOG_DEBUG("Eliminating " << entryStateQueue.size() << " entry states as a last step."); std::vector sortedStates(entryStateQueue.begin(), entryStateQueue.end()); std::shared_ptr queuePriorities = std::make_shared(sortedStates); @@ -855,7 +855,7 @@ namespace storm { storm::storage::FlexibleSparseMatrix flexibleMatrix(transitionMatrix); storm::storage::FlexibleSparseMatrix flexibleBackwardTransitions(backwardTransitions); - storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder order = storm::settings::getModule().getEliminationOrder(); + storm::settings::modules::EliminationSettings::EliminationOrder order = storm::settings::getModule().getEliminationOrder(); boost::optional> 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().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::State) { + if (storm::settings::getModule().getEliminationMethod() == storm::settings::modules::EliminationSettings::EliminationMethod::State) { performOrdinaryStateElimination(flexibleMatrix, flexibleBackwardTransitions, subsystem, initialStates, computeResultsForInitialStatesOnly, values, distanceBasedPriorities); - } else if (storm::settings::getModule().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::Hybrid) { + } else if (storm::settings::getModule().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().isEliminateEntryStatesLastSet(), level + 1, maximalSccSize, entryStateQueue, computeResultsForInitialStatesOnly, distanceBasedPriorities); + uint_fast64_t depth = treatScc(matrix, values, entryStates, newSccAsBitVector, initialStates, forwardTransitions, backwardTransitions, eliminateEntryStates || !storm::settings::getModule().isEliminateEntryStatesLastSet(), level + 1, maximalSccSize, entryStateQueue, computeResultsForInitialStatesOnly, distanceBasedPriorities); maximalDepth = std::max(maximalDepth, depth); } } else { @@ -970,8 +970,8 @@ namespace storm { } std::vector distances = getStateDistances(transitionMatrix, transitionMatrixTransposed, initialStates, oneStepProbabilities, - storm::settings::getModule().getEliminationOrder() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Forward || - storm::settings::getModule().getEliminationOrder() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::ForwardReversed); + storm::settings::getModule().getEliminationOrder() == storm::settings::modules::EliminationSettings::EliminationOrder::Forward || + storm::settings::getModule().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) { diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp index 452b20fd3..434327b16 100644 --- a/src/settings/SettingsManager.cpp +++ b/src/settings/SettingsManager.cpp @@ -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::addModule(); storm::settings::addModule(); - storm::settings::addModule(); + storm::settings::addModule(); storm::settings::addModule(); } diff --git a/src/settings/modules/SparseDtmcEliminationModelCheckerSettings.cpp b/src/settings/modules/EliminationSettings.cpp similarity index 77% rename from src/settings/modules/SparseDtmcEliminationModelCheckerSettings.cpp rename to src/settings/modules/EliminationSettings.cpp index 841a24115..4c26ae0b5 100644 --- a/src/settings/modules/SparseDtmcEliminationModelCheckerSettings.cpp +++ b/src/settings/modules/EliminationSettings.cpp @@ -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 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 diff --git a/src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h b/src/settings/modules/EliminationSettings.h similarity index 82% rename from src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h rename to src/settings/modules/EliminationSettings.h index 176c84a67..22c53daac 100644 --- a/src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h +++ b/src/settings/modules/EliminationSettings.h @@ -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_ */ \ No newline at end of file +#endif /* STORM_SETTINGS_MODULES_ELIMINATIONSETTINGS_H_ */ \ No newline at end of file diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp index 3ffd665ad..4dd7bdbe3 100644 --- a/src/storm-dyftee.cpp +++ b/src/storm-dyftee.cpp @@ -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::addModule(); //storm::settings::addModule(); - storm::settings::addModule(); + storm::settings::addModule(); } /*! diff --git a/src/utility/stateelimination.cpp b/src/utility/stateelimination.cpp index f71e08a5b..22d830e53 100644 --- a/src/utility/stateelimination.cpp +++ b/src/utility/stateelimination.cpp @@ -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 @@ -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().getEliminationOrder(); + storm::settings::modules::EliminationSettings::EliminationOrder order = storm::settings::getModule().getEliminationOrder(); std::vector 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(sortedStates); } else if (eliminationOrderIsPenaltyBased(order)) { std::vector> statePenalties(sortedStates.size()); - typename DynamicStatePriorityQueue::PenaltyFunctionType penaltyFunction = order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::RegularExpression ? computeStatePenaltyRegularExpression : computeStatePenalty; + typename DynamicStatePriorityQueue::PenaltyFunctionType penaltyFunction = order == storm::settings::modules::EliminationSettings::EliminationOrder::RegularExpression ? computeStatePenaltyRegularExpression : computeStatePenalty; for (uint_fast64_t index = 0; index < sortedStates.size(); ++index) { statePenalties[index] = std::make_pair(sortedStates[index], penaltyFunction(sortedStates[index], transitionMatrix, backwardTransitions, oneStepProbabilities)); } diff --git a/src/utility/stateelimination.h b/src/utility/stateelimination.h index 8dc3ab600..8703c4b4d 100644 --- a/src/utility/stateelimination.h +++ b/src/utility/stateelimination.h @@ -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 uint_fast64_t estimateComplexity(ValueType const& value);