diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 5a10795b6..a2932b9c9 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -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 nondeterministicChoiceIndices; - // The state reward vector. std::vector stateRewards; @@ -108,10 +105,10 @@ namespace storm { result = std::unique_ptr>(new storm::models::Ctmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); break; case storm::ir::Program::MDP: - result = std::unique_ptr>(new storm::models::Mdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.nondeterministicChoiceIndices), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); + result = std::unique_ptr>(new storm::models::Mdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); break; case storm::ir::Program::CTMDP: - result = std::unique_ptr>(new storm::models::Ctmdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.nondeterministicChoiceIndices), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); + result = std::unique_ptr>(new storm::models::Ctmdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), 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>> buildMatrices(storm::ir::Program const& program, VariableInformation const& variableInformation, std::vector const& transitionRewards, StateInformation& stateInformation, bool deterministicModel, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, storm::storage::SparseMatrixBuilder& transitionRewardMatrixBuilder) { - std::vector nondeterministicChoiceIndices; + static std::vector> buildMatrices(storm::ir::Program const& program, VariableInformation const& variableInformation, std::vector const& transitionRewards, StateInformation& stateInformation, bool deterministicModel, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, storm::storage::SparseMatrixBuilder& transitionRewardMatrixBuilder) { std::vector> 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 transitionMatrixBuilder(0, 0, 0, !deterministicModel, 0); storm::storage::SparseMatrixBuilder transitionRewardMatrixBuilder(0, 0, 0, !deterministicModel, 0); - std::pair, std::vector>> 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(); diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index d1259d573..a4cd0844a 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -49,7 +49,7 @@ namespace storm { } std::pair, storm::storage::TotalScheduler> computeUnboundedUntilProbabilities(bool min, storm::storage::BitVector const& leftStates, storm::storage::BitVector const& rightStates, bool qualitative) const { - return storm::modelchecker::prctl::SparseMdpPrctlModelChecker::computeUnboundedUntilProbabilities(min, this->getModel().getTransitionMatrix(), this->getModel().getNondeterministicChoiceIndices(), this->getModel().getBackwardTransitions(), this->getModel().getInitialStates(), leftStates, rightStates, nondeterministicLinearEquationSolver, qualitative); + return storm::modelchecker::prctl::SparseMdpPrctlModelChecker::computeUnboundedUntilProbabilities(min, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getInitialStates(), leftStates, rightStates, nondeterministicLinearEquationSolver, qualitative); } std::vector checkTimeBoundedUntil(storm::property::csl::TimeBoundedUntil const& formula, bool qualitative) const { @@ -86,18 +86,16 @@ namespace storm { return result; } - static void computeBoundedReachabilityProbabilities(bool min, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, std::vector const& exitRates, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps) { + static void computeBoundedReachabilityProbabilities(bool min, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& 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 aMarkovian = transitionMatrix.getSubmatrix(markovianNonGoalStates, nondeterministicChoiceIndices, true); - typename storm::storage::SparseMatrix aMarkovianToProbabilistic = transitionMatrix.getSubmatrix(markovianNonGoalStates, probabilisticNonGoalStates, nondeterministicChoiceIndices); - std::vector markovianNondeterministicChoiceIndices = storm::utility::vector::getConstrainedOffsetVector(nondeterministicChoiceIndices, markovianNonGoalStates); - typename storm::storage::SparseMatrix aProbabilistic = transitionMatrix.getSubmatrix(probabilisticNonGoalStates, nondeterministicChoiceIndices); - typename storm::storage::SparseMatrix aProbabilisticToMarkovian = transitionMatrix.getSubmatrix(probabilisticNonGoalStates, markovianNonGoalStates, nondeterministicChoiceIndices); - std::vector probabilisticNondeterministicChoiceIndices = storm::utility::vector::getConstrainedOffsetVector(nondeterministicChoiceIndices, probabilisticNonGoalStates); + typename storm::storage::SparseMatrix aMarkovian = transitionMatrix.getSubmatrix(true, markovianNonGoalStates, markovianNonGoalStates, true); + typename storm::storage::SparseMatrix aMarkovianToProbabilistic = transitionMatrix.getSubmatrix(true, markovianNonGoalStates, probabilisticNonGoalStates); + typename storm::storage::SparseMatrix aProbabilistic = transitionMatrix.getSubmatrix(true, probabilisticNonGoalStates, probabilisticNonGoalStates); + typename storm::storage::SparseMatrix 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 bMarkovian(markovianNonGoalStates.getNumberOfSetBits()); // Compute the two fixed right-hand side vectors, one for Markovian states and one for the probabilistic ones. - std::vector bProbabilisticFixed = transitionMatrix.getConstrainedRowSumVector(probabilisticNonGoalStates, nondeterministicChoiceIndices, goalStates); + std::vector bProbabilisticFixed = transitionMatrix.getConstrainedRowSumVector(probabilisticNonGoalStates, goalStates); std::vector bMarkovianFixed; bMarkovianFixed.reserve(markovianNonGoalStates.getNumberOfSetBits()); for (auto state : markovianNonGoalStates) { bMarkovianFixed.push_back(storm::utility::constantZero()); - 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 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 const& nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices(); typename storm::storage::SparseMatrix const& transitionMatrix = this->getModel().getTransitionMatrix(); std::vector const& exitRates = this->getModel().getExitRates(); storm::storage::BitVector const& markovianStates = this->getModel().getMarkovianStates(); @@ -207,7 +204,7 @@ namespace storm { std::vector vProbabilistic(probabilisticNonGoalStates.getNumberOfSetBits()); std::vector 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()) { @@ -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 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 b; - std::vector sspNondeterministicChoiceIndices; - sspNondeterministicChoiceIndices.reserve(numberOfStatesNotInMecs + mecDecomposition.size() + 1); - typename storm::storage::SparseMatrixBuilder sspMatrixBuilder; + typename storm::storage::SparseMatrixBuilder 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 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 sspMatrix = sspMatrixBuilder.build(currentChoice + 1); std::vector x(numberOfStatesNotInMecs + mecDecomposition.size()); - nondeterministicLinearEquationSolver->solveEquationSystem(min, sspMatrix, x, b, sspNondeterministicChoiceIndices); + nondeterministicLinearEquationSolver->solveEquationSystem(min, sspMatrix, x, b); // Prepare result vector. std::vector 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 x(maybeStates.getNumberOfSetBits()); - std::vector subNondeterministicChoiceIndices = storm::utility::vector::getConstrainedOffsetVector(this->getModel().getNondeterministicChoiceIndices(), maybeStates); - storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(maybeStates, this->getModel().getNondeterministicChoiceIndices()); + storm::storage::SparseMatrix 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 rewardValues(stateRewards); @@ -576,7 +567,7 @@ namespace storm { // Solve the corresponding system of equations. std::shared_ptr> nondeterministiclinearEquationSolver = storm::utility::solver::getNondeterministicLinearEquationSolver(); - nondeterministiclinearEquationSolver->solveEquationSystem(min, submatrix, x, b, subNondeterministicChoiceIndices); + nondeterministiclinearEquationSolver->solveEquationSystem(min, submatrix, x, b); // Create resulting vector. std::vector result(this->getModel().getNumberOfStates()); diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 0e319e67f..868f78722 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -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 submatrix = this->getModel().getTransitionMatrix().getSubmatrix(true, statesWithProbabilityGreater0, statesWithProbabilityGreater0, false); - // Get the "new" nondeterministic choice indices for the submatrix. - std::vector 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 subresult(statesWithProbabilityGreater0.getNumberOfSetBits()); storm::utility::vector::setVectorValues(subresult, rightStatesInReducedSystem, storm::utility::constantOne()); - 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 result(this->getModel().getNumberOfStates()); storm::utility::vector::setVectorValues(result, nextStates, storm::utility::constantOne()); - 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, storm::storage::TotalScheduler> computeUnboundedUntilProbabilities(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, std::vector nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::shared_ptr> nondeterministicLinearEquationSolver, bool qualitative) { + static std::pair, storm::storage::TotalScheduler> computeUnboundedUntilProbabilities(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::shared_ptr> 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 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 submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, false); - // Get the "new" nondeterministic choice indices for the submatrix. - std::vector 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 b = transitionMatrix.getConstrainedRowGroupSumVector(maybeStates, nondeterministicChoiceIndices, statesWithProbability1); + std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(maybeStates, statesWithProbability1); // Create vector for results for maybe states. std::vector 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(result, maybeStates, x); @@ -344,13 +338,13 @@ namespace storm { storm::utility::vector::setVectorValues(result, statesWithProbability1, storm::utility::constantOne()); // 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, 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 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 submatrix = this->getModel().getTransitionMatrix().getSubmatrix(true, maybeStates, maybeStates, false); - // Get the "new" nondeterministic choice indices for the submatrix. - std::vector 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 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 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 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 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(result, maybeStates, x); @@ -535,7 +526,7 @@ namespace storm { storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::constantInfinity()); // 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 const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, std::vector const& result, std::vector const* stateRewardVector = nullptr, storm::storage::SparseMatrix const* transitionRewardMatrix = nullptr) { + static storm::storage::TotalScheduler computeExtremalScheduler(bool minimize, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& result, std::vector const* stateRewardVector = nullptr, storm::storage::SparseMatrix const* transitionRewardMatrix = nullptr) { std::vector temporaryResult(result.size()); std::vector nondeterministicResult(transitionMatrix.getRowCount()); transitionMatrix.multiplyWithVector(result, nondeterministicResult); @@ -560,12 +550,12 @@ namespace storm { totalRewardVector = transitionMatrix.getPointwiseProductRowSumVector(*transitionRewardMatrix); if (stateRewardVector != nullptr) { std::vector 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 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); diff --git a/src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h b/src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h index 77fa27543..2a584a4d0 100644 --- a/src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h @@ -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 const& matrix, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices) const { + void solveEquationSystem(storm::storage::SparseMatrix const& matrix, std::vector& x, std::vector 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. diff --git a/src/models/AbstractDeterministicModel.h b/src/models/AbstractDeterministicModel.h index 4ef21986e..c72b914de 100644 --- a/src/models/AbstractDeterministicModel.h +++ b/src/models/AbstractDeterministicModel.h @@ -70,11 +70,7 @@ class AbstractDeterministicModel: public AbstractModel { AbstractDeterministicModel(AbstractDeterministicModel && other) : AbstractModel(std::move(other)) { // Intentionally left empty. } - - virtual typename storm::storage::SparseMatrix::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 diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index 3a77907a6..301c806d3 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -203,8 +203,10 @@ class AbstractModel: public std::enable_shared_from_this> { * @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::const_rows getRows(uint_fast64_t state) const = 0; - + virtual typename storm::storage::SparseMatrix::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. diff --git a/src/models/AbstractNondeterministicModel.h b/src/models/AbstractNondeterministicModel.h index fdc005b41..0058377a6 100644 --- a/src/models/AbstractNondeterministicModel.h +++ b/src/models/AbstractNondeterministicModel.h @@ -30,12 +30,11 @@ namespace storm { */ AbstractNondeterministicModel(storm::storage::SparseMatrix const& transitionMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, - std::vector const& nondeterministicChoiceIndices, boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix, boost::optional>> const& optionalChoiceLabeling) : AbstractModel(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&& transitionMatrix, storm::models::AtomicPropositionsLabeling&& stateLabeling, - std::vector&& nondeterministicChoiceIndices, boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix, boost::optional>>&& optionalChoiceLabeling) - // The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class : AbstractModel(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(other), - nondeterministicChoiceIndices(other.nondeterministicChoiceIndices) { + AbstractNondeterministicModel(AbstractNondeterministicModel const& other) : AbstractModel(other) { // Intentionally left empty. } /*! * Move Constructor. */ - AbstractNondeterministicModel(AbstractNondeterministicModel&& other) : AbstractModel(std::move(other)), - nondeterministicChoiceIndices(std::move(other.nondeterministicChoiceIndices)) { + AbstractNondeterministicModel(AbstractNondeterministicModel&& other) : AbstractModel(std::move(other)) { // Intentionally left empty. } @@ -97,7 +92,7 @@ namespace storm { * measured in bytes. */ virtual uint_fast64_t getSizeInMemory() const { - return AbstractModel::getSizeInMemory() + nondeterministicChoiceIndices.size() * sizeof(uint_fast64_t); + return AbstractModel::getSizeInMemory(); } /*! @@ -107,13 +102,9 @@ namespace storm { * of a certain state. */ std::vector const& getNondeterministicChoiceIndices() const { - return nondeterministicChoiceIndices; + return this->getTransitionMatrix().getRowGroupIndices(); } - virtual typename storm::storage::SparseMatrix::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::getHash(nondeterministicChoiceIndices); boost::hash_combine(result, AbstractModel::getHash()); - boost::hash_combine(result, hashTmp); return result; } @@ -157,13 +146,13 @@ namespace storm { AbstractModel::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::const_rows row = this->transitionMatrix.getRow(nondeterministicChoiceIndices[state] + choice); + typename storm::storage::SparseMatrix::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 nondeterministicChoiceIndices; }; } // namespace models } // namespace storm diff --git a/src/models/Ctmc.h b/src/models/Ctmc.h index 25d128996..229ccfe9e 100644 --- a/src/models/Ctmc.h +++ b/src/models/Ctmc.h @@ -88,12 +88,7 @@ public: } virtual std::shared_ptr> applyScheduler(storm::storage::Scheduler const& scheduler) const override { - std::vector 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 newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), nondeterministicChoiceIndices, scheduler); + storm::storage::SparseMatrix newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), scheduler); return std::shared_ptr>(new Ctmc(newTransitionMatrix, this->getStateLabeling(), this->hasStateRewards() ? this->getStateRewardVector() : boost::optional>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() : boost::optional>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional>>())); } diff --git a/src/models/Ctmdp.h b/src/models/Ctmdp.h index f1a162a2f..4e690d871 100644 --- a/src/models/Ctmdp.h +++ b/src/models/Ctmdp.h @@ -39,11 +39,10 @@ public: */ Ctmdp(storm::storage::SparseMatrix const& probabilityMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, - std::vector const& nondeterministicChoiceIndices, - boost::optional> const& optionalStateRewardVector, + boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix, boost::optional>> const& optionalChoiceLabeling) - : AbstractNondeterministicModel(probabilityMatrix, stateLabeling, nondeterministicChoiceIndices, optionalStateRewardVector, optionalTransitionRewardMatrix, + : AbstractNondeterministicModel(probabilityMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) { if (!this->checkValidityOfProbabilityMatrix()) { LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); @@ -62,12 +61,11 @@ public: */ Ctmdp(storm::storage::SparseMatrix&& probabilityMatrix, storm::models::AtomicPropositionsLabeling&& stateLabeling, - std::vector&& nondeterministicChoiceIndices, - boost::optional>&& optionalStateRewardVector, + boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix, boost::optional>> const& optionalChoiceLabeling) // The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class - : AbstractNondeterministicModel(std::move(probabilityMatrix), std::move(stateLabeling), std::move(nondeterministicChoiceIndices), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix), std::move(optionalChoiceLabeling)) { + : AbstractNondeterministicModel(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> applyScheduler(storm::storage::Scheduler const& scheduler) const override { - storm::storage::SparseMatrix newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), this->getNondeterministicChoiceIndices(), scheduler); - - // Construct the new nondeterministic choice indices for the resulting matrix. - std::vector 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>(new Ctmdp(newTransitionMatrix, this->getStateLabeling(), nondeterministicChoiceIndices, this->hasStateRewards() ? this->getStateRewardVector() : boost::optional>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() : boost::optional>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional>>())); + storm::storage::SparseMatrix newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), scheduler); + return std::shared_ptr>(new Ctmdp(newTransitionMatrix, this->getStateLabeling(), this->hasStateRewards() ? this->getStateRewardVector() : boost::optional>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() : boost::optional>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional>>())); } private: diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index 03f03ec7f..b599774f9 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -286,13 +286,7 @@ public: } virtual std::shared_ptr> applyScheduler(storm::storage::Scheduler const& scheduler) const override { - std::vector 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 newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), nondeterministicChoiceIndices, scheduler); - + storm::storage::SparseMatrix newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), scheduler); return std::shared_ptr>(new Dtmc(newTransitionMatrix, this->getStateLabeling(), this->hasStateRewards() ? this->getStateRewardVector() : boost::optional>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() : boost::optional>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional>>())); } diff --git a/src/models/MarkovAutomaton.h b/src/models/MarkovAutomaton.h index 5f1a3aeb9..2e8f6f840 100644 --- a/src/models/MarkovAutomaton.h +++ b/src/models/MarkovAutomaton.h @@ -24,10 +24,10 @@ namespace storm { public: MarkovAutomaton(storm::storage::SparseMatrix const& transitionMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, - std::vector& nondeterministicChoiceIndices, storm::storage::BitVector const& markovianStates, std::vector const& exitRates, + storm::storage::BitVector const& markovianStates, std::vector const& exitRates, boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix, boost::optional>> const& optionalChoiceLabeling) - : AbstractNondeterministicModel(transitionMatrix, stateLabeling, nondeterministicChoiceIndices, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling), + : AbstractNondeterministicModel(transitionMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling), markovianStates(markovianStates), exitRates(exitRates), closed(false) { this->turnRatesToProbabilities(); @@ -42,12 +42,11 @@ namespace storm { MarkovAutomaton(storm::storage::SparseMatrix&& transitionMatrix, storm::models::AtomicPropositionsLabeling&& stateLabeling, - std::vector&& nondeterministicChoiceIndices, storm::storage::BitVector const& markovianStates, std::vector const& exitRates, boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix, boost::optional>>&& optionalChoiceLabeling) - : AbstractNondeterministicModel(std::move(transitionMatrix), std::move(stateLabeling), std::move(nondeterministicChoiceIndices), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix), + : AbstractNondeterministicModel(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 newTransitionMatrixBuilder; - std::vector newNondeterministicChoiceIndices(this->getNumberOfStates() + 1); + storm::storage::SparseMatrixBuilder 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 newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), this->getNondeterministicChoiceIndices(), scheduler); - - // Construct the new nondeterministic choice indices for the resulting matrix. - std::vector 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>(new MarkovAutomaton(newTransitionMatrix, this->getStateLabeling(), nondeterministicChoiceIndices, markovianStates, exitRates, this->hasStateRewards() ? this->getStateRewardVector() : boost::optional>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() : boost::optional>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional>>())); + storm::storage::SparseMatrix newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), scheduler); + return std::shared_ptr>(new MarkovAutomaton(newTransitionMatrix, this->getStateLabeling(), markovianStates, exitRates, this->hasStateRewards() ? this->getStateRewardVector() : boost::optional>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() : boost::optional>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional>>())); } virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const override { AbstractModel::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::const_rows row = this->transitionMatrix.getRow(this->getNondeterministicChoiceIndices()[state] + choice); + typename storm::storage::SparseMatrix::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]; } } diff --git a/src/models/Mdp.h b/src/models/Mdp.h index 235d4f8cf..61858fefa 100644 --- a/src/models/Mdp.h +++ b/src/models/Mdp.h @@ -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 const& transitionMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, - std::vector const& nondeterministicChoiceIndices, - boost::optional> const& optionalStateRewardVector, + boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix, boost::optional>> const& optionalChoiceLabeling) - : AbstractNondeterministicModel(transitionMatrix, stateLabeling, nondeterministicChoiceIndices, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) { + : AbstractNondeterministicModel(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&& transitionMatrix, storm::models::AtomicPropositionsLabeling&& stateLabeling, - std::vector&& nondeterministicChoiceIndices, - boost::optional>&& optionalStateRewardVector, + boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix, boost::optional>>&& optionalChoiceLabeling) // The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class - : AbstractNondeterministicModel(std::move(transitionMatrix), std::move(stateLabeling), std::move(nondeterministicChoiceIndices), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix), + : AbstractNondeterministicModel(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> const& choiceLabeling = this->getChoiceLabeling(); storm::storage::SparseMatrixBuilder transitionMatrixBuilder; - std::vector nondeterministicChoiceIndices; std::vector> 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()); newChoiceLabeling.emplace_back(); ++currentRow; } } - - nondeterministicChoiceIndices.push_back(currentRow); - - Mdp restrictedMdp(transitionMatrixBuilder.build(), storm::models::AtomicPropositionsLabeling(this->getStateLabeling()), std::move(nondeterministicChoiceIndices), this->hasStateRewards() ? boost::optional>(this->getStateRewardVector()) : boost::optional>(), this->hasTransitionRewards() ? boost::optional>(this->getTransitionRewardMatrix()) : boost::optional>(), boost::optional>>(newChoiceLabeling)); + + Mdp restrictedMdp(transitionMatrixBuilder.build(), storm::models::AtomicPropositionsLabeling(this->getStateLabeling()), this->hasStateRewards() ? boost::optional>(this->getStateRewardVector()) : boost::optional>(), this->hasTransitionRewards() ? boost::optional>(this->getTransitionRewardMatrix()) : boost::optional>(), boost::optional>>(newChoiceLabeling)); return restrictedMdp; } @@ -192,15 +185,8 @@ public: } virtual std::shared_ptr> applyScheduler(storm::storage::Scheduler const& scheduler) const override { - storm::storage::SparseMatrix newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), this->getNondeterministicChoiceIndices(), scheduler); - - // Construct the new nondeterministic choice indices for the resulting matrix. - std::vector 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>(new Mdp(newTransitionMatrix, this->getStateLabeling(), nondeterministicChoiceIndices, this->hasStateRewards() ? this->getStateRewardVector() : boost::optional>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() : boost::optional>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional>>())); + storm::storage::SparseMatrix newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), scheduler); + return std::shared_ptr>(new Mdp(newTransitionMatrix, this->getStateLabeling(), this->hasStateRewards() ? this->getStateRewardVector() : boost::optional>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() : boost::optional>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional>>())); } private: diff --git a/src/parser/MarkovAutomatonParser.cpp b/src/parser/MarkovAutomatonParser.cpp index a43dcf4fd..2e673da76 100644 --- a/src/parser/MarkovAutomatonParser.cpp +++ b/src/parser/MarkovAutomatonParser.cpp @@ -19,7 +19,7 @@ namespace storm { throw storm::exceptions::WrongFormatException() << "Transition rewards are unsupported for Markov automata."; } - storm::models::MarkovAutomaton 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>(), boost::optional>>()); + storm::models::MarkovAutomaton resultingAutomaton(std::move(transitionResult.transitionMatrix), std::move(resultLabeling), std::move(transitionResult.markovianStates), std::move(transitionResult.exitRates), std::move(stateRewards), boost::optional>(), boost::optional>>()); return resultingAutomaton; } diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/parser/MarkovAutomatonSparseTransitionParser.cpp index 6f5ff617c..aa7a1406e 100644 --- a/src/parser/MarkovAutomatonSparseTransitionParser.cpp +++ b/src/parser/MarkovAutomatonSparseTransitionParser.cpp @@ -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; } diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.h b/src/parser/MarkovAutomatonSparseTransitionParser.h index 683605361..48ed619ef 100644 --- a/src/parser/MarkovAutomatonSparseTransitionParser.h +++ b/src/parser/MarkovAutomatonSparseTransitionParser.h @@ -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 transitionMatrix; - // A vector indicating which rows of the matrix represent the choices of a given state. - std::vector nondeterministicChoiceIndices; - // A bit vector indicating which choices are Markovian. By duality, all other choices are probabilitic. storm::storage::BitVector markovianChoices; diff --git a/src/parser/NondeterministicModelParser.cpp b/src/parser/NondeterministicModelParser.cpp index f83edb50e..51aebff56 100644 --- a/src/parser/NondeterministicModelParser.cpp +++ b/src/parser/NondeterministicModelParser.cpp @@ -37,13 +37,13 @@ NondeterministicModelParserResultContainer parseNondeterministicModel(st storm::models::AtomicPropositionsLabeling resultLabeling(std::move(storm::parser::AtomicPropositionLabelingParser(stateCount, labelingFile))); - NondeterministicModelParserResultContainer result(std::move(resultTransitionSystem), std::move(nondeterministicSparseTransitionParserResult.second), std::move(resultLabeling)); + NondeterministicModelParserResultContainer 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 parseNondeterministicModel(st storm::models::Mdp NondeterministicModelParserAsMdp(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { NondeterministicModelParserResultContainer parserResult = parseNondeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); - return storm::models::Mdp(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.rowMapping), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); + return storm::models::Mdp(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); } /*! @@ -69,7 +69,7 @@ storm::models::Mdp NondeterministicModelParserAsMdp(std::string const & storm::models::Ctmdp NondeterministicModelParserAsCtmdp(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { NondeterministicModelParserResultContainer parserResult = parseNondeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); - return storm::models::Ctmdp(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.rowMapping), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); + return storm::models::Ctmdp(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); } } /* namespace parser */ diff --git a/src/parser/NondeterministicModelParser.h b/src/parser/NondeterministicModelParser.h index 449a9b162..6c49dad0c 100644 --- a/src/parser/NondeterministicModelParser.h +++ b/src/parser/NondeterministicModelParser.h @@ -39,16 +39,15 @@ class NondeterministicModelParserResultContainer { public: storm::storage::SparseMatrix transitionSystem; storm::models::AtomicPropositionsLabeling labeling; - std::vector rowMapping; boost::optional> stateRewards; boost::optional> transitionRewards; - NondeterministicModelParserResultContainer(storm::storage::SparseMatrix& transitionSystem, std::vector& rowMapping, storm::models::AtomicPropositionsLabeling& labeling) : transitionSystem(transitionSystem), labeling(labeling), rowMapping(rowMapping) { } - NondeterministicModelParserResultContainer(storm::storage::SparseMatrix&& transitionSystem, std::vector&& rowMapping, storm::models::AtomicPropositionsLabeling&& labeling) : transitionSystem(std::move(transitionSystem)), labeling(std::move(labeling)), rowMapping(std::move(rowMapping)) { } + NondeterministicModelParserResultContainer(storm::storage::SparseMatrix& transitionSystem, storm::models::AtomicPropositionsLabeling& labeling) : transitionSystem(transitionSystem), labeling(labeling) { } + NondeterministicModelParserResultContainer(storm::storage::SparseMatrix&& 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() {} }; diff --git a/src/solver/GmmxxNondeterministicLinearEquationSolver.cpp b/src/solver/GmmxxNondeterministicLinearEquationSolver.cpp index d83fe1657..29829f535 100644 --- a/src/solver/GmmxxNondeterministicLinearEquationSolver.cpp +++ b/src/solver/GmmxxNondeterministicLinearEquationSolver.cpp @@ -42,7 +42,7 @@ namespace storm { } template - void GmmxxNondeterministicLinearEquationSolver::solveEquationSystem(bool minimize, storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices, std::vector* multiplyResult, std::vector* newX) const { + void GmmxxNondeterministicLinearEquationSolver::solveEquationSystem(bool minimize, storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* newX) const { // Transform the transition probability matrix to the gmm++ format to use its arithmetic. std::unique_ptr> gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(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 - void GmmxxNondeterministicLinearEquationSolver::performMatrixVectorMultiplication(bool minimize, storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& nondeterministicChoiceIndices, std::vector* b, uint_fast64_t n, std::vector* multiplyResult) const { + void GmmxxNondeterministicLinearEquationSolver::performMatrixVectorMultiplication(bool minimize, storm::storage::SparseMatrix const& A, std::vector& x, std::vector* b, uint_fast64_t n, std::vector* multiplyResult) const { // Transform the transition probability matrix to the gmm++ format to use its arithmetic. std::unique_ptr> gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(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()); } } diff --git a/src/solver/GmmxxNondeterministicLinearEquationSolver.h b/src/solver/GmmxxNondeterministicLinearEquationSolver.h index ac5e4d3fc..799853173 100644 --- a/src/solver/GmmxxNondeterministicLinearEquationSolver.h +++ b/src/solver/GmmxxNondeterministicLinearEquationSolver.h @@ -30,9 +30,9 @@ namespace storm { virtual NondeterministicLinearEquationSolver* clone() const; - virtual void performMatrixVectorMultiplication(bool minimize, storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& nondeterministicChoiceIndices, std::vector* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const override; + virtual void performMatrixVectorMultiplication(bool minimize, storm::storage::SparseMatrix const& A, std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const override; - virtual void solveEquationSystem(bool minimize, storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices, std::vector* multiplyResult = nullptr, std::vector* newX = nullptr) const override; + virtual void solveEquationSystem(bool minimize, storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr, std::vector* newX = nullptr) const override; private: // The required precision for the iterative methods. diff --git a/src/solver/NativeNondeterministicLinearEquationSolver.cpp b/src/solver/NativeNondeterministicLinearEquationSolver.cpp index 763ff6628..5dc25f2c1 100644 --- a/src/solver/NativeNondeterministicLinearEquationSolver.cpp +++ b/src/solver/NativeNondeterministicLinearEquationSolver.cpp @@ -40,7 +40,7 @@ namespace storm { } template - void NativeNondeterministicLinearEquationSolver::solveEquationSystem(bool minimize, storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices, std::vector* multiplyResult, std::vector* newX) const { + void NativeNondeterministicLinearEquationSolver::solveEquationSystem(bool minimize, storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* 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 - void NativeNondeterministicLinearEquationSolver::performMatrixVectorMultiplication(bool minimize, storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& nondeterministicChoiceIndices, std::vector* b, uint_fast64_t n, std::vector* multiplyResult) const { + void NativeNondeterministicLinearEquationSolver::performMatrixVectorMultiplication(bool minimize, storm::storage::SparseMatrix const& A, std::vector& x, std::vector* b, uint_fast64_t n, std::vector* 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()); } } diff --git a/src/solver/NativeNondeterministicLinearEquationSolver.h b/src/solver/NativeNondeterministicLinearEquationSolver.h index 51c8ddd97..69542a166 100644 --- a/src/solver/NativeNondeterministicLinearEquationSolver.h +++ b/src/solver/NativeNondeterministicLinearEquationSolver.h @@ -30,9 +30,9 @@ namespace storm { virtual NondeterministicLinearEquationSolver* clone() const override; - virtual void performMatrixVectorMultiplication(bool minimize, storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& nondeterministicChoiceIndices, std::vector* b = nullptr, uint_fast64_t n = 1, std::vector* newX = nullptr) const override; + virtual void performMatrixVectorMultiplication(bool minimize, storm::storage::SparseMatrix const& A, std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1, std::vector* newX = nullptr) const override; - virtual void solveEquationSystem(bool minimize, storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices, std::vector* multiplyResult = nullptr, std::vector* newX = nullptr) const override; + virtual void solveEquationSystem(bool minimize, storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr, std::vector* newX = nullptr) const override; private: // The required precision for the iterative methods. diff --git a/src/solver/NondeterministicLinearEquationSolver.h b/src/solver/NondeterministicLinearEquationSolver.h index 8c5bc2334..b90773ee6 100644 --- a/src/solver/NondeterministicLinearEquationSolver.h +++ b/src/solver/NondeterministicLinearEquationSolver.h @@ -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 const& A, std::vector& x, std::vector const& b, std::vector const& rowGroupIndices, std::vector* multiplyResult = nullptr, std::vector* newX = nullptr) const = 0; + virtual void solveEquationSystem(bool minimize, storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr, std::vector* 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 const& A, std::vector& x, std::vector const& rowGroupIndices, std::vector* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const = 0; + virtual void performMatrixVectorMultiplication(bool minimize, storm::storage::SparseMatrix const& A, std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const = 0; }; } // namespace solver diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index f9178b275..949e64eb3 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -335,6 +335,11 @@ namespace storm { return rowGroupIndices.size() - 1; } + template + uint_fast64_t SparseMatrix::getRowGroupSize(uint_fast64_t group) const { + return this->getRowGroupIndices()[group + 1] - this->getRowGroupIndices()[group]; + } + template std::vector const& SparseMatrix::getRowGroupIndices() const { return rowGroupIndices; @@ -348,7 +353,7 @@ namespace storm { } template - void SparseMatrix::makeRowGroupsAbsorbing(storm::storage::BitVector const& rowGroupConstraint, std::vector const& rowGroupIndices) { + void SparseMatrix::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 - std::vector SparseMatrix::getConstrainedRowGroupSumVector(storm::storage::BitVector const& rowGroupConstraint, std::vector const& rowGroupIndices, storm::storage::BitVector const& columnConstraint) const { + std::vector SparseMatrix::getConstrainedRowGroupSumVector(storm::storage::BitVector const& rowGroupConstraint, storm::storage::BitVector const& columnConstraint) const { std::vector result; result.reserve(rowGroupConstraint.getNumberOfSetBits()); for (auto rowGroup : rowGroupConstraint) { @@ -509,7 +514,7 @@ namespace storm { } template - SparseMatrix SparseMatrix::selectRowsFromRowGroups(std::vector const& rowGroupToRowIndexMapping, std::vector const& rowGroupIndices, bool insertDiagonalEntries) const { + SparseMatrix SparseMatrix::selectRowsFromRowGroups(std::vector 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]; diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 83eb4e46d..f85dfdd52 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -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 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 getConstrainedRowGroupSumVector(storm::storage::BitVector const& rowGroupConstraint, std::vector const& rowGroupIndices, storm::storage::BitVector const& columnConstraint) const; + std::vector 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 const& rowGroupToRowIndexMapping, std::vector const& rowGroupIndices, bool insertDiagonalEntries = true) const; + SparseMatrix selectRowsFromRowGroups(std::vector const& rowGroupToRowIndexMapping, bool insertDiagonalEntries = true) const; /*! * Transposes the matrix. diff --git a/src/utility/graph.h b/src/utility/graph.h index 8cb7c044e..01d0a7f4f 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -347,7 +347,7 @@ namespace storm { */ template std::pair performProb01Max(storm::models::AbstractNondeterministicModel 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 std::pair performProb01Min(storm::models::AbstractNondeterministicModel 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); } /*! diff --git a/src/utility/matrix.h b/src/utility/matrix.h index 93a15b43e..446fb413f 100644 --- a/src/utility/matrix.h +++ b/src/utility/matrix.h @@ -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 - storm::storage::SparseMatrix applyScheduler(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::Scheduler const& scheduler) { - storm::storage::SparseMatrixBuilder matrixBuilder(nondeterministicChoiceIndices.size() - 1, transitionMatrix.getColumnCount()); + storm::storage::SparseMatrix applyScheduler(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::Scheduler const& scheduler) { + storm::storage::SparseMatrixBuilder 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 << "."; } diff --git a/test/functional/solver/GmmxxNondeterministicLinearEquationSolverTest.cpp b/test/functional/solver/GmmxxNondeterministicLinearEquationSolverTest.cpp index 58bf724b1..ae9542bbb 100644 --- a/test/functional/solver/GmmxxNondeterministicLinearEquationSolverTest.cpp +++ b/test/functional/solver/GmmxxNondeterministicLinearEquationSolverTest.cpp @@ -5,64 +5,61 @@ #include "src/settings/Settings.h" TEST(GmmxxNondeterministicLinearEquationSolver, SolveWithStandardOptions) { - ASSERT_NO_THROW(storm::storage::SparseMatrixBuilder builder); - storm::storage::SparseMatrixBuilder builder; + storm::storage::SparseMatrixBuilder builder(0, 0, 0, true); + ASSERT_NO_THROW(builder.newRowGroup(0)); ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9)); storm::storage::SparseMatrix A; ASSERT_NO_THROW(A = builder.build(2)); - - std::vector nondeterministicChoiceIndices = {0, 2}; std::vector x(1); std::vector b = {0.099, 0.5}; - - ASSERT_NO_THROW(storm::solver::GmmxxNondeterministicLinearEquationSolver solver); - + storm::solver::GmmxxNondeterministicLinearEquationSolver 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 builder); - storm::storage::SparseMatrixBuilder builder; + storm::storage::SparseMatrixBuilder 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 A; ASSERT_NO_THROW(A = builder.build()); - std::vector nondeterministicChoiceIndices = {0, 2, 3, 4}; std::vector x = {0, 1, 0}; ASSERT_NO_THROW(storm::solver::GmmxxNondeterministicLinearEquationSolver solver); storm::solver::GmmxxNondeterministicLinearEquationSolver 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()); } \ No newline at end of file diff --git a/test/functional/solver/NativeNondeterministicLinearEquationSolverTest.cpp b/test/functional/solver/NativeNondeterministicLinearEquationSolverTest.cpp index 246da6fdf..0ccdafd84 100644 --- a/test/functional/solver/NativeNondeterministicLinearEquationSolverTest.cpp +++ b/test/functional/solver/NativeNondeterministicLinearEquationSolverTest.cpp @@ -5,64 +5,61 @@ #include "src/settings/Settings.h" TEST(NativeNondeterministicLinearEquationSolver, SolveWithStandardOptions) { - ASSERT_NO_THROW(storm::storage::SparseMatrixBuilder builder); - storm::storage::SparseMatrixBuilder builder; + storm::storage::SparseMatrixBuilder builder(0, 0, 0, true); + ASSERT_NO_THROW(builder.newRowGroup(0)); ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9)); storm::storage::SparseMatrix A; ASSERT_NO_THROW(A = builder.build(2)); - std::vector nondeterministicChoiceIndices = {0, 2}; - std::vector x(1); std::vector b = {0.099, 0.5}; - - ASSERT_NO_THROW(storm::solver::NativeNondeterministicLinearEquationSolver solver); - + storm::solver::NativeNondeterministicLinearEquationSolver 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 builder); - storm::storage::SparseMatrixBuilder builder; + storm::storage::SparseMatrixBuilder 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 A; ASSERT_NO_THROW(A = builder.build()); - std::vector nondeterministicChoiceIndices = {0, 2, 3, 4}; std::vector x = {0, 1, 0}; ASSERT_NO_THROW(storm::solver::NativeNondeterministicLinearEquationSolver solver); storm::solver::NativeNondeterministicLinearEquationSolver 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()); } \ No newline at end of file diff --git a/test/functional/storage/MaximalEndComponentDecompositionTest.cpp b/test/functional/storage/MaximalEndComponentDecompositionTest.cpp index 76f0cd125..a85e9ef3f 100644 --- a/test/functional/storage/MaximalEndComponentDecompositionTest.cpp +++ b/test/functional/storage/MaximalEndComponentDecompositionTest.cpp @@ -7,7 +7,7 @@ TEST(MaximalEndComponentDecomposition, FullSystem1) { storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.lab", "", ""); std::shared_ptr> markovAutomaton = parser.getModel>(); - + storm::storage::MaximalEndComponentDecomposition mecDecomposition; ASSERT_NO_THROW(mecDecomposition = storm::storage::MaximalEndComponentDecomposition(*markovAutomaton)); diff --git a/test/functional/storage/SparseMatrixTest.cpp b/test/functional/storage/SparseMatrixTest.cpp index b2a53c566..69517a6d4 100644 --- a/test/functional/storage/SparseMatrixTest.cpp +++ b/test/functional/storage/SparseMatrixTest.cpp @@ -237,12 +237,10 @@ TEST(SparseMatrix, MakeRowGroupAbsorbing) { storm::storage::SparseMatrix matrix; ASSERT_NO_THROW(matrix = matrixBuilder.build()); - std::vector 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 matrixBuilder2(0, 0, 0, true); ASSERT_NO_THROW(matrixBuilder2.newRowGroup(0)); @@ -301,8 +299,6 @@ TEST(SparseMatrix, ConstrainedRowSumVector) { storm::storage::SparseMatrix matrix2; ASSERT_NO_THROW(matrix2 = matrixBuilder2.build()); - std::vector 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 constrainedRowSum2 = matrix2.getConstrainedRowGroupSumVector(rowGroupConstraint, rowGroupIndices, columnConstraint2)); - std::vector constrainedRowSum2 = matrix2.getConstrainedRowGroupSumVector(rowGroupConstraint, rowGroupIndices, columnConstraint2); + ASSERT_NO_THROW(std::vector constrainedRowSum2 = matrix2.getConstrainedRowGroupSumVector(rowGroupConstraint, columnConstraint2)); + std::vector constrainedRowSum2 = matrix2.getConstrainedRowGroupSumVector(rowGroupConstraint, columnConstraint2); ASSERT_TRUE(constrainedRowSum2 == std::vector({0, 2.3})); } @@ -359,8 +355,8 @@ TEST(SparseMatrix, Submatrix) { std::vector rowGroupToIndexMapping = {0, 0, 1, 0}; - ASSERT_NO_THROW(storm::storage::SparseMatrix matrix4 = matrix.selectRowsFromRowGroups(rowGroupToIndexMapping, rowGroupIndices)); - storm::storage::SparseMatrix matrix4 = matrix.selectRowsFromRowGroups(rowGroupToIndexMapping, rowGroupIndices); + ASSERT_NO_THROW(storm::storage::SparseMatrix matrix4 = matrix.selectRowsFromRowGroups(rowGroupToIndexMapping)); + storm::storage::SparseMatrix matrix4 = matrix.selectRowsFromRowGroups(rowGroupToIndexMapping); storm::storage::SparseMatrixBuilder matrixBuilder5(4, 4, 8); ASSERT_NO_THROW(matrixBuilder5.addNextValue(0, 1, 1.0));