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

Added some comments to scheduler guessing. 

Former-commit-id: 6a256210a3
tempestpy_adaptions
dehnert 12 years ago
parent
d168b1848e
commit
b36b460a4e
2 changed files with 83 additions and 111 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. 138
      src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
  2. 56
      src/utility/graph.h

138
src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
View File

@ -288,8 +288,6 @@ namespace storm {
// Create resulting vector.
std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
std::vector<uint_fast64_t> guessedScheduler;
// Check whether we need to compute exact probabilities for some states.
if (this->getInitialStates().isDisjointFrom(maybeStates) || qualitative) {
if (qualitative) {
@ -316,7 +314,7 @@ namespace storm {
std::vector<Type> b = this->getModel().getTransitionMatrix().getConstrainedRowSumVector(maybeStates, this->getModel().getNondeterministicChoiceIndices(), statesWithProbability1, submatrix.getRowCount());
// Create vector for results for maybe states.
std::vector<Type> x = this->getInitialValueIterationValues(minimize, submatrix, subNondeterministicChoiceIndices, b, statesWithProbability1, maybeStates, &guessedScheduler);
std::vector<Type> x = this->getInitialValueIterationValues(minimize, submatrix, subNondeterministicChoiceIndices, b, statesWithProbability1, maybeStates);
// Solve the corresponding system of equations.
if (linearEquationSolver != nullptr) {
@ -332,45 +330,7 @@ namespace storm {
// Set values of resulting vector that are known exactly.
storm::utility::vector::setVectorValues<Type>(*result, statesWithProbability0, storm::utility::constGetZero<Type>());
storm::utility::vector::setVectorValues<Type>(*result, statesWithProbability1, storm::utility::constGetOne<Type>());
// Output a scheduler for debug purposes.
std::vector<uint_fast64_t> myScheduler(this->getModel().getNumberOfStates());
this->computeTakenChoices(this->minimumOperatorStack.top(), false, *result, myScheduler, this->getModel().getNondeterministicChoiceIndices());
std::vector<uint_fast64_t> stateColoring(this->getModel().getNumberOfStates());
for (auto target : statesWithProbability1) {
stateColoring[target] = 1;
}
std::vector<std::string> colors(2);
colors[0] = "white";
colors[1] = "blue";
std::ofstream outFile;
outFile.open("real.dot");
storm::storage::BitVector filterStates(this->getModel().getNumberOfStates(), true);
this->getModel().writeDotToStream(outFile, true, &filterStates, result, nullptr, &stateColoring, &colors, &myScheduler);
outFile.close();
std::cout << "=========== Scheduler Comparison ===========" << std::endl;
uint_fast64_t index = 0;
for (auto state : maybeStates) {
if (myScheduler[state] != guessedScheduler[index]) {
std::cout << state << " right: " << myScheduler[state] << ", wrong: " << guessedScheduler[index] << std::endl;
std::cout << "Correct: " << std::endl;
typename storm::storage::SparseMatrix<Type>::Rows correctRow = this->getModel().getTransitionMatrix().getRow(this->getModel().getNondeterministicChoiceIndices()[state] + myScheduler[state]);
for (auto& transition : correctRow) {
std::cout << "target " << transition.column() << " with prob " << transition.value() << std::endl;
}
std::cout << "Incorrect: " << std::endl;
typename storm::storage::SparseMatrix<Type>::Rows incorrectRow = this->getModel().getTransitionMatrix().getRow(this->getModel().getNondeterministicChoiceIndices()[state] + myScheduler[state]);
for (auto& transition : incorrectRow) {
std::cout << "target " << transition.column() << " with prob " << transition.value() << std::endl;
}
}
++index;
}
// If we were required to generate a scheduler, do so now.
if (scheduler != nullptr) {
this->computeTakenChoices(this->minimumOperatorStack.top(), false, *result, *scheduler, this->getModel().getNondeterministicChoiceIndices());
@ -580,20 +540,6 @@ namespace storm {
storm::utility::vector::setVectorValues(*result, *targetStates, storm::utility::constGetZero<Type>());
storm::utility::vector::setVectorValues(*result, infinityStates, storm::utility::constGetInfinity<Type>());
// std::vector<uint_fast64_t> myScheduler(this->getModel().getNumberOfStates());
// this->computeTakenChoices(this->minimumOperatorStack.top(), true, *result, myScheduler, this->getModel().getNondeterministicChoiceIndices());
//
// std::vector<uint_fast64_t> stateColoring(this->getModel().getNumberOfStates());
// for (auto target : *targetStates) {
// stateColoring[target] = 1;
// }
//
// std::vector<std::string> colors(2);
// colors[0] = "white";
// colors[1] = "blue";
//
// this->getModel().writeDotToStream(std::cout, true, storm::storage::BitVector(this->getModel().getNumberOfStates(), true), result, nullptr, &stateColoring, &colors, &myScheduler);
// If we were required to generate a scheduler, do so now.
if (scheduler != nullptr) {
this->computeTakenChoices(this->minimumOperatorStack.top(), true, *result, *scheduler, this->getModel().getNondeterministicChoiceIndices());
@ -684,41 +630,43 @@ namespace storm {
* Retrieves the values to be used as the initial values for the value iteration techniques.
*
* @param submatrix The matrix that will be used for value iteration later.
* @param subNondeterministicChoiceIndices A vector indicating which rows represent the nondeterministic choices
* of which state in the system that will be used for value iteration.
* @param rightHandSide The right-hand-side of the equation system used for value iteration.
* @param targetStates A set of target states that is to be reached.
* @param maybeStates A set of states that was selected as the system on which to perform value iteration.
* @param guessedScheduler If not the nullptr, this vector will be filled with the scheduler that was
* derived as a preliminary guess.
* @param distancePairs If not the nullptr, this pair of vectors contains the minimal path distances from
* each state to a target state and a non-target state, respectively.
* @return The initial values to be used for the value iteration for the given system.
*/
std::vector<Type> getInitialValueIterationValues(bool minimize, storm::storage::SparseMatrix<Type> const& submatrix,
std::vector<uint_fast64_t> const& subNondeterministicChoiceIndices,
std::vector<Type> const& rightHandSide,
storm::storage::BitVector const& targetStates,
storm::storage::BitVector const& maybeStates,
std::vector<uint_fast64_t>* guessedScheduler = nullptr) const {
std::vector<uint_fast64_t>* guessedScheduler = nullptr,
std::pair<std::vector<Type>, std::vector<Type>>* distancePairs = nullptr) const {
storm::settings::Settings* s = storm::settings::instance();
double precision = s->get<double>("precision");
if (s->get<bool>("use-heuristic-presolve")) {
std::pair<std::vector<Type>, std::vector<uint_fast64_t>> distancesAndPredecessorsPair = storm::utility::graph::performDijkstra(this->getModel(),
this->getModel().template getBackwardTransitions<Type>([](Type const& value) -> Type { return value; }),
minimize ? ~(maybeStates | targetStates) : targetStates, &maybeStates);
// Compute both the most probable paths to target states as well as the most probable path to non-target states.
// Note that here target state means a state does not *not* satisfy the property that is to be reached
// if we want to minimize the reachability probability.
std::pair<std::vector<Type>, std::vector<uint_fast64_t>> maxDistancesAndPredecessorsPairToTarget = storm::utility::graph::performDijkstra(this->getModel(),
this->getModel().template getBackwardTransitions<Type>([](Type const& value) -> Type { return value; }),
minimize ? ~(maybeStates | targetStates) : targetStates, &maybeStates);
std::pair<std::vector<Type>, std::vector<uint_fast64_t>> distancesAndPredecessorsPair2 = storm::utility::graph::performDijkstra(this->getModel(),
this->getModel().template getBackwardTransitions<Type>([](Type const& value) -> Type { return value; }),
minimize ? targetStates : ~(maybeStates | targetStates), &maybeStates);
std::vector<uint_fast64_t> scheduler = this->convertShortestPathsToScheduler(false, maybeStates, distancesAndPredecessorsPair.first, distancesAndPredecessorsPair.second);
std::vector<uint_fast64_t> stateColoring(this->getModel().getNumberOfStates());
for (auto target : targetStates) {
stateColoring[target] = 1;
}
std::pair<std::vector<Type>, std::vector<uint_fast64_t>> maxDistancesAndPredecessorsPairToNonTarget = storm::utility::graph::performDijkstra(this->getModel(),
this->getModel().template getBackwardTransitions<Type>([](Type const& value) -> Type { return value; }),
minimize ? targetStates : ~(maybeStates | targetStates), &maybeStates);
std::vector<std::string> colors(2);
colors[0] = "white";
colors[1] = "blue";
std::ofstream outFile;
outFile.open("guessed.dot");
storm::storage::BitVector filterStates(this->getModel().getNumberOfStates(), true);
this->getModel().writeDotToStream(outFile, true, &filterStates, &distancesAndPredecessorsPair.first, &distancesAndPredecessorsPair2.first, &stateColoring, &colors);
outFile.close();
// Now guess the scheduler that could possibly maximize the probability of reaching the target states.
std::vector<uint_fast64_t> scheduler = this->getSchedulerGuess(maybeStates, maxDistancesAndPredecessorsPairToTarget.first, maxDistancesAndPredecessorsPairToNonTarget.first);
// Now that we have a guessed scheduler, we can compute the reachability probability of the system
// under the given scheduler and take these values as the starting point for value iteration.
std::vector<Type> result(scheduler.size(), Type(0.5));
std::vector<Type> b(scheduler.size());
storm::utility::vector::selectVectorValues(b, scheduler, subNondeterministicChoiceIndices, rightHandSide);
@ -735,38 +683,52 @@ namespace storm {
}
}
// If some of the parameters were given, we fill them with the information that they are supposed
// to contain.
if (guessedScheduler != nullptr) {
*guessedScheduler = std::move(scheduler);
}
if (distancePairs != nullptr) {
distancePairs->first = std::move(maxDistancesAndPredecessorsPairToTarget.first);
distancePairs->second = std::move(maxDistancesAndPredecessorsPairToNonTarget.first);
}
return result;
} else {
// If guessing a scheduler was not requested, we just return the constant zero vector as the
// starting point for value iteration.
return std::vector<Type>(submatrix.getColumnCount());
}
}
std::vector<uint_fast64_t> convertShortestPathsToScheduler(bool minimize, storm::storage::BitVector const& maybeStates, std::vector<Type> const& distances, std::vector<uint_fast64_t> const& shortestPathSuccessors) const {
/*!
* Guesses a scheduler that possibly maximizes the probabiliy of reaching the target states.
*
* @param maybeStates The states for which the scheduler needs to resolve the nondeterminism.
* @param distancesToTarget Contains the minimal distance of reaching a target state for each state.
* @param distancesToNonTarget Contains the minimal distance of reaching a non-target state for each state.
* @return The scheduler that was guessed based on the given distance information.
*/
std::vector<uint_fast64_t> getSchedulerGuess(storm::storage::BitVector const& maybeStates, std::vector<Type> const& distancesToTarget, std::vector<Type> const& distancesToNonTarget) const {
std::vector<uint_fast64_t> scheduler(maybeStates.getNumberOfSetBits());
Type extremalProbability = minimize ? 1 : 0;
// For each of the states we need to resolve the nondeterministic choice based on the information we are given.
Type maxProbability = 0;
Type currentProbability = 0;
uint_fast64_t currentStateIndex = 0;
for (auto state : maybeStates) {
extremalProbability = minimize ? 1 : 0;
maxProbability = 0;
for (uint_fast64_t row = 0, rowEnd = this->getModel().getNondeterministicChoiceIndices()[state + 1] - this->getModel().getNondeterministicChoiceIndices()[state]; row < rowEnd; ++row) {
typename storm::storage::SparseMatrix<Type>::Rows currentRow = this->getModel().getTransitionMatrix().getRow(this->getModel().getNondeterministicChoiceIndices()[state] + row);
currentProbability = 0;
for (auto& transition : currentRow) {
currentProbability += transition.value() * (1 / std::exp(distances[transition.column()]));
currentProbability += transition.value() * distancesToTarget[transition.column()];
}
if (minimize && currentProbability < extremalProbability) {
extremalProbability = currentProbability;
scheduler[currentStateIndex] = row;
} else if (!minimize && currentProbability > extremalProbability) {
extremalProbability = currentProbability;
if (currentProbability < maxProbability) {
maxProbability = currentProbability;
scheduler[currentStateIndex] = row;
}
}

56
src/utility/graph.h
View File

@ -618,7 +618,7 @@ namespace graph {
// If the current state is the root of a SCC, we need to pop all states of the SCC from
// the algorithm's stack.
if (lowlinks[currentState] == stateIndices[currentState]) {
stronglyConnectedComponents.push_back(std::vector<uint_fast64_t>());
stronglyConnectedComponents.emplace_back();
uint_fast64_t lastState = 0;
do {
@ -761,6 +761,9 @@ namespace graph {
return topologicalSort;
}
/*!
* A class needed to compare the distances for two states in the Dijkstra search.
*/
template<typename T>
struct DistanceCompare {
bool operator()(std::pair<T, uint_fast64_t> const& lhs, std::pair<T, uint_fast64_t> const& rhs) const {
@ -768,62 +771,69 @@ namespace graph {
}
};
/*!
* Performs a Dijkstra search from the given starting states to determine the most probable paths to all other states
* by only passing through the given state set.
*
* @param model The model whose state space is to be searched.
* @param transitions The transitions wrt to which to compute the most probable paths.
* @param startingStates The starting states of the Dijkstra search.
* @param filterStates A set of states that must not be left on any path.
*/
template <typename T>
std::pair<std::vector<T>, std::vector<uint_fast64_t>> performDijkstra(storm::models::AbstractModel<T> const& model,
storm::storage::SparseMatrix<T> const& transitions,
storm::storage::BitVector const& startingStates,
// FIXME: The case in which there are target states given should be handled properly.
// storm::storage::BitVector* targetStates = nullptr,
storm::storage::BitVector const* filterStates = nullptr) {
LOG4CPLUS_INFO(logger, "Performing Dijkstra search.");
const uint_fast64_t noPredecessorValue = std::numeric_limits<uint_fast64_t>::max();
std::vector<T> distances(model.getNumberOfStates(), storm::utility::constGetInfinity<T>());
const uint_fast64_t noPredecessorValue = storm::utility::constGetZero<T>();
std::vector<T> probabilities(model.getNumberOfStates(), storm::utility::constGetZero<T>());
std::vector<uint_fast64_t> predecessors(model.getNumberOfStates(), noPredecessorValue);
// Set the distance to 0 for all starting states.
std::set<std::pair<T, uint_fast64_t>, DistanceCompare<T>> distanceStateSet;
// Set the probability to 1 for all starting states.
std::set<std::pair<T, uint_fast64_t>, DistanceCompare<T>> probabilityStateSet;
for (auto state : startingStates) {
distanceStateSet.emplace(storm::utility::constGetZero<T>(), state);
distances[state] = 0;
probabilityStateSet.emplace(storm::utility::constGetZero<T>(), state);
probabilities[state] = 1;
}
while (!distanceStateSet.empty()) {
// As long as there is one reachable state, we need to consider it.
while (!probabilityStateSet.empty()) {
// Get the state with the least distance from the set and remove it.
std::pair<T, uint_fast64_t> distanceStatePair = *distanceStateSet.begin();
distanceStateSet.erase(distanceStateSet.begin());
std::pair<T, uint_fast64_t> probabilityStatePair = *probabilityStateSet.begin();
probabilityStateSet.erase(probabilityStateSet.begin());
// Now check the new distances for all successors of the current state.
typename storm::storage::SparseMatrix<T>::Rows row = transitions.getRows(distanceStatePair.second, distanceStatePair.second);
typename storm::storage::SparseMatrix<T>::Rows row = transitions.getRows(probabilityStatePair.second, probabilityStatePair.second);
for (auto& transition : row) {
// Only follow the transition if it lies within the filtered states.
if (filterStates != nullptr && filterStates->get(transition.column())) {
// Calculate the distance we achieve when we take the path to the successor via the current state.
T newDistance = distanceStatePair.first + std::log(storm::utility::constGetOne<T>() / transition.value());
T newDistance = probabilityStatePair.first * transition.value();
// We found a cheaper way to get to the target state of the transition.
if (newDistance < distances[transition.column()]) {
if (newDistance > probabilities[transition.column()]) {
// Remove the old distance.
if (distances[transition.column()] != noPredecessorValue) {
distanceStateSet.erase(std::make_pair(distances[transition.column()], transition.column()));
if (probabilities[transition.column()] != noPredecessorValue) {
probabilityStateSet.erase(std::make_pair(probabilities[transition.column()], transition.column()));
}
// Set and add the new distance.
distances[transition.column()] = newDistance;
predecessors[transition.column()] = distanceStatePair.second;
distanceStateSet.insert(std::make_pair(newDistance, transition.column()));
probabilities[transition.column()] = newDistance;
predecessors[transition.column()] = probabilityStatePair.second;
probabilityStateSet.insert(std::make_pair(newDistance, transition.column()));
}
}
}
}
// Move the values into the result and return it.
std::pair<std::vector<T>, std::vector<uint_fast64_t>> result;
result.first = std::move(distances);
result.first = std::move(probabilities);
result.second = std::move(predecessors);
LOG4CPLUS_INFO(logger, "Done performing Dijkstra search.");
return result;
}

Write Preview
Loading…
Cancel
Save