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

Cleaned interfaces of models from std::shared_ptr. Improved some code in graph utility.

main
dehnert 12 years ago
parent
4b68cb7bbf
commit
f44f0ce410
12 changed files with 291 additions and 245 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. 30
      src/modelchecker/prctl/AbstractModelChecker.h
  2. 233
      src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
  3. 36
      src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
  4. 22
      src/models/AbstractModel.h
  5. 4
      src/models/AbstractNondeterministicModel.h
  6. 4
      src/models/Ctmdp.h
  7. 10
      src/models/Dtmc.h
  8. 4
      src/models/Mdp.h
  9. 27
      src/storage/BitVector.h
  10. 2
      src/storage/SparseMatrix.h
  11. 158
      src/utility/graph.h
  12. 6
      test/functional/parser/ParseMdpTest.cpp

30
src/modelchecker/prctl/AbstractModelChecker.h
View File

@ -86,7 +86,8 @@ public:
/*!
* Returns a pointer to the model checker object that is of the requested type as given by the template parameters.
* @returns A pointer to the model checker object that is of the requested type as given by the template parameters.
*
* @return A pointer to the model checker object that is of the requested type as given by the template parameters.
* If the model checker is not of the requested type, type casting will fail and result in an exception.
*/
template <template <class T> class Target>
@ -105,7 +106,7 @@ public:
* Retrieves the model associated with this model checker as a constant reference to an object of the type given
* by the template parameter.
*
* @returns A constant reference of the specified type to the model associated with this model checker. If the model
* @return A constant reference of the specified type to the model associated with this model checker. If the model
* is not of the requested type, type casting will fail and result in an exception.
*/
template <class Model>
@ -118,6 +119,15 @@ public:
throw bc;
}
}
/*!
* Retrieves the initial states of the model.
*
* @return A bit vector that represents the initial states of the model.
*/
storm::storage::BitVector const& getInitialStates() const {
return model.getLabeledStates("init");
}
/*!
* Checks the given abstract prctl formula on the model and prints the result (depending on the actual type of the formula)
@ -148,7 +158,7 @@ public:
result = stateFormula.check(*this);
LOG4CPLUS_INFO(logger, "Result for initial states:");
std::cout << "Result for initial states:" << std::endl;
for (auto initialState : model.getLabeledStates("init")) {
for (auto initialState : this->getInitialStates()) {
LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result->get(initialState) ? "satisfied" : "not satisfied"));
std::cout << "\t" << initialState << ": " << result->get(initialState) << std::endl;
}
@ -178,7 +188,7 @@ public:
result = this->checkNoBoundOperator(noBoundFormula);
LOG4CPLUS_INFO(logger, "Result for initial states:");
std::cout << "Result for initial states:" << std::endl;
for (auto initialState : model.getLabeledStates("init")) {
for (auto initialState : this->getInitialStates()) {
LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (*result)[initialState]);
std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl;
}
@ -196,7 +206,7 @@ public:
* Checks the given formula consisting of a single atomic proposition.
*
* @param formula The formula to be checked.
* @returns The set of states satisfying the formula represented by a bit vector.
* @return The set of states satisfying the formula represented by a bit vector.
*/
storm::storage::BitVector* checkAp(storm::property::prctl::Ap<Type> const& formula) const {
if (formula.getAp() == "true") {
@ -217,7 +227,7 @@ public:
* Checks the given formula that is a logical "and" of two formulae.
*
* @param formula The formula to be checked.
* @returns The set of states satisfying the formula represented by a bit vector.
* @return The set of states satisfying the formula represented by a bit vector.
*/
storm::storage::BitVector* checkAnd(storm::property::prctl::And<Type> const& formula) const {
storm::storage::BitVector* result = formula.getLeft().check(*this);
@ -231,7 +241,7 @@ public:
* Checks the given formula that is a logical "or" of two formulae.
*
* @param formula The formula to check.
* @returns The set of states satisfying the formula represented by a bit vector.
* @return The set of states satisfying the formula represented by a bit vector.
*/
virtual storm::storage::BitVector* checkOr(storm::property::prctl::Or<Type> const& formula) const {
storm::storage::BitVector* result = formula.getLeft().check(*this);
@ -245,7 +255,7 @@ public:
* Checks the given formula that is a logical "not" of a sub-formula.
*
* @param formula The formula to check.
* @returns The set of states satisfying the formula represented by a bit vector.
* @return The set of states satisfying the formula represented by a bit vector.
*/
storm::storage::BitVector* checkNot(const storm::property::prctl::Not<Type>& formula) const {
storm::storage::BitVector* result = formula.getChild().check(*this);
@ -258,7 +268,7 @@ public:
* Checks the given formula that is a P operator over a path formula featuring a value bound.
*
* @param formula The formula to check.
* @returns The set of states satisfying the formula represented by a bit vector.
* @return The set of states satisfying the formula represented by a bit vector.
*/
storm::storage::BitVector* checkProbabilisticBoundOperator(storm::property::prctl::ProbabilisticBoundOperator<Type> const& formula) const {
// First, we need to compute the probability for satisfying the path formula for each state.
@ -284,7 +294,7 @@ public:
* Checks the given formula that is an R operator over a reward formula featuring a value bound.
*
* @param formula The formula to check.
* @returns The set of states satisfying the formula represented by a bit vector.
* @return The set of states satisfying the formula represented by a bit vector.
*/
storm::storage::BitVector* checkRewardBoundOperator(const storm::property::prctl::RewardBoundOperator<Type>& formula) const {
// First, we need to compute the probability for satisfying the path formula for each state.

233
src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
View File

@ -88,31 +88,40 @@ public:
// First, we need to compute the states that satisfy the sub-formulas of the bounded until-formula.
storm::storage::BitVector* leftStates = formula.getLeft().check(*this);
storm::storage::BitVector* rightStates = formula.getRight().check(*this);
std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
// If we identify the states that have probability 0 of reaching the target states, we can exclude them in the
// further analysis.
storm::storage::BitVector maybeStates = storm::utility::graph::performProbGreater0(this->getModel(), *leftStates, *rightStates, true, formula.getBound());
// Now we can eliminate the rows and columns from the original transition probability matrix that have probability 0.
storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates);
// Compute the new set of target states in the reduced system.
storm::storage::BitVector rightStatesInReducedSystem = maybeStates % *rightStates;
storm::storage::BitVector statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(this->getModel(), *leftStates, *rightStates, true, formula.getBound());
LOG4CPLUS_INFO(logger, "Found " << statesWithProbabilityGreater0.getNumberOfSetBits() << " 'maybe' states.");
// Make all rows absorbing that satisfy the second sub-formula.
submatrix.makeRowsAbsorbing(rightStatesInReducedSystem);
// Create the vector with which to multiply.
std::vector<Type> subresult(maybeStates.getNumberOfSetBits());
storm::utility::vector::setVectorValues(subresult, rightStatesInReducedSystem, storm::utility::constGetOne<Type>());
// Perform the matrix vector multiplication as often as required by the formula bound.
this->performMatrixVectorMultiplication(submatrix, subresult, nullptr, formula.getBound());
// Create result vector and set its values accordingly.
std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
storm::utility::vector::setVectorValues(*result, maybeStates, subresult);
storm::utility::vector::setVectorValues<Type>(*result, ~maybeStates, storm::utility::constGetZero<Type>());
// Check if we already know the result (i.e. probability 0) for all initial states and
// don't compute anything in this case.
if (this->getInitialStates().isSubsetOf(~statesWithProbabilityGreater0)) {
LOG4CPLUS_INFO(logger, "The probabilities for the initial states were determined in a preprocessing step."
<< " No exact probabilities were computed.");
} else { // Otherwise, we have have to compute the probabilities.
// Now we can eliminate the rows and columns from the original transition probability matrix that have probability 0.
storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(statesWithProbabilityGreater0);
// Compute the new set of target states in the reduced system.
storm::storage::BitVector rightStatesInReducedSystem = statesWithProbabilityGreater0 % *rightStates;
// Make all rows absorbing that satisfy the second sub-formula.
submatrix.makeRowsAbsorbing(rightStatesInReducedSystem);
// Create the vector with which to multiply.
std::vector<Type> subresult(statesWithProbabilityGreater0.getNumberOfSetBits());
storm::utility::vector::setVectorValues(subresult, rightStatesInReducedSystem, storm::utility::constGetOne<Type>());
// Perform the matrix vector multiplication as often as required by the formula bound.
this->performMatrixVectorMultiplication(submatrix, subresult, nullptr, formula.getBound());
// Create result vector and set its values accordingly.
storm::utility::vector::setVectorValues(*result, statesWithProbabilityGreater0, subresult);
storm::utility::vector::setVectorValues<Type>(*result, ~statesWithProbabilityGreater0, storm::utility::constGetZero<Type>());
}
// Delete obsolete intermediates and return result.
delete leftStates;
@ -143,7 +152,7 @@ public:
delete nextStates;
// Perform one single matrix-vector multiplication.
this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result);
this->performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), *result);
// Return result.
return result;
@ -231,42 +240,49 @@ public:
delete rightStates;
// Perform some logging.
storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1);
LOG4CPLUS_INFO(logger, "Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states.");
LOG4CPLUS_INFO(logger, "Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states.");
storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1);
LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
// Create resulting vector.
std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
// Only try to solve system if there are states for which the probability is unknown.
uint_fast64_t maybeStatesSetBitCount = maybeStates.getNumberOfSetBits();
if (maybeStatesSetBitCount > 0 && !qualitative) {
// Now we can eliminate the rows and columns from the original transition probability matrix.
storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates);
// Converting the matrix from the fixpoint notation to the form needed for the equation
// system. That is, we go from x = A*x + b to (I-A)x = b.
submatrix.convertToEquationSystem();
// Initialize the x vector with 0.5 for each element. This is the initial guess for
// the iterative solvers. It should be safe as for all 'maybe' states we know that the
// probability is strictly larger than 0.
std::vector<Type> x(maybeStatesSetBitCount, Type(0.5));
// Prepare the right-hand side of the equation system. For entry i this corresponds to
// the accumulated probability of going from state i to some 'yes' state.
std::vector<Type> b = this->getModel().getTransitionMatrix()->getConstrainedRowSumVector(maybeStates, statesWithProbability1);
// Now solve the created system of linear equations.
this->solveEquationSystem(submatrix, x, b);
// Set values of resulting vector according to result.
storm::utility::vector::setVectorValues<Type>(*result, maybeStates, x);
} else if (qualitative) {
// If we only need a qualitative result, we can safely assume that the results will only be compared to
// bounds which are either 0 or 1. Setting the value to 0.5 is thus safe.
storm::utility::vector::setVectorValues<Type>(*result, maybeStates, Type(0.5));
}
// Check whether we need to compute exact probabilities for some states.
if (this->getInitialStates().isDisjointFrom(maybeStates) || qualitative) {
if (qualitative) {
LOG4CPLUS_INFO(logger, "The formula was checked qualitatively. No exact probabilities were computed.");
} else {
LOG4CPLUS_INFO(logger, "The probabilities for the initial states were determined in a preprocessing step."
<< " No exact probabilities were computed.");
}
// Set the values for all maybe-states to 0.5 to indicate that their probability values
// are neither 0 nor 1.
storm::utility::vector::setVectorValues<Type>(*result, maybeStates, Type(0.5));
} else {
// Otherwise, we have have to compute the probabilities.
// First, we can eliminate the rows and columns from the original transition probability matrix.
storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(maybeStates);
// Converting the matrix from the fixpoint notation to the form needed for the equation
// system. That is, we go from x = A*x + b to (I-A)x = b.
submatrix.convertToEquationSystem();
// Initialize the x vector with 0.5 for each element. This is the initial guess for
// the iterative solvers. It should be safe as for all 'maybe' states we know that the
// probability is strictly larger than 0.
std::vector<Type> x(maybeStates.getNumberOfSetBits(), Type(0.5));
// Prepare the right-hand side of the equation system. For entry i this corresponds to
// the accumulated probability of going from state i to some 'yes' state.
std::vector<Type> b = this->getModel().getTransitionMatrix().getConstrainedRowSumVector(maybeStates, statesWithProbability1);
// Now solve the created system of linear equations.
this->solveEquationSystem(submatrix, x, b);
// Set values of resulting vector according to result.
storm::utility::vector::setVectorValues<Type>(*result, maybeStates, x);
}
// Set values of resulting vector that are known exactly.
storm::utility::vector::setVectorValues<Type>(*result, statesWithProbability0, storm::utility::constGetZero<Type>());
@ -294,10 +310,10 @@ public:
}
// Initialize result to state rewards of the model.
std::vector<Type>* result = new std::vector<Type>(*this->getModel().getStateRewardVector());
std::vector<Type>* result = new std::vector<Type>(this->getModel().getStateRewardVector());
// Perform the actual matrix-vector multiplication as long as the bound of the formula is met.
this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, nullptr, formula.getBound());
this->performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), *result, nullptr, formula.getBound());
// Return result.
return result;
@ -324,24 +340,24 @@ public:
// Compute the reward vector to add in each step based on the available reward models.
std::vector<Type> totalRewardVector;
if (this->getModel().hasTransitionRewards()) {
totalRewardVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix());
totalRewardVector = this->getModel().getTransitionMatrix().getPointwiseProductRowSumVector(this->getModel().getTransitionRewardMatrix());
if (this->getModel().hasStateRewards()) {
gmm::add(*this->getModel().getStateRewardVector(), totalRewardVector);
storm::utility::vector::addVectorsInPlace(totalRewardVector, this->getModel().getStateRewardVector());
}
} else {
totalRewardVector = std::vector<Type>(*this->getModel().getStateRewardVector());
totalRewardVector = std::vector<Type>(this->getModel().getStateRewardVector());
}
// Initialize result to either the state rewards of the model or the null vector.
std::vector<Type>* result = nullptr;
if (this->getModel().hasStateRewards()) {
result = new std::vector<Type>(*this->getModel().getStateRewardVector());
result = new std::vector<Type>(this->getModel().getStateRewardVector());
} else {
result = new std::vector<Type>(this->getModel().getNumberOfStates());
}
// Perform the actual matrix-vector multiplication as long as the bound of the formula is met.
this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, &totalRewardVector, formula.getBound());
this->performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), *result, &totalRewardVector, formula.getBound());
// Return result.
return result;
@ -372,56 +388,67 @@ public:
storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true);
storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(this->getModel(), trueStates, *targetStates);
infinityStates.complement();
LOG4CPLUS_INFO(logger, "Found " << infinityStates.getNumberOfSetBits() << " 'infinity' states.");
// Create resulting vector.
std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
// Check whether there are states for which we have to compute the result.
storm::storage::BitVector maybeStates = ~(*targetStates) & ~infinityStates;
const int maybeStatesSetBitCount = maybeStates.getNumberOfSetBits();
if (maybeStatesSetBitCount > 0) {
// Now we can eliminate the rows and columns from the original transition probability matrix.
storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates);
// Converting the matrix from the fixpoint notation to the form needed for the equation
// system. That is, we go from x = A*x + b to (I-A)x = b.
submatrix.convertToEquationSystem();
// Initialize the x vector with 1 for each element. This is the initial guess for
// the iterative solvers.
std::vector<Type> x(maybeStatesSetBitCount, storm::utility::constGetOne<Type>());
// Prepare the right-hand side of the equation system.
std::vector<Type> b(maybeStatesSetBitCount);
if (this->getModel().hasTransitionRewards()) {
// If a transition-based reward model is available, we initialize the right-hand
// side to the vector resulting from summing the rows of the pointwise product
// of the transition probability matrix and the transition reward matrix.
std::vector<Type> pointwiseProductRowSumVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix());
storm::utility::vector::selectVectorValues(b, maybeStates, pointwiseProductRowSumVector);
if (this->getModel().hasStateRewards()) {
// If a state-based reward model is also available, we need to add this vector
// as well. As the state reward vector contains entries not just for the states
// that we still consider (i.e. maybeStates), we need to extract these values
// first.
std::vector<Type> subStateRewards(maybeStatesSetBitCount);
storm::utility::vector::selectVectorValues(subStateRewards, maybeStates, *this->getModel().getStateRewardVector());
gmm::add(subStateRewards, b);
}
} else {
// If only a state-based reward model is available, we take this vector as the
// right-hand side. As the state reward vector contains entries not just for the
// states that we still consider (i.e. maybeStates), we need to extract these values
// first.
storm::utility::vector::selectVectorValues(b, maybeStates, *this->getModel().getStateRewardVector());
}
// Now solve the resulting equation system.
this->solveEquationSystem(submatrix, x, b);
// Set values of resulting vector according to result.
storm::utility::vector::setVectorValues<Type>(*result, maybeStates, x);
}
// Check whether we need to compute exact rewards for some states.
if (this->getInitialStates().isDisjointFrom(maybeStates)) {
LOG4CPLUS_INFO(logger, "The rewards for the initial states were determined in a preprocessing step."
<< " No exact rewards were computed.");
// Set the values for all maybe-states to 1 to indicate that their reward values
// are neither 0 nor infinity.
storm::utility::vector::setVectorValues<Type>(*result, maybeStates, storm::utility::constGetOne<Type>());
} else {
// In this case we have to compute the reward values for the remaining states.
const int maybeStatesSetBitCount = maybeStates.getNumberOfSetBits();
// Now we can eliminate the rows and columns from the original transition probability matrix.
storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(maybeStates);
// Converting the matrix from the fixpoint notation to the form needed for the equation
// system. That is, we go from x = A*x + b to (I-A)x = b.
submatrix.convertToEquationSystem();
// Initialize the x vector with 1 for each element. This is the initial guess for
// the iterative solvers.
std::vector<Type> x(maybeStatesSetBitCount, storm::utility::constGetOne<Type>());
// Prepare the right-hand side of the equation system.
std::vector<Type> b(maybeStatesSetBitCount);
if (this->getModel().hasTransitionRewards()) {
// If a transition-based reward model is available, we initialize the right-hand
// side to the vector resulting from summing the rows of the pointwise product
// of the transition probability matrix and the transition reward matrix.
std::vector<Type> pointwiseProductRowSumVector = this->getModel().getTransitionMatrix().getPointwiseProductRowSumVector(this->getModel().getTransitionRewardMatrix());
storm::utility::vector::selectVectorValues(b, maybeStates, pointwiseProductRowSumVector);
if (this->getModel().hasStateRewards()) {
// If a state-based reward model is also available, we need to add this vector
// as well. As the state reward vector contains entries not just for the states
// that we still consider (i.e. maybeStates), we need to extract these values
// first.
std::vector<Type> subStateRewards(maybeStatesSetBitCount);
storm::utility::vector::selectVectorValues(subStateRewards, maybeStates, this->getModel().getStateRewardVector());
storm::utility::vector::addVectorsInPlace(b, subStateRewards);
}
} else {
// If only a state-based reward model is available, we take this vector as the
// right-hand side. As the state reward vector contains entries not just for the
// states that we still consider (i.e. maybeStates), we need to extract these values
// first.
storm::utility::vector::selectVectorValues(b, maybeStates, this->getModel().getStateRewardVector());
}
// Now solve the resulting equation system.
this->solveEquationSystem(submatrix, x, b);
// Set values of resulting vector according to result.
storm::utility::vector::setVectorValues<Type>(*result, maybeStates, x);
}
// Set values of resulting vector that are known exactly.
storm::utility::vector::setVectorValues(*result, *targetStates, storm::utility::constGetZero<Type>());

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

@ -104,7 +104,7 @@ public:
}
// Now we can eliminate the rows and columns from the original transition probability matrix that have probability 0.
storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates, *this->getModel().getNondeterministicChoiceIndices());
storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(maybeStates, this->getModel().getNondeterministicChoiceIndices());
// Get the "new" nondeterministic choice indices for the submatrix.
std::vector<uint_fast64_t> subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates);
@ -154,7 +154,7 @@ public:
// Delete obsolete sub-result.
delete nextStates;
this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, *this->getModel().getNondeterministicChoiceIndices());
this->performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), *result, this->getModel().getNondeterministicChoiceIndices());
// Return result.
return result;
@ -259,7 +259,7 @@ public:
if (maybeStatesSetBitCount > 0) {
// First, we can eliminate the rows and columns from the original transition probability matrix for states
// whose probabilities are already known.
storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates, *this->getModel().getNondeterministicChoiceIndices());
storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(maybeStates, this->getModel().getNondeterministicChoiceIndices());
// Get the "new" nondeterministic choice indices for the submatrix.
std::vector<uint_fast64_t> subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates);
@ -269,7 +269,7 @@ public:
// Prepare the right-hand side of the equation system. For entry i this corresponds to
// the accumulated probability of going from state i to some 'yes' state.
std::vector<Type> b = this->getModel().getTransitionMatrix()->getConstrainedRowSumVector(maybeStates, *this->getModel().getNondeterministicChoiceIndices(), statesWithProbability1, submatrix.getRowCount());
std::vector<Type> b = this->getModel().getTransitionMatrix().getConstrainedRowSumVector(maybeStates, this->getModel().getNondeterministicChoiceIndices(), statesWithProbability1, submatrix.getRowCount());
// Solve the corresponding system of equations.
this->solveEquationSystem(submatrix, x, b, subNondeterministicChoiceIndices);
@ -304,9 +304,9 @@ public:
}
// Initialize result to state rewards of the model.
std::vector<Type>* result = new std::vector<Type>(*this->getModel().getStateRewardVector());
std::vector<Type>* result = new std::vector<Type>(this->getModel().getStateRewardVector());
this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, *this->getModel().getNondeterministicChoiceIndices(), nullptr, formula.getBound());
this->performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), *result, this->getModel().getNondeterministicChoiceIndices(), nullptr, formula.getBound());
// Return result.
return result;
@ -333,23 +333,23 @@ public:
// Compute the reward vector to add in each step based on the available reward models.
std::vector<Type> totalRewardVector;
if (this->getModel().hasTransitionRewards()) {
totalRewardVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix());
totalRewardVector = this->getModel().getTransitionMatrix().getPointwiseProductRowSumVector(this->getModel().getTransitionRewardMatrix());
if (this->getModel().hasStateRewards()) {
gmm::add(*this->getModel().getStateRewardVector(), totalRewardVector);
storm::utility::vector::addVectorsInPlace(totalRewardVector, this->getModel().getStateRewardVector());
}
} else {
totalRewardVector = std::vector<Type>(*this->getModel().getStateRewardVector());
totalRewardVector = std::vector<Type>(this->getModel().getStateRewardVector());
}
// Initialize result to either the state rewards of the model or the null vector.
std::vector<Type>* result = nullptr;
if (this->getModel().hasStateRewards()) {
result = new std::vector<Type>(*this->getModel().getStateRewardVector());
result = new std::vector<Type>(this->getModel().getStateRewardVector());
} else {
result = new std::vector<Type>(this->getModel().getNumberOfStates());
}
this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, *this->getModel().getNondeterministicChoiceIndices(), &totalRewardVector, formula.getBound());
this->performMatrixVectorMultiplication(this->getModel().getTransitionMatrix(), *result, this->getModel().getNondeterministicChoiceIndices(), &totalRewardVector, formula.getBound());
// Delete temporary variables and return result.
return result;
@ -399,7 +399,7 @@ public:
if (maybeStatesSetBitCount > 0) {
// First, we can eliminate the rows and columns from the original transition probability matrix for states
// whose probabilities are already known.
storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates, *this->getModel().getNondeterministicChoiceIndices());
storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(maybeStates, this->getModel().getNondeterministicChoiceIndices());
// Get the "new" nondeterministic choice indices for the submatrix.
std::vector<uint_fast64_t> subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates);
@ -415,8 +415,8 @@ public:
// If a transition-based reward model is available, we initialize the right-hand
// side to the vector resulting from summing the rows of the pointwise product
// of the transition probability matrix and the transition reward matrix.
std::vector<Type> pointwiseProductRowSumVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix());
storm::utility::vector::selectVectorValues(b, maybeStates, *this->getModel().getNondeterministicChoiceIndices(), pointwiseProductRowSumVector);
std::vector<Type> pointwiseProductRowSumVector = this->getModel().getTransitionMatrix().getPointwiseProductRowSumVector(this->getModel().getTransitionRewardMatrix());
storm::utility::vector::selectVectorValues(b, maybeStates, this->getModel().getNondeterministicChoiceIndices(), pointwiseProductRowSumVector);
if (this->getModel().hasStateRewards()) {
// If a state-based reward model is also available, we need to add this vector
@ -424,15 +424,15 @@ public:
// that we still consider (i.e. maybeStates), we need to extract these values
// first.
std::vector<Type> subStateRewards(b.size());
storm::utility::vector::selectVectorValuesRepeatedly(subStateRewards, maybeStates, *this->getModel().getNondeterministicChoiceIndices(), *this->getModel().getStateRewardVector());
gmm::add(subStateRewards, b);
storm::utility::vector::selectVectorValuesRepeatedly(subStateRewards, maybeStates, this->getModel().getNondeterministicChoiceIndices(), this->getModel().getStateRewardVector());
storm::utility::vector::addVectorsInPlace(b, subStateRewards);
}
} else {
// If only a state-based reward model is available, we take this vector as the
// right-hand side. As the state reward vector contains entries not just for the
// states that we still consider (i.e. maybeStates), we need to extract these values
// first.
storm::utility::vector::selectVectorValuesRepeatedly(b, maybeStates, *this->getModel().getNondeterministicChoiceIndices(), *this->getModel().getStateRewardVector());
storm::utility::vector::selectVectorValuesRepeatedly(b, maybeStates, this->getModel().getNondeterministicChoiceIndices(), this->getModel().getStateRewardVector());
}
// Solve the corresponding system of equations.
@ -573,7 +573,7 @@ private:
*/
std::vector<uint_fast64_t> computeNondeterministicChoiceIndicesForConstraint(storm::storage::BitVector const& constraint) const {
// First, get a reference to the full nondeterministic choice indices.
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = *this->getModel().getNondeterministicChoiceIndices();
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices();
// Reserve the known amount of slots for the resulting vector.
std::vector<uint_fast64_t> subNondeterministicChoiceIndices(constraint.getNumberOfSetBits() + 1);

22
src/models/AbstractModel.h
View File

@ -208,7 +208,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
* @return The size of the state space of the model.
*/
virtual uint_fast64_t getNumberOfStates() const {
return this->getTransitionMatrix()->getColumnCount();
return this->getTransitionMatrix().getColumnCount();
}
/*!
@ -216,7 +216,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
* @return The number of (non-zero) transitions of the model.
*/
virtual uint_fast64_t getNumberOfTransitions() const {
return this->getTransitionMatrix()->getNonZeroEntryCount();
return this->getTransitionMatrix().getNonZeroEntryCount();
}
/*!
@ -245,24 +245,24 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
* @return A pointer to the matrix representing the transition probability
* function.
*/
std::shared_ptr<storm::storage::SparseMatrix<T>> getTransitionMatrix() const {
return transitionMatrix;
storm::storage::SparseMatrix<T> const& getTransitionMatrix() const {
return *transitionMatrix;
}
/*!
* Returns a pointer to the matrix representing the transition rewards.
* @return A pointer to the matrix representing the transition rewards.
*/
std::shared_ptr<storm::storage::SparseMatrix<T>> getTransitionRewardMatrix() const {
return transitionRewardMatrix;
storm::storage::SparseMatrix<T> const& getTransitionRewardMatrix() const {
return *transitionRewardMatrix;
}
/*!
* Returns a pointer to the vector representing the state rewards.
* @return A pointer to the vector representing the state rewards.
*/
std::shared_ptr<std::vector<T>> getStateRewardVector() const {
return stateRewardVector;
std::vector<T> const& getStateRewardVector() const {
return *stateRewardVector;
}
/*!
@ -277,8 +277,8 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
* Returns the state labeling associated with this model.
* @return The state labeling associated with this model.
*/
std::shared_ptr<storm::models::AtomicPropositionsLabeling> getStateLabeling() const {
return stateLabeling;
storm::models::AtomicPropositionsLabeling const& getStateLabeling() const {
return *stateLabeling;
}
/*!
@ -323,7 +323,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
out << "Model type: \t\t" << this->getType() << std::endl;
out << "States: \t\t" << this->getNumberOfStates() << std::endl;
out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl;
this->getStateLabeling()->printAtomicPropositionsInformationToStream(out);
this->getStateLabeling().printAtomicPropositionsInformationToStream(out);
out << "Size in memory: \t"
<< (this->getSizeInMemory())/1024 << " kbytes" << std::endl;
out << "-------------------------------------------------------------- "

4
src/models/AbstractNondeterministicModel.h
View File

@ -73,8 +73,8 @@ class AbstractNondeterministicModel: public AbstractModel<T> {
* @param the vector indicating which matrix rows represent non-deterministic choices
* of a certain state.
*/
std::shared_ptr<std::vector<uint_fast64_t>> getNondeterministicChoiceIndices() const {
return nondeterministicChoiceIndices;
std::vector<uint_fast64_t> const& getNondeterministicChoiceIndices() const {
return *nondeterministicChoiceIndices;
}
/*!

4
src/models/Ctmdp.h
View File

@ -84,8 +84,8 @@ private:
// Get the settings object to customize linear solving.
storm::settings::Settings* s = storm::settings::instance();
double precision = s->get<double>("precision");
for (uint_fast64_t row = 0; row < this->getTransitionMatrix()->getRowCount(); row++) {
T sum = this->getTransitionMatrix()->getRowSum(row);
for (uint_fast64_t row = 0; row < this->getTransitionMatrix().getRowCount(); row++) {
T sum = this->getTransitionMatrix().getRowSum(row);
if (sum == 0) continue;
if (std::abs(sum - 1) > precision) return false;
}

10
src/models/Dtmc.h
View File

@ -49,8 +49,8 @@ public:
LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
}
if (this->getTransitionRewardMatrix() != nullptr) {
if (!this->getTransitionRewardMatrix()->containsAllPositionsOf(*this->getTransitionMatrix())) {
if (this->hasTransitionRewards()) {
if (!this->getTransitionRewardMatrix().containsAllPositionsOf(this->getTransitionMatrix())) {
LOG4CPLUS_ERROR(logger, "Transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist.");
throw storm::exceptions::InvalidArgumentException() << "There are transition rewards for nonexistent transitions.";
}
@ -89,14 +89,14 @@ private:
storm::settings::Settings* s = storm::settings::instance();
double precision = s->get<double>("precision");
if (this->getTransitionMatrix()->getRowCount() != this->getTransitionMatrix()->getColumnCount()) {
if (this->getTransitionMatrix().getRowCount() != this->getTransitionMatrix().getColumnCount()) {
// not square
LOG4CPLUS_ERROR(logger, "Probability matrix is not square.");
return false;
}
for (uint_fast64_t row = 0; row < this->getTransitionMatrix()->getRowCount(); ++row) {
T sum = this->getTransitionMatrix()->getRowSum(row);
for (uint_fast64_t row = 0; row < this->getTransitionMatrix().getRowCount(); ++row) {
T sum = this->getTransitionMatrix().getRowSum(row);
if (sum == 0) {
LOG4CPLUS_ERROR(logger, "Row " << row << " has sum 0");
return false;

4
src/models/Mdp.h
View File

@ -86,8 +86,8 @@ private:
// Get the settings object to customize linear solving.
storm::settings::Settings* s = storm::settings::instance();
double precision = s->get<double>("precision");
for (uint_fast64_t row = 0; row < this->getTransitionMatrix()->getRowCount(); row++) {
T sum = this->getTransitionMatrix()->getRowSum(row);
for (uint_fast64_t row = 0; row < this->getTransitionMatrix().getRowCount(); row++) {
T sum = this->getTransitionMatrix().getRowSum(row);
if (sum == 0) continue;
if (std::abs(sum - 1) > precision) {
return false;

27
src/storage/BitVector.h
View File

@ -420,6 +420,7 @@ public:
* Performs a logical "implies" with the given bit vector. In case the sizes of the bit vectors
* do not match, only the matching portion is considered and the overlapping bits
* are set to 0.
*
* @param bv A reference to the bit vector to use for the operation.
* @return A bit vector corresponding to the logical "implies" of the two bit vectors.
*/
@ -439,14 +440,15 @@ public:
/*!
* Checks whether all bits that are set in the current bit vector are also set in the given bit
* vector.
*
* @param bv A reference to the bit vector whose bits are (possibly) a superset of the bits of
* the current bit vector.
* @returns True iff all bits that are set in the current bit vector are also set in the given bit
* @return True iff all bits that are set in the current bit vector are also set in the given bit
* vector.
*/
bool isContainedIn(BitVector const& bv) const {
bool isSubsetOf(BitVector const& bv) const {
for (uint_fast64_t i = 0; i < this->bucketCount; ++i) {
if ((this->bucketArray[i] & bv.bucketArray[i]) != bv.bucketArray[i]) {
if ((this->bucketArray[i] & bv.bucketArray[i]) != this->bucketArray[i]) {
return false;
}
}
@ -456,6 +458,7 @@ public:
/*!
* Checks whether none of the bits that are set in the current bit vector are also set in the
* given bit vector.
*
* @param bv A reference to the bit vector whose bits are (possibly) disjoint from the bits in
* the current bit vector.
* @returns True iff none of the bits that are set in the current bit vector are also set in the
@ -504,9 +507,25 @@ public:
return result;
}
/*!
* Returns a list containing all indices such that the bits at these indices are set to true
* in the bit vector.
*
* @return A vector of indices of set bits in the bit vector.
*/
std::vector<uint_fast64_t> getSetIndicesList() const {
std::vector<uint_fast64_t> result;
result.reserve(this->getNumberOfSetBits());
for (auto index : *this) {
result.push_back(index);
}
return result;
}
/*!
* Adds all indices of bits set to one to the provided list.
* Adds all indices of bits set to one to the given list.
*
* @param list The list to which to append the indices.
*/
void addSetIndicesToVector(std::vector<uint_fast64_t>& vector) const {

2
src/storage/SparseMatrix.h
View File

@ -920,7 +920,7 @@ public:
* @returns A vector containing the sum of the elements in each row of the matrix resulting from
* pointwise multiplication of the current matrix with the given matrix.
*/
std::vector<T> getPointwiseProductRowSumVector(storm::storage::SparseMatrix<T> const& otherMatrix) {
std::vector<T> getPointwiseProductRowSumVector(storm::storage::SparseMatrix<T> const& otherMatrix) const {
// Prepare result.
std::vector<T> result(rowCount, storm::utility::constGetZero<T>());

158
src/utility/graph.h
View File

@ -46,10 +46,8 @@ namespace graph {
// Add all psi states as the already satisfy the condition.
statesWithProbabilityGreater0 |= psiStates;
// Initialize the stack used for the BFS with the states.
std::vector<uint_fast64_t> stack;
stack.reserve(model.getNumberOfStates());
psiStates.addSetIndicesToVector(stack);
// Initialize the stack used for the DFS with the states.
std::vector<uint_fast64_t> stack = psiStates.getSetIndicesList();
// Initialize the stack for the step bound, if the number of steps is bounded.
std::vector<uint_fast64_t> stepStack;
@ -63,7 +61,7 @@ namespace graph {
}
}
// Perform the actual BFS.
// Perform the actual DFS.
uint_fast64_t currentState, currentStepBound;
while (!stack.empty()) {
currentState = stack.back();
@ -74,17 +72,17 @@ namespace graph {
stepStack.pop_back();
}
for (auto it = backwardTransitions.constColumnIteratorBegin(currentState); it != backwardTransitions.constColumnIteratorEnd(currentState); ++it) {
if (phiStates.get(*it) && (!statesWithProbabilityGreater0.get(*it) || (useStepBound && remainingSteps[*it] < currentStepBound - 1))) {
// If we don't have a number of maximal steps to take, just add the state to the stack.
for (auto predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) {
if (phiStates.get(*predecessorIt) && (!statesWithProbabilityGreater0.get(*predecessorIt) || (useStepBound && remainingSteps[*predecessorIt] < currentStepBound - 1))) {
// If we don't have a bound on the number of steps to take, just add the state to the stack.
if (!useStepBound) {
statesWithProbabilityGreater0.set(*it, true);
stack.push_back(*it);
statesWithProbabilityGreater0.set(*predecessorIt, true);
stack.push_back(*predecessorIt);
} else if (currentStepBound > 0) {
// If there is at least one more step to go, we need to push the state and the new number of steps.
remainingSteps[*it] = currentStepBound - 1;
statesWithProbabilityGreater0.set(*it, true);
stack.push_back(*it);
remainingSteps[*predecessorIt] = currentStepBound - 1;
statesWithProbabilityGreater0.set(*predecessorIt, true);
stack.push_back(*predecessorIt);
stepStack.push_back(currentStepBound - 1);
}
}
@ -174,17 +172,11 @@ namespace graph {
// Prepare resulting bit vector.
storm::storage::BitVector statesWithProbabilityGreater0(model.getNumberOfStates());
// Get some temporaries for convenience.
std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix = model.getTransitionMatrix();
std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices();
// Add all psi states as the already satisfy the condition.
statesWithProbabilityGreater0 |= psiStates;
// Initialize the stack used for the BFS with the states
std::vector<uint_fast64_t> stack;
stack.reserve(model.getNumberOfStates());
psiStates.addSetIndicesToVector(stack);
// Initialize the stack used for the DFS with the states
std::vector<uint_fast64_t> stack = psiStates.getSetIndicesList();
// Initialize the stack for the step bound, if the number of steps is bounded.
std::vector<uint_fast64_t> stepStack;
@ -198,7 +190,7 @@ namespace graph {
}
}
// Perform the actual BFS.
// Perform the actual DFS.
uint_fast64_t currentState, currentStepBound;
while (!stack.empty()) {
currentState = stack.back();
@ -209,17 +201,17 @@ namespace graph {
stepStack.pop_back();
}
for (auto it = backwardTransitions.constColumnIteratorBegin(currentState), ite = backwardTransitions.constColumnIteratorEnd(currentState); it != ite; ++it) {
if (phiStates.get(*it) && (!statesWithProbabilityGreater0.get(*it) || (useStepBound && remainingSteps[*it] < currentStepBound - 1))) {
for (auto predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) {
if (phiStates.get(*predecessorIt) && (!statesWithProbabilityGreater0.get(*predecessorIt) || (useStepBound && remainingSteps[*predecessorIt] < currentStepBound - 1))) {
// If we don't have a bound on the number of steps to take, just add the state to the stack.
if (!useStepBound) {
statesWithProbabilityGreater0.set(*it, true);
stack.push_back(*it);
statesWithProbabilityGreater0.set(*predecessorIt, true);
stack.push_back(*predecessorIt);
} else if (currentStepBound > 0) {
// If there is at least one more step to go, we need to push the state and the new number of steps.
remainingSteps[*it] = currentStepBound - 1;
statesWithProbabilityGreater0.set(*it, true);
stack.push_back(*it);
remainingSteps[*predecessorIt] = currentStepBound - 1;
statesWithProbabilityGreater0.set(*predecessorIt, true);
stack.push_back(*predecessorIt);
stepStack.push_back(currentStepBound - 1);
}
}
@ -265,11 +257,11 @@ namespace graph {
template <typename T>
storm::storage::BitVector performProb1E(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::SparseMatrix<bool> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
// Get some temporaries for convenience.
std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix = model.getTransitionMatrix();
std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices();
storm::storage::SparseMatrix<T> const& transitionMatrix = model.getTransitionMatrix();
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices();
// Initialize the environment for the iterative algorithm.
storm::storage::BitVector currentStates(model.getNumberOfStates(), true);
std::vector<uint_fast64_t> stack;
stack.reserve(model.getNumberOfStates());
@ -285,14 +277,14 @@ namespace graph {
currentState = stack.back();
stack.pop_back();
for(auto it = backwardTransitions.constColumnIteratorBegin(currentState), ite = backwardTransitions.constColumnIteratorEnd(currentState); it != ite; ++it) {
if (phiStates.get(*it) && !nextStates.get(*it)) {
for(auto predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) {
if (phiStates.get(*predecessorIt) && !nextStates.get(*predecessorIt)) {
// Check whether the predecessor has only successors in the current state set for one of the
// nondeterminstic choices.
for (uint_fast64_t row = (*nondeterministicChoiceIndices)[*it]; row < (*nondeterministicChoiceIndices)[*it + 1]; ++row) {
for (auto row = nondeterministicChoiceIndices[*predecessorIt]; row < nondeterministicChoiceIndices[*predecessorIt + 1]; ++row) {
bool allSuccessorsInCurrentStates = true;
for (auto colIt = transitionMatrix->constColumnIteratorBegin(row); colIt != transitionMatrix->constColumnIteratorEnd(row); ++colIt) {
if (!currentStates.get(*colIt)) {
for (auto targetIt = transitionMatrix.constColumnIteratorBegin(row), targetIte = transitionMatrix.constColumnIteratorEnd(row); targetIt != targetIte; ++targetIt) {
if (!currentStates.get(*targetIt)) {
allSuccessorsInCurrentStates = false;
break;
}
@ -302,8 +294,8 @@ namespace graph {
// add it to the set of states for the next iteration and perform a backward search from
// that state.
if (allSuccessorsInCurrentStates) {
nextStates.set(*it, true);
stack.push_back(*it);
nextStates.set(*predecessorIt, true);
stack.push_back(*predecessorIt);
break;
}
}
@ -364,16 +356,14 @@ namespace graph {
storm::storage::BitVector statesWithProbabilityGreater0(model.getNumberOfStates());
// Get some temporaries for convenience.
std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix = model.getTransitionMatrix();
std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices();
storm::storage::SparseMatrix<T> const& transitionMatrix = model.getTransitionMatrix();
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices();
// Add all psi states as the already satisfy the condition.
statesWithProbabilityGreater0 |= psiStates;
// Initialize the stack used for the BFS with the states
std::vector<uint_fast64_t> stack;
stack.reserve(model.getNumberOfStates());
psiStates.addSetIndicesToVector(stack);
// Initialize the stack used for the DFS with the states
std::vector<uint_fast64_t> stack = psiStates.getSetIndicesList();
// Initialize the stack for the step bound, if the number of steps is bounded.
std::vector<uint_fast64_t> stepStack;
@ -387,7 +377,7 @@ namespace graph {
}
}
// Perform the actual BFS.
// Perform the actual DFS.
uint_fast64_t currentState, currentStepBound;
while(!stack.empty()) {
currentState = stack.back();
@ -398,15 +388,15 @@ namespace graph {
stepStack.pop_back();
}
for(auto it = backwardTransitions.constColumnIteratorBegin(currentState), ite = backwardTransitions.constColumnIteratorEnd(currentState); it != ite; ++it) {
if (phiStates.get(*it) && (!statesWithProbabilityGreater0.get(*it) || (useStepBound && remainingSteps[*it] < currentStepBound - 1))) {
for(auto predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) {
if (phiStates.get(*predecessorIt) && (!statesWithProbabilityGreater0.get(*predecessorIt) || (useStepBound && remainingSteps[*predecessorIt] < currentStepBound - 1))) {
// Check whether the predecessor has at least one successor in the current state set for every
// nondeterministic choice.
bool addToStatesWithProbabilityGreater0 = true;
for (auto rowIt = nondeterministicChoiceIndices->begin() + *it; rowIt != nondeterministicChoiceIndices->begin() + *it + 1; ++rowIt) {
for (auto row = nondeterministicChoiceIndices[*predecessorIt]; row < nondeterministicChoiceIndices[*predecessorIt + 1]; ++row) {
bool hasAtLeastOneSuccessorWithProbabilityGreater0 = false;
for (auto colIt = transitionMatrix->constColumnIteratorBegin(*rowIt); colIt != transitionMatrix->constColumnIteratorEnd(*rowIt); ++colIt) {
if (statesWithProbabilityGreater0.get(*colIt)) {
for (auto successorIt = transitionMatrix.constColumnIteratorBegin(row), successorIte = transitionMatrix.constColumnIteratorEnd(row); successorIt != successorIte; ++successorIt) {
if (statesWithProbabilityGreater0.get(*successorIt)) {
hasAtLeastOneSuccessorWithProbabilityGreater0 = true;
break;
}
@ -422,13 +412,13 @@ namespace graph {
if (addToStatesWithProbabilityGreater0) {
// If we don't have a bound on the number of steps to take, just add the state to the stack.
if (!useStepBound) {
statesWithProbabilityGreater0.set(*it, true);
stack.push_back(*it);
statesWithProbabilityGreater0.set(*predecessorIt, true);
stack.push_back(*predecessorIt);
} else if (currentStepBound > 0) {
// If there is at least one more step to go, we need to push the state and the new number of steps.
remainingSteps[*it] = currentStepBound - 1;
statesWithProbabilityGreater0.set(*it, true);
stack.push_back(*it);
remainingSteps[*predecessorIt] = currentStepBound - 1;
statesWithProbabilityGreater0.set(*predecessorIt, true);
stack.push_back(*predecessorIt);
stepStack.push_back(currentStepBound - 1);
}
}
@ -473,8 +463,8 @@ namespace graph {
template <typename T>
storm::storage::BitVector performProb1A(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::SparseMatrix<bool> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
// Get some temporaries for convenience.
std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix = model.getTransitionMatrix();
std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices();
storm::storage::SparseMatrix<T> const& transitionMatrix = model.getTransitionMatrix();
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices();
// Initialize the environment for the iterative algorithm.
storm::storage::BitVector currentStates(model.getNumberOfStates(), true);
@ -493,14 +483,14 @@ namespace graph {
currentState = stack.back();
stack.pop_back();
for(auto it = backwardTransitions.constColumnIteratorBegin(currentState), ite = backwardTransitions.constColumnIteratorEnd(currentState); it != ite; ++it) {
if (phiStates.get(*it) && !nextStates.get(*it)) {
for(auto predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) {
if (phiStates.get(*predecessorIt) && !nextStates.get(*predecessorIt)) {
// Check whether the predecessor has only successors in the current state set for all of the
// nondeterminstic choices.
bool allSuccessorsInCurrentStatesForAllChoices = true;
for (uint_fast64_t row = (*nondeterministicChoiceIndices)[*it]; row < (*nondeterministicChoiceIndices)[*it + 1]; ++row) {
for (auto colIt = transitionMatrix->constColumnIteratorBegin(row); colIt != transitionMatrix->constColumnIteratorEnd(row); ++colIt) {
if (!currentStates.get(*colIt)) {
for (auto row = nondeterministicChoiceIndices[*predecessorIt]; row < nondeterministicChoiceIndices[*predecessorIt + 1]; ++row) {
for (auto successorIt = transitionMatrix.constColumnIteratorBegin(row), successorIte = transitionMatrix.constColumnIteratorEnd(row); successorIt != successorIte; ++successorIt) {
if (!currentStates.get(*successorIt)) {
allSuccessorsInCurrentStatesForAllChoices = false;
goto afterCheckLoop;
}
@ -512,8 +502,8 @@ namespace graph {
// add it to the set of states for the next iteration and perform a backward search from
// that state.
if (allSuccessorsInCurrentStatesForAllChoices) {
nextStates.set(*it, true);
stack.push_back(*it);
nextStates.set(*predecessorIt, true);
stack.push_back(*predecessorIt);
}
}
}
@ -584,7 +574,7 @@ namespace graph {
recursionStepForward:
while (!recursionStateStack.empty()) {
uint_fast64_t currentState = recursionStateStack.back();
typename storm::storage::SparseMatrix<T>::ConstIndexIterator currentIt = recursionIteratorStack.back();
typename storm::storage::SparseMatrix<T>::ConstIndexIterator successorIt = recursionIteratorStack.back();
// Perform the treatment of newly discovered state as defined by Tarjan's algorithm
visitedStates.set(currentState, true);
@ -595,29 +585,29 @@ namespace graph {
tarjanStackStates.set(currentState, true);
// Now, traverse all successors of the current state.
for(; currentIt != matrix.constColumnIteratorEnd(currentState); ++currentIt) {
for(; successorIt != matrix.constColumnIteratorEnd(currentState); ++successorIt) {
// If we have not visited the successor already, we need to perform the procedure
// recursively on the newly found state.
if (!visitedStates.get(*currentIt)) {
if (!visitedStates.get(*successorIt)) {
// Save current iterator position so we can continue where we left off later.
recursionIteratorStack.pop_back();
recursionIteratorStack.push_back(currentIt);
recursionIteratorStack.push_back(successorIt);
// Put unvisited successor on top of our recursion stack and remember that.
recursionStateStack.push_back(*currentIt);
statesInStack[*currentIt] = true;
recursionStateStack.push_back(*successorIt);
statesInStack[*successorIt] = true;
// Also, put initial value for iterator on corresponding recursion stack.
recursionIteratorStack.push_back(matrix.constColumnIteratorBegin(*currentIt));
recursionIteratorStack.push_back(matrix.constColumnIteratorBegin(*successorIt));
// Perform the actual recursion step in an iterative way.
goto recursionStepForward;
recursionStepBackward:
lowlinks[currentState] = std::min(lowlinks[currentState], lowlinks[*currentIt]);
} else if (tarjanStackStates.get(*currentIt)) {
lowlinks[currentState] = std::min(lowlinks[currentState], lowlinks[*successorIt]);
} else if (tarjanStackStates.get(*successorIt)) {
// Update the lowlink of the current state.
lowlinks[currentState] = std::min(lowlinks[currentState], stateIndices[*currentIt]);
lowlinks[currentState] = std::min(lowlinks[currentState], stateIndices[*successorIt]);
}
}
@ -648,7 +638,7 @@ namespace graph {
// original recursive call.
if (recursionStateStack.size() > 0) {
currentState = recursionStateStack.back();
currentIt = recursionIteratorStack.back();
successorIt = recursionIteratorStack.back();
goto recursionStepBackward;
}
@ -680,7 +670,7 @@ namespace graph {
uint_fast64_t currentIndex = 0;
for (uint_fast64_t state = 0; state < numberOfStates; ++state) {
if (!visitedStates.get(state)) {
performSccDecompositionHelper(state, currentIndex, stateIndices, lowlinks, tarjanStack, tarjanStackStates, visitedStates, *model.getTransitionMatrix(), scc);
performSccDecompositionHelper(state, currentIndex, stateIndices, lowlinks, tarjanStack, tarjanStackStates, visitedStates, model.getTransitionMatrix(), scc);
}
}
@ -723,22 +713,22 @@ namespace graph {
recursionStepForward:
while (!recursionStack.empty()) {
uint_fast64_t currentState = recursionStack.back();
typename storm::storage::SparseMatrix<T>::ConstIndexIterator currentIt = iteratorRecursionStack.back();
typename storm::storage::SparseMatrix<T>::ConstIndexIterator successorIt = iteratorRecursionStack.back();
visitedStates.set(currentState, true);
recursionStepBackward:
for (; currentIt != matrix.constColumnIteratorEnd(currentState); ++currentIt) {
if (!visitedStates.get(*currentIt)) {
for (; successorIt != matrix.constColumnIteratorEnd(currentState); ++successorIt) {
if (!visitedStates.get(*successorIt)) {
// Put unvisited successor on top of our recursion stack and remember that.
recursionStack.push_back(*currentIt);
recursionStack.push_back(*successorIt);
// Save current iterator position so we can continue where we left off later.
iteratorRecursionStack.pop_back();
iteratorRecursionStack.push_back(currentIt + 1);
iteratorRecursionStack.push_back(successorIt + 1);
// Also, put initial value for iterator on corresponding recursion stack.
iteratorRecursionStack.push_back(matrix.constColumnIteratorBegin(*currentIt));
iteratorRecursionStack.push_back(matrix.constColumnIteratorBegin(*successorIt));
goto recursionStepForward;
}
@ -756,7 +746,7 @@ namespace graph {
// original recursive call.
if (recursionStack.size() > 0) {
currentState = recursionStack.back();
currentIt = iteratorRecursionStack.back();
successorIt = iteratorRecursionStack.back();
goto recursionStepBackward;
}

6
test/functional/parser/ParseMdpTest.cpp
View File

@ -17,12 +17,12 @@ TEST(ParseMdpTest, parseAndOutput) {
STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/pctl_general_input_01.lab"));
std::shared_ptr<storm::models::Mdp<double>> mdp = mdpParser->getMdp();
std::shared_ptr<storm::storage::SparseMatrix<double>> matrix = mdp->getTransitionMatrix();
storm::storage::SparseMatrix<double> const& matrix = mdp->getTransitionMatrix();
ASSERT_EQ(mdp->getNumberOfStates(), (uint_fast64_t)3);
ASSERT_EQ(mdp->getNumberOfTransitions(), (uint_fast64_t)11);
ASSERT_EQ(matrix->getRowCount(), (uint_fast64_t)(2 * 3));
ASSERT_EQ(matrix->getColumnCount(), (uint_fast64_t)3);
ASSERT_EQ(matrix.getRowCount(), (uint_fast64_t)(2 * 3));
ASSERT_EQ(matrix.getColumnCount(), (uint_fast64_t)3);
delete mdpParser;

Write Preview
Loading…
Cancel
Save