From 0a89d65f93b48d8c1f3a202b5e0d517880e488f7 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 2 Dec 2013 14:05:49 +0100 Subject: [PATCH] Started refactoring Markov automaton model checker. Former-commit-id: c4278de4f0773364b7cf0a85e77cd3310dd49812 --- .../MILPMinimalLabelSetGenerator.h | 6 +- .../SMTMinimalCommandSetGenerator.h | 6 +- .../SparseMarkovAutomatonCslModelChecker.h | 228 ++++--- .../prctl/SparseMdpPrctlModelChecker.h | 85 +-- ...ractNondeterministicLinearEquationSolver.h | 6 + ...mmxxNondeterministicLinearEquationSolver.h | 8 +- src/storm.cpp | 21 +- src/utility/solver.cpp | 25 + src/utility/solver.h | 11 +- src/utility/vector.h | 600 +++++++++--------- .../GmmxxMdpPrctlModelCheckerTest.cpp | 8 +- .../SparseMdpPrctlModelCheckerTest.cpp | 8 +- .../GmmxxMdpPrctModelCheckerTest.cpp | 4 +- .../SparseMdpPrctlModelCheckerTest.cpp | 4 +- 14 files changed, 513 insertions(+), 507 deletions(-) create mode 100644 src/utility/solver.cpp diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index 910948391..5023c342e 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -961,7 +961,7 @@ namespace storm { // (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set. double maximalReachabilityProbability = 0; - storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(labeledMdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver()); + storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(labeledMdp); std::vector result = modelchecker.checkUntil(false, phiStates, psiStates, false).first; for (auto state : labeledMdp.getInitialStates()) { maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]); @@ -977,7 +977,7 @@ namespace storm { ChoiceInformation choiceInformation = determineRelevantAndProblematicChoices(labeledMdp, stateInformation, psiStates); // (4) Encode resulting system as MILP problem. - std::unique_ptr solver = storm::utility::solver::getLpSolver("MinimalCommandSetCounterexample"); + std::shared_ptr solver = storm::utility::solver::getLpSolver("MinimalCommandSetCounterexample"); // (4.1) Create variables. VariableInformation variableInformation = createVariables(*solver, labeledMdp, stateInformation, choiceInformation); @@ -1025,7 +1025,7 @@ namespace storm { storm::property::prctl::AbstractPathFormula const& pathFormula = probBoundFormula->getPathFormula(); storm::storage::BitVector phiStates; storm::storage::BitVector psiStates; - storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(labeledMdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver()); + storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(labeledMdp); try { storm::property::prctl::Until const& untilFormula = dynamic_cast const&>(pathFormula); diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index 2bbc1357c..a4041a070 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -1635,7 +1635,7 @@ namespace storm { // (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set. double maximalReachabilityProbability = 0; - storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(labeledMdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver()); + storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(labeledMdp); std::vector result = modelchecker.checkUntil(false, phiStates, psiStates, false).first; for (auto state : labeledMdp.getInitialStates()) { maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]); @@ -1701,7 +1701,7 @@ namespace storm { modelCheckingClock = std::chrono::high_resolution_clock::now(); commandSet.insert(relevancyInformation.knownLabels); storm::models::Mdp subMdp = labeledMdp.restrictChoiceLabels(commandSet); - storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(subMdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver()); + storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(subMdp); LOG4CPLUS_DEBUG(logger, "Invoking model checker."); std::vector result = modelchecker.checkUntil(false, phiStates, psiStates, false).first; LOG4CPLUS_DEBUG(logger, "Computed model checking results."); @@ -1786,7 +1786,7 @@ namespace storm { storm::property::prctl::AbstractPathFormula const& pathFormula = probBoundFormula->getPathFormula(); storm::storage::BitVector phiStates; storm::storage::BitVector psiStates; - storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(labeledMdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver()); + storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(labeledMdp); try { storm::property::prctl::Until const& untilFormula = dynamic_cast const&>(pathFormula); diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index 75b3e81cb..123503cac 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -2,7 +2,6 @@ #define STORM_MODELCHECKER_CSL_SPARSEMARKOVAUTOMATONCSLMODELCHECKER_H_ #include -#include #include "src/modelchecker/csl/AbstractModelChecker.h" #include "src/models/MarkovAutomaton.h" @@ -22,7 +21,7 @@ namespace storm { class SparseMarkovAutomatonCslModelChecker : public AbstractModelChecker { public: - explicit SparseMarkovAutomatonCslModelChecker(storm::models::MarkovAutomaton const& model) : AbstractModelChecker(model), minimumOperatorStack() { + explicit SparseMarkovAutomatonCslModelChecker(storm::models::MarkovAutomaton const& model, std::shared_ptr> nondeterministicLinearEquationSolver = storm::utility::solver::getNondeterministicLinearEquationSolver()) : AbstractModelChecker(model), minimumOperatorStack(), nondeterministicLinearEquationSolver(nondeterministicLinearEquationSolver) { // Intentionally left empty. } @@ -78,10 +77,10 @@ namespace storm { // * 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 = computeNondeterministicChoiceIndicesForConstraint(nondeterministicChoiceIndices, markovianNonGoalStates); + 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 = computeNondeterministicChoiceIndicesForConstraint(nondeterministicChoiceIndices, probabilisticNonGoalStates); + std::vector probabilisticNondeterministicChoiceIndices = storm::utility::vector::getConstrainedOffsetVector(nondeterministicChoiceIndices, probabilisticNonGoalStates); // 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,7 +127,7 @@ namespace storm { } } - std::unique_ptr> nondeterministiclinearEquationSolver = storm::utility::solver::getNondeterministicLinearEquationSolver(); + std::shared_ptr> nondeterministiclinearEquationSolver = storm::utility::solver::getNondeterministicLinearEquationSolver(); // Perform the actual value iteration // * loop until the step bound has been reached @@ -234,9 +233,20 @@ namespace storm { } std::vector checkLongRunAverage(bool min, storm::storage::BitVector const& goalStates) const { + // Check whether the automaton is closed. if (!this->getModel().isClosed()) { throw storm::exceptions::InvalidArgumentException() << "Unable to compute long-run average on non-closed Markov automaton."; } + + // If there are no goal states, we avoid the computation and directly return zero. + if (goalStates.empty()) { + return std::vector(this->getModel().getNumberOfStates(), storm::utility::constGetZero()); + } + + // Likewise, if all bits are set, we can avoid the computation and set. + if ((~goalStates).empty()) { + return std::vector(this->getModel().getNumberOfStates(), storm::utility::constGetOne()); + } // Start by decomposing the Markov automaton into its MECs. storm::storage::MaximalEndComponentDecomposition mecDecomposition(this->getModel()); @@ -245,7 +255,7 @@ namespace storm { typename storm::storage::SparseMatrix const& transitionMatrix = this->getModel().getTransitionMatrix(); std::vector const& nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices(); - // Now compute the long-run average for all end components in isolation. + // Now start with compute the long-run average for all end components in isolation. std::vector lraValuesForEndComponents; // While doing so, we already gather some information for the following steps. @@ -255,67 +265,16 @@ namespace storm { for (uint_fast64_t currentMecIndex = 0; currentMecIndex < mecDecomposition.size(); ++currentMecIndex) { storm::storage::MaximalEndComponent const& mec = mecDecomposition[currentMecIndex]; - std::unique_ptr solver = storm::utility::solver::getLpSolver("LRA for MEC " + std::to_string(currentMecIndex)); - solver->setModelSense(min ? storm::solver::LpSolver::MAXIMIZE : storm::solver::LpSolver::MINIMIZE); - - // First, we need to create the variables for the problem. - std::map stateToVariableIndexMap; - for (auto const& stateChoicesPair : mec) { - stateToVariableIndexMap[stateChoicesPair.first] = solver->createContinuousVariable("x" + std::to_string(stateChoicesPair.first), storm::solver::LpSolver::UNBOUNDED, 0, 0, 0); - } - uint_fast64_t lraValueVariableIndex = solver->createContinuousVariable("k", storm::solver::LpSolver::UNBOUNDED, 0, 0, 1); - - // Now we encode the problem as constraints. - std::vector variables; - std::vector coefficients; + // Gather information for later use. for (auto const& stateChoicesPair : mec) { uint_fast64_t state = stateChoicesPair.first; - // Gather information for later use. statesInMecs.set(state); stateToMecIndexMap[state] = currentMecIndex; - - // Now, based on the type of the state, create a suitable constraint. - if (this->getModel().isMarkovianState(state)) { - variables.clear(); - coefficients.clear(); - - variables.push_back(stateToVariableIndexMap.at(state)); - coefficients.push_back(1); - - typename storm::storage::SparseMatrix::Rows row = transitionMatrix.getRow(nondeterministicChoiceIndices[state]); - for (auto element : row) { - variables.push_back(stateToVariableIndexMap.at(element.column())); - coefficients.push_back(-element.value()); - } - - variables.push_back(lraValueVariableIndex); - coefficients.push_back(storm::utility::constGetOne() / this->getModel().getExitRate(state)); - - solver->addConstraint("state" + std::to_string(state), variables, coefficients, min ? storm::solver::LpSolver::LESS_EQUAL : storm::solver::LpSolver::GREATER_EQUAL, goalStates.get(state) ? storm::utility::constGetOne() / this->getModel().getExitRate(state) : storm::utility::constGetZero()); - } else { - // For probabilistic states, we want to add the constraint x_s <= sum P(s, a, s') * x_s' where a is the current action - // and the sum ranges over all states s'. - for (auto choice : stateChoicesPair.second) { - variables.clear(); - coefficients.clear(); - - variables.push_back(stateToVariableIndexMap.at(state)); - coefficients.push_back(1); - - typename storm::storage::SparseMatrix::Rows row = transitionMatrix.getRow(choice); - for (auto element : row) { - variables.push_back(stateToVariableIndexMap.at(element.column())); - coefficients.push_back(-element.value()); - } - - solver->addConstraint("state" + std::to_string(state), variables, coefficients, min ? storm::solver::LpSolver::LESS_EQUAL : storm::solver::LpSolver::GREATER_EQUAL, storm::utility::constGetZero()); - } - } } - - solver->optimize(); - lraValuesForEndComponents.push_back(solver->getContinuousValue(lraValueVariableIndex)); + + // Compute the LRA value for the current MEC. + lraValuesForEndComponents.push_back(this->computeLraForMaximalEndComponent(min, transitionMatrix, nondeterministicChoiceIndices, this->getModel().getMarkovianStates(), this->getModel().getExitRates(), goalStates, mec)); } // For fast transition rewriting, we build some auxiliary data structures. @@ -429,7 +388,7 @@ namespace storm { // Finalize the matrix and solve the corresponding system of equations. sspMatrix.finalize(); std::vector x(numberOfStatesNotInMecs + mecDecomposition.size()); - std::unique_ptr> nondeterministiclinearEquationSolver = storm::utility::solver::getNondeterministicLinearEquationSolver(); + std::shared_ptr> nondeterministiclinearEquationSolver = storm::utility::solver::getNondeterministicLinearEquationSolver(); nondeterministiclinearEquationSolver->solveEquationSystem(min, sspMatrix, x, b, sspNondeterministicChoiceIndices); // Prepare result vector. @@ -451,10 +410,102 @@ namespace storm { } std::vector checkExpectedTime(bool min, storm::storage::BitVector const& goalStates) const { + // Reduce the problem of computing the expected time to computing expected rewards where the rewards + // for all probabilistic states are zero and the reward values of Markovian states is 1. + std::vector rewardValues(this->getModel().getNumberOfStates(), storm::utility::constGetZero()); + storm::utility::vector::setVectorValues(rewardValues, this->getModel().getMarkovianStates(), storm::utility::constGetOne()); + return this->computeExpectedRewards(min, goalStates, rewardValues); + } + + protected: + /*! + * Computes the long-run average value for the given maximal end component of a Markov automaton. + * + * @param min Sets whether the long-run average is to be minimized or maximized. + * @param transitionMatrix The transition matrix of the underlying Markov automaton. + * @param nondeterministicChoiceIndices A vector indicating at which row the choice of a given state begins. + * @param markovianStates A bit vector storing all markovian states. + * @param exitRates A vector with exit rates for all states. Exit rates of probabilistic states are assumed to be zero. + * @param goalStates A bit vector indicating which states are to be considered as goal states. + * @param mec The maximal end component to consider for computing the long-run average. + * @return The long-run average of being in a goal state for the given MEC. + */ + static ValueType computeLraForMaximalEndComponent(bool min, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::BitVector const& markovianStates, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec) { + std::shared_ptr solver = storm::utility::solver::getLpSolver("LRA for MEC"); + solver->setModelSense(min ? storm::solver::LpSolver::MAXIMIZE : storm::solver::LpSolver::MINIMIZE); + + // First, we need to create the variables for the problem. + std::map stateToVariableIndexMap; + for (auto const& stateChoicesPair : mec) { + stateToVariableIndexMap[stateChoicesPair.first] = solver->createContinuousVariable("x" + std::to_string(stateChoicesPair.first), storm::solver::LpSolver::UNBOUNDED, 0, 0, 0); + } + uint_fast64_t lraValueVariableIndex = solver->createContinuousVariable("k", storm::solver::LpSolver::UNBOUNDED, 0, 0, 1); + + // Now we encode the problem as constraints. + std::vector variables; + std::vector coefficients; + for (auto const& stateChoicesPair : mec) { + uint_fast64_t state = stateChoicesPair.first; + + // Now, based on the type of the state, create a suitable constraint. + if (markovianStates.get(state)) { + variables.clear(); + coefficients.clear(); + + variables.push_back(stateToVariableIndexMap.at(state)); + coefficients.push_back(1); + + typename storm::storage::SparseMatrix::Rows row = transitionMatrix.getRow(nondeterministicChoiceIndices[state]); + for (auto element : row) { + variables.push_back(stateToVariableIndexMap.at(element.column())); + coefficients.push_back(-element.value()); + } + + variables.push_back(lraValueVariableIndex); + coefficients.push_back(storm::utility::constGetOne() / exitRates[state]); + + solver->addConstraint("state" + std::to_string(state), variables, coefficients, min ? storm::solver::LpSolver::LESS_EQUAL : storm::solver::LpSolver::GREATER_EQUAL, goalStates.get(state) ? storm::utility::constGetOne() / exitRates[state] : storm::utility::constGetZero()); + } else { + // For probabilistic states, we want to add the constraint x_s <= sum P(s, a, s') * x_s' where a is the current action + // and the sum ranges over all states s'. + for (auto choice : stateChoicesPair.second) { + variables.clear(); + coefficients.clear(); + + variables.push_back(stateToVariableIndexMap.at(state)); + coefficients.push_back(1); + + typename storm::storage::SparseMatrix::Rows row = transitionMatrix.getRow(choice); + for (auto element : row) { + variables.push_back(stateToVariableIndexMap.at(element.column())); + coefficients.push_back(-element.value()); + } + + solver->addConstraint("state" + std::to_string(state), variables, coefficients, min ? storm::solver::LpSolver::LESS_EQUAL : storm::solver::LpSolver::GREATER_EQUAL, storm::utility::constGetZero()); + } + } + } + + solver->optimize(); + return solver->getContinuousValue(lraValueVariableIndex); + } + + /*! + * Computes the expected reward that is gained from each state before entering any of the goal states. + * + * @param min Indicates whether minimal or maximal rewards are to be computed. + * @param goalStates The goal states that define until which point rewards are gained. + * @param stateRewards A vector that defines the reward gained in each state. For probabilistic states, this is an instantaneous reward + * that is fully gained and for Markovian states the actually gained reward is dependent on the expected time to stay in the + * state, i.e. it is gouverned by the exit rate of the state. + * @return A vector that contains the expected reward for each state of the model. + */ + std::vector computeExpectedRewards(bool min, storm::storage::BitVector const& goalStates, std::vector const& stateRewards) const { + // Check whether the automaton is closed. if (!this->getModel().isClosed()) { throw storm::exceptions::InvalidArgumentException() << "Unable to compute expected time on non-closed Markov automaton."; } - + // First, we need to check which states have infinite expected time (by definition). storm::storage::BitVector infinityStates; if (min) { @@ -501,77 +552,50 @@ namespace storm { infinityStates = storm::storage::BitVector(this->getModel().getNumberOfStates()); } } - + // Now we identify the states for which values need to be computed. storm::storage::BitVector maybeStates = ~(goalStates | infinityStates); // 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 = computeNondeterministicChoiceIndicesForConstraint(this->getModel().getNondeterministicChoiceIndices(), maybeStates); + std::vector subNondeterministicChoiceIndices = storm::utility::vector::getConstrainedOffsetVector(this->getModel().getNondeterministicChoiceIndices(), maybeStates); storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(maybeStates, this->getModel().getNondeterministicChoiceIndices()); - - // Now prepare the mean sojourn times for all states so they can be used as the right-hand side of the equation system. - std::vector meanSojournTimes(this->getModel().getExitRates()); + + // 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); for (auto state : this->getModel().getMarkovianStates()) { - meanSojournTimes[state] = storm::utility::constGetOne() / meanSojournTimes[state]; + rewardValues[state] = rewardValues[state] / this->getModel().getExitRates()[state]; } // Finally, prepare the actual right-hand side. std::vector b(submatrix.getRowCount()); - storm::utility::vector::selectVectorValuesRepeatedly(b, maybeStates, this->getModel().getNondeterministicChoiceIndices(), meanSojournTimes); + storm::utility::vector::selectVectorValuesRepeatedly(b, maybeStates, this->getModel().getNondeterministicChoiceIndices(), rewardValues); // Solve the corresponding system of equations. - std::unique_ptr> nondeterministiclinearEquationSolver = storm::utility::solver::getNondeterministicLinearEquationSolver(); + std::shared_ptr> nondeterministiclinearEquationSolver = storm::utility::solver::getNondeterministicLinearEquationSolver(); nondeterministiclinearEquationSolver->solveEquationSystem(min, submatrix, x, b, subNondeterministicChoiceIndices); // Create resulting vector. std::vector result(this->getModel().getNumberOfStates()); - + // Set values of resulting vector according to previous result and return the result. storm::utility::vector::setVectorValues(result, maybeStates, x); storm::utility::vector::setVectorValues(result, goalStates, storm::utility::constGetZero()); storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::constGetInfinity()); - + return result; } - protected: /*! * A stack used for storing whether we are currently computing min or max probabilities or rewards, respectively. * The topmost element is true if and only if we are currently computing minimum probabilities or rewards. */ mutable std::stack minimumOperatorStack; - private: /*! - * Computes the nondeterministic choice indices vector resulting from reducing the full system to the states given - * by the parameter constraint. - * - * @param constraint A bit vector specifying which states are kept. - * @returns A vector of the nondeterministic choice indices of the subsystem induced by the given constraint. + * A solver that is used for solving systems of linear equations that are the result of nondeterministic choices. */ - static std::vector computeNondeterministicChoiceIndicesForConstraint(std::vector const& nondeterministicChoiceIndices, storm::storage::BitVector const& constraint) { - // Reserve the known amount of slots for the resulting vector. - std::vector subNondeterministicChoiceIndices(constraint.getNumberOfSetBits() + 1); - uint_fast64_t currentRowCount = 0; - uint_fast64_t currentIndexCount = 1; - - // Set the first element as this will clearly begin at offset 0. - subNondeterministicChoiceIndices[0] = 0; - - // Loop over all states that need to be kept and copy the relative indices of the nondeterministic choices over - // to the resulting vector. - for (auto index : constraint) { - subNondeterministicChoiceIndices[currentIndexCount] = currentRowCount + nondeterministicChoiceIndices[index + 1] - nondeterministicChoiceIndices[index]; - currentRowCount += nondeterministicChoiceIndices[index + 1] - nondeterministicChoiceIndices[index]; - ++currentIndexCount; - } - - // Put a sentinel element at the end. - subNondeterministicChoiceIndices[constraint.getNumberOfSetBits()] = currentRowCount; - - return subNondeterministicChoiceIndices; - } + std::shared_ptr> nondeterministicLinearEquationSolver; }; } } diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 59f910895..b51bb5565 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -18,6 +18,7 @@ #include "src/models/Mdp.h" #include "src/utility/vector.h" #include "src/utility/graph.h" +#include "src/utility/solver.h" #include "src/settings/Settings.h" #include "src/storage/TotalScheduler.h" @@ -37,7 +38,7 @@ namespace storm { * * @param model The MDP to be checked. */ - explicit SparseMdpPrctlModelChecker(storm::models::Mdp const& model, storm::solver::AbstractNondeterministicLinearEquationSolver* linearEquationSolver) : AbstractModelChecker(model), minimumOperatorStack(), linearEquationSolver(linearEquationSolver) { + explicit SparseMdpPrctlModelChecker(storm::models::Mdp const& model, std::shared_ptr> nondeterministicLinearEquationSolver = storm::utility::solver::getNondeterministicLinearEquationSolver()) : AbstractModelChecker(model), minimumOperatorStack(), nondeterministicLinearEquationSolver(nondeterministicLinearEquationSolver) { // Intentionally left empty. } @@ -46,7 +47,7 @@ namespace storm { * constructed model checker will have the model of the given model checker as its associated model. */ explicit SparseMdpPrctlModelChecker(storm::modelchecker::prctl::SparseMdpPrctlModelChecker const& modelchecker) - : AbstractModelChecker(modelchecker), minimumOperatorStack(), linearEquationSolver(new storm::solver::AbstractNondeterministicLinearEquationSolver()) { + : AbstractModelChecker(modelchecker), minimumOperatorStack(), nondeterministicLinearEquationSolver(storm::utility::solver::getNondeterministicLinearEquationSolver()) { // Intentionally left empty. } @@ -115,7 +116,7 @@ namespace storm { storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(statesWithProbabilityGreater0, this->getModel().getNondeterministicChoiceIndices()); // Get the "new" nondeterministic choice indices for the submatrix. - std::vector subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(statesWithProbabilityGreater0); + 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 = statesWithProbabilityGreater0 % psiStates; @@ -127,11 +128,7 @@ namespace storm { std::vector subresult(statesWithProbabilityGreater0.getNumberOfSetBits()); storm::utility::vector::setVectorValues(subresult, rightStatesInReducedSystem, storm::utility::constGetOne()); - if (linearEquationSolver != nullptr) { - this->linearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), submatrix, subresult, subNondeterministicChoiceIndices, nullptr, stepBound); - } else { - throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available."; - } + this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), submatrix, subresult, subNondeterministicChoiceIndices, nullptr, stepBound); // Set the values of the resulting vector accordingly. storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0, subresult); @@ -172,11 +169,7 @@ namespace storm { std::vector result(this->getModel().getNumberOfStates()); storm::utility::vector::setVectorValues(result, nextStates, storm::utility::constGetOne()); - if (linearEquationSolver != nullptr) { - this->linearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), result, this->getModel().getNondeterministicChoiceIndices()); - } else { - throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available."; - } + this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), result, this->getModel().getNondeterministicChoiceIndices()); return result; } @@ -325,7 +318,7 @@ namespace storm { storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(maybeStates, this->getModel().getNondeterministicChoiceIndices()); // Get the "new" nondeterministic choice indices for the submatrix. - std::vector subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates); + 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. @@ -335,11 +328,7 @@ namespace storm { std::vector x(maybeStates.getNumberOfSetBits()); // Solve the corresponding system of equations. - if (linearEquationSolver != nullptr) { - this->linearEquationSolver->solveEquationSystem(minimize, submatrix, x, b, subNondeterministicChoiceIndices); - } else { - throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available."; - } + this->nondeterministicLinearEquationSolver->solveEquationSystem(minimize, submatrix, x, b, subNondeterministicChoiceIndices); // Set values of resulting vector according to result. storm::utility::vector::setVectorValues(result, maybeStates, x); @@ -376,11 +365,7 @@ namespace storm { // Initialize result to state rewards of the model. std::vector result(this->getModel().getStateRewardVector()); - if (linearEquationSolver != nullptr) { - this->linearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), result, this->getModel().getNondeterministicChoiceIndices(), nullptr, formula.getBound()); - } else { - throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available."; - } + this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), result, this->getModel().getNondeterministicChoiceIndices(), nullptr, formula.getBound()); return result; } @@ -422,11 +407,7 @@ namespace storm { result.resize(this->getModel().getNumberOfStates()); } - if (linearEquationSolver != nullptr) { - this->linearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), result, this->getModel().getNondeterministicChoiceIndices(), &totalRewardVector, formula.getBound()); - } else { - throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available."; - } + this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), result, this->getModel().getNondeterministicChoiceIndices(), &totalRewardVector, formula.getBound()); return result; } @@ -500,7 +481,7 @@ namespace storm { storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(maybeStates, this->getModel().getNondeterministicChoiceIndices()); // Get the "new" nondeterministic choice indices for the submatrix. - std::vector subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates); + 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. @@ -534,11 +515,7 @@ namespace storm { std::vector x(maybeStates.getNumberOfSetBits()); // Solve the corresponding system of equations. - if (linearEquationSolver != nullptr) { - this->linearEquationSolver->solveEquationSystem(minimize, submatrix, x, b, subNondeterministicChoiceIndices); - } else { - throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available."; - } + this->nondeterministicLinearEquationSolver->solveEquationSystem(minimize, submatrix, x, b, subNondeterministicChoiceIndices); // Set values of resulting vector according to result. storm::utility::vector::setVectorValues(result, maybeStates, x); @@ -601,45 +578,11 @@ namespace storm { */ mutable std::stack minimumOperatorStack; - private: /*! - * Computes the nondeterministic choice indices vector resulting from reducing the full system to the states given - * by the parameter constraint. - * - * @param constraint A bit vector specifying which states are kept. - * @returns A vector of the nondeterministic choice indices of the subsystem induced by the given constraint. + * A solver that is used for solving systems of linear equations that are the result of nondeterministic choices. */ - std::vector computeNondeterministicChoiceIndicesForConstraint(storm::storage::BitVector const& constraint) const { - // First, get a reference to the full nondeterministic choice indices. - std::vector const& nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices(); - - // Reserve the known amount of slots for the resulting vector. - std::vector subNondeterministicChoiceIndices(constraint.getNumberOfSetBits() + 1); - uint_fast64_t currentRowCount = 0; - uint_fast64_t currentIndexCount = 1; - - // Set the first element as this will clearly begin at offset 0. - subNondeterministicChoiceIndices[0] = 0; - - // Loop over all states that need to be kept and copy the relative indices of the nondeterministic choices over - // to the resulting vector. - for (auto index : constraint) { - subNondeterministicChoiceIndices[currentIndexCount] = currentRowCount + nondeterministicChoiceIndices[index + 1] - nondeterministicChoiceIndices[index]; - currentRowCount += nondeterministicChoiceIndices[index + 1] - nondeterministicChoiceIndices[index]; - ++currentIndexCount; - } - - // Put a sentinel element at the end. - subNondeterministicChoiceIndices[constraint.getNumberOfSetBits()] = currentRowCount; - - return subNondeterministicChoiceIndices; - } - - // An object that is used for solving linear equations and performing matrix-vector multiplication. - std::unique_ptr> linearEquationSolver; - + std::shared_ptr> nondeterministicLinearEquationSolver; }; - } // namespace prctl } // namespace modelchecker } // namespace storm diff --git a/src/solver/AbstractNondeterministicLinearEquationSolver.h b/src/solver/AbstractNondeterministicLinearEquationSolver.h index f0036a397..4ab08cf90 100644 --- a/src/solver/AbstractNondeterministicLinearEquationSolver.h +++ b/src/solver/AbstractNondeterministicLinearEquationSolver.h @@ -86,8 +86,10 @@ namespace storm { // auto startTime = std::chrono::high_resolution_clock::now(); // std::chrono::nanoseconds totalTime(0); + bool multiplyResultMemoryProvided = true; if (multiplyResult == nullptr) { multiplyResult = new std::vector(A.getRowCount()); + multiplyResultMemoryProvided = false; } std::vector* currentX = &x; bool xMemoryProvided = true; @@ -134,6 +136,10 @@ namespace storm { } else if (!xMemoryProvided) { delete newX; } + + if (!multiplyResultMemoryProvided) { + delete multiplyResult; + } // // Check if the solver converged and issue a warning otherwise. // if (converged) { diff --git a/src/solver/GmmxxNondeterministicLinearEquationSolver.h b/src/solver/GmmxxNondeterministicLinearEquationSolver.h index bef5c838f..205e724f1 100644 --- a/src/solver/GmmxxNondeterministicLinearEquationSolver.h +++ b/src/solver/GmmxxNondeterministicLinearEquationSolver.h @@ -52,8 +52,10 @@ namespace storm { gmm::csr_matrix* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(A); // Set up the environment for the power method. + bool multiplyResultMemoryProvided = true; if (multiplyResult == nullptr) { multiplyResult = new std::vector(A.getRowCount()); + multiplyResultMemoryProvided = false; } std::vector* currentX = &x; @@ -101,7 +103,11 @@ namespace storm { delete newX; } delete gmmxxMatrix; - + + if (!multiplyResultMemoryProvided) { + delete multiplyResult; + } + // Check if the solver converged and issue a warning otherwise. if (converged) { LOG4CPLUS_INFO(logger, "Iterative solver converged after " << iterations << " iterations."); diff --git a/src/storm.cpp b/src/storm.cpp index 820b2be7f..6aee44050 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -231,18 +231,7 @@ storm::modelchecker::prctl::AbstractModelChecker* createPrctlModelChecke */ storm::modelchecker::prctl::AbstractModelChecker* createPrctlModelChecker(storm::models::Mdp& mdp) { // Create the appropriate model checker. - storm::settings::Settings* s = storm::settings::Settings::getInstance(); - std::string const chosenMatrixLibrary = s->getOptionByLongName("matrixLibrary").getArgument(0).getValueAsString(); - if (chosenMatrixLibrary == "gmm++") { - return new storm::modelchecker::prctl::SparseMdpPrctlModelChecker(mdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver()); - } else if (chosenMatrixLibrary == "native") { - return new storm::modelchecker::prctl::SparseMdpPrctlModelChecker(mdp, new storm::solver::AbstractNondeterministicLinearEquationSolver()); - } - - // The control flow should never reach this point, as there is a default setting for matrixlib. - std::string message = "No matrix library suitable for MDP model checking has been set."; - throw storm::exceptions::InvalidSettingsException() << message; - return nullptr; + return new storm::modelchecker::prctl::SparseMdpPrctlModelChecker(mdp); } /*! @@ -473,10 +462,10 @@ int main(const int argc, const char* argv[]) { LOG4CPLUS_INFO(logger, "Model is a Markov automaton."); std::shared_ptr> markovAutomaton = parser.getModel>(); markovAutomaton->close(); - storm::modelchecker::csl::SparseMarkovAutomatonCslModelChecker mc(*markovAutomaton); -// std::cout << mc.checkExpectedTime(true, markovAutomaton->getLabeledStates("goal")) << std::endl; -// std::cout << mc.checkLongRunAverage(true, markovAutomaton->getLabeledStates("goal")) << std::endl; -// std::cout << mc.checkTimeBoundedEventually(true, markovAutomaton->getLabeledStates("goal"), 0, 1) << std::endl; + storm::modelchecker::csl::SparseMarkovAutomatonCslModelChecker mc(*markovAutomaton, std::shared_ptr>(new storm::solver::AbstractNondeterministicLinearEquationSolver())); + std::cout << mc.checkExpectedTime(true, markovAutomaton->getLabeledStates("goal")) << std::endl; + std::cout << mc.checkLongRunAverage(true, markovAutomaton->getLabeledStates("goal")) << std::endl; + std::cout << mc.checkTimeBoundedEventually(true, markovAutomaton->getLabeledStates("goal"), 0, 1) << std::endl; std::cout << mc.checkTimeBoundedEventually(true, markovAutomaton->getLabeledStates("goal"), 1, 2) << std::endl; break; } diff --git a/src/utility/solver.cpp b/src/utility/solver.cpp new file mode 100644 index 000000000..16578aaf8 --- /dev/null +++ b/src/utility/solver.cpp @@ -0,0 +1,25 @@ +#include "src/utility/solver.h" + +namespace storm { + namespace utility { + namespace solver { + std::shared_ptr getLpSolver(std::string const& name) { + return std::shared_ptr(new storm::solver::GurobiLpSolver(name)); + } + + template + std::shared_ptr> getNondeterministicLinearEquationSolver() { + std::string const& matrixLibrary = storm::settings::Settings::getInstance()->getOptionByLongName("matrixLibrary").getArgument(0).getValueAsString(); + if (matrixLibrary == "gmm++") { + return std::shared_ptr>(new storm::solver::GmmxxNondeterministicLinearEquationSolver()); + } else if (matrixLibrary == "native") { + return std::shared_ptr>(new storm::solver::AbstractNondeterministicLinearEquationSolver()); + } + + throw storm::exceptions::InvalidSettingsException() << "No suitable nondeterministic linear equation solver selected."; + } + + template std::shared_ptr> getNondeterministicLinearEquationSolver(); + } + } +} \ No newline at end of file diff --git a/src/utility/solver.h b/src/utility/solver.h index fdf838174..165ba9c00 100644 --- a/src/utility/solver.h +++ b/src/utility/solver.h @@ -5,19 +5,16 @@ #include "src/solver/GmmxxNondeterministicLinearEquationSolver.h" #include "src/solver/GurobiLpSolver.h" +#include "src/exceptions/InvalidSettingsException.h" + namespace storm { namespace utility { namespace solver { - std::unique_ptr getLpSolver(std::string const& name) { - return std::unique_ptr(new storm::solver::GurobiLpSolver(name)); - } + std::shared_ptr getLpSolver(std::string const& name); template - std::unique_ptr> getNondeterministicLinearEquationSolver() { - return std::unique_ptr>(new storm::solver::AbstractNondeterministicLinearEquationSolver()); -// return std::unique_ptr>(new storm::solver::GmmxxNondeterministicLinearEquationSolver()); - } + std::shared_ptr> getNondeterministicLinearEquationSolver(); } } } diff --git a/src/utility/vector.h b/src/utility/vector.h index 0ee5033d2..c9bf3b35d 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -1,10 +1,3 @@ -/* - * vector.h - * - * Created on: 06.12.2012 - * Author: Christian Dehnert - */ - #ifndef STORM_UTILITY_VECTOR_H_ #define STORM_UTILITY_VECTOR_H_ @@ -14,295 +7,318 @@ #include #include -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" - -extern log4cplus::Logger logger; - namespace storm { - -namespace utility { - -namespace vector { - -/*! - * Sets the provided values at the provided positions in the given vector. - * - * @param vector The vector in which the values are to be set. - * @param positions The positions at which the values are to be set. - * @param values The values that are to be set. - */ -template -void setVectorValues(std::vector& vector, storm::storage::BitVector const& positions, std::vector const& values) { - uint_fast64_t oldPosition = 0; - for (auto position : positions) { - vector[position] = values[oldPosition++]; - } -} - -/*! - * Sets the provided value at the provided positions in the given vector. - * - * @param vector The vector in which the value is to be set. - * @param positions The positions at which the value is to be set. - * @param value The value that is to be set. - */ -template -void setVectorValues(std::vector& vector, storm::storage::BitVector const& positions, T value) { - for (auto position : positions) { - vector[position] = value; - } -} - -/*! - * Sets the provided value at the provided positions in the given vector. - * - * @param vector The vector in which the value is to be set. - * @param positions The positions at which the value is to be set. - * @param value The value that is to be set. - */ -template -void setVectorValues(Eigen::Matrix& eigenVector, storm::storage::BitVector const& positions, T value) { - for (auto position : positions) { - eigenVector(position, 0) = value; - } -} - -/*! - * Selects the elements from a vector at the specified positions and writes them consecutively into another vector. - * @param vector The vector into which the selected elements are to be written. - * @param positions The positions at which to select the elements from the values vector. - * @param values The vector from which to select the elements. - */ -template -void selectVectorValues(std::vector& vector, storm::storage::BitVector const& positions, std::vector const& values) { - uint_fast64_t oldPosition = 0; - for (auto position : positions) { - vector[oldPosition++] = values[position]; - } -} - -/*! - * Selects groups of elements from a vector at the specified positions and writes them consecutively into another vector. - * - * @param vector The vector into which the selected elements are to be written. - * @param positions The positions of the groups of elements that are to be selected. - * @param rowGrouping A vector that specifies the begin and end of each group of elements in the values vector. - * @param values The vector from which to select groups of elements. - */ -template -void selectVectorValues(std::vector& vector, storm::storage::BitVector const& positions, std::vector const& rowGrouping, std::vector const& values) { - uint_fast64_t oldPosition = 0; - for (auto position : positions) { - for (uint_fast64_t i = rowGrouping[position]; i < rowGrouping[position + 1]; ++i) { - vector[oldPosition++] = values[i]; - } - } -} - -/*! - * Selects one element out of each row group and writes it to the target vector. - * - * @param vector The target vector to which the values are written. - * @param rowGroupToRowIndexMapping A mapping from row group indices to an offset that specifies which of the values to - * take from the row group. - * @param rowGrouping A vector that specifies the begin and end of each group of elements in the values vector. - * @param values The vector from which to select the values. - */ -template -void selectVectorValues(std::vector& vector, std::vector const& rowGroupToRowIndexMapping, std::vector const& rowGrouping, std::vector const& values) { - uint_fast64_t oldPosition = 0; - for (uint_fast64_t i = 0; i < vector.size(); ++i) { - vector[i] = values[rowGrouping[i] + rowGroupToRowIndexMapping[i]]; - } -} - -/*! - * Selects values from a vector at the specified positions and writes them into another vector as often as given by - * the size of the corresponding group of elements. - * - * @param vector The vector into which the selected elements are written. - * @param positions The positions at which to select the values. - * @param rowGrouping A vector that specifies the begin and end of each group of elements in the values vector. This - * implicitly defines the number of times any element is written to the output vector. - */ -template -void selectVectorValuesRepeatedly(std::vector& vector, storm::storage::BitVector const& positions, std::vector const& rowGrouping, std::vector const& values) { - uint_fast64_t oldPosition = 0; - for (auto position : positions) { - for (uint_fast64_t i = rowGrouping[position]; i < rowGrouping[position + 1]; ++i) { - vector[oldPosition++] = values[position]; - } - } -} - -/*! - * Subtracts the given vector from the constant one-vector and writes the result to the input vector. - * - * @param vector The vector that is to be subtracted from the constant one-vector. - */ -template -void subtractFromConstantOneVector(std::vector& vector) { - for (auto& element : vector) { - element = storm::utility::constGetOne() - element; - } -} - -/*! - * Adds the two given vectors and writes the result into the first operand. - * - * @param target The first summand and target vector. - * @param summand The second summand. - */ -template -void addVectorsInPlace(std::vector& target, std::vector const& summand) { - if (target.size() != summand.size()) { - LOG4CPLUS_ERROR(logger, "Lengths of vectors do not match, which makes operation impossible."); - throw storm::exceptions::InvalidArgumentException() << "Length of vectors do not match, which makes operation impossible."; - } - - std::transform(target.begin(), target.end(), summand.begin(), target.begin(), std::plus()); -} - -/*! - * Reduces the given source vector by selecting an element according to the given filter out of each row group. - * - * @param source The source vector which is to be reduced. - * @param target The target vector into which a single element from each row group is written. - * @param rowGrouping A vector that specifies the begin and end of each group of elements in the values vector. - * @param filter A function that compares two elements v1 and v2 according to some filter criterion. This function must - * return true iff v1 is supposed to be taken instead of v2. - * @param choices If non-null, this vector is used to store the choices made during the selection. - */ -template -void reduceVector(std::vector const& source, std::vector& target, std::vector const& rowGrouping, std::function filter, std::vector* choices = nullptr) { - uint_fast64_t currentSourceRow = 0; - uint_fast64_t currentTargetRow = -1; - uint_fast64_t currentLocalRow = 0; - for (auto it = source.cbegin(), ite = source.cend(); it != ite; ++it, ++currentSourceRow, ++currentLocalRow) { - // Check whether we have considered all source rows for the current target row. - if (rowGrouping[currentTargetRow + 1] <= currentSourceRow || currentSourceRow == 0) { - currentLocalRow = 0; - ++currentTargetRow; - target[currentTargetRow] = source[currentSourceRow]; - if (choices != nullptr) { - (*choices)[currentTargetRow] = 0; + namespace utility { + namespace vector { + + /*! + * Sets the provided values at the provided positions in the given vector. + * + * @param vector The vector in which the values are to be set. + * @param positions The positions at which the values are to be set. + * @param values The values that are to be set. + */ + template + void setVectorValues(std::vector& vector, storm::storage::BitVector const& positions, std::vector const& values) { + uint_fast64_t oldPosition = 0; + for (auto position : positions) { + vector[position] = values[oldPosition++]; + } } - continue; - } - // We have to upate the value, so only overwrite the current value if the value passes the filter. - if (filter(*it, target[currentTargetRow])) { - target[currentTargetRow] = *it; - if (choices != nullptr) { - (*choices)[currentTargetRow] = currentLocalRow; + /*! + * Sets the provided value at the provided positions in the given vector. + * + * @param vector The vector in which the value is to be set. + * @param positions The positions at which the value is to be set. + * @param value The value that is to be set. + */ + template + void setVectorValues(std::vector& vector, storm::storage::BitVector const& positions, T value) { + for (auto position : positions) { + vector[position] = value; + } } - } - } -} - -/*! - * Reduces the given source vector by selecting the smallest element out of each row group. - * - * @param source The source vector which is to be reduced. - * @param target The target vector into which a single element from each row group is written. - * @param rowGrouping A vector that specifies the begin and end of each group of elements in the source vector. - * @param choices If non-null, this vector is used to store the choices made during the selection. - */ -template -void reduceVectorMin(std::vector const& source, std::vector& target, std::vector const& rowGrouping, std::vector* choices = nullptr) { - reduceVector(source, target, rowGrouping, std::less(), choices); -} - -/*! - * Reduces the given source vector by selecting the largest element out of each row group. - * - * @param source The source vector which is to be reduced. - * @param target The target vector into which a single element from each row group is written. - * @param rowGrouping A vector that specifies the begin and end of each group of elements in the source vector. - * @param choices If non-null, this vector is used to store the choices made during the selection. - */ -template -void reduceVectorMax(std::vector const& source, std::vector& target, std::vector const& rowGrouping, std::vector* choices = nullptr) { - reduceVector(source, target, rowGrouping, std::greater(), choices); -} - -/*! - * Compares the given elements and determines whether they are equal modulo the given precision. The provided flag - * additionaly specifies whether the error is computed in relative or absolute terms. - * - * @param val1 The first value to compare. - * @param val2 The second value to compare. - * @param precision The precision up to which the elements are compared. - * @param relativeError If set, the error is computed relative to the second value. - * @return True iff the elements are considered equal. - */ -template -bool equalModuloPrecision(T const& val1, T const& val2, T precision, bool relativeError = true) { - if (relativeError) { - if (std::abs(val1 - val2)/val2 > precision) return false; - } else { - if (std::abs(val1 - val2) > precision) return false; - } - return true; -} - -/*! - * Compares the two vectors and determines whether they are equal modulo the provided precision. Depending on whether the - * flag is set, the difference between the vectors is computed relative to the value or in absolute terms. - * - * @param vectorLeft The first vector of the comparison. - * @param vectorRight The second vector of the comparison. - * @param precision The precision up to which the vectors are to be checked for equality. - * @param relativeError If set, the difference between the vectors is computed relative to the value or in absolute terms. - */ -template -bool equalModuloPrecision(std::vector const& vectorLeft, std::vector const& vectorRight, T precision, bool relativeError) { - if (vectorLeft.size() != vectorRight.size()) { - LOG4CPLUS_ERROR(logger, "Lengths of vectors do not match, which makes comparison impossible."); - throw storm::exceptions::InvalidArgumentException() << "Lengths of vectors do not match, which makes comparison impossible."; - } - - for (uint_fast64_t i = 0; i < vectorLeft.size(); ++i) { - if (!equalModuloPrecision(vectorLeft[i], vectorRight[i], precision, relativeError)) { - return false; - } - } - - return true; -} - -/*! - * Compares the two vectors at the specified positions and determines whether they are equal modulo the provided - * precision. Depending on whether the flag is set, the difference between the vectors is computed relative to the value - * or in absolute terms. - * - * @param vectorLeft The first vector of the comparison. - * @param vectorRight The second vector of the comparison. - * @param precision The precision up to which the vectors are to be checked for equality. - * @param positions A vector representing a set of positions at which the vectors are compared. - * @param relativeError If set, the difference between the vectors is computed relative to the value or in absolute terms. - */ -template -bool equalModuloPrecision(std::vector const& vectorLeft, std::vector const& vectorRight, std::vector const& positions, T precision, bool relativeError) { - if (vectorLeft.size() != vectorRight.size()) { - LOG4CPLUS_ERROR(logger, "Lengths of vectors do not match, which makes comparison impossible."); - throw storm::exceptions::InvalidArgumentException() << "Lengths of vectors do not match, which makes comparison impossible."; - } - - for (uint_fast64_t position : positions) { - if (!equalModuloPrecision(vectorLeft[position], vectorRight[position], precision, relativeError)) { - return false; - } - } - - return true; -} - -} // namespace vector - -} // namespace utility - + + /*! + * Sets the provided value at the provided positions in the given vector. + * + * @param vector The vector in which the value is to be set. + * @param positions The positions at which the value is to be set. + * @param value The value that is to be set. + */ + template + void setVectorValues(Eigen::Matrix& eigenVector, storm::storage::BitVector const& positions, T value) { + for (auto position : positions) { + eigenVector(position, 0) = value; + } + } + + /*! + * Selects the elements from a vector at the specified positions and writes them consecutively into another vector. + * @param vector The vector into which the selected elements are to be written. + * @param positions The positions at which to select the elements from the values vector. + * @param values The vector from which to select the elements. + */ + template + void selectVectorValues(std::vector& vector, storm::storage::BitVector const& positions, std::vector const& values) { + uint_fast64_t oldPosition = 0; + for (auto position : positions) { + vector[oldPosition++] = values[position]; + } + } + + /*! + * Selects groups of elements from a vector at the specified positions and writes them consecutively into another vector. + * + * @param vector The vector into which the selected elements are to be written. + * @param positions The positions of the groups of elements that are to be selected. + * @param rowGrouping A vector that specifies the begin and end of each group of elements in the values vector. + * @param values The vector from which to select groups of elements. + */ + template + void selectVectorValues(std::vector& vector, storm::storage::BitVector const& positions, std::vector const& rowGrouping, std::vector const& values) { + uint_fast64_t oldPosition = 0; + for (auto position : positions) { + for (uint_fast64_t i = rowGrouping[position]; i < rowGrouping[position + 1]; ++i) { + vector[oldPosition++] = values[i]; + } + } + } + + /*! + * Selects one element out of each row group and writes it to the target vector. + * + * @param vector The target vector to which the values are written. + * @param rowGroupToRowIndexMapping A mapping from row group indices to an offset that specifies which of the values to + * take from the row group. + * @param rowGrouping A vector that specifies the begin and end of each group of elements in the values vector. + * @param values The vector from which to select the values. + */ + template + void selectVectorValues(std::vector& vector, std::vector const& rowGroupToRowIndexMapping, std::vector const& rowGrouping, std::vector const& values) { + uint_fast64_t oldPosition = 0; + for (uint_fast64_t i = 0; i < vector.size(); ++i) { + vector[i] = values[rowGrouping[i] + rowGroupToRowIndexMapping[i]]; + } + } + + /*! + * Selects values from a vector at the specified positions and writes them into another vector as often as given by + * the size of the corresponding group of elements. + * + * @param vector The vector into which the selected elements are written. + * @param positions The positions at which to select the values. + * @param rowGrouping A vector that specifies the begin and end of each group of elements in the values vector. This + * implicitly defines the number of times any element is written to the output vector. + */ + template + void selectVectorValuesRepeatedly(std::vector& vector, storm::storage::BitVector const& positions, std::vector const& rowGrouping, std::vector const& values) { + uint_fast64_t oldPosition = 0; + for (auto position : positions) { + for (uint_fast64_t i = rowGrouping[position]; i < rowGrouping[position + 1]; ++i) { + vector[oldPosition++] = values[position]; + } + } + } + + /*! + * Subtracts the given vector from the constant one-vector and writes the result to the input vector. + * + * @param vector The vector that is to be subtracted from the constant one-vector. + */ + template + void subtractFromConstantOneVector(std::vector& vector) { + for (auto& element : vector) { + element = storm::utility::constGetOne() - element; + } + } + + /*! + * Adds the two given vectors and writes the result into the first operand. + * + * @param target The first summand and target vector. + * @param summand The second summand. + */ + template + void addVectorsInPlace(std::vector& target, std::vector const& summand) { + if (target.size() != summand.size()) { + LOG4CPLUS_ERROR(logger, "Lengths of vectors do not match, which makes operation impossible."); + throw storm::exceptions::InvalidArgumentException() << "Length of vectors do not match, which makes operation impossible."; + } + + std::transform(target.begin(), target.end(), summand.begin(), target.begin(), std::plus()); + } + + /*! + * Reduces the given source vector by selecting an element according to the given filter out of each row group. + * + * @param source The source vector which is to be reduced. + * @param target The target vector into which a single element from each row group is written. + * @param rowGrouping A vector that specifies the begin and end of each group of elements in the values vector. + * @param filter A function that compares two elements v1 and v2 according to some filter criterion. This function must + * return true iff v1 is supposed to be taken instead of v2. + * @param choices If non-null, this vector is used to store the choices made during the selection. + */ + template + void reduceVector(std::vector const& source, std::vector& target, std::vector const& rowGrouping, std::function filter, std::vector* choices = nullptr) { + uint_fast64_t currentSourceRow = 0; + uint_fast64_t currentTargetRow = -1; + uint_fast64_t currentLocalRow = 0; + for (auto it = source.cbegin(), ite = source.cend(); it != ite; ++it, ++currentSourceRow, ++currentLocalRow) { + // Check whether we have considered all source rows for the current target row. + if (rowGrouping[currentTargetRow + 1] <= currentSourceRow || currentSourceRow == 0) { + currentLocalRow = 0; + ++currentTargetRow; + target[currentTargetRow] = source[currentSourceRow]; + if (choices != nullptr) { + (*choices)[currentTargetRow] = 0; + } + continue; + } + + // We have to upate the value, so only overwrite the current value if the value passes the filter. + if (filter(*it, target[currentTargetRow])) { + target[currentTargetRow] = *it; + if (choices != nullptr) { + (*choices)[currentTargetRow] = currentLocalRow; + } + } + } + } + + /*! + * Reduces the given source vector by selecting the smallest element out of each row group. + * + * @param source The source vector which is to be reduced. + * @param target The target vector into which a single element from each row group is written. + * @param rowGrouping A vector that specifies the begin and end of each group of elements in the source vector. + * @param choices If non-null, this vector is used to store the choices made during the selection. + */ + template + void reduceVectorMin(std::vector const& source, std::vector& target, std::vector const& rowGrouping, std::vector* choices = nullptr) { + reduceVector(source, target, rowGrouping, std::less(), choices); + } + + /*! + * Reduces the given source vector by selecting the largest element out of each row group. + * + * @param source The source vector which is to be reduced. + * @param target The target vector into which a single element from each row group is written. + * @param rowGrouping A vector that specifies the begin and end of each group of elements in the source vector. + * @param choices If non-null, this vector is used to store the choices made during the selection. + */ + template + void reduceVectorMax(std::vector const& source, std::vector& target, std::vector const& rowGrouping, std::vector* choices = nullptr) { + reduceVector(source, target, rowGrouping, std::greater(), choices); + } + + /*! + * Compares the given elements and determines whether they are equal modulo the given precision. The provided flag + * additionaly specifies whether the error is computed in relative or absolute terms. + * + * @param val1 The first value to compare. + * @param val2 The second value to compare. + * @param precision The precision up to which the elements are compared. + * @param relativeError If set, the error is computed relative to the second value. + * @return True iff the elements are considered equal. + */ + template + bool equalModuloPrecision(T const& val1, T const& val2, T precision, bool relativeError = true) { + if (relativeError) { + if (std::abs(val1 - val2)/val2 > precision) return false; + } else { + if (std::abs(val1 - val2) > precision) return false; + } + return true; + } + + /*! + * Compares the two vectors and determines whether they are equal modulo the provided precision. Depending on whether the + * flag is set, the difference between the vectors is computed relative to the value or in absolute terms. + * + * @param vectorLeft The first vector of the comparison. + * @param vectorRight The second vector of the comparison. + * @param precision The precision up to which the vectors are to be checked for equality. + * @param relativeError If set, the difference between the vectors is computed relative to the value or in absolute terms. + */ + template + bool equalModuloPrecision(std::vector const& vectorLeft, std::vector const& vectorRight, T precision, bool relativeError) { + if (vectorLeft.size() != vectorRight.size()) { + LOG4CPLUS_ERROR(logger, "Lengths of vectors do not match, which makes comparison impossible."); + throw storm::exceptions::InvalidArgumentException() << "Lengths of vectors do not match, which makes comparison impossible."; + } + + for (uint_fast64_t i = 0; i < vectorLeft.size(); ++i) { + if (!equalModuloPrecision(vectorLeft[i], vectorRight[i], precision, relativeError)) { + return false; + } + } + + return true; + } + + /*! + * Compares the two vectors at the specified positions and determines whether they are equal modulo the provided + * precision. Depending on whether the flag is set, the difference between the vectors is computed relative to the value + * or in absolute terms. + * + * @param vectorLeft The first vector of the comparison. + * @param vectorRight The second vector of the comparison. + * @param precision The precision up to which the vectors are to be checked for equality. + * @param positions A vector representing a set of positions at which the vectors are compared. + * @param relativeError If set, the difference between the vectors is computed relative to the value or in absolute terms. + */ + template + bool equalModuloPrecision(std::vector const& vectorLeft, std::vector const& vectorRight, std::vector const& positions, T precision, bool relativeError) { + if (vectorLeft.size() != vectorRight.size()) { + LOG4CPLUS_ERROR(logger, "Lengths of vectors do not match, which makes comparison impossible."); + throw storm::exceptions::InvalidArgumentException() << "Lengths of vectors do not match, which makes comparison impossible."; + } + + for (uint_fast64_t position : positions) { + if (!equalModuloPrecision(vectorLeft[position], vectorRight[position], precision, relativeError)) { + return false; + } + } + + return true; + } + + /*! + * Takes the given offset vector and applies the given contraint. That is, it produces another offset vector that contains + * the relative offsets of the entries given by the constraint. + * + * @param offsetVector The offset vector to constrain. + * @param constraint The constraint to apply to the offset vector. + * @return An offset vector that contains all selected relative offsets. + */ + template + std::vector getConstrainedOffsetVector(std::vector const& offsetVector, storm::storage::BitVector const& constraint) { + // Reserve the known amount of slots for the resulting vector. + std::vector subVector(constraint.getNumberOfSetBits() + 1); + uint_fast64_t currentRowCount = 0; + uint_fast64_t currentIndexCount = 1; + + // Set the first element as this will clearly begin at offset 0. + subVector[0] = 0; + + // Loop over all states that need to be kept and copy the relative indices of the nondeterministic choices over + // to the resulting vector. + for (auto index : constraint) { + subVector[currentIndexCount] = currentRowCount + offsetVector[index + 1] - offsetVector[index]; + currentRowCount += offsetVector[index + 1] - offsetVector[index]; + ++currentIndexCount; + } + + // Put a sentinel element at the end. + subVector[constraint.getNumberOfSetBits()] = currentRowCount; + + return subVector; + } + + } // namespace vector + } // namespace utility } // namespace storm #endif /* STORM_UTILITY_VECTOR_H_ */ diff --git a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index 7bd87856f..d7ac097b5 100644 --- a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -17,7 +17,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { ASSERT_EQ(mdp->getNumberOfStates(), 169ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); - storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver()); + storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, std::shared_ptr>(new storm::solver::GmmxxNondeterministicLinearEquationSolver())); storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("two"); storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); @@ -105,7 +105,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> stateRewardMdp = stateRewardParser.getModel>(); - storm::modelchecker::prctl::SparseMdpPrctlModelChecker stateRewardModelChecker(*stateRewardMdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver()); + storm::modelchecker::prctl::SparseMdpPrctlModelChecker stateRewardModelChecker(*stateRewardMdp, std::shared_ptr>(new storm::solver::GmmxxNondeterministicLinearEquationSolver())); apFormula = new storm::property::prctl::Ap("done"); reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); @@ -133,7 +133,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> stateAndTransitionRewardMdp = stateAndTransitionRewardParser.getModel>(); - storm::modelchecker::prctl::SparseMdpPrctlModelChecker stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver()); + storm::modelchecker::prctl::SparseMdpPrctlModelChecker stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::shared_ptr>(new storm::solver::GmmxxNondeterministicLinearEquationSolver())); apFormula = new storm::property::prctl::Ap("done"); reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); @@ -167,7 +167,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_EQ(mdp->getNumberOfStates(), 3172ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 7144ull); - storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver()); + storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, std::shared_ptr>(new storm::solver::GmmxxNondeterministicLinearEquationSolver())); storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("elected"); storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); diff --git a/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp index c07c583e8..29b74594d 100644 --- a/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp @@ -16,7 +16,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { ASSERT_EQ(mdp->getNumberOfStates(), 169ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); - storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, new storm::solver::AbstractNondeterministicLinearEquationSolver()); + storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, std::shared_ptr>(new storm::solver::AbstractNondeterministicLinearEquationSolver())); storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("two"); storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); @@ -104,7 +104,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> stateRewardMdp = stateRewardParser.getModel>(); - storm::modelchecker::prctl::SparseMdpPrctlModelChecker stateRewardModelChecker(*stateRewardMdp, new storm::solver::AbstractNondeterministicLinearEquationSolver()); + storm::modelchecker::prctl::SparseMdpPrctlModelChecker stateRewardModelChecker(*stateRewardMdp, std::shared_ptr>(new storm::solver::AbstractNondeterministicLinearEquationSolver())); apFormula = new storm::property::prctl::Ap("done"); reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); @@ -132,7 +132,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> stateAndTransitionRewardMdp = stateAndTransitionRewardParser.getModel>(); - storm::modelchecker::prctl::SparseMdpPrctlModelChecker stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, new storm::solver::AbstractNondeterministicLinearEquationSolver()); + storm::modelchecker::prctl::SparseMdpPrctlModelChecker stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::shared_ptr>(new storm::solver::AbstractNondeterministicLinearEquationSolver())); apFormula = new storm::property::prctl::Ap("done"); reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); @@ -166,7 +166,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_EQ(mdp->getNumberOfStates(), 3172ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 7144ull); - storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, new storm::solver::AbstractNondeterministicLinearEquationSolver()); + storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, std::shared_ptr>(new storm::solver::AbstractNondeterministicLinearEquationSolver())); storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("elected"); storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); diff --git a/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp index 8d575caab..da34f7fec 100644 --- a/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp @@ -17,7 +17,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_EQ(mdp->getNumberOfStates(), 2095783ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385ull); - storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver()); + storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, std::shared_ptr>(new storm::solver::GmmxxNondeterministicLinearEquationSolver())); storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("elected"); storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); @@ -104,7 +104,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Consensus) { ASSERT_EQ(mdp->getNumberOfStates(), 63616ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 213472ull); - storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver()); + storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, std::shared_ptr>(new storm::solver::GmmxxNondeterministicLinearEquationSolver())); storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("finished"); storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); diff --git a/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp index 2a24197a1..a9e489fd1 100644 --- a/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp @@ -17,7 +17,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_EQ(mdp->getNumberOfStates(), 2095783ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385ull); - storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, new storm::solver::AbstractNondeterministicLinearEquationSolver()); + storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, std::shared_ptr>(new storm::solver::AbstractNondeterministicLinearEquationSolver())); storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("elected"); storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); @@ -106,7 +106,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) { ASSERT_EQ(mdp->getNumberOfStates(), 63616ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 213472ull); - storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, new storm::solver::AbstractNondeterministicLinearEquationSolver()); + storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, std::shared_ptr>(new storm::solver::AbstractNondeterministicLinearEquationSolver())); storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("finished"); storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula);