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

merge 

Former-commit-id: 27c7010322
main
dehnert 11 years ago
parent
3f44b1295f 534c8c8a44
commit
36a65392e0
5 changed files with 82 additions and 41 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. 87
      src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
  2. 7
      src/settings/modules/ParametricSettings.cpp
  3. 8
      src/settings/modules/ParametricSettings.h
  4. 2
      src/settings/modules/SparseDtmcEliminationModelCheckerSettings.cpp
  5. 19
      src/stormParametric.cpp

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

@ -231,18 +231,18 @@ namespace storm {
storm::storage::BitVector statesReachingPhi = storm::utility::graph::performProbGreater0(backwardTransitions, trueStates, phiStates);
// The set of states we need to consider are those that have a non-zero probability to satisfy the condition or are on some path that has a psi state in it.
STORM_LOG_DEBUG("Initial state: " << model.getInitialStates());
STORM_LOG_DEBUG("Phi states: " << phiStates);
STORM_LOG_DEBUG("Psi state: " << psiStates);
STORM_LOG_DEBUG("States with probability greater 0 of satisfying the condition: " << statesWithProbabilityGreater0);
STORM_LOG_DEBUG("States with psi predecessor: " << statesWithPsiPredecessor);
STORM_LOG_DEBUG("States reaching phi: " << statesReachingPhi);
STORM_LOG_TRACE("Initial state: " << model.getInitialStates());
STORM_LOG_TRACE("Phi states: " << phiStates);
STORM_LOG_TRACE("Psi state: " << psiStates);
STORM_LOG_TRACE("States with probability greater 0 of satisfying the condition: " << statesWithProbabilityGreater0);
STORM_LOG_TRACE("States with psi predecessor: " << statesWithPsiPredecessor);
STORM_LOG_TRACE("States reaching phi: " << statesReachingPhi);
storm::storage::BitVector maybeStates = statesWithProbabilityGreater0 | (statesWithPsiPredecessor & statesReachingPhi);
STORM_LOG_DEBUG("Found " << maybeStates.getNumberOfSetBits() << " relevant states: " << maybeStates);
STORM_LOG_TRACE("Found " << maybeStates.getNumberOfSetBits() << " relevant states: " << maybeStates);
// Determine the set of initial states of the sub-DTMC.
storm::storage::BitVector newInitialStates = model.getInitialStates() % maybeStates;
STORM_LOG_DEBUG("Found new initial states: " << newInitialStates << " (old: " << model.getInitialStates() << ")");
STORM_LOG_TRACE("Found new initial states: " << newInitialStates << " (old: " << model.getInitialStates() << ")");
// Create a dummy vector for the one-step probabilities.
std::vector<ValueType> oneStepProbabilities(maybeStates.getNumberOfSetBits(), storm::utility::zero<ValueType>());
@ -264,10 +264,10 @@ namespace storm {
// Keep only the states that we do not eliminate in the maybe states.
maybeStates = phiStates | psiStates;
STORM_LOG_DEBUG("Phi states in reduced model " << phiStates);
STORM_LOG_DEBUG("Psi states in reduced model " << psiStates);
STORM_LOG_TRACE("Phi states in reduced model " << phiStates);
STORM_LOG_TRACE("Psi states in reduced model " << psiStates);
storm::storage::BitVector statesToEliminate = ~maybeStates & ~newInitialStates;
STORM_LOG_DEBUG("Eliminating the states " << statesToEliminate);
STORM_LOG_TRACE("Eliminating the states " << statesToEliminate);
// Before starting the model checking process, we assign priorities to states so we can use them to
// impose ordering constraints later.
@ -301,10 +301,10 @@ namespace storm {
for (auto const& trans1 : flexibleMatrix.getRow(*newInitialStates.begin())) {
auto initialStateSuccessor = trans1.getColumn();
STORM_LOG_DEBUG("Exploring successor " << initialStateSuccessor << " of the initial state.");
STORM_LOG_TRACE("Exploring successor " << initialStateSuccessor << " of the initial state.");
if (phiStates.get(initialStateSuccessor)) {
STORM_LOG_DEBUG("Is a phi state.");
STORM_LOG_TRACE("Is a phi state.");
// If the state is both a phi and a psi state, we do not need to eliminate chains.
if (psiStates.get(initialStateSuccessor)) {
@ -327,7 +327,7 @@ namespace storm {
typename FlexibleSparseMatrix::row_type const& successorRow = flexibleMatrix.getRow(element.getColumn());
// Eliminate the successor only if there possibly is a psi state reachable through it.
if (successorRow.size() > 1 || (!successorRow.empty() && successorRow.front().getColumn() != element.getColumn())) {
STORM_LOG_DEBUG("Found non-psi successor " << element.getColumn() << " that needs to be eliminated.");
STORM_LOG_TRACE("Found non-psi successor " << element.getColumn() << " that needs to be eliminated.");
eliminateState(flexibleMatrix, oneStepProbabilities, element.getColumn(), flexibleBackwardTransitions, missingStateRewards, false, true, phiStates);
hasNonPsiSuccessor = true;
}
@ -338,7 +338,7 @@ namespace storm {
}
} else {
STORM_LOG_ASSERT(psiStates.get(initialStateSuccessor), "Expected psi state.");
STORM_LOG_DEBUG("Is a psi state.");
STORM_LOG_TRACE("Is a psi state.");
// At this point, we know that the state satisfies psi and not phi.
// This means, we must compute the probability to reach phi states, which in turn means that we need
@ -356,7 +356,7 @@ namespace storm {
if (!phiStates.get(element.getColumn())) {
typename FlexibleSparseMatrix::row_type const& successorRow = flexibleMatrix.getRow(element.getColumn());
if (successorRow.size() > 1 || (!successorRow.empty() && successorRow.front().getColumn() != element.getColumn())) {
STORM_LOG_DEBUG("Found non-phi successor " << element.getColumn() << " that needs to be eliminated.");
STORM_LOG_TRACE("Found non-phi successor " << element.getColumn() << " that needs to be eliminated.");
eliminateState(flexibleMatrix, oneStepProbabilities, element.getColumn(), flexibleBackwardTransitions, missingStateRewards, false, true, psiStates);
hasNonPhiSuccessor = true;
}
@ -464,15 +464,15 @@ namespace storm {
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_LOG_INFO("Eliminating " << states.size() << " states using the state elimination technique." << std::endl);
STORM_LOG_DEBUG("Eliminating " << states.size() << " states using the state elimination technique." << std::endl);
for (auto const& state : states) {
eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions, stateRewards);
}
STORM_LOG_INFO("Eliminated " << states.size() << " states." << std::endl);
STORM_LOG_DEBUG("Eliminated " << states.size() << " states." << std::endl);
} else if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::Hybrid) {
// When using the hybrid technique, we recursively treat the SCCs up to some size.
std::vector<storm::storage::sparse::state_type> entryStateQueue;
STORM_LOG_INFO("Eliminating " << subsystem.size() << " states using the hybrid elimination technique." << std::endl);
STORM_LOG_DEBUG("Eliminating " << subsystem.size() << " states using the hybrid elimination technique." << std::endl);
maximalDepth = treatScc(flexibleMatrix, oneStepProbabilities, initialStates, subsystem, transitionMatrix, flexibleBackwardTransitions, false, 0, storm::settings::sparseDtmcEliminationModelCheckerSettings().getMaximalSccSize(), entryStateQueue, stateRewards, statePriorities);
// If the entry states were to be eliminated last, we need to do so now.
@ -482,7 +482,7 @@ namespace storm {
eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions, stateRewards);
}
}
STORM_LOG_INFO("Eliminated " << subsystem.size() << " states." << std::endl);
STORM_LOG_DEBUG("Eliminated " << subsystem.size() << " states." << std::endl);
}
// Finally eliminate initial state.
@ -503,7 +503,7 @@ namespace storm {
STORM_LOG_ASSERT(flexibleMatrix.getRow(*initialStates.begin()).front().getColumn() == *initialStates.begin(), "Remaining entry should be a self-loop, but it is not.");
ValueType loopProbability = flexibleMatrix.getRow(*initialStates.begin()).front().getValue();
loopProbability = storm::utility::one<ValueType>() / (storm::utility::one<ValueType>() - loopProbability);
STORM_LOG_INFO("Scaling the reward of the initial state " << stateRewards.get()[(*initialStates.begin())] << " with " << loopProbability);
STORM_LOG_DEBUG("Scaling the reward of the initial state " << stateRewards.get()[(*initialStates.begin())] << " with " << loopProbability);
stateRewards.get()[(*initialStates.begin())] *= loopProbability;
flexibleMatrix.getRow(*initialStates.begin()).clear();
}
@ -536,12 +536,21 @@ namespace storm {
STORM_PRINT_AND_LOG(" * maximal depth of SCC decomposition: " << maximalDepth << std::endl);
}
}
// Now, we return the value for the only initial state.
STORM_LOG_DEBUG("Simplifying and returning result.");
if (stateRewards) {
return storm::utility::simplify(stateRewards.get()[*initialStates.begin()]);
// if (storm::settings::parametricSettings().isSimplifySet()) {
// return storm::utility::simplify(stateRewards.get()[*initialStates.begin()]);
// } else {
return storm::utility::simplify(stateRewards.get()[*initialStates.begin()]);
// }
} else {
return storm::utility::simplify(oneStepProbabilities[*initialStates.begin()]);
// if (storm::settings::parametricSettings().isSimplifySet()) {
// return storm::utility::simplify(oneStepProbabilities[*initialStates.begin()]);
// } else {
return oneStepProbabilities[*initialStates.begin()];
// }
}
}
@ -596,11 +605,11 @@ namespace storm {
// If the SCCs are large enough, we try to split them further.
if (scc.getNumberOfSetBits() > maximalSccSize) {
STORM_LOG_DEBUG("SCC is large enough (" << scc.getNumberOfSetBits() << " states) to be decomposed further.");
STORM_LOG_TRACE("SCC is large enough (" << scc.getNumberOfSetBits() << " states) to be decomposed further.");
// Here, we further decompose the SCC into sub-SCCs.
storm::storage::StronglyConnectedComponentDecomposition<ValueType> decomposition(forwardTransitions, scc & ~entryStates, false, false);
STORM_LOG_DEBUG("Decomposed SCC into " << decomposition.size() << " sub-SCCs.");
STORM_LOG_TRACE("Decomposed SCC into " << decomposition.size() << " sub-SCCs.");
// Store a bit vector of remaining SCCs so we can be flexible when it comes to the order in which
// we eliminate the SCCs.
@ -621,15 +630,15 @@ namespace storm {
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.");
STORM_LOG_TRACE("Eliminating " << trivialSccs.size() << " trivial SCCs.");
for (auto const& stateIndexPair : trivialSccs) {
eliminateState(matrix, oneStepProbabilities, stateIndexPair.first, backwardTransitions, stateRewards);
remainingSccs.set(stateIndexPair.second, false);
}
STORM_LOG_DEBUG("Eliminated all trivial SCCs.");
STORM_LOG_TRACE("Eliminated all trivial SCCs.");
// And then recursively treat the remaining sub-SCCs.
STORM_LOG_DEBUG("Eliminating " << remainingSccs.getNumberOfSetBits() << " remaining SCCs on level " << level << ".");
STORM_LOG_TRACE("Eliminating " << remainingSccs.getNumberOfSetBits() << " remaining SCCs on level " << level << ".");
for (auto sccIndex : remainingSccs) {
storm::storage::StronglyConnectedComponent const& newScc = decomposition.getBlock(sccIndex);
@ -653,7 +662,7 @@ namespace storm {
} else {
// In this case, we perform simple state elimination in the current SCC.
STORM_LOG_DEBUG("SCC of size " << scc.getNumberOfSetBits() << " is small enough to be eliminated directly.");
STORM_LOG_TRACE("SCC of size " << scc.getNumberOfSetBits() << " is small enough to be eliminated directly.");
storm::storage::BitVector remainingStates = scc & ~entryStates;
std::vector<uint_fast64_t> states(remainingStates.begin(), remainingStates.end());
@ -669,16 +678,16 @@ namespace storm {
eliminateState(matrix, oneStepProbabilities, state, backwardTransitions, stateRewards);
}
STORM_LOG_DEBUG("Eliminated all states of SCC.");
STORM_LOG_TRACE("Eliminated all states of SCC.");
}
// Finally, eliminate the entry states (if we are required to do so).
if (eliminateEntryStates) {
STORM_LOG_DEBUG("Finally, eliminating/adding entry states.");
STORM_LOG_TRACE("Finally, eliminating/adding entry states.");
for (auto state : entryStates) {
eliminateState(matrix, oneStepProbabilities, state, backwardTransitions, stateRewards);
}
STORM_LOG_DEBUG("Eliminated/added entry states.");
STORM_LOG_TRACE("Eliminated/added entry states.");
} else {
for (auto state : entryStates) {
entryStateQueue.push_back(state);
@ -698,7 +707,7 @@ namespace storm {
auto eliminationStart = std::chrono::high_resolution_clock::now();
++counter;
STORM_LOG_DEBUG("Eliminating state " << state << ".");
STORM_LOG_TRACE("Eliminating state " << state << ".");
if (counter > matrix.getNumberOfRows() / 10) {
++chunkCounter;
STORM_LOG_INFO("Eliminated " << (chunkCounter * 10) << "% of the states." << std::endl);
@ -744,7 +753,7 @@ namespace storm {
}
}
STORM_LOG_DEBUG((hasSelfLoop ? "State has self-loop." : "State does not have a self-loop."));
STORM_LOG_TRACE((hasSelfLoop ? "State has self-loop." : "State does not have a self-loop."));
// Now connect the predecessors of the state being eliminated with its successors.
typename FlexibleSparseMatrix::row_type& currentStatePredecessors = backwardTransitions.getRow(state);
@ -767,10 +776,10 @@ namespace storm {
// Skip the state if the elimination is constrained, but the predecessor is not in the constraint.
if (constrained && !predecessorConstraint.get(predecessor)) {
newCurrentStatePredecessors.emplace_back(predecessor, storm::utility::one<ValueType>());
STORM_LOG_DEBUG("Not eliminating predecessor " << predecessor << ", because it does not fit the filter.");
STORM_LOG_TRACE("Not eliminating predecessor " << predecessor << ", because it does not fit the filter.");
continue;
}
STORM_LOG_DEBUG("Eliminating predecessor " << predecessor << ".");
STORM_LOG_TRACE("Eliminating predecessor " << predecessor << ".");
// First, find the probability with which the predecessor can move to the current state, because
// the other probabilities need to be scaled with this factor.
@ -834,7 +843,7 @@ namespace storm {
if (!stateRewards) {
// Add the probabilities to go to a target state in just one step if we have to compute probabilities.
oneStepProbabilities[predecessor] += storm::utility::simplify(multiplyFactor * oneStepProbabilities[state]);
STORM_LOG_DEBUG("Fixed new next-state probabilities of predecessor states.");
STORM_LOG_TRACE("Fixed new next-state probabilities of predecessor states.");
} else {
// If we are computing rewards, we basically scale the state reward of the state to eliminate and
// add the result to the state reward of the predecessor.
@ -914,7 +923,7 @@ namespace storm {
// Now move the new predecessors in place.
successorBackwardTransitions = std::move(newPredecessors);
}
STORM_LOG_DEBUG("Fixed predecessor lists of successor states.");
STORM_LOG_TRACE("Fixed predecessor lists of successor states.");
if (removeForwardTransitions) {
// Clear the eliminated row to reduce memory consumption.

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

@ -10,6 +10,7 @@ namespace storm {
const std::string ParametricSettings::encodeSmt2StrategyOptionName = "smt2strategy";
const std::string ParametricSettings::exportSmt2DestinationPathOptionName = "smt2path";
const std::string ParametricSettings::exportResultDestinationPathOptionName = "resultfile";
const std::string ParametricSettings::derivativesOptionName = "derivatives";
ParametricSettings::ParametricSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
this->addOption(storm::settings::OptionBuilder(moduleName, encodeSmt2StrategyOptionName, true, "Set the smt2 encoding strategy.")
@ -18,6 +19,7 @@ namespace storm {
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "the location.").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, exportResultDestinationPathOptionName, true, "A path to a file where the smt2 encoding should be saved.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "the location.").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, derivativesOptionName, false, "Sets whether to generate the derivatives of the resulting rational function.").build());
}
bool ParametricSettings::exportResultToFile() const {
@ -47,6 +49,11 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown smt2encoding strategy '" << strategy << "'.");
}
}
bool ParametricSettings::isDerivativesSet() const {
return this->getOption(derivativesOptionName).getHasOptionBeenSet();
}
} // namespace modules
} // namespace settings
} // namespace storm

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

@ -58,6 +58,13 @@ namespace storm {
* @return The encoding strategy to be used.
*/
Smt2EncodingStrategy smt2EncodingStrategy() const;
/*!
* Retrieves whether or not derivatives of the resulting rational function are to be generated.
*
* @return True if the derivatives are to be generated.
*/
bool isDerivativesSet() const;
const static std::string moduleName;
@ -65,6 +72,7 @@ namespace storm {
const static std::string encodeSmt2StrategyOptionName;
const static std::string exportSmt2DestinationPathOptionName;
const static std::string exportResultDestinationPathOptionName;
const static std::string derivativesOptionName;
};
} // namespace modules

2
src/settings/modules/SparseDtmcEliminationModelCheckerSettings.cpp
View File

@ -14,7 +14,7 @@ namespace storm {
SparseDtmcEliminationModelCheckerSettings::SparseDtmcEliminationModelCheckerSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
std::vector<std::string> orders = {"fw", "fwrev", "bw", "bwrev", "rand"};
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());
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("fwrev").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());

19
src/stormParametric.cpp
View File

@ -103,6 +103,23 @@ void check() {
printApproximateResult(valueFunction);
}
std::cout << std::endl;
// Generate derivatives for sensitivity analysis if requested.
if (std::is_same<ValueType, storm::RationalFunction>::value && storm::settings::parametricSettings().isDerivativesSet()) {
auto allVariables = valueFunction.gatherVariables();
if (!allVariables.empty()) {
std::map<storm::Variable, storm::RationalFunction> derivatives;
for (auto const& variable : allVariables) {
derivatives[variable] = valueFunction.derivative(variable);
}
std::cout << std::endl << "Derivatives (variable; derivative):" << std::endl;
for (auto const& variableDerivativePair : derivatives) {
std::cout << "(" << variableDerivativePair.first << "; " << variableDerivativePair.second << ")" << std::endl;
}
}
}
}
}
@ -131,4 +148,4 @@ int main(const int argc, const char** argv) {
} catch (std::exception const& exception) {
STORM_LOG_ERROR("An unexpected exception occurred and caused StoRM to terminate. The message of this exception is: " << exception.what());
}
}
}
Write Preview
Loading…
Cancel
Save