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

Moved from additional row grouping to the one embedded in the matrix itself. 

Former-commit-id: 9d7a1fff10
tempestpy_adaptions
dehnert 11 years ago
parent
d092897247
commit
12743e0a7e
30 changed files with 197 additions and 306 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. 22
      src/adapters/ExplicitModelAdapter.h
  2. 45
      src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
  3. 62
      src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
  4. 10
      src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h
  5. 6
      src/models/AbstractDeterministicModel.h
  6. 6
      src/models/AbstractModel.h
  7. 35
      src/models/AbstractNondeterministicModel.h
  8. 7
      src/models/Ctmc.h
  9. 21
      src/models/Ctmdp.h
  10. 8
      src/models/Dtmc.h
  11. 43
      src/models/MarkovAutomaton.h
  12. 36
      src/models/Mdp.h
  13. 2
      src/parser/MarkovAutomatonParser.cpp
  14. 5
      src/parser/MarkovAutomatonSparseTransitionParser.cpp
  15. 5
      src/parser/MarkovAutomatonSparseTransitionParser.h
  16. 8
      src/parser/NondeterministicModelParser.cpp
  17. 9
      src/parser/NondeterministicModelParser.h
  18. 12
      src/solver/GmmxxNondeterministicLinearEquationSolver.cpp
  19. 4
      src/solver/GmmxxNondeterministicLinearEquationSolver.h
  20. 12
      src/solver/NativeNondeterministicLinearEquationSolver.cpp
  21. 4
      src/solver/NativeNondeterministicLinearEquationSolver.h
  22. 6
      src/solver/NondeterministicLinearEquationSolver.h
  23. 15
      src/storage/SparseMatrix.cpp
  24. 17
      src/storage/SparseMatrix.h
  25. 4
      src/utility/graph.h
  26. 11
      src/utility/matrix.h
  27. 41
      test/functional/solver/GmmxxNondeterministicLinearEquationSolverTest.cpp
  28. 31
      test/functional/solver/NativeNondeterministicLinearEquationSolverTest.cpp
  29. 2
      test/functional/storage/MaximalEndComponentDecompositionTest.cpp
  30. 14
      test/functional/storage/SparseMatrixTest.cpp

22
src/adapters/ExplicitModelAdapter.h
View File

@ -58,7 +58,7 @@ namespace storm {
// A structure holding the individual components of a model.
struct ModelComponents {
ModelComponents() : transitionMatrix(), stateLabeling(), nondeterministicChoiceIndices(), stateRewards(), transitionRewardMatrix(), choiceLabeling() {
ModelComponents() : transitionMatrix(), stateLabeling(), stateRewards(), transitionRewardMatrix(), choiceLabeling() {
// Intentionally left empty.
}
@ -68,9 +68,6 @@ namespace storm {
// The state labeling.
storm::models::AtomicPropositionsLabeling stateLabeling;
// A vector indicating at which row the choices for a particular state begin.
std::vector<uint_fast64_t> nondeterministicChoiceIndices;
// The state reward vector.
std::vector<ValueType> stateRewards;
@ -108,10 +105,10 @@ namespace storm {
result = std::unique_ptr<storm::models::AbstractModel<ValueType>>(new storm::models::Ctmc<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
break;
case storm::ir::Program::MDP:
result = std::unique_ptr<storm::models::AbstractModel<ValueType>>(new storm::models::Mdp<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.nondeterministicChoiceIndices), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
result = std::unique_ptr<storm::models::AbstractModel<ValueType>>(new storm::models::Mdp<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
break;
case storm::ir::Program::CTMDP:
result = std::unique_ptr<storm::models::AbstractModel<ValueType>>(new storm::models::Ctmdp<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.nondeterministicChoiceIndices), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
result = std::unique_ptr<storm::models::AbstractModel<ValueType>>(new storm::models::Ctmdp<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
break;
default:
LOG4CPLUS_ERROR(logger, "Error while creating model from probabilistic program: cannot handle this model type.");
@ -455,8 +452,7 @@ namespace storm {
* @return A tuple containing a vector with all rows at which the nondeterministic choices of each state begin
* and a vector containing the labels associated with each choice.
*/
static std::pair<std::vector<uint_fast64_t>, std::vector<boost::container::flat_set<uint_fast64_t>>> buildMatrices(storm::ir::Program const& program, VariableInformation const& variableInformation, std::vector<storm::ir::TransitionReward> const& transitionRewards, StateInformation& stateInformation, bool deterministicModel, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, storm::storage::SparseMatrixBuilder<ValueType>& transitionRewardMatrixBuilder) {
std::vector<uint_fast64_t> nondeterministicChoiceIndices;
static std::vector<boost::container::flat_set<uint_fast64_t>> buildMatrices(storm::ir::Program const& program, VariableInformation const& variableInformation, std::vector<storm::ir::TransitionReward> const& transitionRewards, StateInformation& stateInformation, bool deterministicModel, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, storm::storage::SparseMatrixBuilder<ValueType>& transitionRewardMatrixBuilder) {
std::vector<boost::container::flat_set<uint_fast64_t>> choiceLabels;
// Initialize a queue and insert the initial state.
@ -524,7 +520,6 @@ namespace storm {
// Now add the resulting distribution as the only choice of the current state.
nondeterministicChoiceIndices.push_back(currentRow);
choiceLabels.push_back(globalChoice.getChoiceLabels());
for (auto const& stateProbabilityPair : globalChoice) {
@ -541,7 +536,6 @@ namespace storm {
++currentRow;
} else {
// If the model is nondeterministic, we add all choices individually.
nondeterministicChoiceIndices.push_back(currentRow);
transitionMatrixBuilder.newRowGroup(currentRow);
transitionRewardMatrixBuilder.newRowGroup(currentRow);
@ -604,9 +598,7 @@ namespace storm {
stateQueue.pop();
}
nondeterministicChoiceIndices.push_back(currentRow);
return std::make_pair(nondeterministicChoiceIndices, choiceLabels);
return choiceLabels;
}
/*!
@ -635,9 +627,7 @@ namespace storm {
// Build the transition and reward matrices.
storm::storage::SparseMatrixBuilder<ValueType> transitionMatrixBuilder(0, 0, 0, !deterministicModel, 0);
storm::storage::SparseMatrixBuilder<ValueType> transitionRewardMatrixBuilder(0, 0, 0, !deterministicModel, 0);
std::pair<std::vector<uint_fast64_t>, std::vector<boost::container::flat_set<uint_fast64_t>>> nondeterministicChoiceIndicesAndChoiceLabelsPair = buildMatrices(program, variableInformation, rewardModel.getTransitionRewards(), stateInformation, deterministicModel, transitionMatrixBuilder, transitionRewardMatrixBuilder);
modelComponents.nondeterministicChoiceIndices = std::move(nondeterministicChoiceIndicesAndChoiceLabelsPair.first);
modelComponents.choiceLabeling = std::move(nondeterministicChoiceIndicesAndChoiceLabelsPair.second);
modelComponents.choiceLabeling = buildMatrices(program, variableInformation, rewardModel.getTransitionRewards(), stateInformation, deterministicModel, transitionMatrixBuilder, transitionRewardMatrixBuilder);
// Finalize the resulting matrices.
modelComponents.transitionMatrix = transitionMatrixBuilder.build();

45
src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
View File

@ -49,7 +49,7 @@ namespace storm {
}
std::pair<std::vector<ValueType>, storm::storage::TotalScheduler> computeUnboundedUntilProbabilities(bool min, storm::storage::BitVector const& leftStates, storm::storage::BitVector const& rightStates, bool qualitative) const {
return storm::modelchecker::prctl::SparseMdpPrctlModelChecker<ValueType>::computeUnboundedUntilProbabilities(min, this->getModel().getTransitionMatrix(), this->getModel().getNondeterministicChoiceIndices(), this->getModel().getBackwardTransitions(), this->getModel().getInitialStates(), leftStates, rightStates, nondeterministicLinearEquationSolver, qualitative);
return storm::modelchecker::prctl::SparseMdpPrctlModelChecker<ValueType>::computeUnboundedUntilProbabilities(min, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getInitialStates(), leftStates, rightStates, nondeterministicLinearEquationSolver, qualitative);
}
std::vector<ValueType> checkTimeBoundedUntil(storm::property::csl::TimeBoundedUntil<ValueType> const& formula, bool qualitative) const {
@ -86,18 +86,16 @@ namespace storm {
return result;
}
static void computeBoundedReachabilityProbabilities(bool min, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, std::vector<ValueType> const& exitRates, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector<ValueType>& markovianNonGoalValues, std::vector<ValueType>& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps) {
static void computeBoundedReachabilityProbabilities(bool min, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& exitRates, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector<ValueType>& markovianNonGoalValues, std::vector<ValueType>& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps) {
// Start by computing four sparse matrices:
// * a matrix aMarkovian with all (discretized) transitions from Markovian non-goal states to all Markovian non-goal states.
// * a matrix aMarkovianToProbabilistic with all (discretized) transitions from Markovian non-goal states to all probabilistic non-goal states.
// * a matrix aProbabilistic with all (non-discretized) transitions from probabilistic non-goal states to other probabilistic non-goal states.
// * a matrix aProbabilisticToMarkovian with all (non-discretized) transitions from probabilistic non-goal states to all Markovian non-goal states.
typename storm::storage::SparseMatrix<ValueType> aMarkovian = transitionMatrix.getSubmatrix(markovianNonGoalStates, nondeterministicChoiceIndices, true);
typename storm::storage::SparseMatrix<ValueType> aMarkovianToProbabilistic = transitionMatrix.getSubmatrix(markovianNonGoalStates, probabilisticNonGoalStates, nondeterministicChoiceIndices);
std::vector<uint_fast64_t> markovianNondeterministicChoiceIndices = storm::utility::vector::getConstrainedOffsetVector(nondeterministicChoiceIndices, markovianNonGoalStates);
typename storm::storage::SparseMatrix<ValueType> aProbabilistic = transitionMatrix.getSubmatrix(probabilisticNonGoalStates, nondeterministicChoiceIndices);
typename storm::storage::SparseMatrix<ValueType> aProbabilisticToMarkovian = transitionMatrix.getSubmatrix(probabilisticNonGoalStates, markovianNonGoalStates, nondeterministicChoiceIndices);
std::vector<uint_fast64_t> probabilisticNondeterministicChoiceIndices = storm::utility::vector::getConstrainedOffsetVector(nondeterministicChoiceIndices, probabilisticNonGoalStates);
typename storm::storage::SparseMatrix<ValueType> aMarkovian = transitionMatrix.getSubmatrix(true, markovianNonGoalStates, markovianNonGoalStates, true);
typename storm::storage::SparseMatrix<ValueType> aMarkovianToProbabilistic = transitionMatrix.getSubmatrix(true, markovianNonGoalStates, probabilisticNonGoalStates);
typename storm::storage::SparseMatrix<ValueType> aProbabilistic = transitionMatrix.getSubmatrix(true, probabilisticNonGoalStates, probabilisticNonGoalStates);
typename storm::storage::SparseMatrix<ValueType> aProbabilisticToMarkovian = transitionMatrix.getSubmatrix(true, probabilisticNonGoalStates, markovianNonGoalStates);
// The matrices with transitions from Markovian states need to be digitized.
// Digitize aMarkovian. Based on whether the transition is a self-loop or not, we apply the two digitization rules.
@ -128,13 +126,13 @@ namespace storm {
std::vector<ValueType> bMarkovian(markovianNonGoalStates.getNumberOfSetBits());
// Compute the two fixed right-hand side vectors, one for Markovian states and one for the probabilistic ones.
std::vector<ValueType> bProbabilisticFixed = transitionMatrix.getConstrainedRowSumVector(probabilisticNonGoalStates, nondeterministicChoiceIndices, goalStates);
std::vector<ValueType> bProbabilisticFixed = transitionMatrix.getConstrainedRowSumVector(probabilisticNonGoalStates, goalStates);
std::vector<ValueType> bMarkovianFixed;
bMarkovianFixed.reserve(markovianNonGoalStates.getNumberOfSetBits());
for (auto state : markovianNonGoalStates) {
bMarkovianFixed.push_back(storm::utility::constantZero<ValueType>());
for (auto& element : transitionMatrix.getRow(nondeterministicChoiceIndices[state])) {
for (auto& element : transitionMatrix.getRowGroup(state)) {
if (goalStates.get(element.first)) {
bMarkovianFixed.back() += (1 - std::exp(-exitRates[state] * delta)) * element.second;
}
@ -158,7 +156,7 @@ namespace storm {
storm::utility::vector::addVectorsInPlace(bProbabilistic, bProbabilisticFixed);
// Now perform the inner value iteration for probabilistic states.
nondeterministiclinearEquationSolver->solveEquationSystem(min, aProbabilistic, probabilisticNonGoalValues, bProbabilistic, probabilisticNondeterministicChoiceIndices, &multiplicationResultScratchMemory, &aProbabilisticScratchMemory);
nondeterministiclinearEquationSolver->solveEquationSystem(min, aProbabilistic, probabilisticNonGoalValues, bProbabilistic, &multiplicationResultScratchMemory, &aProbabilisticScratchMemory);
// (Re-)compute bMarkovian = bMarkovianFixed + aMarkovianToProbabilistic * vProbabilistic.
aMarkovianToProbabilistic.multiplyWithVector(probabilisticNonGoalValues, bMarkovian);
@ -171,7 +169,7 @@ namespace storm {
// After the loop, perform one more step of the value iteration for PS states.
aProbabilisticToMarkovian.multiplyWithVector(markovianNonGoalValues, bProbabilistic);
storm::utility::vector::addVectorsInPlace(bProbabilistic, bProbabilisticFixed);
nondeterministiclinearEquationSolver->solveEquationSystem(min, aProbabilistic, probabilisticNonGoalValues, bProbabilistic, probabilisticNondeterministicChoiceIndices, &multiplicationResultScratchMemory, &aProbabilisticScratchMemory);
nondeterministiclinearEquationSolver->solveEquationSystem(min, aProbabilistic, probabilisticNonGoalValues, bProbabilistic, &multiplicationResultScratchMemory, &aProbabilisticScratchMemory);
}
std::vector<ValueType> checkTimeBoundedEventually(bool min, storm::storage::BitVector const& goalStates, ValueType lowerBound, ValueType upperBound) const {
@ -186,7 +184,6 @@ namespace storm {
}
// Get some data fields for convenient access.
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices();
typename storm::storage::SparseMatrix<ValueType> const& transitionMatrix = this->getModel().getTransitionMatrix();
std::vector<ValueType> const& exitRates = this->getModel().getExitRates();
storm::storage::BitVector const& markovianStates = this->getModel().getMarkovianStates();
@ -207,7 +204,7 @@ namespace storm {
std::vector<ValueType> vProbabilistic(probabilisticNonGoalStates.getNumberOfSetBits());
std::vector<ValueType> vMarkovian(markovianNonGoalStates.getNumberOfSetBits());
computeBoundedReachabilityProbabilities(min, transitionMatrix, nondeterministicChoiceIndices, exitRates, markovianStates, goalStates, markovianNonGoalStates, probabilisticNonGoalStates, vMarkovian, vProbabilistic, delta, numberOfSteps);
computeBoundedReachabilityProbabilities(min, transitionMatrix, exitRates, markovianStates, goalStates, markovianNonGoalStates, probabilisticNonGoalStates, vMarkovian, vProbabilistic, delta, numberOfSteps);
// (4) If the lower bound of interval was non-zero, we need to take the current values as the starting values for a subsequent value iteration.
if (lowerBound != storm::utility::constantZero<ValueType>()) {
@ -225,7 +222,7 @@ namespace storm {
std::cout << "Performing " << numberOfSteps << " iterations (delta=" << delta << ") for interval [0, " << lowerBound << "]." << std::endl;
// Compute the bounded reachability for interval [0, b-a].
computeBoundedReachabilityProbabilities(min, transitionMatrix, nondeterministicChoiceIndices, exitRates, markovianStates, storm::storage::BitVector(this->getModel().getNumberOfStates()), markovianStates, ~markovianStates, vAllMarkovian, vAllProbabilistic, delta, numberOfSteps);
computeBoundedReachabilityProbabilities(min, transitionMatrix, exitRates, markovianStates, storm::storage::BitVector(this->getModel().getNumberOfStates()), markovianStates, ~markovianStates, vAllMarkovian, vAllProbabilistic, delta, numberOfSteps);
// Create the result vector out of vAllProbabilistic and vAllMarkovian and return it.
std::vector<ValueType> result(this->getModel().getNumberOfStates());
@ -305,14 +302,12 @@ namespace storm {
// Finally, we are ready to create the SSP matrix and right-hand side of the SSP.
std::vector<ValueType> b;
std::vector<uint_fast64_t> sspNondeterministicChoiceIndices;
sspNondeterministicChoiceIndices.reserve(numberOfStatesNotInMecs + mecDecomposition.size() + 1);
typename storm::storage::SparseMatrixBuilder<ValueType> sspMatrixBuilder;
typename storm::storage::SparseMatrixBuilder<ValueType> sspMatrixBuilder(0, 0, 0, true, numberOfStatesNotInMecs + mecDecomposition.size() + 1);
// If the source state is not contained in any MEC, we copy its choices (and perform the necessary modifications).
uint_fast64_t currentChoice = 0;
for (auto state : statesNotContainedInAnyMec) {
sspNondeterministicChoiceIndices.push_back(currentChoice);
sspMatrixBuilder.newRowGroup(currentChoice);
for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice, ++currentChoice) {
std::vector<ValueType> auxiliaryStateToProbabilityMap(mecDecomposition.size());
@ -341,7 +336,7 @@ namespace storm {
// Now we are ready to construct the choices for the auxiliary states.
for (uint_fast64_t mecIndex = 0; mecIndex < mecDecomposition.size(); ++mecIndex) {
storm::storage::MaximalEndComponent const& mec = mecDecomposition[mecIndex];
sspNondeterministicChoiceIndices.push_back(currentChoice);
sspMatrixBuilder.newRowGroup(currentChoice);
for (auto const& stateChoicesPair : mec) {
uint_fast64_t state = stateChoicesPair.first;
@ -389,14 +384,11 @@ namespace storm {
b.push_back(lraValuesForEndComponents[mecIndex]);
}
// Add the sentinel element at the end.
sspNondeterministicChoiceIndices.push_back(currentChoice);
// Finalize the matrix and solve the corresponding system of equations.
storm::storage::SparseMatrix<ValueType> sspMatrix = sspMatrixBuilder.build(currentChoice + 1);
std::vector<ValueType> x(numberOfStatesNotInMecs + mecDecomposition.size());
nondeterministicLinearEquationSolver->solveEquationSystem(min, sspMatrix, x, b, sspNondeterministicChoiceIndices);
nondeterministicLinearEquationSolver->solveEquationSystem(min, sspMatrix, x, b);
// Prepare result vector.
std::vector<ValueType> result(this->getModel().getNumberOfStates());
@ -561,8 +553,7 @@ namespace storm {
// Then, we can eliminate the rows and columns for all states whose values are already known to be 0.
std::vector<ValueType> x(maybeStates.getNumberOfSetBits());
std::vector<uint_fast64_t> subNondeterministicChoiceIndices = storm::utility::vector::getConstrainedOffsetVector(this->getModel().getNondeterministicChoiceIndices(), maybeStates);
storm::storage::SparseMatrix<ValueType> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(maybeStates, this->getModel().getNondeterministicChoiceIndices());
storm::storage::SparseMatrix<ValueType> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(true, maybeStates, maybeStates);
// Now prepare the expected reward values for all states so they can be used as the right-hand side of the equation system.
std::vector<ValueType> rewardValues(stateRewards);
@ -576,7 +567,7 @@ namespace storm {
// Solve the corresponding system of equations.
std::shared_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> nondeterministiclinearEquationSolver = storm::utility::solver::getNondeterministicLinearEquationSolver<ValueType>();
nondeterministiclinearEquationSolver->solveEquationSystem(min, submatrix, x, b, subNondeterministicChoiceIndices);
nondeterministiclinearEquationSolver->solveEquationSystem(min, submatrix, x, b);
// Create resulting vector.
std::vector<ValueType> result(this->getModel().getNumberOfStates());

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

@ -100,9 +100,9 @@ namespace storm {
// Determine the states that have 0 probability of reaching the target states.
storm::storage::BitVector statesWithProbabilityGreater0;
if (this->minimumOperatorStack.top()) {
statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0A(this->getModel().getTransitionMatrix(), this->getModel().getNondeterministicChoiceIndices(), this->getModel().getBackwardTransitions(), phiStates, psiStates, true, stepBound);
statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0A(this->getModel().getTransitionMatrix(), this->getModel().getTransitionMatrix().getRowGroupIndices(), this->getModel().getBackwardTransitions(), phiStates, psiStates, true, stepBound);
} else {
statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0E(this->getModel().getTransitionMatrix(), this->getModel().getNondeterministicChoiceIndices(), this->getModel().getBackwardTransitions(), phiStates, psiStates, true, stepBound);
statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0E(this->getModel().getTransitionMatrix(), this->getModel().getTransitionMatrix().getRowGroupIndices(), this->getModel().getBackwardTransitions(), phiStates, psiStates, true, stepBound);
}
// Check if we already know the result (i.e. probability 0) for all initial states and
@ -119,20 +119,17 @@ namespace storm {
// 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(true, statesWithProbabilityGreater0, statesWithProbabilityGreater0, false);
// Get the "new" nondeterministic choice indices for the submatrix.
std::vector<uint_fast64_t> subNondeterministicChoiceIndices = storm::utility::vector::getConstrainedOffsetVector(this->getModel().getNondeterministicChoiceIndices(), statesWithProbabilityGreater0);
// Compute the new set of target states in the reduced system.
storm::storage::BitVector rightStatesInReducedSystem = psiStates % statesWithProbabilityGreater0;
// Make all rows absorbing that satisfy the second sub-formula.
submatrix.makeRowGroupsAbsorbing(rightStatesInReducedSystem, subNondeterministicChoiceIndices);
submatrix.makeRowGroupsAbsorbing(rightStatesInReducedSystem);
// Create the vector with which to multiply.
std::vector<Type> subresult(statesWithProbabilityGreater0.getNumberOfSetBits());
storm::utility::vector::setVectorValues(subresult, rightStatesInReducedSystem, storm::utility::constantOne<Type>());
this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), submatrix, subresult, subNondeterministicChoiceIndices, nullptr, stepBound);
this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), submatrix, subresult, nullptr, stepBound);
// Set the values of the resulting vector accordingly.
storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0, subresult);
@ -173,7 +170,7 @@ namespace storm {
std::vector<Type> result(this->getModel().getNumberOfStates());
storm::utility::vector::setVectorValues(result, nextStates, storm::utility::constantOne<Type>());
this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), result, this->getModel().getNondeterministicChoiceIndices());
this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), result);
return result;
}
@ -282,17 +279,17 @@ namespace storm {
* @return The probabilities for the satisfying phi until psi for each state of the model. If the
* qualitative flag is set, exact probabilities might not be computed.
*/
static std::pair<std::vector<Type>, storm::storage::TotalScheduler> computeUnboundedUntilProbabilities(bool minimize, storm::storage::SparseMatrix<Type> const& transitionMatrix, std::vector<uint_fast64_t> nondeterministicChoiceIndices, storm::storage::SparseMatrix<Type> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::shared_ptr<storm::solver::NondeterministicLinearEquationSolver<Type>> nondeterministicLinearEquationSolver, bool qualitative) {
static std::pair<std::vector<Type>, storm::storage::TotalScheduler> computeUnboundedUntilProbabilities(bool minimize, storm::storage::SparseMatrix<Type> const& transitionMatrix, storm::storage::SparseMatrix<Type> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::shared_ptr<storm::solver::NondeterministicLinearEquationSolver<Type>> nondeterministicLinearEquationSolver, bool qualitative) {
size_t numberOfStates = phiStates.size();
// We need to identify the states which have to be taken out of the matrix, i.e.
// all states that have probability 0 and 1 of satisfying the until-formula.
std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01;
if (minimize) {
statesWithProbability01 = storm::utility::graph::performProb01Min(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates);
statesWithProbability01 = storm::utility::graph::performProb01Min(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, phiStates, psiStates);
} else {
statesWithProbability01 = storm::utility::graph::performProb01Max(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates);
statesWithProbability01 = storm::utility::graph::performProb01Max(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, phiStates, psiStates);
}
storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first);
storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second);
@ -322,18 +319,15 @@ namespace storm {
// whose probabilities are already known.
storm::storage::SparseMatrix<Type> submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, false);
// Get the "new" nondeterministic choice indices for the submatrix.
std::vector<uint_fast64_t> subNondeterministicChoiceIndices = storm::utility::vector::getConstrainedOffsetVector(nondeterministicChoiceIndices, maybeStates);
// 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 = transitionMatrix.getConstrainedRowGroupSumVector(maybeStates, nondeterministicChoiceIndices, statesWithProbability1);
std::vector<Type> b = transitionMatrix.getConstrainedRowGroupSumVector(maybeStates, statesWithProbability1);
// Create vector for results for maybe states.
std::vector<Type> x(maybeStates.getNumberOfSetBits());
// Solve the corresponding system of equations.
nondeterministicLinearEquationSolver->solveEquationSystem(minimize, submatrix, x, b, subNondeterministicChoiceIndices);
nondeterministicLinearEquationSolver->solveEquationSystem(minimize, submatrix, x, b);
// Set values of resulting vector according to result.
storm::utility::vector::setVectorValues<Type>(result, maybeStates, x);
@ -344,13 +338,13 @@ namespace storm {
storm::utility::vector::setVectorValues<Type>(result, statesWithProbability1, storm::utility::constantOne<Type>());
// Finally, compute a scheduler that achieves the extramal value.
storm::storage::TotalScheduler scheduler = computeExtremalScheduler(minimize, transitionMatrix, nondeterministicChoiceIndices, result);
storm::storage::TotalScheduler scheduler = computeExtremalScheduler(minimize, transitionMatrix, result);
return std::make_pair(result, scheduler);
}
std::pair<std::vector<Type>, storm::storage::TotalScheduler> checkUntil(bool minimize, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) const {
return computeUnboundedUntilProbabilities(minimize, this->getModel().getTransitionMatrix(), this->getModel().getNondeterministicChoiceIndices(), this->getModel().getBackwardTransitions(), this->getModel().getInitialStates(), phiStates, psiStates, this->nondeterministicLinearEquationSolver, qualitative);
return computeUnboundedUntilProbabilities(minimize, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getInitialStates(), phiStates, psiStates, this->nondeterministicLinearEquationSolver, qualitative);
}
/*!
@ -374,7 +368,7 @@ namespace storm {
// Initialize result to state rewards of the model.
std::vector<Type> result(this->getModel().getStateRewardVector());
this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), result, this->getModel().getNondeterministicChoiceIndices(), nullptr, formula.getBound());
this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), result, nullptr, formula.getBound());
return result;
}
@ -416,7 +410,7 @@ namespace storm {
result.resize(this->getModel().getNumberOfStates());
}
this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), result, this->getModel().getNondeterministicChoiceIndices(), &totalRewardVector, formula.getBound());
this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), result, &totalRewardVector, formula.getBound());
return result;
}
@ -462,9 +456,9 @@ namespace storm {
storm::storage::BitVector infinityStates;
storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true);
if (minimize) {
infinityStates = std::move(storm::utility::graph::performProb1A(this->getModel().getTransitionMatrix(), this->getModel().getNondeterministicChoiceIndices(), this->getModel().getBackwardTransitions(), trueStates, targetStates));
infinityStates = std::move(storm::utility::graph::performProb1A(this->getModel().getTransitionMatrix(), this->getModel().getTransitionMatrix().getRowGroupIndices(), this->getModel().getBackwardTransitions(), trueStates, targetStates));
} else {
infinityStates = std::move(storm::utility::graph::performProb1E(this->getModel().getTransitionMatrix(), this->getModel().getNondeterministicChoiceIndices(), this->getModel().getBackwardTransitions(), trueStates, targetStates));
infinityStates = std::move(storm::utility::graph::performProb1E(this->getModel().getTransitionMatrix(), this->getModel().getTransitionMatrix().getRowGroupIndices(), this->getModel().getBackwardTransitions(), trueStates, targetStates));
}
infinityStates.complement();
storm::storage::BitVector maybeStates = ~targetStates & ~infinityStates;
@ -489,9 +483,6 @@ namespace storm {
// whose reward values are already known.
storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(true, maybeStates, maybeStates, false);
// Get the "new" nondeterministic choice indices for the submatrix.
std::vector<uint_fast64_t> subNondeterministicChoiceIndices = storm::utility::vector::getConstrainedOffsetVector(this->getModel().getNondeterministicChoiceIndices(), maybeStates);
// 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(submatrix.getRowCount());
@ -501,7 +492,7 @@ namespace storm {
// 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);
storm::utility::vector::selectVectorValues(b, maybeStates, this->getModel().getTransitionMatrix().getRowGroupIndices(), pointwiseProductRowSumVector);
if (this->getModel().hasStateRewards()) {
// If a state-based reward model is also available, we need to add this vector
@ -509,7 +500,7 @@ namespace storm {
// 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());
storm::utility::vector::selectVectorValuesRepeatedly(subStateRewards, maybeStates, this->getModel().getTransitionMatrix().getRowGroupIndices(), this->getModel().getStateRewardVector());
storm::utility::vector::addVectorsInPlace(b, subStateRewards);
}
} else {
@ -517,14 +508,14 @@ namespace storm {
// 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().getTransitionMatrix().getRowGroupIndices(), this->getModel().getStateRewardVector());
}
// Create vector for results for maybe states.
std::vector<Type> x(maybeStates.getNumberOfSetBits());
// Solve the corresponding system of equations.
this->nondeterministicLinearEquationSolver->solveEquationSystem(minimize, submatrix, x, b, subNondeterministicChoiceIndices);
this->nondeterministicLinearEquationSolver->solveEquationSystem(minimize, submatrix, x, b);
// Set values of resulting vector according to result.
storm::utility::vector::setVectorValues<Type>(result, maybeStates, x);
@ -535,7 +526,7 @@ namespace storm {
storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::constantInfinity<Type>());
// Finally, compute a scheduler that achieves the extramal value.
storm::storage::TotalScheduler scheduler = computeExtremalScheduler(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), this->getModel().getNondeterministicChoiceIndices(), result, this->getModel().hasStateRewards() ? &this->getModel().getStateRewardVector() : nullptr, this->getModel().hasTransitionRewards() ? &this->getModel().getTransitionRewardMatrix() : nullptr);
storm::storage::TotalScheduler scheduler = computeExtremalScheduler(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), result, this->getModel().hasStateRewards() ? &this->getModel().getStateRewardVector() : nullptr, this->getModel().hasTransitionRewards() ? &this->getModel().getTransitionRewardMatrix() : nullptr);
return std::make_pair(result, scheduler);
}
@ -547,9 +538,8 @@ namespace storm {
* @param minimize If set, all choices are resolved such that the solution value becomes minimal and maximal otherwise.
* @param nondeterministicResult The model checking result for nondeterministic choices of all states.
* @param takenChoices The output vector that is to store the taken choices.
* @param nondeterministicChoiceIndices The assignment of states to their nondeterministic choices in the matrix.
*/
static storm::storage::TotalScheduler computeExtremalScheduler(bool minimize, storm::storage::SparseMatrix<Type> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, std::vector<Type> const& result, std::vector<Type> const* stateRewardVector = nullptr, storm::storage::SparseMatrix<Type> const* transitionRewardMatrix = nullptr) {
static storm::storage::TotalScheduler computeExtremalScheduler(bool minimize, storm::storage::SparseMatrix<Type> const& transitionMatrix, std::vector<Type> const& result, std::vector<Type> const* stateRewardVector = nullptr, storm::storage::SparseMatrix<Type> const* transitionRewardMatrix = nullptr) {
std::vector<Type> temporaryResult(result.size());
std::vector<Type> nondeterministicResult(transitionMatrix.getRowCount());
transitionMatrix.multiplyWithVector(result, nondeterministicResult);
@ -560,12 +550,12 @@ namespace storm {
totalRewardVector = transitionMatrix.getPointwiseProductRowSumVector(*transitionRewardMatrix);
if (stateRewardVector != nullptr) {
std::vector<Type> stateRewards(totalRewardVector.size());
storm::utility::vector::selectVectorValuesRepeatedly(stateRewards, storm::storage::BitVector(stateRewardVector->size(), true), nondeterministicChoiceIndices, *stateRewardVector);
storm::utility::vector::selectVectorValuesRepeatedly(stateRewards, storm::storage::BitVector(stateRewardVector->size(), true), transitionMatrix.getRowGroupIndices(), *stateRewardVector);
storm::utility::vector::addVectorsInPlace(totalRewardVector, stateRewards);
}
} else {
totalRewardVector.resize(nondeterministicResult.size());
storm::utility::vector::selectVectorValuesRepeatedly(totalRewardVector, storm::storage::BitVector(stateRewardVector->size(), true), nondeterministicChoiceIndices, *stateRewardVector);
storm::utility::vector::selectVectorValuesRepeatedly(totalRewardVector, storm::storage::BitVector(stateRewardVector->size(), true), transitionMatrix.getRowGroupIndices(), *stateRewardVector);
}
storm::utility::vector::addVectorsInPlace(nondeterministicResult, totalRewardVector);
}
@ -573,9 +563,9 @@ namespace storm {
std::vector<uint_fast64_t> choices(result.size());
if (minimize) {
storm::utility::vector::reduceVectorMin(nondeterministicResult, temporaryResult, nondeterministicChoiceIndices, &choices);
storm::utility::vector::reduceVectorMin(nondeterministicResult, temporaryResult, transitionMatrix.getRowGroupIndices(), &choices);
} else {
storm::utility::vector::reduceVectorMax(nondeterministicResult, temporaryResult, nondeterministicChoiceIndices, &choices);
storm::utility::vector::reduceVectorMax(nondeterministicResult, temporaryResult, transitionMatrix.getRowGroupIndices(), &choices);
}
return storm::storage::TotalScheduler(choices);

10
src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h
View File

@ -58,7 +58,7 @@ private:
* @return The solution of the system of linear equations in form of the elements of the vector
* x.
*/
void solveEquationSystem(storm::storage::SparseMatrix<Type> const& matrix, std::vector<Type>& x, std::vector<Type> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices) const {
void solveEquationSystem(storm::storage::SparseMatrix<Type> const& matrix, std::vector<Type>& x, std::vector<Type> const& b) const {
// Get the settings object to customize solving.
storm::settings::Settings* s = storm::settings::Settings::getInstance();
@ -92,14 +92,14 @@ private:
converged = false;
while (!converged && localIterations < maxIterations) {
// Compute x' = A*x + b.
matrix.multiplyWithVector(scc, nondeterministicChoiceIndices, *currentX, multiplyResult);
storm::utility::addVectors(scc, nondeterministicChoiceIndices, multiplyResult, b);
matrix.multiplyWithVector(scc, *currentX, multiplyResult);
storm::utility::addVectors(scc, matrix.getRowGroupIndices(), multiplyResult, b);
// Reduce the vector x' by applying min/max for all non-deterministic choices.
if (this->minimumOperatorStack.top()) {
storm::utility::reduceVectorMin(multiplyResult, newX, scc, nondeterministicChoiceIndices);
storm::utility::reduceVectorMin(multiplyResult, newX, scc, matrix.getRowGroupIndices());
} else {
storm::utility::reduceVectorMax(multiplyResult, newX, scc, nondeterministicChoiceIndices);
storm::utility::reduceVectorMax(multiplyResult, newX, scc, matrix.getRowGroupIndices());
}
// Determine whether the method converged.

6
src/models/AbstractDeterministicModel.h
View File

@ -70,11 +70,7 @@ class AbstractDeterministicModel: public AbstractModel<T> {
AbstractDeterministicModel(AbstractDeterministicModel && other) : AbstractModel<T>(std::move(other)) {
// Intentionally left empty.
}
virtual typename storm::storage::SparseMatrix<T>::const_rows getRows(uint_fast64_t state) const override {
return this->transitionMatrix.getRows(state, state);
}
/*!
* Calculates a hash over all values contained in this Model.
* @return size_t A Hash Value

6
src/models/AbstractModel.h
View File

@ -203,8 +203,10 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
* @param state The state for which to retrieve the rows.
* @return An object representing the matrix rows associated with the given state.
*/
virtual typename storm::storage::SparseMatrix<T>::const_rows getRows(uint_fast64_t state) const = 0;
virtual typename storm::storage::SparseMatrix<T>::const_rows getRows(uint_fast64_t state) const {
return this->transitionMatrix.getRowGroup(state);
}
/*!
* Returns the state space size of the model.
* @return The size of the state space of the model.

35
src/models/AbstractNondeterministicModel.h
View File

@ -30,12 +30,11 @@ namespace storm {
*/
AbstractNondeterministicModel(storm::storage::SparseMatrix<T> const& transitionMatrix,
storm::models::AtomicPropositionsLabeling const& stateLabeling,
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices,
boost::optional<std::vector<T>> const& optionalStateRewardVector,
boost::optional<storm::storage::SparseMatrix<T>> const& optionalTransitionRewardMatrix,
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> const& optionalChoiceLabeling)
: AbstractModel<T>(transitionMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) {
this->nondeterministicChoiceIndices = nondeterministicChoiceIndices;
// Intentionally left empty.
}
/*! Constructs an abstract non-determinstic model from the given parameters.
@ -49,13 +48,11 @@ namespace storm {
*/
AbstractNondeterministicModel(storm::storage::SparseMatrix<T>&& transitionMatrix,
storm::models::AtomicPropositionsLabeling&& stateLabeling,
std::vector<uint_fast64_t>&& nondeterministicChoiceIndices,
boost::optional<std::vector<T>>&& optionalStateRewardVector,
boost::optional<storm::storage::SparseMatrix<T>>&& optionalTransitionRewardMatrix,
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>&& optionalChoiceLabeling)
// The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class
: AbstractModel<T>(std::move(transitionMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix),
std::move(optionalChoiceLabeling)), nondeterministicChoiceIndices(std::move(nondeterministicChoiceIndices)) {
std::move(optionalChoiceLabeling)) {
// Intentionally left empty.
}
@ -69,16 +66,14 @@ namespace storm {
/*!
* Copy Constructor.
*/
AbstractNondeterministicModel(AbstractNondeterministicModel const& other) : AbstractModel<T>(other),
nondeterministicChoiceIndices(other.nondeterministicChoiceIndices) {
AbstractNondeterministicModel(AbstractNondeterministicModel const& other) : AbstractModel<T>(other) {
// Intentionally left empty.
}
/*!
* Move Constructor.
*/
AbstractNondeterministicModel(AbstractNondeterministicModel&& other) : AbstractModel<T>(std::move(other)),
nondeterministicChoiceIndices(std::move(other.nondeterministicChoiceIndices)) {
AbstractNondeterministicModel(AbstractNondeterministicModel&& other) : AbstractModel<T>(std::move(other)) {
// Intentionally left empty.
}
@ -97,7 +92,7 @@ namespace storm {
* measured in bytes.
*/
virtual uint_fast64_t getSizeInMemory() const {
return AbstractModel<T>::getSizeInMemory() + nondeterministicChoiceIndices.size() * sizeof(uint_fast64_t);
return AbstractModel<T>::getSizeInMemory();
}
/*!
@ -107,13 +102,9 @@ namespace storm {
* of a certain state.
*/
std::vector<uint_fast64_t> const& getNondeterministicChoiceIndices() const {
return nondeterministicChoiceIndices;
return this->getTransitionMatrix().getRowGroupIndices();
}
virtual typename storm::storage::SparseMatrix<T>::const_rows getRows(uint_fast64_t state) const override {
return this->transitionMatrix.getRows(nondeterministicChoiceIndices[state], nondeterministicChoiceIndices[state + 1] - 1);
}
/*!
* Retrieves the backward transition relation of the model, i.e. a set of transitions
* between states that correspond to the reversed transition relation of this model.
@ -132,9 +123,7 @@ namespace storm {
*/
virtual size_t getHash() const override {
std::size_t result = 0;
std::size_t hashTmp = storm::utility::Hash<uint_fast64_t>::getHash(nondeterministicChoiceIndices);
boost::hash_combine(result, AbstractModel<T>::getHash());
boost::hash_combine(result, hashTmp);
return result;
}
@ -157,13 +146,13 @@ namespace storm {
AbstractModel<T>::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false);
// Write the probability distributions for all the states.
for (uint_fast64_t state = 0, highestStateIndex = this->getNumberOfStates() - 1; state <= highestStateIndex; ++state) {
uint_fast64_t rowCount = nondeterministicChoiceIndices[state + 1] - nondeterministicChoiceIndices[state];
for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) {
uint_fast64_t rowCount = this->getNondeterministicChoiceIndices()[state + 1] - this->getNondeterministicChoiceIndices()[state];
bool highlightChoice = true;
// For this, we need to iterate over all available nondeterministic choices in the current state.
for (uint_fast64_t choice = 0; choice < rowCount; ++choice) {
typename storm::storage::SparseMatrix<T>::const_rows row = this->transitionMatrix.getRow(nondeterministicChoiceIndices[state] + choice);
typename storm::storage::SparseMatrix<T>::const_rows row = this->transitionMatrix.getRow(this->getNondeterministicChoiceIndices()[state] + choice);
if (scheduler != nullptr) {
// If the scheduler picked the current choice, we will not make it dotted, but highlight it.
@ -234,17 +223,13 @@ namespace storm {
newChoiceLabeling.resize(choiceCount);
for (size_t state = 0; state < stateCount; ++state) {
for (size_t choice = this->nondeterministicChoiceIndices.at(state); choice < this->nondeterministicChoiceIndices.at(state + 1); ++choice) {
for (size_t choice = this->getNondeterministicChoiceIndices()[state]; choice < this->getNondeterministicChoiceIndices()[state + 1]; ++choice) {
newChoiceLabeling.at(choice).insert(state);
}
}
this->choiceLabeling.reset(newChoiceLabeling);
}
protected:
/*! A vector of indices mapping states to the choices (rows) in the transition matrix. */
std::vector<uint_fast64_t> nondeterministicChoiceIndices;
};
} // namespace models
} // namespace storm

7
src/models/Ctmc.h
View File

@ -88,12 +88,7 @@ public:
}
virtual std::shared_ptr<AbstractModel<T>> applyScheduler(storm::storage::Scheduler const& scheduler) const override {
std::vector<uint_fast64_t> nondeterministicChoiceIndices(this->getNumberOfStates() + 1);
for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) {
nondeterministicChoiceIndices[state] = state;
}
nondeterministicChoiceIndices[this->getNumberOfStates()] = this->getNumberOfStates();
storm::storage::SparseMatrix<T> newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), nondeterministicChoiceIndices, scheduler);
storm::storage::SparseMatrix<T> newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), scheduler);
return std::shared_ptr<AbstractModel<T>>(new Ctmc(newTransitionMatrix, this->getStateLabeling(), this->hasStateRewards() ? this->getStateRewardVector() : boost::optional<std::vector<T>>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() : boost::optional<storm::storage::SparseMatrix<T>>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>()));
}

21
src/models/Ctmdp.h
View File

@ -39,11 +39,10 @@ public:
*/
Ctmdp(storm::storage::SparseMatrix<T> const& probabilityMatrix,
storm::models::AtomicPropositionsLabeling const& stateLabeling,
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices,
boost::optional<std::vector<T>> const& optionalStateRewardVector,
boost::optional<std::vector<T>> const& optionalStateRewardVector,
boost::optional<storm::storage::SparseMatrix<T>> const& optionalTransitionRewardMatrix,
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> const& optionalChoiceLabeling)
: AbstractNondeterministicModel<T>(probabilityMatrix, stateLabeling, nondeterministicChoiceIndices, optionalStateRewardVector, optionalTransitionRewardMatrix,
: AbstractNondeterministicModel<T>(probabilityMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix,
optionalChoiceLabeling) {
if (!this->checkValidityOfProbabilityMatrix()) {
LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
@ -62,12 +61,11 @@ public:
*/
Ctmdp(storm::storage::SparseMatrix<T>&& probabilityMatrix,
storm::models::AtomicPropositionsLabeling&& stateLabeling,
std::vector<uint_fast64_t>&& nondeterministicChoiceIndices,
boost::optional<std::vector<T>>&& optionalStateRewardVector,
boost::optional<std::vector<T>>&& optionalStateRewardVector,
boost::optional<storm::storage::SparseMatrix<T>>&& optionalTransitionRewardMatrix,
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> const& optionalChoiceLabeling)
// The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class
: AbstractNondeterministicModel<T>(std::move(probabilityMatrix), std::move(stateLabeling), std::move(nondeterministicChoiceIndices), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix), std::move(optionalChoiceLabeling)) {
: AbstractNondeterministicModel<T>(std::move(probabilityMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix), std::move(optionalChoiceLabeling)) {
if (!this->checkValidityOfProbabilityMatrix()) {
LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
@ -116,15 +114,8 @@ public:
}
virtual std::shared_ptr<AbstractModel<T>> applyScheduler(storm::storage::Scheduler const& scheduler) const override {
storm::storage::SparseMatrix<T> newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), this->getNondeterministicChoiceIndices(), scheduler);
// Construct the new nondeterministic choice indices for the resulting matrix.
std::vector<uint_fast64_t> nondeterministicChoiceIndices(this->getNumberOfStates() + 1);
for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) {
nondeterministicChoiceIndices[state] = state;
}
nondeterministicChoiceIndices[this->getNumberOfStates()] = this->getNumberOfStates();
return std::shared_ptr<AbstractModel<T>>(new Ctmdp(newTransitionMatrix, this->getStateLabeling(), nondeterministicChoiceIndices, this->hasStateRewards() ? this->getStateRewardVector() : boost::optional<std::vector<T>>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() : boost::optional<storm::storage::SparseMatrix<T>>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>()));
storm::storage::SparseMatrix<T> newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), scheduler);
return std::shared_ptr<AbstractModel<T>>(new Ctmdp(newTransitionMatrix, this->getStateLabeling(), this->hasStateRewards() ? this->getStateRewardVector() : boost::optional<std::vector<T>>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() : boost::optional<storm::storage::SparseMatrix<T>>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>()));
}
private:

8
src/models/Dtmc.h
View File

@ -286,13 +286,7 @@ public:
}
virtual std::shared_ptr<AbstractModel<T>> applyScheduler(storm::storage::Scheduler const& scheduler) const override {
std::vector<uint_fast64_t> nondeterministicChoiceIndices(this->getNumberOfStates() + 1);
for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) {
nondeterministicChoiceIndices[state] = state;
}
nondeterministicChoiceIndices[this->getNumberOfStates()] = this->getNumberOfStates();
storm::storage::SparseMatrix<T> newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), nondeterministicChoiceIndices, scheduler);
storm::storage::SparseMatrix<T> newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), scheduler);
return std::shared_ptr<AbstractModel<T>>(new Dtmc(newTransitionMatrix, this->getStateLabeling(), this->hasStateRewards() ? this->getStateRewardVector() : boost::optional<std::vector<T>>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() : boost::optional<storm::storage::SparseMatrix<T>>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>()));
}

43
src/models/MarkovAutomaton.h
View File

@ -24,10 +24,10 @@ namespace storm {
public:
MarkovAutomaton(storm::storage::SparseMatrix<T> const& transitionMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling,
std::vector<uint_fast64_t>& nondeterministicChoiceIndices, storm::storage::BitVector const& markovianStates, std::vector<T> const& exitRates,
storm::storage::BitVector const& markovianStates, std::vector<T> const& exitRates,
boost::optional<std::vector<T>> const& optionalStateRewardVector, boost::optional<storm::storage::SparseMatrix<T>> const& optionalTransitionRewardMatrix,
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> const& optionalChoiceLabeling)
: AbstractNondeterministicModel<T>(transitionMatrix, stateLabeling, nondeterministicChoiceIndices, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling),
: AbstractNondeterministicModel<T>(transitionMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling),
markovianStates(markovianStates), exitRates(exitRates), closed(false) {
this->turnRatesToProbabilities();
@ -42,12 +42,11 @@ namespace storm {
MarkovAutomaton(storm::storage::SparseMatrix<T>&& transitionMatrix,
storm::models::AtomicPropositionsLabeling&& stateLabeling,
std::vector<uint_fast64_t>&& nondeterministicChoiceIndices,
storm::storage::BitVector const& markovianStates, std::vector<T> const& exitRates,
boost::optional<std::vector<T>>&& optionalStateRewardVector,
boost::optional<storm::storage::SparseMatrix<T>>&& optionalTransitionRewardMatrix,
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>&& optionalChoiceLabeling)
: AbstractNondeterministicModel<T>(std::move(transitionMatrix), std::move(stateLabeling), std::move(nondeterministicChoiceIndices), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix),
: AbstractNondeterministicModel<T>(std::move(transitionMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix),
std::move(optionalChoiceLabeling)), markovianStates(markovianStates), exitRates(std::move(exitRates)), closed(false) {
this->turnRatesToProbabilities();
@ -81,7 +80,7 @@ namespace storm {
}
bool isHybridState(uint_fast64_t state) const {
return isMarkovianState(state) && (this->getNondeterministicChoiceIndices()[state + 1] - this->getNondeterministicChoiceIndices()[state] > 1);
return isMarkovianState(state) && (this->getTransitionMatrix().getRowGroupSize(state) > 1);
}
bool isMarkovianState(uint_fast64_t state) const {
@ -127,8 +126,7 @@ namespace storm {
uint_fast64_t newNumberOfRows = this->getNumberOfChoices() - numberOfHybridStates;
// Create the matrix for the new transition relation and the corresponding nondeterministic choice vector.
storm::storage::SparseMatrixBuilder<T> newTransitionMatrixBuilder;
std::vector<uint_fast64_t> newNondeterministicChoiceIndices(this->getNumberOfStates() + 1);
storm::storage::SparseMatrixBuilder<T> newTransitionMatrixBuilder(0, 0, 0, true, this->getNumberOfStates() + 1);
// Now copy over all choices that need to be kept.
uint_fast64_t currentChoice = 0;
@ -139,7 +137,7 @@ namespace storm {
}
// Record the new beginning of choices of this state.
newNondeterministicChoiceIndices[state] = currentChoice;
newTransitionMatrixBuilder.newRowGroup(currentChoice);
// If we are currently treating a hybrid state, we need to skip its first choice.
if (this->isHybridState(state)) {
@ -147,7 +145,7 @@ namespace storm {
this->markovianStates.set(state, false);
}
for (uint_fast64_t row = this->nondeterministicChoiceIndices[state] + (this->isHybridState(state) ? 1 : 0); row < this->nondeterministicChoiceIndices[state + 1]; ++row) {
for (uint_fast64_t row = this->getNondeterminsticChoiceIndices()[state] + (this->isHybridState(state) ? 1 : 0); row < this->getNondeterminsticChoiceIndices()[state + 1]; ++row) {
for (auto const& entry : this->transitionMatrix.getRow(row)) {
newTransitionMatrixBuilder.addNextValue(currentChoice, entry.first, entry.second);
}
@ -155,12 +153,8 @@ namespace storm {
}
}
// Put a sentinel element at the end.
newNondeterministicChoiceIndices.back() = currentChoice;
// Finalize the matrix and put the new transition data in place.
this->transitionMatrix = newTransitionMatrixBuilder.build();
this->nondeterministicChoiceIndices = std::move(newNondeterministicChoiceIndices);
// Mark the automaton as closed.
closed = true;
@ -172,33 +166,21 @@ namespace storm {
throw storm::exceptions::InvalidStateException() << "Applying a scheduler to a non-closed Markov automaton is illegal; it needs to be closed first.";
}
storm::storage::SparseMatrix<T> newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), this->getNondeterministicChoiceIndices(), scheduler);
// Construct the new nondeterministic choice indices for the resulting matrix.
std::vector<uint_fast64_t> nondeterministicChoiceIndices(this->getNumberOfStates() + 1);
for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) {
nondeterministicChoiceIndices[state] = state;
}
nondeterministicChoiceIndices[this->getNumberOfStates()] = this->getNumberOfStates();
return std::shared_ptr<AbstractModel<T>>(new MarkovAutomaton(newTransitionMatrix, this->getStateLabeling(), nondeterministicChoiceIndices, markovianStates, exitRates, this->hasStateRewards() ? this->getStateRewardVector() : boost::optional<std::vector<T>>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() : boost::optional<storm::storage::SparseMatrix<T>>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>()));
storm::storage::SparseMatrix<T> newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), scheduler);
return std::shared_ptr<AbstractModel<T>>(new MarkovAutomaton(newTransitionMatrix, this->getStateLabeling(), markovianStates, exitRates, this->hasStateRewards() ? this->getStateRewardVector() : boost::optional<std::vector<T>>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() : boost::optional<storm::storage::SparseMatrix<T>>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>()));
}
virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector<T> const* firstValue = nullptr, std::vector<T> const* secondValue = nullptr, std::vector<uint_fast64_t> const* stateColoring = nullptr, std::vector<std::string> const* colors = nullptr, std::vector<uint_fast64_t>* scheduler = nullptr, bool finalizeOutput = true) const override {
AbstractModel<T>::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false);
for (uint_fast64_t i = 0; i < this->getNondeterministicChoiceIndices().size(); ++i) {
std::cout << i << ": " << this->getNondeterministicChoiceIndices()[i] << " ";
}
// Write the probability distributions for all the states.
for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) {
uint_fast64_t rowCount = this->getNondeterministicChoiceIndices()[state + 1] - this->getNondeterministicChoiceIndices()[state];
uint_fast64_t rowCount = this->getTransitionMatrix().getRowGroupIndices()[state + 1] - this->getTransitionMatrix().getRowGroupIndices()[state];
bool highlightChoice = true;
// For this, we need to iterate over all available nondeterministic choices in the current state.
for (uint_fast64_t choice = 0; choice < rowCount; ++choice) {
typename storm::storage::SparseMatrix<T>::const_rows row = this->transitionMatrix.getRow(this->getNondeterministicChoiceIndices()[state] + choice);
typename storm::storage::SparseMatrix<T>::const_rows row = this->transitionMatrix.getRow(this->getTransitionMatrix().getRowGroupIndices()[state] + choice);
if (scheduler != nullptr) {
// If the scheduler picked the current choice, we will not make it dotted, but highlight it.
@ -267,6 +249,7 @@ namespace storm {
outStream << "}" << std::endl;
}
}
private:
/*!
@ -275,7 +258,7 @@ namespace storm {
*/
void turnRatesToProbabilities() {
for (auto state : this->markovianStates) {
for (auto& transition : this->transitionMatrix.getRow(this->getNondeterministicChoiceIndices()[state])) {
for (auto& transition : this->transitionMatrix.getRowGroup(state)) {
transition.second /= this->exitRates[state];
}
}

36
src/models/Mdp.h
View File

@ -38,8 +38,6 @@ public:
*
* @param probabilityMatrix The transition probability relation of the MDP given by a matrix.
* @param stateLabeling The labeling that assigns a set of atomic propositions to each state.
* @param nondeterministicChoiceIndices The row indices in the sparse matrix at which the nondeterministic
* choices of a given state begin.
* @param optionalStateRewardVector A vector assigning rewards to states.
* @param optionalTransitionRewardVector A sparse matrix that represents an assignment of rewards to the transitions.
* @param optionalChoiceLabeling A vector that represents the labels associated with each nondeterministic choice of
@ -47,11 +45,10 @@ public:
*/
Mdp(storm::storage::SparseMatrix<T> const& transitionMatrix,
storm::models::AtomicPropositionsLabeling const& stateLabeling,
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices,
boost::optional<std::vector<T>> const& optionalStateRewardVector,
boost::optional<std::vector<T>> const& optionalStateRewardVector,
boost::optional<storm::storage::SparseMatrix<T>> const& optionalTransitionRewardMatrix,
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> const& optionalChoiceLabeling)
: AbstractNondeterministicModel<T>(transitionMatrix, stateLabeling, nondeterministicChoiceIndices, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) {
: AbstractNondeterministicModel<T>(transitionMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) {
if (!this->checkValidityOfProbabilityMatrix()) {
LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
@ -75,12 +72,11 @@ public:
*/
Mdp(storm::storage::SparseMatrix<T>&& transitionMatrix,
storm::models::AtomicPropositionsLabeling&& stateLabeling,
std::vector<uint_fast64_t>&& nondeterministicChoiceIndices,
boost::optional<std::vector<T>>&& optionalStateRewardVector,
boost::optional<std::vector<T>>&& optionalStateRewardVector,
boost::optional<storm::storage::SparseMatrix<T>>&& optionalTransitionRewardMatrix,
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>&& optionalChoiceLabeling)
// The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class
: AbstractNondeterministicModel<T>(std::move(transitionMatrix), std::move(stateLabeling), std::move(nondeterministicChoiceIndices), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix),
: AbstractNondeterministicModel<T>(std::move(transitionMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix),
std::move(optionalChoiceLabeling)) {
if (!this->checkValidityOfProbabilityMatrix()) {
LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
@ -144,20 +140,19 @@ public:
std::vector<boost::container::flat_set<uint_fast64_t>> const& choiceLabeling = this->getChoiceLabeling();
storm::storage::SparseMatrixBuilder<T> transitionMatrixBuilder;
std::vector<uint_fast64_t> nondeterministicChoiceIndices;
std::vector<boost::container::flat_set<uint_fast64_t>> newChoiceLabeling;
// Check for each choice of each state, whether the choice labels are fully contained in the given label set.
uint_fast64_t currentRow = 0;
for(uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) {
bool stateHasValidChoice = false;
for (uint_fast64_t choice = this->getNondeterministicChoiceIndices()[state]; choice < this->getNondeterministicChoiceIndices()[state + 1]; ++choice) {
for (uint_fast64_t choice = this->getTransitionMatrix().getRowGroupIndices()[state]; choice < this->getTransitionMatrix().getRowGroupIndices()[state + 1]; ++choice) {
bool choiceValid = std::includes(enabledChoiceLabels.begin(), enabledChoiceLabels.end(), choiceLabeling[choice].begin(), choiceLabeling[choice].end());
// If the choice is valid, copy over all its elements.
if (choiceValid) {
if (!stateHasValidChoice) {
nondeterministicChoiceIndices.push_back(currentRow);
transitionMatrixBuilder.newRowGroup(currentRow);
}
stateHasValidChoice = true;
for (auto const& entry : this->getTransitionMatrix().getRow(choice)) {
@ -170,16 +165,14 @@ public:
// If no choice of the current state may be taken, we insert a self-loop to the state instead.
if (!stateHasValidChoice) {
nondeterministicChoiceIndices.push_back(currentRow);
transitionMatrixBuilder.newRowGroup(currentRow);
transitionMatrixBuilder.addNextValue(currentRow, state, storm::utility::constantOne<T>());
newChoiceLabeling.emplace_back();
++currentRow;
}
}
nondeterministicChoiceIndices.push_back(currentRow);
Mdp<T> restrictedMdp(transitionMatrixBuilder.build(), storm::models::AtomicPropositionsLabeling(this->getStateLabeling()), std::move(nondeterministicChoiceIndices), this->hasStateRewards() ? boost::optional<std::vector<T>>(this->getStateRewardVector()) : boost::optional<std::vector<T>>(), this->hasTransitionRewards() ? boost::optional<storm::storage::SparseMatrix<T>>(this->getTransitionRewardMatrix()) : boost::optional<storm::storage::SparseMatrix<T>>(), boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>(newChoiceLabeling));
Mdp<T> restrictedMdp(transitionMatrixBuilder.build(), storm::models::AtomicPropositionsLabeling(this->getStateLabeling()), this->hasStateRewards() ? boost::optional<std::vector<T>>(this->getStateRewardVector()) : boost::optional<std::vector<T>>(), this->hasTransitionRewards() ? boost::optional<storm::storage::SparseMatrix<T>>(this->getTransitionRewardMatrix()) : boost::optional<storm::storage::SparseMatrix<T>>(), boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>(newChoiceLabeling));
return restrictedMdp;
}
@ -192,15 +185,8 @@ public:
}
virtual std::shared_ptr<AbstractModel<T>> applyScheduler(storm::storage::Scheduler const& scheduler) const override {
storm::storage::SparseMatrix<T> newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), this->getNondeterministicChoiceIndices(), scheduler);
// Construct the new nondeterministic choice indices for the resulting matrix.
std::vector<uint_fast64_t> nondeterministicChoiceIndices(this->getNumberOfStates() + 1);
for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) {
nondeterministicChoiceIndices[state] = state;
}
nondeterministicChoiceIndices[this->getNumberOfStates()] = this->getNumberOfStates();
return std::shared_ptr<AbstractModel<T>>(new Mdp(newTransitionMatrix, this->getStateLabeling(), nondeterministicChoiceIndices, this->hasStateRewards() ? this->getStateRewardVector() : boost::optional<std::vector<T>>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() : boost::optional<storm::storage::SparseMatrix<T>>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>()));
storm::storage::SparseMatrix<T> newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), scheduler);
return std::shared_ptr<AbstractModel<T>>(new Mdp(newTransitionMatrix, this->getStateLabeling(), this->hasStateRewards() ? this->getStateRewardVector() : boost::optional<std::vector<T>>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() : boost::optional<storm::storage::SparseMatrix<T>>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>()));
}
private:

2
src/parser/MarkovAutomatonParser.cpp
View File

@ -19,7 +19,7 @@ namespace storm {
throw storm::exceptions::WrongFormatException() << "Transition rewards are unsupported for Markov automata.";
}
storm::models::MarkovAutomaton<double> resultingAutomaton(std::move(transitionResult.transitionMatrix), std::move(resultLabeling), std::move(transitionResult.nondeterministicChoiceIndices), std::move(transitionResult.markovianStates), std::move(transitionResult.exitRates), std::move(stateRewards), boost::optional<storm::storage::SparseMatrix<double>>(), boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
storm::models::MarkovAutomaton<double> resultingAutomaton(std::move(transitionResult.transitionMatrix), std::move(resultLabeling), std::move(transitionResult.markovianStates), std::move(transitionResult.exitRates), std::move(stateRewards), boost::optional<storm::storage::SparseMatrix<double>>(), boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
return resultingAutomaton;
}

5
src/parser/MarkovAutomatonSparseTransitionParser.cpp
View File

@ -159,7 +159,6 @@ namespace storm {
if (source > lastsource + 1) {
if (fixDeadlocks) {
for (uint_fast64_t index = lastsource + 1; index < source; ++index) {
result.nondeterministicChoiceIndices[index] = currentChoice;
matrixBuilder.newRowGroup(currentChoice);
matrixBuilder.addNextValue(currentChoice, index, 1);
++currentChoice;
@ -172,7 +171,6 @@ namespace storm {
if (source != lastsource) {
// If we skipped to a new state we need to record the beginning of the choices in the nondeterministic choice indices.
result.nondeterministicChoiceIndices[source] = currentChoice;
matrixBuilder.newRowGroup(currentChoice);
}
@ -240,9 +238,6 @@ namespace storm {
// As we have added all entries at this point, we need to finalize the matrix.
result.transitionMatrix = matrixBuilder.build();
// Put a sentinel element at the end.
result.nondeterministicChoiceIndices[firstPassResult.highestStateIndex + 1] = currentChoice;
return result;
}

5
src/parser/MarkovAutomatonSparseTransitionParser.h
View File

@ -39,16 +39,13 @@ namespace storm {
*/
struct ResultType {
ResultType(FirstPassResult const& firstPassResult) : transitionMatrix(), nondeterministicChoiceIndices(firstPassResult.highestStateIndex + 2), markovianChoices(firstPassResult.numberOfChoices), markovianStates(firstPassResult.highestStateIndex + 1), exitRates(firstPassResult.highestStateIndex + 1) {
ResultType(FirstPassResult const& firstPassResult) : transitionMatrix(), markovianChoices(firstPassResult.numberOfChoices), markovianStates(firstPassResult.highestStateIndex + 1), exitRates(firstPassResult.highestStateIndex + 1) {
// Intentionally left empty.
}
// A matrix representing the transitions of the model.
storm::storage::SparseMatrix<double> transitionMatrix;
// A vector indicating which rows of the matrix represent the choices of a given state.
std::vector<uint_fast64_t> nondeterministicChoiceIndices;
// A bit vector indicating which choices are Markovian. By duality, all other choices are probabilitic.
storm::storage::BitVector markovianChoices;

8
src/parser/NondeterministicModelParser.cpp
View File

@ -37,13 +37,13 @@ NondeterministicModelParserResultContainer<double> parseNondeterministicModel(st
storm::models::AtomicPropositionsLabeling resultLabeling(std::move(storm::parser::AtomicPropositionLabelingParser(stateCount, labelingFile)));
NondeterministicModelParserResultContainer<double> result(std::move(resultTransitionSystem), std::move(nondeterministicSparseTransitionParserResult.second), std::move(resultLabeling));
NondeterministicModelParserResultContainer<double> result(std::move(resultTransitionSystem), std::move(resultLabeling));
if (stateRewardFile != "") {
result.stateRewards.reset(storm::parser::SparseStateRewardParser(stateCount, stateRewardFile));
}
if (transitionRewardFile != "") {
RewardMatrixInformationStruct* rewardMatrixInfo = new RewardMatrixInformationStruct(rowCount, stateCount, &result.rowMapping);
RewardMatrixInformationStruct* rewardMatrixInfo = new RewardMatrixInformationStruct(rowCount, stateCount, &result.transitionSystem.getRowGroupIndices());
result.transitionRewards.reset(storm::parser::NondeterministicSparseTransitionParser(transitionRewardFile, rewardMatrixInfo).first);
delete rewardMatrixInfo;
}
@ -58,7 +58,7 @@ NondeterministicModelParserResultContainer<double> parseNondeterministicModel(st
storm::models::Mdp<double> NondeterministicModelParserAsMdp(std::string const & transitionSystemFile, std::string const & labelingFile,
std::string const & stateRewardFile, std::string const & transitionRewardFile) {
NondeterministicModelParserResultContainer<double> parserResult = parseNondeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
return storm::models::Mdp<double>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.rowMapping), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
return storm::models::Mdp<double>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
}
/*!
@ -69,7 +69,7 @@ storm::models::Mdp<double> NondeterministicModelParserAsMdp(std::string const &
storm::models::Ctmdp<double> NondeterministicModelParserAsCtmdp(std::string const & transitionSystemFile, std::string const & labelingFile,
std::string const & stateRewardFile, std::string const & transitionRewardFile) {
NondeterministicModelParserResultContainer<double> parserResult = parseNondeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
return storm::models::Ctmdp<double>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.rowMapping), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
return storm::models::Ctmdp<double>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
}
} /* namespace parser */

9
src/parser/NondeterministicModelParser.h
View File

@ -39,16 +39,15 @@ class NondeterministicModelParserResultContainer {
public:
storm::storage::SparseMatrix<T> transitionSystem;
storm::models::AtomicPropositionsLabeling labeling;
std::vector<uint_fast64_t> rowMapping;
boost::optional<std::vector<T>> stateRewards;
boost::optional<storm::storage::SparseMatrix<T>> transitionRewards;
NondeterministicModelParserResultContainer(storm::storage::SparseMatrix<T>& transitionSystem, std::vector<uint_fast64_t>& rowMapping, storm::models::AtomicPropositionsLabeling& labeling) : transitionSystem(transitionSystem), labeling(labeling), rowMapping(rowMapping) { }
NondeterministicModelParserResultContainer(storm::storage::SparseMatrix<T>&& transitionSystem, std::vector<uint_fast64_t>&& rowMapping, storm::models::AtomicPropositionsLabeling&& labeling) : transitionSystem(std::move(transitionSystem)), labeling(std::move(labeling)), rowMapping(std::move(rowMapping)) { }
NondeterministicModelParserResultContainer(storm::storage::SparseMatrix<T>& transitionSystem, storm::models::AtomicPropositionsLabeling& labeling) : transitionSystem(transitionSystem), labeling(labeling) { }
NondeterministicModelParserResultContainer(storm::storage::SparseMatrix<T>&& transitionSystem, storm::models::AtomicPropositionsLabeling&& labeling) : transitionSystem(std::move(transitionSystem)), labeling(std::move(labeling)) { }
NondeterministicModelParserResultContainer(const NondeterministicModelParserResultContainer & other) : transitionSystem(other.transitionSystem),
labeling(other.labeling), rowMapping(other.rowMapping), stateRewards(other.stateRewards), transitionRewards(other.transitionRewards) {}
labeling(other.labeling), stateRewards(other.stateRewards), transitionRewards(other.transitionRewards) {}
NondeterministicModelParserResultContainer(NondeterministicModelParserResultContainer && other) : transitionSystem(std::move(other.transitionSystem)),
labeling(std::move(other.labeling)), rowMapping(std::move(other.rowMapping)), stateRewards(std::move(other.stateRewards)), transitionRewards(std::move(other.transitionRewards)) {}
labeling(std::move(other.labeling)), stateRewards(std::move(other.stateRewards)), transitionRewards(std::move(other.transitionRewards)) {}
private:
NondeterministicModelParserResultContainer() {}
};

12
src/solver/GmmxxNondeterministicLinearEquationSolver.cpp
View File

@ -42,7 +42,7 @@ namespace storm {
}
template<typename ValueType>
void GmmxxNondeterministicLinearEquationSolver<ValueType>::solveEquationSystem(bool minimize, storm::storage::SparseMatrix<ValueType> const& A, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, std::vector<ValueType>* multiplyResult, std::vector<ValueType>* newX) const {
void GmmxxNondeterministicLinearEquationSolver<ValueType>::solveEquationSystem(bool minimize, storm::storage::SparseMatrix<ValueType> const& A, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult, std::vector<ValueType>* newX) const {
// Transform the transition probability matrix to the gmm++ format to use its arithmetic.
std::unique_ptr<gmm::csr_matrix<ValueType>> gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<ValueType>(A);
@ -75,9 +75,9 @@ namespace storm {
// Reduce the vector x by applying min/max over all nondeterministic choices.
if (minimize) {
storm::utility::vector::reduceVectorMin(*multiplyResult, *newX, nondeterministicChoiceIndices);
storm::utility::vector::reduceVectorMin(*multiplyResult, *newX, A.getRowGroupIndices());
} else {
storm::utility::vector::reduceVectorMax(*multiplyResult, *newX, nondeterministicChoiceIndices);
storm::utility::vector::reduceVectorMax(*multiplyResult, *newX, A.getRowGroupIndices());
}
// Determine whether the method converged.
@ -111,7 +111,7 @@ namespace storm {
}
template<typename ValueType>
void GmmxxNondeterministicLinearEquationSolver<ValueType>::performMatrixVectorMultiplication(bool minimize, storm::storage::SparseMatrix<ValueType> const& A, std::vector<ValueType>& x, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, std::vector<ValueType>* b, uint_fast64_t n, std::vector<ValueType>* multiplyResult) const {
void GmmxxNondeterministicLinearEquationSolver<ValueType>::performMatrixVectorMultiplication(bool minimize, storm::storage::SparseMatrix<ValueType> const& A, std::vector<ValueType>& x, std::vector<ValueType>* b, uint_fast64_t n, std::vector<ValueType>* multiplyResult) const {
// Transform the transition probability matrix to the gmm++ format to use its arithmetic.
std::unique_ptr<gmm::csr_matrix<ValueType>> gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<ValueType>(A);
@ -130,9 +130,9 @@ namespace storm {
}
if (minimize) {
storm::utility::vector::reduceVectorMin(*multiplyResult, x, nondeterministicChoiceIndices);
storm::utility::vector::reduceVectorMin(*multiplyResult, x, A.getRowGroupIndices());
} else {
storm::utility::vector::reduceVectorMax(*multiplyResult, x, nondeterministicChoiceIndices);
storm::utility::vector::reduceVectorMax(*multiplyResult, x, A.getRowGroupIndices());
}
}

4
src/solver/GmmxxNondeterministicLinearEquationSolver.h
View File

@ -30,9 +30,9 @@ namespace storm {
virtual NondeterministicLinearEquationSolver<Type>* clone() const;
virtual void performMatrixVectorMultiplication(bool minimize, storm::storage::SparseMatrix<Type> const& A, std::vector<Type>& x, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, std::vector<Type>* b = nullptr, uint_fast64_t n = 1, std::vector<Type>* multiplyResult = nullptr) const override;
virtual void performMatrixVectorMultiplication(bool minimize, storm::storage::SparseMatrix<Type> const& A, std::vector<Type>& x, std::vector<Type>* b = nullptr, uint_fast64_t n = 1, std::vector<Type>* multiplyResult = nullptr) const override;
virtual void solveEquationSystem(bool minimize, storm::storage::SparseMatrix<Type> const& A, std::vector<Type>& x, std::vector<Type> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, std::vector<Type>* multiplyResult = nullptr, std::vector<Type>* newX = nullptr) const override;
virtual void solveEquationSystem(bool minimize, storm::storage::SparseMatrix<Type> const& A, std::vector<Type>& x, std::vector<Type> const& b, std::vector<Type>* multiplyResult = nullptr, std::vector<Type>* newX = nullptr) const override;
private:
// The required precision for the iterative methods.

12
src/solver/NativeNondeterministicLinearEquationSolver.cpp
View File

@ -40,7 +40,7 @@ namespace storm {
}
template<typename ValueType>
void NativeNondeterministicLinearEquationSolver<ValueType>::solveEquationSystem(bool minimize, storm::storage::SparseMatrix<ValueType> const& A, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, std::vector<ValueType>* multiplyResult, std::vector<ValueType>* newX) const {
void NativeNondeterministicLinearEquationSolver<ValueType>::solveEquationSystem(bool minimize, storm::storage::SparseMatrix<ValueType> const& A, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult, std::vector<ValueType>* newX) const {
// Set up the environment for the power method. If scratch memory was not provided, we need to create it.
bool multiplyResultMemoryProvided = true;
@ -71,9 +71,9 @@ namespace storm {
// Reduce the vector x' by applying min/max for all non-deterministic choices as given by the topmost
// element of the min/max operator stack.
if (minimize) {
storm::utility::vector::reduceVectorMin(*multiplyResult, *newX, nondeterministicChoiceIndices);
storm::utility::vector::reduceVectorMin(*multiplyResult, *newX, A.getRowGroupIndices());
} else {
storm::utility::vector::reduceVectorMax(*multiplyResult, *newX, nondeterministicChoiceIndices);
storm::utility::vector::reduceVectorMax(*multiplyResult, *newX, A.getRowGroupIndices());
}
// Determine whether the method converged.
@ -107,7 +107,7 @@ namespace storm {
}
template<typename ValueType>
void NativeNondeterministicLinearEquationSolver<ValueType>::performMatrixVectorMultiplication(bool minimize, storm::storage::SparseMatrix<ValueType> const& A, std::vector<ValueType>& x, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, std::vector<ValueType>* b, uint_fast64_t n, std::vector<ValueType>* multiplyResult) const {
void NativeNondeterministicLinearEquationSolver<ValueType>::performMatrixVectorMultiplication(bool minimize, storm::storage::SparseMatrix<ValueType> const& A, std::vector<ValueType>& x, std::vector<ValueType>* b, uint_fast64_t n, std::vector<ValueType>* multiplyResult) const {
// If scratch memory was not provided, we need to create it.
bool multiplyResultMemoryProvided = true;
@ -128,9 +128,9 @@ namespace storm {
// Reduce the vector x' by applying min/max for all non-deterministic choices as given by the topmost
// element of the min/max operator stack.
if (minimize) {
storm::utility::vector::reduceVectorMin(*multiplyResult, x, nondeterministicChoiceIndices);
storm::utility::vector::reduceVectorMin(*multiplyResult, x, A.getRowGroupIndices());
} else {
storm::utility::vector::reduceVectorMax(*multiplyResult, x, nondeterministicChoiceIndices);
storm::utility::vector::reduceVectorMax(*multiplyResult, x, A.getRowGroupIndices());
}
}

4
src/solver/NativeNondeterministicLinearEquationSolver.h
View File

@ -30,9 +30,9 @@ namespace storm {
virtual NondeterministicLinearEquationSolver<ValueType>* clone() const override;
virtual void performMatrixVectorMultiplication(bool minimize, storm::storage::SparseMatrix<ValueType> const& A, std::vector<ValueType>& x, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, std::vector<ValueType>* b = nullptr, uint_fast64_t n = 1, std::vector<ValueType>* newX = nullptr) const override;
virtual void performMatrixVectorMultiplication(bool minimize, storm::storage::SparseMatrix<ValueType> const& A, std::vector<ValueType>& x, std::vector<ValueType>* b = nullptr, uint_fast64_t n = 1, std::vector<ValueType>* newX = nullptr) const override;
virtual void solveEquationSystem(bool minimize, storm::storage::SparseMatrix<ValueType> const& A, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, std::vector<ValueType>* multiplyResult = nullptr, std::vector<ValueType>* newX = nullptr) const override;
virtual void solveEquationSystem(bool minimize, storm::storage::SparseMatrix<ValueType> const& A, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult = nullptr, std::vector<ValueType>* newX = nullptr) const override;
private:
// The required precision for the iterative methods.

6
src/solver/NondeterministicLinearEquationSolver.h
View File

@ -32,14 +32,13 @@ namespace storm {
* @param x The solution vector x. The initial values of x represent a guess of the real values to the
* solver, but may be ignored.
* @param b The vector to add after matrix-vector multiplication.
* @param rowGroupIndices A vector indicating which rows of the matrix belong to one group.
* @param multiplyResult If non-null, this memory is used as a scratch memory. If given, the length of this
* vector must be equal to the number of rows of A.
* @param newX If non-null, this memory is used as a scratch memory. If given, the length of this
* vector must be equal to the length of the vector x (and thus to the number of columns of A).
* @return The solution vector x of the system of linear equations as the content of the parameter x.
*/
virtual void solveEquationSystem(bool minimize, storm::storage::SparseMatrix<ValueType> const& A, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<uint_fast64_t> const& rowGroupIndices, std::vector<ValueType>* multiplyResult = nullptr, std::vector<ValueType>* newX = nullptr) const = 0;
virtual void solveEquationSystem(bool minimize, storm::storage::SparseMatrix<ValueType> const& A, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult = nullptr, std::vector<ValueType>* newX = nullptr) const = 0;
/*!
* Performs (repeated) matrix-vector multiplication with the given parameters, i.e. computes
@ -52,14 +51,13 @@ namespace storm {
* @param A The matrix that is to be multiplied with the vector.
* @param x The initial vector that is to be multiplied with the matrix. This is also the output parameter,
* i.e. after the method returns, this vector will contain the computed values.
* @param rowGroupIndices A vector indicating which rows of the matrix belong to one group.
* @param b If not null, this vector is added after each multiplication.
* @param n Specifies the number of iterations the matrix-vector multiplication is performed.
* @param multiplyResult If non-null, this memory is used as a scratch memory. If given, the length of this
* vector must be equal to the number of rows of A.
* @return The result of the repeated matrix-vector multiplication as the content of the vector x.
*/
virtual void performMatrixVectorMultiplication(bool minimize, storm::storage::SparseMatrix<ValueType> const& A, std::vector<ValueType>& x, std::vector<uint_fast64_t> const& rowGroupIndices, std::vector<ValueType>* b = nullptr, uint_fast64_t n = 1, std::vector<ValueType>* multiplyResult = nullptr) const = 0;
virtual void performMatrixVectorMultiplication(bool minimize, storm::storage::SparseMatrix<ValueType> const& A, std::vector<ValueType>& x, std::vector<ValueType>* b = nullptr, uint_fast64_t n = 1, std::vector<ValueType>* multiplyResult = nullptr) const = 0;
};
} // namespace solver

15
src/storage/SparseMatrix.cpp
View File

@ -335,6 +335,11 @@ namespace storm {
return rowGroupIndices.size() - 1;
}
template<typename T>
uint_fast64_t SparseMatrix<T>::getRowGroupSize(uint_fast64_t group) const {
return this->getRowGroupIndices()[group + 1] - this->getRowGroupIndices()[group];
}
template<typename T>
std::vector<uint_fast64_t> const& SparseMatrix<T>::getRowGroupIndices() const {
return rowGroupIndices;
@ -348,7 +353,7 @@ namespace storm {
}
template<typename T>
void SparseMatrix<T>::makeRowGroupsAbsorbing(storm::storage::BitVector const& rowGroupConstraint, std::vector<uint_fast64_t> const& rowGroupIndices) {
void SparseMatrix<T>::makeRowGroupsAbsorbing(storm::storage::BitVector const& rowGroupConstraint) {
for (auto rowGroup : rowGroupConstraint) {
for (uint_fast64_t row = this->getRowGroupIndices()[rowGroup]; row < this->getRowGroupIndices()[rowGroup + 1]; ++row) {
makeRowDirac(row, rowGroup);
@ -364,7 +369,7 @@ namespace storm {
// If the row has no elements in it, we cannot make it absorbing, because we would need to move all elements
// in the vector of nonzeros otherwise.
if (columnValuePtr >= columnValuePtrEnd) {
throw storm::exceptions::InvalidStateException() << "Illegal call to SparseMatrix::makeRowAbsorbing: cannot make row " << row << " absorbing, but there is no entry in this row.";
throw storm::exceptions::InvalidStateException() << "Illegal call to SparseMatrix::makeRowDirac: cannot make row " << row << " absorbing, but there is no entry in this row.";
}
// If there is at least one entry in this row, we can just set it to one, modify its column value to the
@ -400,7 +405,7 @@ namespace storm {
}
template<typename T>
std::vector<T> SparseMatrix<T>::getConstrainedRowGroupSumVector(storm::storage::BitVector const& rowGroupConstraint, std::vector<uint_fast64_t> const& rowGroupIndices, storm::storage::BitVector const& columnConstraint) const {
std::vector<T> SparseMatrix<T>::getConstrainedRowGroupSumVector(storm::storage::BitVector const& rowGroupConstraint, storm::storage::BitVector const& columnConstraint) const {
std::vector<T> result;
result.reserve(rowGroupConstraint.getNumberOfSetBits());
for (auto rowGroup : rowGroupConstraint) {
@ -509,7 +514,7 @@ namespace storm {
}
template<typename T>
SparseMatrix<T> SparseMatrix<T>::selectRowsFromRowGroups(std::vector<uint_fast64_t> const& rowGroupToRowIndexMapping, std::vector<uint_fast64_t> const& rowGroupIndices, bool insertDiagonalEntries) const {
SparseMatrix<T> SparseMatrix<T>::selectRowsFromRowGroups(std::vector<uint_fast64_t> const& rowGroupToRowIndexMapping, bool insertDiagonalEntries) const {
// First, we need to count how many non-zero entries the resulting matrix will have and reserve space for
// diagonal entries if requested.
uint_fast64_t subEntries = 0;
@ -867,7 +872,7 @@ namespace storm {
// Iterate over all row groups.
for (uint_fast64_t group = 0; group < matrix.getRowGroupCount(); ++group) {
out << "\t---- group " << group << " ---- out of " << (matrix.getRowGroupCount() - 1) << " ---- " << std::endl;
out << "\t---- group " << group << "/" << (matrix.getRowGroupCount() - 1) << " ---- " << std::endl;
for (uint_fast64_t i = matrix.getRowGroupIndices()[group]; i < matrix.getRowGroupIndices()[group + 1]; ++i) {
uint_fast64_t nextIndex = matrix.rowIndications[i];

17
src/storage/SparseMatrix.h
View File

@ -346,6 +346,14 @@ namespace storm {
*/
uint_fast64_t getRowGroupCount() const;
/*!
* Returns the size of the given row group.
*
* @param group The group whose size to retrieve.
* @return The number of rows that belong to the given row group.
*/
uint_fast64_t getRowGroupSize(uint_fast64_t group) const;
/*!
* Returns the grouping of rows of this matrix.
*
@ -364,9 +372,8 @@ namespace storm {
* This function makes the groups of rows given by the bit vector absorbing.
*
* @param rowGroupConstraint A bit vector indicating which row groups to make absorbing.
* @param rowGroupIndices A vector indicating which rows belong to a given row group.
*/
void makeRowGroupsAbsorbing(storm::storage::BitVector const& rowGroupConstraint, std::vector<uint_fast64_t> const& rowGroupIndices);
void makeRowGroupsAbsorbing(storm::storage::BitVector const& rowGroupConstraint);
/*!
* This function makes the given row Dirac. This means that all entries will be set to 0 except the one
@ -402,12 +409,11 @@ namespace storm {
* groups.
*
* @param rowGroupConstraint A bit vector that indicates which row groups are to be considered.
* @param rowGroupIndices A vector indicating which rows belong to a given row group.
* @param columnConstraint A bit vector that indicates which columns to sum.
* @return A vector whose entries represent the sums of selected columns for all rows in selected row
* groups.
*/
std::vector<T> getConstrainedRowGroupSumVector(storm::storage::BitVector const& rowGroupConstraint, std::vector<uint_fast64_t> const& rowGroupIndices, storm::storage::BitVector const& columnConstraint) const;
std::vector<T> getConstrainedRowGroupSumVector(storm::storage::BitVector const& rowGroupConstraint, storm::storage::BitVector const& columnConstraint) const;
/*!
* Creates a submatrix of the current matrix by dropping all rows and columns whose bits are not
@ -427,12 +433,11 @@ namespace storm {
* Selects exactly one row from each row group of this matrix and returns the resulting matrix.
*
* @param rowGroupToRowIndexMapping A mapping from each row group index to a selected row in this group.
* @param rowGroupIndices A vector indicating which rows belong to a given row group.
* @param insertDiagonalEntries If set to true, the resulting matrix will have zero entries in column i for
* each row in row group i. This can then be used for inserting other values later.
* @return A submatrix of the current matrix by selecting one row out of each row group.
*/
SparseMatrix selectRowsFromRowGroups(std::vector<uint_fast64_t> const& rowGroupToRowIndexMapping, std::vector<uint_fast64_t> const& rowGroupIndices, bool insertDiagonalEntries = true) const;
SparseMatrix selectRowsFromRowGroups(std::vector<uint_fast64_t> const& rowGroupToRowIndexMapping, bool insertDiagonalEntries = true) const;
/*!
* Transposes the matrix.

4
src/utility/graph.h
View File

@ -347,7 +347,7 @@ namespace storm {
*/
template <typename T>
std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Max(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
return performProb01Max(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), model.getBackwardTransitions(), phiStates, psiStates);
return performProb01Max(model.getTransitionMatrix(), model.getTransitionMatrix().getRowGroupIndices(), model.getBackwardTransitions(), phiStates, psiStates);
}
/*!
@ -554,7 +554,7 @@ namespace storm {
*/
template <typename T>
std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
return performProb01Min(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), model.getBackwardTransitions(), phiStates, psiStates);
return performProb01Min(model.getTransitionMatrix(), model.getTransitionMatrix().getRowGroupIndices(), model.getBackwardTransitions(), phiStates, psiStates);
}
/*!

11
src/utility/matrix.h
View File

@ -14,19 +14,18 @@ namespace storm {
* dropped from the transition matrix. If a state has no choice enabled, it is equipped with a self-loop instead.
*
* @param transitionMatrix The transition matrix of the original system.
* @param nondeterministicChoiceIndices A vector indicating at which rows the choices for the states begin.
* @param scheduler The scheduler to apply to the system.
* @return A transition matrix that corresponds to all transitions of the given system that are selected by the given scheduler.
*/
template <typename T>
storm::storage::SparseMatrix<T> applyScheduler(storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::Scheduler const& scheduler) {
storm::storage::SparseMatrixBuilder<T> matrixBuilder(nondeterministicChoiceIndices.size() - 1, transitionMatrix.getColumnCount());
storm::storage::SparseMatrix<T> applyScheduler(storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::Scheduler const& scheduler) {
storm::storage::SparseMatrixBuilder<T> matrixBuilder(transitionMatrix.getRowGroupCount(), transitionMatrix.getColumnCount());
for (uint_fast64_t state = 0; state < nondeterministicChoiceIndices.size() - 1; ++state) {
for (uint_fast64_t state = 0; state < transitionMatrix.getRowGroupCount(); ++state) {
if (scheduler.isChoiceDefined(state)) {
// Check whether the choice is valid for this state.
uint_fast64_t choice = nondeterministicChoiceIndices[state] + scheduler.getChoice(state);
if (choice >= nondeterministicChoiceIndices[state + 1]) {
uint_fast64_t choice = transitionMatrix.getRowGroupIndices()[state] + scheduler.getChoice(state);
if (choice >= transitionMatrix.getRowGroupIndices()[state + 1]) {
throw storm::exceptions::InvalidStateException() << "Scheduler defines illegal choice " << choice << " for state " << state << ".";
}

41
test/functional/solver/GmmxxNondeterministicLinearEquationSolverTest.cpp
View File

@ -5,64 +5,61 @@
#include "src/settings/Settings.h"
TEST(GmmxxNondeterministicLinearEquationSolver, SolveWithStandardOptions) {
ASSERT_NO_THROW(storm::storage::SparseMatrixBuilder<double> builder);
storm::storage::SparseMatrixBuilder<double> builder;
storm::storage::SparseMatrixBuilder<double> builder(0, 0, 0, true);
ASSERT_NO_THROW(builder.newRowGroup(0));
ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9));
storm::storage::SparseMatrix<double> A;
ASSERT_NO_THROW(A = builder.build(2));
std::vector<uint_fast64_t> nondeterministicChoiceIndices = {0, 2};
std::vector<double> x(1);
std::vector<double> b = {0.099, 0.5};
ASSERT_NO_THROW(storm::solver::GmmxxNondeterministicLinearEquationSolver<double> solver);
storm::solver::GmmxxNondeterministicLinearEquationSolver<double> solver;
ASSERT_NO_THROW(solver.solveEquationSystem(true, A, x, b, nondeterministicChoiceIndices));
ASSERT_NO_THROW(solver.solveEquationSystem(true, A, x, b));
ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_NO_THROW(solver.solveEquationSystem(false, A, x, b, nondeterministicChoiceIndices));
ASSERT_NO_THROW(solver.solveEquationSystem(false, A, x, b));
ASSERT_LT(std::abs(x[0] - 0.989991), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
}
TEST(GmmxxNondeterministicLinearEquationSolver, MatrixVectorMultiplication) {
ASSERT_NO_THROW(storm::storage::SparseMatrixBuilder<double> builder);
storm::storage::SparseMatrixBuilder<double> builder;
storm::storage::SparseMatrixBuilder<double> builder(0, 0, 0, true);
ASSERT_NO_THROW(builder.newRowGroup(0));
ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9));
ASSERT_NO_THROW(builder.addNextValue(0, 1, 0.099));
ASSERT_NO_THROW(builder.addNextValue(0, 2, 0.001));
ASSERT_NO_THROW(builder.addNextValue(1, 1, 0.5));
ASSERT_NO_THROW(builder.addNextValue(1, 2, 0.5));
ASSERT_NO_THROW(builder.newRowGroup(2));
ASSERT_NO_THROW(builder.addNextValue(2, 1, 1));
ASSERT_NO_THROW(builder.newRowGroup(3));
ASSERT_NO_THROW(builder.addNextValue(3, 2, 1));
storm::storage::SparseMatrix<double> A;
ASSERT_NO_THROW(A = builder.build());
std::vector<uint_fast64_t> nondeterministicChoiceIndices = {0, 2, 3, 4};
std::vector<double> x = {0, 1, 0};
ASSERT_NO_THROW(storm::solver::GmmxxNondeterministicLinearEquationSolver<double> solver);
storm::solver::GmmxxNondeterministicLinearEquationSolver<double> solver;
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, A, x, nondeterministicChoiceIndices, nullptr, 1));
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, A, x, nullptr, 1));
ASSERT_LT(std::abs(x[0] - 0.099), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
x = {0, 1, 0};
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, A, x, nondeterministicChoiceIndices, nullptr, 2));
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, A, x, nullptr, 2));
ASSERT_LT(std::abs(x[0] - 0.1881), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
x = {0, 1, 0};
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, A, x, nondeterministicChoiceIndices, nullptr, 20));
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, A, x, nullptr, 20));
ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
x = {0, 1, 0};
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(false, A, x, nondeterministicChoiceIndices, nullptr, 1));
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(false, A, x, nullptr, 1));
ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
x = {0, 1, 0};
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(false, A, x, nondeterministicChoiceIndices, nullptr, 20));
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(false, A, x, nullptr, 20));
ASSERT_LT(std::abs(x[0] - 0.9238082658), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
}

31
test/functional/solver/NativeNondeterministicLinearEquationSolverTest.cpp
View File

@ -5,64 +5,61 @@
#include "src/settings/Settings.h"
TEST(NativeNondeterministicLinearEquationSolver, SolveWithStandardOptions) {
ASSERT_NO_THROW(storm::storage::SparseMatrixBuilder<double> builder);
storm::storage::SparseMatrixBuilder<double> builder;
storm::storage::SparseMatrixBuilder<double> builder(0, 0, 0, true);
ASSERT_NO_THROW(builder.newRowGroup(0));
ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9));
storm::storage::SparseMatrix<double> A;
ASSERT_NO_THROW(A = builder.build(2));
std::vector<uint_fast64_t> nondeterministicChoiceIndices = {0, 2};
std::vector<double> x(1);
std::vector<double> b = {0.099, 0.5};
ASSERT_NO_THROW(storm::solver::NativeNondeterministicLinearEquationSolver<double> solver);
storm::solver::NativeNondeterministicLinearEquationSolver<double> solver;
ASSERT_NO_THROW(solver.solveEquationSystem(true, A, x, b, nondeterministicChoiceIndices));
ASSERT_NO_THROW(solver.solveEquationSystem(true, A, x, b));
ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
ASSERT_NO_THROW(solver.solveEquationSystem(false, A, x, b, nondeterministicChoiceIndices));
ASSERT_NO_THROW(solver.solveEquationSystem(false, A, x, b));
ASSERT_LT(std::abs(x[0] - 0.989991), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
}
TEST(NativeNondeterministicLinearEquationSolver, MatrixVectorMultiplication) {
ASSERT_NO_THROW(storm::storage::SparseMatrixBuilder<double> builder);
storm::storage::SparseMatrixBuilder<double> builder;
storm::storage::SparseMatrixBuilder<double> builder(0, 0, 0, true);
ASSERT_NO_THROW(builder.newRowGroup(0));
ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9));
ASSERT_NO_THROW(builder.addNextValue(0, 1, 0.099));
ASSERT_NO_THROW(builder.addNextValue(0, 2, 0.001));
ASSERT_NO_THROW(builder.addNextValue(1, 1, 0.5));
ASSERT_NO_THROW(builder.addNextValue(1, 2, 0.5));
ASSERT_NO_THROW(builder.newRowGroup(2));
ASSERT_NO_THROW(builder.addNextValue(2, 1, 1));
ASSERT_NO_THROW(builder.newRowGroup(3));
ASSERT_NO_THROW(builder.addNextValue(3, 2, 1));
storm::storage::SparseMatrix<double> A;
ASSERT_NO_THROW(A = builder.build());
std::vector<uint_fast64_t> nondeterministicChoiceIndices = {0, 2, 3, 4};
std::vector<double> x = {0, 1, 0};
ASSERT_NO_THROW(storm::solver::NativeNondeterministicLinearEquationSolver<double> solver);
storm::solver::NativeNondeterministicLinearEquationSolver<double> solver;
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, A, x, nondeterministicChoiceIndices, nullptr, 1));
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, A, x, nullptr, 1));
ASSERT_LT(std::abs(x[0] - 0.099), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
x = {0, 1, 0};
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, A, x, nondeterministicChoiceIndices, nullptr, 2));
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, A, x, nullptr, 2));
ASSERT_LT(std::abs(x[0] - 0.1881), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
x = {0, 1, 0};
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, A, x, nondeterministicChoiceIndices, nullptr, 20));
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(true, A, x, nullptr, 20));
ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
x = {0, 1, 0};
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(false, A, x, nondeterministicChoiceIndices, nullptr, 1));
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(false, A, x, nullptr, 1));
ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
x = {0, 1, 0};
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(false, A, x, nondeterministicChoiceIndices, nullptr, 20));
ASSERT_NO_THROW(solver.performMatrixVectorMultiplication(false, A, x, nullptr, 20));
ASSERT_LT(std::abs(x[0] - 0.9238082658), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
}

2
test/functional/storage/MaximalEndComponentDecompositionTest.cpp
View File

@ -7,7 +7,7 @@ TEST(MaximalEndComponentDecomposition, FullSystem1) {
storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.lab", "", "");
std::shared_ptr<storm::models::MarkovAutomaton<double>> markovAutomaton = parser.getModel<storm::models::MarkovAutomaton<double>>();
storm::storage::MaximalEndComponentDecomposition<double> mecDecomposition;
ASSERT_NO_THROW(mecDecomposition = storm::storage::MaximalEndComponentDecomposition<double>(*markovAutomaton));

14
test/functional/storage/SparseMatrixTest.cpp
View File

@ -237,12 +237,10 @@ TEST(SparseMatrix, MakeRowGroupAbsorbing) {
storm::storage::SparseMatrix<double> matrix;
ASSERT_NO_THROW(matrix = matrixBuilder.build());
std::vector<uint_fast64_t> rowGroupIndices = {0, 2, 4, 5};
storm::storage::BitVector absorbingRowGroups(3);
absorbingRowGroups.set(1);
ASSERT_NO_THROW(matrix.makeRowGroupsAbsorbing(absorbingRowGroups, rowGroupIndices));
ASSERT_NO_THROW(matrix.makeRowGroupsAbsorbing(absorbingRowGroups));
storm::storage::SparseMatrixBuilder<double> matrixBuilder2(0, 0, 0, true);
ASSERT_NO_THROW(matrixBuilder2.newRowGroup(0));
@ -301,8 +299,6 @@ TEST(SparseMatrix, ConstrainedRowSumVector) {
storm::storage::SparseMatrix<double> matrix2;
ASSERT_NO_THROW(matrix2 = matrixBuilder2.build());
std::vector<uint_fast64_t> rowGroupIndices = {0, 2, 4, 5};
storm::storage::BitVector rowGroupConstraint(3);
rowGroupConstraint.set(1);
@ -310,8 +306,8 @@ TEST(SparseMatrix, ConstrainedRowSumVector) {
columnConstraint2.set(2);
columnConstraint2.set(3);
ASSERT_NO_THROW(std::vector<double> constrainedRowSum2 = matrix2.getConstrainedRowGroupSumVector(rowGroupConstraint, rowGroupIndices, columnConstraint2));
std::vector<double> constrainedRowSum2 = matrix2.getConstrainedRowGroupSumVector(rowGroupConstraint, rowGroupIndices, columnConstraint2);
ASSERT_NO_THROW(std::vector<double> constrainedRowSum2 = matrix2.getConstrainedRowGroupSumVector(rowGroupConstraint, columnConstraint2));
std::vector<double> constrainedRowSum2 = matrix2.getConstrainedRowGroupSumVector(rowGroupConstraint, columnConstraint2);
ASSERT_TRUE(constrainedRowSum2 == std::vector<double>({0, 2.3}));
}
@ -359,8 +355,8 @@ TEST(SparseMatrix, Submatrix) {
std::vector<uint_fast64_t> rowGroupToIndexMapping = {0, 0, 1, 0};
ASSERT_NO_THROW(storm::storage::SparseMatrix<double> matrix4 = matrix.selectRowsFromRowGroups(rowGroupToIndexMapping, rowGroupIndices));
storm::storage::SparseMatrix<double> matrix4 = matrix.selectRowsFromRowGroups(rowGroupToIndexMapping, rowGroupIndices);
ASSERT_NO_THROW(storm::storage::SparseMatrix<double> matrix4 = matrix.selectRowsFromRowGroups(rowGroupToIndexMapping));
storm::storage::SparseMatrix<double> matrix4 = matrix.selectRowsFromRowGroups(rowGroupToIndexMapping);
storm::storage::SparseMatrixBuilder<double> matrixBuilder5(4, 4, 8);
ASSERT_NO_THROW(matrixBuilder5.addNextValue(0, 1, 1.0));

Write Preview
Loading…
Cancel
Save