diff --git a/src/modelchecker/prctl/GmmxxMdpPrctlModelChecker.h b/src/modelchecker/prctl/GmmxxMdpPrctlModelChecker.h index 768237cca..a1190a0fa 100644 --- a/src/modelchecker/prctl/GmmxxMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/GmmxxMdpPrctlModelChecker.h @@ -95,6 +95,7 @@ private: /*! * Solves the given equation system under the given parameters using the power method. * + * @param minimize If set, all choices are resolved such that the solution value becomes minimal and maximal otherwise. * @param A The matrix A specifying the coefficients of the equations. * @param x The vector x for which to solve the equations. The initial value of the elements of * this vector are used as the initial guess and might thus influence performance and convergence. @@ -102,7 +103,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& A, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices, std::vector* takenChoices = nullptr) const override { + 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 override { // Get the settings object to customize solving. storm::settings::Settings* s = storm::settings::instance(); @@ -130,7 +131,7 @@ private: gmm::add(b, multiplyResult); // Reduce the vector x' by applying min/max for all non-deterministic choices. - if (this->minimumOperatorStack.top()) { + if (minimize) { storm::utility::vector::reduceVectorMin(multiplyResult, *newX, nondeterministicChoiceIndices); } else { storm::utility::vector::reduceVectorMax(multiplyResult, *newX, nondeterministicChoiceIndices); @@ -148,7 +149,7 @@ private: // If we were requested to record the taken choices, we have to construct the vector now. if (takenChoices != nullptr) { - this->computeTakenChoices(multiplyResult, *takenChoices, nondeterministicChoiceIndices); + this->computeTakenChoices(minimize, multiplyResult, *takenChoices, nondeterministicChoiceIndices); } // If we performed an odd number of iterations, we need to swap the x and currentX, because the newest result diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 335760964..f9f329c58 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -242,12 +242,13 @@ public: * checker. If the qualitative flag is set, exact probabilities might not be computed. */ virtual std::vector* checkUntil(const storm::property::prctl::Until& formula, bool qualitative) const { - return this->checkUntil(formula, qualitative, nullptr); + return this->checkUntil(this->minimumOperatorStack.top(), formula, qualitative, nullptr); } /*! * Check the given formula that is an until formula. * + * @param minimize If set, the probability is minimized and maximized otherwise. * @param formula The formula to check. * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the * results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only @@ -259,7 +260,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(const storm::property::prctl::Until& formula, bool qualitative, std::vector* scheduler) const { + 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); @@ -267,7 +268,7 @@ public: // Then, 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 (this->minimumOperatorStack.top()) { + if (minimize) { statesWithProbability01 = storm::utility::graph::performProb01Min(this->getModel(), *leftStates, *rightStates); } else { statesWithProbability01 = storm::utility::graph::performProb01Max(this->getModel(), *leftStates, *rightStates); @@ -316,7 +317,7 @@ public: std::vector b = this->getModel().getTransitionMatrix().getConstrainedRowSumVector(maybeStates, this->getModel().getNondeterministicChoiceIndices(), statesWithProbability1, submatrix.getRowCount()); // Solve the corresponding system of equations. - this->solveEquationSystem(submatrix, x, b, subNondeterministicChoiceIndices); + this->solveEquationSystem(minimize, submatrix, x, b, subNondeterministicChoiceIndices); // Set values of resulting vector according to result. storm::utility::vector::setVectorValues(*result, maybeStates, x); @@ -411,12 +412,13 @@ public: * checker. If the qualitative flag is set, exact values might not be computed. */ virtual std::vector* checkReachabilityReward(const storm::property::prctl::ReachabilityReward& formula, bool qualitative) const { - return this->checkReachabilityReward(formula, qualitative, nullptr); + return this->checkReachabilityReward(this->minimumOperatorStack.top(), formula, qualitative, nullptr); } /*! * Checks the given formula that is a reachability reward formula. * + * @param minimize If set, the reward is to be minimized and maximized otherwise. * @param formula The formula to check. * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the * results are only compared against the bound 0. If set to true, this will most likely results that are only @@ -428,7 +430,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(const storm::property::prctl::ReachabilityReward& formula, bool qualitative, std::vector* scheduler) const { + 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,7 +443,7 @@ public: // Determine which states have a reward of infinity by definition. storm::storage::BitVector infinityStates; storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); - if (this->minimumOperatorStack.top()) { + if (minimize) { infinityStates = std::move(storm::utility::graph::performProb1A(this->getModel(), this->getModel().getBackwardTransitions(), trueStates, *targetStates)); } else { infinityStates = std::move(storm::utility::graph::performProb1E(this->getModel(), this->getModel().getBackwardTransitions(), trueStates, *targetStates)); @@ -504,7 +506,7 @@ public: } // Solve the corresponding system of equations. - this->solveEquationSystem(submatrix, x, b, subNondeterministicChoiceIndices, scheduler); + this->solveEquationSystem(minimize, submatrix, x, b, subNondeterministicChoiceIndices, scheduler); // Set values of resulting vector according to result. storm::utility::vector::setVectorValues(*result, maybeStates, x); @@ -523,13 +525,14 @@ protected: /*! * Computes the vector of choices that need to be made to minimize/maximize the model checking result for each state. * + * @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. */ - void computeTakenChoices(std::vector const& nondeterministicResult, std::vector& takenChoices, std::vector const& nondeterministicChoiceIndices) const { + void computeTakenChoices(bool minimize, std::vector const& nondeterministicResult, std::vector& takenChoices, std::vector const& nondeterministicChoiceIndices) const { std::vector temporaryResult(nondeterministicChoiceIndices.size() - 1); - if (this->minimumOperatorStack.top()) { + if (minimize) { storm::utility::vector::reduceVectorMin(nondeterministicResult, temporaryResult, nondeterministicChoiceIndices, &takenChoices); } else { storm::utility::vector::reduceVectorMax(nondeterministicResult, temporaryResult, nondeterministicChoiceIndices, &takenChoices); @@ -582,6 +585,7 @@ private: /*! * Solves the equation system A*x = b given by the parameters. * + * @param minimize If set, all choices are resolved such that the solution value becomes minimal and maximal otherwise. * @param A The matrix specifying the coefficients of the linear equations. * @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. @@ -592,7 +596,7 @@ private: * as there are states in the MDP. * @returns The solution vector x of the system of linear equations as the content of the parameter x. */ - virtual void solveEquationSystem(storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices, std::vector* takenChoices = nullptr) const { + 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. storm::settings::Settings* s = storm::settings::instance(); @@ -618,7 +622,7 @@ private: // 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 (this->minimumOperatorStack.top()) { + if (minimize) { storm::utility::vector::reduceVectorMin(multiplyResult, *newX, nondeterministicChoiceIndices); } else { storm::utility::vector::reduceVectorMax(multiplyResult, *newX, nondeterministicChoiceIndices); @@ -636,7 +640,7 @@ private: // If we were requested to record the taken choices, we have to construct the vector now. if (takenChoices != nullptr) { - this->computeTakenChoices(multiplyResult, *takenChoices, nondeterministicChoiceIndices); + this->computeTakenChoices(minimize, multiplyResult, *takenChoices, nondeterministicChoiceIndices); } // If we performed an odd number of iterations, we need to swap the x and currentX, because the newest result diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index 9aff2fa10..5d03f9a6e 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -441,7 +441,7 @@ protected: // If we are to include some values for the state as well, we do so now. if (firstValue != nullptr || secondValue != nullptr) { - outStream << "["; + outStream << " ["; if (firstValue != nullptr) { outStream << (*firstValue)[state]; if (secondValue != nullptr) { @@ -458,7 +458,7 @@ protected: // Now, we color the states if there were colors given. if (stateColoring != nullptr && colors != nullptr) { outStream << ", "; - outStream << " fillcolor = \"" << (*colors)[(*stateColoring)[state]] << "\""; + outStream << " style = filled, fillcolor = " << (*colors)[(*stateColoring)[state]]; } } outStream << " ]";