diff --git a/src/modelchecker/prctl/GmmxxMdpPrctlModelChecker.h b/src/modelchecker/prctl/GmmxxMdpPrctlModelChecker.h index a1190a0fa..ff3ebd971 100644 --- a/src/modelchecker/prctl/GmmxxMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/GmmxxMdpPrctlModelChecker.h @@ -126,6 +126,7 @@ private: // Proceed with the iterations as long as the method did not converge or reach the user-specified maximum number // of iterations. while (!converged && iterations < maxIterations) { + std::cout << "iter: " << iterations << std::endl; // Compute x' = A*x + b. gmm::mult(*gmmxxMatrix, *currentX, multiplyResult); gmm::add(b, multiplyResult); @@ -140,6 +141,13 @@ private: // Determine whether the method converged. converged = storm::utility::vector::equalModuloPrecision(*currentX, *newX, precision, relative); + if (!converged) { + for (uint_fast64_t i = 0; i < newX->size(); ++i) { + std::cout << (*currentX)[i] << " vs. " << (*newX)[i] << std::endl; + } + } + + // Update environment variables. swap = currentX; currentX = newX; diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 8cbbd3474..eea889769 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -68,7 +68,7 @@ public: * @param formula The formula to check. * @returns The set of states satisfying the formula represented by a bit vector. */ - std::vector* checkNoBoundOperator(const storm::property::prctl::AbstractNoBoundOperator& formula) const { + virtual std::vector* checkNoBoundOperator(const storm::property::prctl::AbstractNoBoundOperator& formula) const { // Check if the operator was an non-optimality operator and report an error in that case. if (!formula.isOptimalityOperator()) { LOG4CPLUS_ERROR(logger, "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models."); @@ -261,7 +261,7 @@ public: * @return The probabilities for the given formula to hold on every state of the model associated with this model * checker. If the qualitative flag is set, exact probabilities might not be computed. */ - std::vector* checkUntil(bool minimize, const storm::property::prctl::Until& formula, bool qualitative, std::vector* scheduler) const { + virtual std::vector* checkUntil(bool minimize, const storm::property::prctl::Until& formula, bool qualitative, std::vector* scheduler) const { // First, we need to compute the states that satisfy the sub-formulas of the until-formula. storm::storage::BitVector* leftStates = formula.getLeft().check(*this); storm::storage::BitVector* rightStates = formula.getRight().check(*this); @@ -310,13 +310,13 @@ public: // Get the "new" nondeterministic choice indices for the submatrix. std::vector subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates); - // Create vector for results for maybe states. - std::vector x(maybeStates.getNumberOfSetBits()); - // 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 = this->getModel().getTransitionMatrix().getConstrainedRowSumVector(maybeStates, this->getModel().getNondeterministicChoiceIndices(), statesWithProbability1, submatrix.getRowCount()); + // Create vector for results for maybe states. + std::vector x = this->getInitialValueIterationValues(submatrix, formula); + // Solve the corresponding system of equations. this->solveEquationSystem(minimize, submatrix, x, b, subNondeterministicChoiceIndices); @@ -431,7 +431,7 @@ public: * @return The reward values for the given formula for every state of the model associated with this model * checker. If the qualitative flag is set, exact values might not be computed. */ - std::vector* checkReachabilityReward(bool minimize, const storm::property::prctl::ReachabilityReward& formula, bool qualitative, std::vector* scheduler) const { + virtual std::vector* checkReachabilityReward(bool minimize, const storm::property::prctl::ReachabilityReward& formula, bool qualitative, std::vector* scheduler) const { // Only compute the result if the model has at least one reward model. if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) { LOG4CPLUS_ERROR(logger, "Missing reward model for formula. Skipping formula"); @@ -441,19 +441,6 @@ public: // Determine the states for which the target predicate holds. storm::storage::BitVector* targetStates = formula.getChild().check(*this); - std::vector usedScheduler(this->getModel().getNumberOfStates()); - - storm::models::Dtmc dtmc(this->getModel().getTransitionMatrix().getSubmatrix(usedScheduler, this->getModel().getNondeterministicChoiceIndices()), - storm::models::AtomicPropositionsLabeling(this->getModel().getStateLabeling()), - this->getModel().hasStateRewards() ? boost::optional>(this->getModel().getStateRewardVector()) : boost::optional>(), - this->getModel().hasTransitionRewards() ? boost::optional>(this->getModel().getTransitionRewardMatrix().getSubmatrix(usedScheduler, this->getModel().getNondeterministicChoiceIndices(), false)) : boost::optional>()); - - dtmc.printModelInformationToStream(std::cout); - - storm::modelchecker::prctl::GmmxxDtmcPrctlModelChecker mc(dtmc); - formula.check(mc, qualitative); - exit(-1); - // Determine which states have a reward of infinity by definition. storm::storage::BitVector infinityStates; storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); @@ -468,8 +455,6 @@ public: LOG4CPLUS_INFO(logger, "Found " << targetStates->getNumberOfSetBits() << " 'target' states."); LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); - - // Create resulting vector. std::vector* result = new std::vector(this->getModel().getNumberOfStates()); @@ -490,9 +475,6 @@ public: // Get the "new" nondeterministic choice indices for the submatrix. std::vector subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates); - // Create vector for results for maybe states. - std::vector x(submatrix.getColumnCount()); - // 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()); @@ -521,6 +503,9 @@ public: storm::utility::vector::selectVectorValuesRepeatedly(b, maybeStates, this->getModel().getNondeterministicChoiceIndices(), this->getModel().getStateRewardVector()); } + // Create vector for results for maybe states. + std::vector x = this->getInitialValueIterationValues(submatrix, formula); + // Solve the corresponding system of equations. this->solveEquationSystem(minimize, submatrix, x, b, subNondeterministicChoiceIndices, scheduler); @@ -613,7 +598,9 @@ private: * @returns 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& nondeterministicChoiceIndices, std::vector* takenChoices = nullptr) const { - // Get the settings object to customize solving. + LOG4CPLUS_INFO(logger, "Starting iterative solver."); + + // Get the settings object to customize solving. storm::settings::Settings* s = storm::settings::instance(); // Get relevant user-defined settings for solving the equations. @@ -708,6 +695,30 @@ private: return subNondeterministicChoiceIndices; } + + /*! + * Retrieves the values to be used as the initial values for the value iteration techniques. + * + * @param submatrix The matrix that will be used for value iteration later. + */ + std::vector getInitialValueIterationValues(storm::storage::SparseMatrix const& submatrix, storm::property::prctl::AbstractPathFormula const& formula) const { + // std::vector scheduler(submatrix.getColumnCount()); + std::vector scheduler(this->getModel().getNumberOfStates()); + + storm::models::Dtmc dtmc(this->getModel().getTransitionMatrix().getSubmatrix(scheduler, this->getModel().getNondeterministicChoiceIndices()), + storm::models::AtomicPropositionsLabeling(this->getModel().getStateLabeling()), + this->getModel().hasStateRewards() ? boost::optional>(this->getModel().getStateRewardVector()) : boost::optional>(), + this->getModel().hasTransitionRewards() ? boost::optional>(this->getModel().getTransitionRewardMatrix().getSubmatrix(scheduler, this->getModel().getNondeterministicChoiceIndices(), false)) : boost::optional>()); + + storm::modelchecker::prctl::GmmxxDtmcPrctlModelChecker modelChecker(dtmc); + + std::vector* modelCheckingResult = formula.check(modelChecker, false); + std::vector result(std::move(*modelCheckingResult)); + delete modelCheckingResult; + + return result; + } + }; } // namespace prctl