From a98723350716b3df42a4d7ce8f614d75f8c6abac Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 26 Oct 2014 16:22:36 +0100 Subject: [PATCH] Started working on more options for sorting and integrating pure state elimination Former-commit-id: 4e09925b29056ceadd42ee910cfc9bb4379da4e6 --- .../reachability/SparseSccModelChecker.cpp | 164 ++++++++---------- .../reachability/SparseSccModelChecker.h | 4 +- src/settings/modules/ParametricSettings.cpp | 49 ++++-- src/settings/modules/ParametricSettings.h | 35 ++-- 4 files changed, 140 insertions(+), 112 deletions(-) diff --git a/src/modelchecker/reachability/SparseSccModelChecker.cpp b/src/modelchecker/reachability/SparseSccModelChecker.cpp index 3e39f0794..ba75757fa 100644 --- a/src/modelchecker/reachability/SparseSccModelChecker.cpp +++ b/src/modelchecker/reachability/SparseSccModelChecker.cpp @@ -17,7 +17,7 @@ namespace storm { namespace reachability { template - ValueType SparseSccModelChecker::computeReachabilityProbability(storm::storage::SparseMatrix const& transitionMatrix, std::vector& oneStepProbabilities, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional> const& distances) { + ValueType SparseSccModelChecker::computeReachabilityProbability(storm::storage::SparseMatrix const& transitionMatrix, std::vector& oneStepProbabilities, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional> const& statePriorities) { auto totalTimeStart = std::chrono::high_resolution_clock::now(); auto conversionStart = std::chrono::high_resolution_clock::now(); @@ -29,22 +29,44 @@ namespace storm { FlexibleSparseMatrix flexibleBackwardTransitions = getFlexibleSparseMatrix(backwardTransitions, true); auto conversionEnd = std::chrono::high_resolution_clock::now(); - // Then, we recursively treat all SCCs. - storm::utility::ConstantsComparator comparator; auto modelCheckingStart = std::chrono::high_resolution_clock::now(); - std::vector entryStateQueue; - uint_fast64_t maximalDepth = treatScc(flexibleMatrix, oneStepProbabilities, initialStates, subsystem, transitionMatrix, flexibleBackwardTransitions, false, 0, storm::settings::parametricSettings().getMaximalSccSize(), entryStateQueue, comparator, distances); - - // If the entry states were to be eliminated last, we need to do so now. - STORM_LOG_DEBUG("Eliminating " << entryStateQueue.size() << " entry states as a last step."); - if (storm::settings::parametricSettings().isEliminateEntryStatesLastSet()) { - for (auto const& state : entryStateQueue) { + uint_fast64_t maximalDepth = 0; + if (storm::settings::parametricSettings().getEliminationMethod() == storm::settings::modules::ParametricSettings::EliminationMethod::State) { + // If we are required to do pure state elimination, we simply create a vector of all states to + // eliminate and sort it according to the given priorities. + + // Remove the initial state from the states which we need to eliminate. + subsystem &= ~initialStates; + std::vector states(subsystem.begin(), subsystem.end()); + + if (statePriorities) { + std::sort(states.begin(), states.end(), [&statePriorities] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return statePriorities.get()[a] < statePriorities.get()[b]; }); + } + + STORM_PRINT_AND_LOG("Eliminating " << states.size() << " states using the state elimination technique."); + for (auto const& state : states) { eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions); } + STORM_PRINT_AND_LOG("Eliminated " << states.size() << " states."); + } else if (storm::settings::parametricSettings().getEliminationMethod() == storm::settings::modules::ParametricSettings::EliminationMethod::Hybrid) { + // When using the hybrid technique, we recursively treat the SCCs up to some size. + storm::utility::ConstantsComparator comparator; + std::vector entryStateQueue; + STORM_PRINT_AND_LOG("Eliminating " << subsystem.size() << " states using the hybrid elimination technique."); + maximalDepth = treatScc(flexibleMatrix, oneStepProbabilities, initialStates, subsystem, transitionMatrix, flexibleBackwardTransitions, false, 0, storm::settings::parametricSettings().getMaximalSccSize(), entryStateQueue, comparator, statePriorities); + + // If the entry states were to be eliminated last, we need to do so now. + STORM_LOG_DEBUG("Eliminating " << entryStateQueue.size() << " entry states as a last step."); + if (storm::settings::parametricSettings().isEliminateEntryStatesLastSet()) { + for (auto const& state : entryStateQueue) { + eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions); + } + } + STORM_PRINT_AND_LOG("Eliminated " << subsystem.size() << " states."); } // Finally eliminate initial state. - STORM_PRINT_AND_LOG("Eliminating initial state " << *initialStates.begin() << std::endl); + STORM_PRINT_AND_LOG("Eliminating initial state " << *initialStates.begin() << "." << std::endl); eliminateState(flexibleMatrix, oneStepProbabilities, *initialStates.begin(), flexibleBackwardTransitions); // Make sure that we have eliminated all transitions from the initial state. @@ -67,7 +89,9 @@ namespace storm { STORM_PRINT_AND_LOG(std::endl); STORM_PRINT_AND_LOG("Other:" << std::endl); STORM_PRINT_AND_LOG(" * number of states eliminated: " << transitionMatrix.getRowCount() << std::endl); - STORM_PRINT_AND_LOG(" * maximal depth of SCC decomposition: " << maximalDepth << std::endl); + if (storm::settings::parametricSettings().getEliminationMethod() == storm::settings::modules::ParametricSettings::EliminationMethod::Hybrid) { + STORM_PRINT_AND_LOG(" * maximal depth of SCC decomposition: " << maximalDepth << std::endl); + } } // Now, we return the value for the only initial state. @@ -134,33 +158,29 @@ namespace storm { // We then build the submatrix that only has the transitions of the maybe states. storm::storage::SparseMatrix submatrix = dtmc.getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); - // To be able to apply heuristics later, we now determine the distance of each state to the initial state. - // We start by setting up the data structures. - std::vector> stateQueue; - stateQueue.reserve(submatrix.getRowCount()); - storm::storage::BitVector statesInQueue(submatrix.getRowCount()); - std::vector distances(submatrix.getRowCount()); - - storm::storage::sparse::state_type currentPosition = 0; - for (auto const& initialState : newInitialStates) { - stateQueue.emplace_back(initialState, 0); - statesInQueue.set(initialState); - } - - // And then perform the BFS. - while (currentPosition < stateQueue.size()) { - std::pair const& stateDistancePair = stateQueue[currentPosition]; - distances[stateDistancePair.first] = stateDistancePair.second; + // Before starting the model checking process, we assign priorities to states so we can use them to + // impose ordering constraints later. + std::vector statePriorities(submatrix.getRowCount()); + if (storm::settings::parametricSettings().getEliminationOrder() == storm::settings::modules::ParametricSettings::EliminationOrder::Random) { + std::vector states(submatrix.getRowCount()); + for (std::size_t index = 0; index < states.size(); ++index) { + states[index] = index; + } - for (auto const& successorEntry : submatrix.getRow(stateDistancePair.first)) { - if (!statesInQueue.get(successorEntry.getColumn())) { - stateQueue.emplace_back(successorEntry.getColumn(), stateDistancePair.second + 1); - statesInQueue.set(successorEntry.getColumn()); - } + std::random_shuffle(states.begin(), states.end()); + + for (std::size_t index = 0; index < states.size(); ++index) { + statePriorities[states[index]] = index; } - ++currentPosition; + } else if (storm::settings::parametricSettings().getEliminationOrder() == storm::settings::modules::ParametricSettings::EliminationOrder::Forward) { + std::size_t distances = storm::utility::graph::getDistances(submatrix, initialStates); } + + // To be able to apply heuristics later, we now determine the distance of each state to the initial state. + // We start by setting up the data structures. + + return computeReachabilityProbability(submatrix, oneStepProbabilities, submatrix.transpose(), newInitialStates, phiStates, psiStates, distances); } @@ -179,7 +199,7 @@ namespace storm { } template - uint_fast64_t SparseSccModelChecker::treatScc(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix const& forwardTransitions, FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector& entryStateQueue, storm::utility::ConstantsComparator const& comparator, boost::optional> const& distances) { + uint_fast64_t SparseSccModelChecker::treatScc(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix const& forwardTransitions, FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector& entryStateQueue, storm::utility::ConstantsComparator const& comparator, boost::optional> const& statePriorities) { uint_fast64_t maximalDepth = level; // If the SCCs are large enough, we try to split them further. @@ -204,14 +224,12 @@ namespace storm { } } - STORM_LOG_DEBUG("Eliminating " << trivialSccs.size() << " trivial SCCs."); - if (storm::settings::parametricSettings().isSortTrivialSccsSet()) { - STORM_LOG_THROW(distances, storm::exceptions::IllegalFunctionCallException, "Cannot sort according to distances because none were provided."); - std::vector const& actualDistances = distances.get(); -// std::sort(trivialSccs.begin(), trivialSccs.end(), [&actualDistances] (std::pair const& state1, std::pair const& state2) -> bool { return actualDistances[state1.first] > actualDistances[state2.first]; } ); - - std::sort(trivialSccs.begin(), trivialSccs.end(), [&oneStepProbabilities,&comparator] (std::pair const& state1, std::pair const& state2) -> bool { return comparator.isZero(oneStepProbabilities[state1.first]) && !comparator.isZero(oneStepProbabilities[state2.first]); } ); + // If we are given priorities, sort the trivial SCCs accordingly. + if (statePriorities) { + std::sort(trivialSccs.begin(), trivialSccs.end(), [&statePriorities] (std::pair const& a, std::pair const& b) { return statePriorities.get()[a.first] < statePriorities.get()[b.first]; }); } + + STORM_LOG_DEBUG("Eliminating " << trivialSccs.size() << " trivial SCCs."); for (auto const& stateIndexPair : trivialSccs) { eliminateState(matrix, oneStepProbabilities, stateIndexPair.first, backwardTransitions); remainingSccs.set(stateIndexPair.second, false); @@ -237,7 +255,7 @@ namespace storm { } // Recursively descend in SCC-hierarchy. - uint_fast64_t depth = treatScc(matrix, oneStepProbabilities, entryStates, newSccAsBitVector, forwardTransitions, backwardTransitions, !storm::settings::parametricSettings().isEliminateEntryStatesLastSet(), level + 1, maximalSccSize, entryStateQueue, comparator, distances); + uint_fast64_t depth = treatScc(matrix, oneStepProbabilities, entryStates, newSccAsBitVector, forwardTransitions, backwardTransitions, !storm::settings::parametricSettings().isEliminateEntryStatesLastSet(), level + 1, maximalSccSize, entryStateQueue, comparator, statePriorities); maximalDepth = std::max(maximalDepth, depth); } @@ -246,65 +264,45 @@ namespace storm { STORM_LOG_DEBUG("SCC of size " << scc.getNumberOfSetBits() << " is small enough to be eliminated directly."); storm::storage::BitVector remainingStates = scc & ~entryStates; - std::vector statesToEliminate(remainingStates.begin(), remainingStates.end()); - if (storm::settings::parametricSettings().isSortTrivialSccsSet()) { -// STORM_LOG_THROW(distances, storm::exceptions::IllegalFunctionCallException, "Cannot sort according to distances because none were provided."); -// std::vector const& actualDistances = distances.get(); -// std::sort(statesToEliminate.begin(), statesToEliminate.end(), [&actualDistances] (storm::storage::sparse::state_type const& state1, storm::storage::sparse::state_type const& state2) -> bool { return actualDistances[state1] > actualDistances[state2]; } ); - - std::sort(statesToEliminate.begin(), statesToEliminate.end(), [&oneStepProbabilities,&comparator] (storm::storage::sparse::state_type const& state1, storm::storage::sparse::state_type const& state2) -> bool { return comparator.isZero(oneStepProbabilities[state1]) && !comparator.isZero(oneStepProbabilities[state2]); } ); - + std::vector states(remainingStates.begin(), remainingStates.end()); + + // If we are given priorities, sort the trivial SCCs accordingly. + if (statePriorities) { + std::sort(states.begin(), states.end(), [&statePriorities] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return statePriorities.get()[a] < statePriorities.get()[b]; }); } // Eliminate the remaining states that do not have a self-loop (in the current, i.e. modified) // transition probability matrix. - for (auto const& state : statesToEliminate) { -// if (!hasSelfLoop(state, matrix)) { - eliminateState(matrix, oneStepProbabilities, state, backwardTransitions); -// remainingStates.set(state, false); -// } + for (auto const& state : states) { + eliminateState(matrix, oneStepProbabilities, state, backwardTransitions); } - STORM_LOG_DEBUG("Eliminated all states without self-loop."); - - // Eliminate the remaining states. -// for (auto const& state : statesToEliminate) { -// eliminateState(matrix, oneStepProbabilities, state, backwardTransitions); -// } - - STORM_LOG_DEBUG("Eliminated all states with self-loop."); + STORM_LOG_DEBUG("Eliminated all states of SCC."); } // Finally, eliminate the entry states (if we are required to do so). - STORM_LOG_DEBUG("Finally, eliminating/adding entry states."); if (eliminateEntryStates) { + STORM_LOG_DEBUG("Finally, eliminating/adding entry states."); for (auto state : entryStates) { eliminateState(matrix, oneStepProbabilities, state, backwardTransitions); } + STORM_LOG_DEBUG("Eliminated/added entry states."); } else { for (auto state : entryStates) { entryStateQueue.push_back(state); } } - STORM_LOG_DEBUG("Eliminated/added entry states."); return maximalDepth; } - static int chunkCounter = 0; - static int counter = 0; + namespace { + static int chunkCounter = 0; + static int counter = 0; + } template void SparseSccModelChecker::eliminateState(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions) { - -// std::cout << "before eliminating state " << state << std::endl; -// matrix.print(); -// std::cout << "one step probs" << std::endl; -// for (uint_fast64_t index = 0; index < oneStepProbabilities.size(); ++index) { -// std::cout << "(" << index << ", " << oneStepProbabilities[index] << ") "; -// } -// std::cout << std::endl; - auto eliminationStart = std::chrono::high_resolution_clock::now(); ++counter; @@ -544,7 +542,7 @@ namespace storm { auto eliminationEnd = std::chrono::high_resolution_clock::now(); auto eliminationTime = eliminationEnd - eliminationStart; - // If the elimination took more than 3 seconds, we print some more information and quit. + // If the elimination took more than 3 seconds, we print some more information. if (std::chrono::duration_cast(eliminationTime).count() > 3000) { STORM_PRINT("Elimination took more than 3 seconds (actually took " << std::chrono::duration_cast(eliminationTime).count() << "ms)." << std::endl); STORM_PRINT("Simplification took " << std::chrono::duration_cast(simplifyTime).count() << "ms." << std::endl); @@ -555,14 +553,6 @@ namespace storm { STORM_PRINT("Number of predecessors: " << numberOfPredecessors << "." << std::endl); STORM_PRINT("Number of predecessor forward transitions " << predecessorForwardTransitionCount << "." << std::endl); } - -// std::cout << "after eliminating state " << state << std::endl; -// matrix.print(); -// std::cout << "one step probs" << std::endl; -// for (uint_fast64_t index = 0; index < oneStepProbabilities.size(); ++index) { -// std::cout << "(" << index << ", " << oneStepProbabilities[index] << ") "; -// } -// std::cout << std::endl; } template diff --git a/src/modelchecker/reachability/SparseSccModelChecker.h b/src/modelchecker/reachability/SparseSccModelChecker.h index 352676228..fbb83d48b 100644 --- a/src/modelchecker/reachability/SparseSccModelChecker.h +++ b/src/modelchecker/reachability/SparseSccModelChecker.h @@ -39,10 +39,10 @@ namespace storm { public: static ValueType computeReachabilityProbability(storm::models::Dtmc const& dtmc, std::shared_ptr> const& filterFormula); - static ValueType computeReachabilityProbability(storm::storage::SparseMatrix const& transitionMatrix, std::vector& oneStepProbabilities, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional> const& distances = {}); + static ValueType computeReachabilityProbability(storm::storage::SparseMatrix const& transitionMatrix, std::vector& oneStepProbabilities, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional> const& statePriorities = {}); private: - static uint_fast64_t treatScc(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix const& forwardTransitions, FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector& entryStateQueue, storm::utility::ConstantsComparator const& comparator, boost::optional> const& distances); + static uint_fast64_t treatScc(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix const& forwardTransitions, FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector& entryStateQueue, storm::utility::ConstantsComparator const& comparator, boost::optional> const& distances = {}); static FlexibleSparseMatrix getFlexibleSparseMatrix(storm::storage::SparseMatrix const& matrix, bool setAllValuesToOne = false); static void eliminateState(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions); static bool eliminateStateInPlace(storm::storage::SparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, storm::storage::SparseMatrix& backwardTransitions); diff --git a/src/settings/modules/ParametricSettings.cpp b/src/settings/modules/ParametricSettings.cpp index 7b9cecbc4..c979e8b0f 100644 --- a/src/settings/modules/ParametricSettings.cpp +++ b/src/settings/modules/ParametricSettings.cpp @@ -7,16 +7,22 @@ namespace storm { namespace modules { const std::string ParametricSettings::moduleName = "parametric"; + const std::string ParametricSettings::eliminationMethodOptionName = "method"; + const std::string ParametricSettings::eliminationOrderOptionName = "order"; const std::string ParametricSettings::entryStatesLastOptionName = "entrylast"; const std::string ParametricSettings::maximalSccSizeOptionName = "sccsize"; - const std::string ParametricSettings::sortTrivialSccOptionName = "sorttrivial"; const std::string ParametricSettings::encodeSmt2StrategyOptionName = "smt2strategy"; const std::string ParametricSettings::exportSmt2DestinationPathOptionName = "smt2path"; const std::string ParametricSettings::exportResultDestinationPathOptionName = "resultfile"; ParametricSettings::ParametricSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) { + std::vector orders = {"fw", "fwrev", "bw", "bwrev"}; + 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}.").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("bw").build()).build()); + + std::vector methods = {"state", "hybrid"}; + this->addOption(storm::settings::OptionBuilder(moduleName, eliminationMethodOptionName, true, "The elimination technique to use. Available are {state, hybrid}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the elimination technique to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(methods)).setDefaultValueString("hybrid").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, entryStatesLastOptionName, true, "Sets whether the entry states are eliminated last.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, sortTrivialSccOptionName, true, "Sets whether the trivial SCCs are to be eliminated in descending order with respect to their distances from the initial state.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, maximalSccSizeOptionName, true, "Sets the maximal size of the SCCs for which state elimination is applied.") .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("maxsize", "The maximal size of an SCC on which state elimination is applied.").setDefaultValueUnsignedInteger(20).setIsOptional(true).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, encodeSmt2StrategyOptionName, true, "Set the smt2 encoding strategy.") @@ -27,6 +33,34 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "the location.").build()).build()); } + ParametricSettings::EliminationMethod ParametricSettings::getEliminationMethod() const { + std::string eliminationMethodAsString = this->getOption(eliminationMethodOptionName).getArgumentByName("name").getValueAsString(); + if (eliminationMethodAsString == "state") { + return EliminationMethod::State; + } else if (eliminationMethodAsString == "hybrid") { + return EliminationMethod::Hybrid; + } else { + STORM_LOG_ASSERT(false, "Illegal elimination method selected."); + } + } + + ParametricSettings::EliminationOrder ParametricSettings::getEliminationOrder() const { + std::string eliminationOrderAsString = this->getOption(eliminationOrderOptionName).getArgumentByName("name").getValueAsString(); + if (eliminationOrderAsString == "fw") { + return EliminationOrder::Forward; + } else if (eliminationOrderAsString == "fwrev") { + return EliminationOrder::ForwardReversed; + } else if (eliminationOrderAsString == "bw") { + return EliminationOrder::Backward; + } else if (eliminationOrderAsString == "bwrev") { + return EliminationOrder::BackwardReversed; + } else if (eliminationOrderAsString == "rand") { + return EliminationOrder::Random; + } else { + STORM_LOG_ASSERT(false, "Illegal elimination order selected."); + } + } + bool ParametricSettings::isEliminateEntryStatesLastSet() const { return this->getOption(entryStatesLastOptionName).getHasOptionBeenSet(); } @@ -35,10 +69,6 @@ namespace storm { return this->getOption(maximalSccSizeOptionName).getArgumentByName("maxsize").getValueAsUnsignedInteger(); } - bool ParametricSettings::isSortTrivialSccsSet() const { - return this->getOption(sortTrivialSccOptionName).getHasOptionBeenSet(); - } - bool ParametricSettings::exportResultToFile() const { return this->getOption(exportResultDestinationPathOptionName).getHasOptionBeenSet(); } @@ -65,14 +95,7 @@ namespace storm { } else { STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown smt2encoding strategy '" << strategy << "'."); } - - - } - - - - } // namespace modules } // namespace settings } // namespace storm \ No newline at end of file diff --git a/src/settings/modules/ParametricSettings.h b/src/settings/modules/ParametricSettings.h index 7bc5e2e29..bb137cdeb 100644 --- a/src/settings/modules/ParametricSettings.h +++ b/src/settings/modules/ParametricSettings.h @@ -22,7 +22,16 @@ namespace storm { */ enum class Smt2EncodingStrategy {FULL_TRANSITION_SYSTEM, ONLY_SCC_ENTRY_STATES, HIGH_INDEGREE, RATIONAL_FUNCTION}; + /*! + * An enum that contains all available state elimination orders. + */ + enum class EliminationOrder { Forward, ForwardReversed, Backward, BackwardReversed, Random }; + /*! + * An enum that contains all available techniques to solve parametric systems. + */ + enum class EliminationMethod { State, Scc, Hybrid}; + /*! * Creates a new set of parametric model checking settings that is managed by the given manager. * @@ -30,6 +39,20 @@ namespace storm { */ ParametricSettings(storm::settings::SettingsManager& settingsManager); + /*! + * Retrieves the selected elimination method. + * + * @return The selected elimination method. + */ + EliminationMethod getEliminationMethod() const; + + /*! + * Retrieves the selected elimination order. + * + * @return The selected elimination order. + */ + EliminationOrder getEliminationOrder() const; + /*! * Retrieves whether the option to eliminate entry states in the very end is set. * @@ -43,14 +66,6 @@ namespace storm { * @return The maximal size of an SCC on which state elimination is to be directly applied. */ uint_fast64_t getMaximalSccSize() const; - - /*! - * Retrieves whether the option to sort the trivial SCCs (in descending order) wrt. to the distance to - * the initial state. - * - * @return True iff the trivial SCCs are to be sorted. - */ - bool isSortTrivialSccsSet() const; /** * Retrieves whether the model checking result should be exported to a file. @@ -82,13 +97,13 @@ namespace storm { */ Smt2EncodingStrategy smt2EncodingStrategy() const; - const static std::string moduleName; private: + const static std::string eliminationMethodOptionName; + const static std::string eliminationOrderOptionName; const static std::string entryStatesLastOptionName; const static std::string maximalSccSizeOptionName; - const static std::string sortTrivialSccOptionName; const static std::string encodeSmt2StrategyOptionName; const static std::string exportSmt2DestinationPathOptionName; const static std::string exportResultDestinationPathOptionName;