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

Started working on more options for sorting and integrating pure state elimination 

Former-commit-id: 4e09925b29
main
dehnert 10 years ago
parent
df7c0f4a95
commit
a987233507
4 changed files with 140 additions and 112 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. 164
      src/modelchecker/reachability/SparseSccModelChecker.cpp
  2. 4
      src/modelchecker/reachability/SparseSccModelChecker.h
  3. 49
      src/settings/modules/ParametricSettings.cpp
  4. 35
      src/settings/modules/ParametricSettings.h

164
src/modelchecker/reachability/SparseSccModelChecker.cpp
View File

@ -17,7 +17,7 @@ namespace storm {
namespace reachability {
template<typename ValueType>
ValueType SparseSccModelChecker<ValueType>::computeReachabilityProbability(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional<std::vector<std::size_t>> const& distances) {
ValueType SparseSccModelChecker<ValueType>::computeReachabilityProbability(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional<std::vector<std::size_t>> 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<ValueType> flexibleBackwardTransitions = getFlexibleSparseMatrix(backwardTransitions, true);
auto conversionEnd = std::chrono::high_resolution_clock::now();
// Then, we recursively treat all SCCs.
storm::utility::ConstantsComparator<ValueType> comparator;
auto modelCheckingStart = std::chrono::high_resolution_clock::now();
std::vector<storm::storage::sparse::state_type> 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<storm::storage::sparse::state_type> 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<ValueType> comparator;
std::vector<storm::storage::sparse::state_type> 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<ValueType> 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<std::pair<storm::storage::sparse::state_type, std::size_t>> stateQueue;
stateQueue.reserve(submatrix.getRowCount());
storm::storage::BitVector statesInQueue(submatrix.getRowCount());
std::vector<std::size_t> 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<storm::storage::sparse::state_type, std::size_t> 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<std::size_t> statePriorities(submatrix.getRowCount());
if (storm::settings::parametricSettings().getEliminationOrder() == storm::settings::modules::ParametricSettings::EliminationOrder::Random) {
std::vector<std::size_t> 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<typename ValueType>
uint_fast64_t SparseSccModelChecker<ValueType>::treatScc(FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, FlexibleSparseMatrix<ValueType>& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector<storm::storage::sparse::state_type>& entryStateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator, boost::optional<std::vector<std::size_t>> const& distances) {
uint_fast64_t SparseSccModelChecker<ValueType>::treatScc(FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, FlexibleSparseMatrix<ValueType>& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector<storm::storage::sparse::state_type>& entryStateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator, boost::optional<std::vector<std::size_t>> 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<std::size_t> const& actualDistances = distances.get();
// std::sort(trivialSccs.begin(), trivialSccs.end(), [&actualDistances] (std::pair<storm::storage::sparse::state_type, uint_fast64_t> const& state1, std::pair<storm::storage::sparse::state_type, uint_fast64_t> const& state2) -> bool { return actualDistances[state1.first] > actualDistances[state2.first]; } );
std::sort(trivialSccs.begin(), trivialSccs.end(), [&oneStepProbabilities,&comparator] (std::pair<storm::storage::sparse::state_type, uint_fast64_t> const& state1, std::pair<storm::storage::sparse::state_type, uint_fast64_t> 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<storm::storage::sparse::state_type, uint_fast64_t> const& a, std::pair<storm::storage::sparse::state_type, uint_fast64_t> 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<uint_fast64_t> 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<std::size_t> 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<uint_fast64_t> 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<typename ValueType>
void SparseSccModelChecker<ValueType>::eliminateState(FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix<ValueType>& 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<std::chrono::milliseconds>(eliminationTime).count() > 3000) {
STORM_PRINT("Elimination took more than 3 seconds (actually took " << std::chrono::duration_cast<std::chrono::milliseconds>(eliminationTime).count() << "ms)." << std::endl);
STORM_PRINT("Simplification took " << std::chrono::duration_cast<std::chrono::milliseconds>(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 <typename ValueType>

4
src/modelchecker/reachability/SparseSccModelChecker.h
View File

@ -39,10 +39,10 @@ namespace storm {
public:
static ValueType computeReachabilityProbability(storm::models::Dtmc<ValueType> const& dtmc, std::shared_ptr<storm::properties::prctl::PrctlFilter<double>> const& filterFormula);
static ValueType computeReachabilityProbability(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional<std::vector<std::size_t>> const& distances = {});
static ValueType computeReachabilityProbability(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional<std::vector<std::size_t>> const& statePriorities = {});
private:
static uint_fast64_t treatScc(FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, FlexibleSparseMatrix<ValueType>& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector<storm::storage::sparse::state_type>& entryStateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator, boost::optional<std::vector<std::size_t>> const& distances);
static uint_fast64_t treatScc(FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, FlexibleSparseMatrix<ValueType>& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector<storm::storage::sparse::state_type>& entryStateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator, boost::optional<std::vector<std::size_t>> const& distances = {});
static FlexibleSparseMatrix<ValueType> getFlexibleSparseMatrix(storm::storage::SparseMatrix<ValueType> const& matrix, bool setAllValuesToOne = false);
static void eliminateState(FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix<ValueType>& backwardTransitions);
static bool eliminateStateInPlace(storm::storage::SparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, storm::storage::SparseMatrix<ValueType>& backwardTransitions);

49
src/settings/modules/ParametricSettings.cpp
View File

@ -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<std::string> 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<std::string> 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

35
src/settings/modules/ParametricSettings.h
View File

@ -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;

Write Preview
Loading…
Cancel
Save