diff --git a/src/storm/utility/policyguessing.cpp b/src/storm/utility/policyguessing.cpp
deleted file mode 100644
index 5949a4047..000000000
--- a/src/storm/utility/policyguessing.cpp
+++ /dev/null
@@ -1,424 +0,0 @@
-#include <stdint.h>
-
-#include "storm/utility/policyguessing.h"
-
-#include "storm/utility/macros.h"
-#include "storm/utility/solver.h"
-#include "storm/solver/LinearEquationSolver.h"
-#include "storm/solver/GmmxxLinearEquationSolver.h"
-#include "graph.h"
-#include "ConstantsComparator.h"
-
-namespace storm {
- namespace utility{
- namespace policyguessing {
-
- template <typename ValueType>
- void solveGame( storm::solver::GameSolver<ValueType>& solver,
- std::vector<ValueType>& x,
- std::vector<ValueType> const& b,
- OptimizationDirection player1Goal,
- OptimizationDirection player2Goal,
- storm::storage::TotalScheduler& player1Scheduler,
- storm::storage::TotalScheduler& player2Scheduler,
- storm::storage::BitVector const& targetChoices,
- ValueType const& prob0Value
- ){
-
- storm::storage::SparseMatrix<ValueType> inducedA;
- std::vector<ValueType> inducedB;
- storm::storage::BitVector probGreater0States;
- getInducedEquationSystem(solver, b, player1Scheduler, player2Scheduler, targetChoices, inducedA, inducedB, probGreater0States);
-
- solveLinearEquationSystem(inducedA, x, inducedB, probGreater0States, prob0Value, solver.getPrecision(), solver.getRelative());
-
- solver.setTrackScheduler();
- bool resultCorrect = false;
- while(!resultCorrect){
- solver.solveGame(player1Goal, player2Goal, x, b);
- player1Scheduler = solver.getPlayer1Scheduler();
- player2Scheduler = solver.getPlayer2Scheduler();
-
- //Check if the policies makes choices that lead to states from which no target state is reachable ("prob0"-states).
- getInducedEquationSystem(solver, b, player1Scheduler, player2Scheduler, targetChoices, inducedA, inducedB, probGreater0States);
- resultCorrect = checkAndFixScheduler(solver, x, b, player1Scheduler, player2Scheduler, targetChoices, inducedA, inducedB, probGreater0States);
- if(!resultCorrect){
- //If the Scheduler could not be fixed, it indicates that our guessed values were to high.
- STORM_LOG_WARN("Policies could not be fixed. Restarting Gamesolver. ");
- solveLinearEquationSystem(inducedA, x, inducedB, probGreater0States, prob0Value, solver.getPrecision(), solver.getRelative());
- //x = std::vector<ValueType>(x.size(), storm::utility::zero<ValueType>());
- }
- }
- }
-
- template <typename ValueType>
- void solveMinMaxLinearEquationSystem( storm::solver::MinMaxLinearEquationSolver<ValueType>& solver,
- storm::storage::SparseMatrix<ValueType> const& A,
- std::vector<ValueType>& x,
- std::vector<ValueType> const& b,
- OptimizationDirection goal,
- storm::storage::TotalScheduler& scheduler,
- storm::storage::BitVector const& targetChoices,
- ValueType const& prob0Value
- ){
- storm::storage::SparseMatrix<ValueType> inducedA;
- std::vector<ValueType> inducedB;
- storm::storage::BitVector probGreater0States;
- getInducedEquationSystem(A, b, scheduler, targetChoices, inducedA, inducedB, probGreater0States);
- solveLinearEquationSystem(inducedA, x, inducedB, probGreater0States, prob0Value, solver.getPrecision(), solver.getRelative());
-
- solver.setTrackScheduler();
- solver.setCachingEnabled(true);
- bool resultCorrect = false;
- while(!resultCorrect){
- solver.solveEquations(goal, x, b);
- scheduler = std::move(*solver.getScheduler());
-
- //Check if the Scheduler makes choices that lead to states from which no target state is reachable ("prob0"-states).
- getInducedEquationSystem(A, b, scheduler, targetChoices, inducedA, inducedB, probGreater0States);
- resultCorrect = checkAndFixScheduler(A, x, b, scheduler, targetChoices, solver.getPrecision(), solver.getRelative(), inducedA, inducedB, probGreater0States);
-
- if(!resultCorrect){
- //If the Scheduler could not be fixed, it indicates that our guessed values were to high.
- STORM_LOG_WARN("Scheduler could not be fixed. Restarting MinMaxsolver." );
- solveLinearEquationSystem(inducedA, x, inducedB, probGreater0States, prob0Value, solver.getPrecision(), solver.getRelative());
- }
- }
-
-
- }
-
- template <typename ValueType>
- void getInducedEquationSystem(storm::solver::GameSolver<ValueType> const& solver,
- std::vector<ValueType> const& b,
- storm::storage::TotalScheduler const& player1Scheduler,
- storm::storage::TotalScheduler const& player2Scheduler,
- storm::storage::BitVector const& targetChoices,
- storm::storage::SparseMatrix<ValueType>& inducedA,
- std::vector<ValueType>& inducedB,
- storm::storage::BitVector& probGreater0States
- ){
- uint_fast64_t numberOfPlayer1States = solver.getPlayer1Matrix().getRowGroupCount();
-
- //Get the rows of the player2matrix that are selected by the policies
- //Note that rows can be selected more then once and in an arbitrary order.
- std::vector<storm::storage::sparse::state_type> selectedRows(numberOfPlayer1States);
- for (uint_fast64_t pl1State = 0; pl1State < numberOfPlayer1States; ++pl1State){
- auto const& pl1Row = solver.getPlayer1Matrix().getRow(solver.getPlayer1Matrix().getRowGroupIndices()[pl1State] + player1Scheduler.getChoice(pl1State));
- STORM_LOG_ASSERT(pl1Row.getNumberOfEntries()==1, "");
- uint_fast64_t pl2State = pl1Row.begin()->getColumn();
- selectedRows[pl1State] = solver.getPlayer2Matrix().getRowGroupIndices()[pl2State] + player2Scheduler.getChoice(pl2State);
- }
- //Get the matrix A, vector b, and the targetStates induced by this selection
- inducedA = solver.getPlayer2Matrix().selectRowsFromRowIndexSequence(selectedRows, false);
- inducedB = std::vector<ValueType>(numberOfPlayer1States);
- storm::utility::vector::selectVectorValues<ValueType>(inducedB, selectedRows, b);
- storm::storage::BitVector inducedTarget(numberOfPlayer1States, false);
- for (uint_fast64_t pl1State = 0; pl1State < numberOfPlayer1States; ++pl1State){
- if(targetChoices.get(selectedRows[pl1State])){
- inducedTarget.set(pl1State);
- }
- }
- //Find the states from which no target state is reachable.
- probGreater0States = storm::utility::graph::performProbGreater0(inducedA.transpose(), storm::storage::BitVector(numberOfPlayer1States, true), inducedTarget);
- }
-
-
- template <typename ValueType>
- void getInducedEquationSystem(storm::storage::SparseMatrix<ValueType> const& A,
- std::vector<ValueType> const& b,
- storm::storage::TotalScheduler const& scheduler,
- storm::storage::BitVector const& targetChoices,
- storm::storage::SparseMatrix<ValueType>& inducedA,
- std::vector<ValueType>& inducedB,
- storm::storage::BitVector& probGreater0States
- ){
- uint_fast64_t numberOfStates = A.getRowGroupCount();
-
- //Get the matrix A, vector b, and the targetStates induced by the Scheduler
- std::vector<storm::storage::sparse::state_type> selectedRows(numberOfStates);
- for(uint_fast64_t stateIndex = 0; stateIndex < numberOfStates; ++stateIndex){
- selectedRows[stateIndex] = (scheduler.getChoice(stateIndex));
- }
- inducedA = A.selectRowsFromRowGroups(selectedRows, false);
- inducedB = std::vector<ValueType>(numberOfStates);
- storm::utility::vector::selectVectorValues<ValueType>(inducedB, selectedRows, A.getRowGroupIndices(), b);
- storm::storage::BitVector inducedTarget(numberOfStates, false);
- for (uint_fast64_t state = 0; state < numberOfStates; ++state){
- if(targetChoices.get(A.getRowGroupIndices()[state] + scheduler.getChoice(state))){
- inducedTarget.set(state);
- }
- }
- //Find the states from which no target state is reachable.
- probGreater0States = storm::utility::graph::performProbGreater0(inducedA.transpose(), storm::storage::BitVector(numberOfStates, true), inducedTarget);
- }
-
- template<typename ValueType>
- void solveLinearEquationSystem(storm::storage::SparseMatrix<ValueType>const& A,
- std::vector<ValueType>& x,
- std::vector<ValueType> const& b,
- storm::storage::BitVector const& probGreater0States,
- ValueType const& prob0Value,
- ValueType const& precision,
- bool relative
- ){
- //Get the submatrix/subvector A,x, and b and invoke linear equation solver
- storm::storage::SparseMatrix<ValueType> subA = A.getSubmatrix(true, probGreater0States, probGreater0States, true);
- storm::storage::SparseMatrix<ValueType> eqSysA(subA);
- eqSysA.convertToEquationSystem();
- std::vector<ValueType> subX(probGreater0States.getNumberOfSetBits());
- storm::utility::vector::selectVectorValues(subX, probGreater0States, x);
- std::vector<ValueType> subB(probGreater0States.getNumberOfSetBits());
- storm::utility::vector::selectVectorValues(subB, probGreater0States, b);
-
- std::unique_ptr<storm::solver::GmmxxLinearEquationSolver<ValueType>> linEqSysSolver(static_cast<storm::solver::GmmxxLinearEquationSolver<ValueType>*>(storm::solver::GmmxxLinearEquationSolverFactory<ValueType>().create(eqSysA).release()));
- linEqSysSolver->setCachingEnabled(true);
- auto eqSettings = linEqSysSolver->getSettings();
- eqSettings.setRelativeTerminationCriterion(relative);
- eqSettings.setMaximalNumberOfIterations(500);
- linEqSysSolver->setSettings(eqSettings);
- std::size_t iterations = 0;
- std::vector<ValueType> copyX(subX.size());
- ValueType precisionChangeFactor = storm::utility::one<ValueType>();
- do {
- eqSettings.setPrecision(eqSettings.getPrecision() * precisionChangeFactor);
- linEqSysSolver->setSettings(eqSettings);
- if(!linEqSysSolver->solveEquations(subX, subB)){
- // break; //Solver did not converge.. so we have to go on with the current solution.
- }
- subA.multiplyWithVector(subX,copyX);
- storm::utility::vector::addVectors(copyX, subB, copyX); // = Ax + b
- ++iterations;
-
- precisionChangeFactor = storm::utility::convertNumber<ValueType>(0.5);
- } while(!storm::utility::vector::equalModuloPrecision(subX, copyX, precision*0.5, relative) && iterations<60);
-
- STORM_LOG_WARN_COND(iterations<60, "Solving linear equation system did not yield a precise result");
-
- STORM_LOG_DEBUG("Required to increase the precision " << iterations << " times in order to obtain a precise result");
- //fill in the result
- storm::utility::vector::setVectorValues(x, probGreater0States, subX);
- storm::utility::vector::setVectorValues(x, (~probGreater0States), prob0Value);
- }
-
-
- template <typename ValueType>
- bool checkAndFixScheduler(storm::solver::GameSolver<ValueType> const& solver,
- std::vector<ValueType> const& x,
- std::vector<ValueType> const& b,
- storm::storage::TotalScheduler& player1Scheduler,
- storm::storage::TotalScheduler& player2Scheduler,
- storm::storage::BitVector const& targetChoices,
- storm::storage::SparseMatrix<ValueType>& inducedA,
- std::vector<ValueType>& inducedB,
- storm::storage::BitVector& probGreater0States
- ){
- if(probGreater0States.getNumberOfSetBits() == probGreater0States.size()) return true;
-
- bool schedulerChanged = true;
- while(schedulerChanged){
- /*
- * Lets try to fix the issue by doing other choices that are equally good.
- * We change the Scheduler in a state if the following conditions apply:
- * 1. The current choice does not lead to target
- * 2. There is another choice that leads to target
- * 3. The value of that choice is equal to the value of the choice given by the Scheduler
- * Note that the values of the result will not change this way.
- * We do this until the Scheduler does not change anymore
- */
- schedulerChanged = false;
- //Player 1:
- for(uint_fast64_t pl1State=0; pl1State < solver.getPlayer1Matrix().getRowGroupCount(); ++pl1State){
- uint_fast64_t pl1RowGroupIndex = solver.getPlayer1Matrix().getRowGroupIndices()[pl1State];
- //Check 1.: The current choice does not lead to target
- if(!probGreater0States.get(pl1State)){
- //1. Is satisfied. Check 2.: There is another choice that leads to target
- ValueType choiceValue = x[pl1State];
- for(uint_fast64_t otherChoice = 0; otherChoice < solver.getPlayer1Matrix().getRowGroupSize(pl1State); ++otherChoice){
- if(otherChoice == player1Scheduler.getChoice(pl1State)) continue;
- //the otherChoice selects a player2 state in which player2 makes his choice (according to the player2Scheduler).
- uint_fast64_t pl2State = solver.getPlayer1Matrix().getRow(pl1RowGroupIndex + otherChoice).begin()->getColumn();
- uint_fast64_t pl2Row = solver.getPlayer2Matrix().getRowGroupIndices()[pl2State] + player2Scheduler.getChoice(pl2State);
- if(rowLeadsToTarget(pl2Row, solver.getPlayer2Matrix(), targetChoices, probGreater0States)){
- //2. is satisfied. Check 3. The value of that choice is equal to the value of the choice given by the Scheduler
- ValueType otherValue = solver.getPlayer2Matrix().multiplyRowWithVector(pl2Row, x) + b[pl2Row];
- if(storm::utility::vector::equalModuloPrecision(choiceValue, otherValue, solver.getPrecision(), solver.getRelative())){
- //3. is satisfied.
- player1Scheduler.setChoice(pl1State, otherChoice);
- probGreater0States.set(pl1State);
- schedulerChanged = true;
- break; //no need to check other choices
- }
- }
- }
- }
- }
- //update probGreater0States
- probGreater0States = storm::utility::graph::performProbGreater0(inducedA.transpose(), storm::storage::BitVector(probGreater0States.size(), true), probGreater0States);
- //Player 2:
- for(uint_fast64_t pl2State=0; pl2State < solver.getPlayer2Matrix().getRowGroupCount(); ++pl2State){
- uint_fast64_t pl2RowGroupIndex = solver.getPlayer2Matrix().getRowGroupIndices()[pl2State];
- //Check 1.: The current choice does not lead to target
- if(!rowLeadsToTarget(pl2RowGroupIndex + player2Scheduler.getChoice(pl2State), solver.getPlayer2Matrix(), targetChoices, probGreater0States)){
- //1. Is satisfied. Check 2. There is another choice that leads to target
- ValueType choiceValue = solver.getPlayer2Matrix().multiplyRowWithVector(pl2RowGroupIndex + player2Scheduler.getChoice(pl2State), x) + b[pl2RowGroupIndex + player2Scheduler.getChoice(pl2State)];
- for(uint_fast64_t otherChoice = 0; otherChoice < solver.getPlayer2Matrix().getRowGroupSize(pl2State); ++otherChoice){
- if(otherChoice == player2Scheduler.getChoice(pl2State)) continue;
- if(rowLeadsToTarget(pl2RowGroupIndex + otherChoice, solver.getPlayer2Matrix(), targetChoices, probGreater0States)){
- //2. is satisfied. Check 3. The value of that choice is equal to the value of the choice given by the Scheduler
- ValueType otherValue = solver.getPlayer2Matrix().multiplyRowWithVector(pl2RowGroupIndex + otherChoice, x) + b[pl2RowGroupIndex + otherChoice];
- if(storm::utility::vector::equalModuloPrecision(choiceValue, otherValue, solver.getPrecision(), solver.getRelative())){
- //3. is satisfied.
- player2Scheduler.setChoice(pl2State, otherChoice);
- schedulerChanged = true;
- break; //no need to check other choices
- }
- }
- }
- }
- }
-
- //update probGreater0States
- getInducedEquationSystem(solver, b, player1Scheduler, player2Scheduler, targetChoices, inducedA, inducedB, probGreater0States);
- if(probGreater0States.getNumberOfSetBits() == probGreater0States.size()){
- return true;
- }
- }
- //Reaching this point means that the Scheduler does not change anymore and we could not fix it.
- return false;
- }
-
- template <typename ValueType>
- bool checkAndFixScheduler(storm::storage::SparseMatrix<ValueType> const& A,
- std::vector<ValueType> const& x,
- std::vector<ValueType> const& b,
- storm::storage::TotalScheduler& scheduler,
- storm::storage::BitVector const& targetChoices,
- ValueType const& precision, bool relative,
- storm::storage::SparseMatrix<ValueType>& inducedA,
- std::vector<ValueType>& inducedB,
- storm::storage::BitVector& probGreater0States
- ){
- if(probGreater0States.getNumberOfSetBits() == probGreater0States.size()) return true;
-
- bool schedulerChanged = true;
- while(schedulerChanged){
- /*
- * Lets try to fix the issue by doing other choices that are equally good.
- * We change the Scheduler in a state if the following conditions apply:
- * 1. The current choice does not lead to target
- * 2. There is another choice that leads to target
- * 3. The value of that choice is equal to the value of the choice given by the Scheduler
- * Note that the values of the result will not change this way.
- * We do this unil the Scheduler does not change anymore
- */
- schedulerChanged = false;
- for(uint_fast64_t state=0; state < A.getRowGroupCount(); ++state){
- uint_fast64_t rowGroupIndex = A.getRowGroupIndices()[state];
- //Check 1.: The current choice does not lead to target
- if(!probGreater0States.get(state)){
- //1. Is satisfied. Check 2.: There is another choice that leads to target
- ValueType choiceValue = x[state];
- for(uint_fast64_t otherChoice = 0; otherChoice < A.getRowGroupSize(state); ++otherChoice){
- if(otherChoice == scheduler.getChoice(state)) continue;
- if(rowLeadsToTarget(rowGroupIndex + otherChoice, A, targetChoices, probGreater0States)){
- //2. is satisfied. Check 3. The value of that choice is equal to the value of the choice given by the Scheduler
- ValueType otherValue = A.multiplyRowWithVector(rowGroupIndex + otherChoice, x) + b[rowGroupIndex + otherChoice];
- if(storm::utility::vector::equalModuloPrecision(choiceValue, otherValue, precision, !relative)){
- //3. is satisfied.
- scheduler.setChoice(state, otherChoice);
- probGreater0States.set(state);
- schedulerChanged = true;
- break; //no need to check other choices
- }
- }
- }
- }
- }
-
- //update probGreater0States and equation system
- getInducedEquationSystem(A, b, scheduler, targetChoices, inducedA, inducedB, probGreater0States);
- if(probGreater0States.getNumberOfSetBits() == probGreater0States.size()){
- return true;
- }
- }
- //Reaching this point means that the Scheduler does not change anymore and we could not fix it.
- return false;
- }
-
-
- template void solveGame<double>( storm::solver::GameSolver<double>& solver,
- std::vector<double>& x,
- std::vector<double> const& b,
- OptimizationDirection player1Goal,
- OptimizationDirection player2Goal,
- storm::storage::TotalScheduler& player1Scheduler,
- storm::storage::TotalScheduler& player2Scheduler,
- storm::storage::BitVector const& targetChoices,
- double const& prob0Value
- );
-
- template void solveMinMaxLinearEquationSystem<double>( storm::solver::MinMaxLinearEquationSolver<double>& solver,
- storm::storage::SparseMatrix<double> const& A,
- std::vector<double>& x,
- std::vector<double> const& b,
- OptimizationDirection goal,
- storm::storage::TotalScheduler& Scheduler,
- storm::storage::BitVector const& targetChoices,
- double const& prob0Value
- );
-
- template void getInducedEquationSystem<double>(storm::solver::GameSolver<double> const& solver,
- std::vector<double> const& b,
- storm::storage::TotalScheduler const& player1Scheduler,
- storm::storage::TotalScheduler const& player2Scheduler,
- storm::storage::BitVector const& targetChoices,
- storm::storage::SparseMatrix<double>& inducedA,
- std::vector<double>& inducedB,
- storm::storage::BitVector& probGreater0States
- );
-
- template void getInducedEquationSystem<double>(storm::storage::SparseMatrix<double>const& A,
- std::vector<double> const& b,
- storm::storage::TotalScheduler const& scheduler,
- storm::storage::BitVector const& targetChoices,
- storm::storage::SparseMatrix<double>& inducedA,
- std::vector<double>& inducedB,
- storm::storage::BitVector& probGreater0States
- );
-
- template void solveLinearEquationSystem<double>(storm::storage::SparseMatrix<double>const& A,
- std::vector<double>& x,
- std::vector<double> const& b,
- storm::storage::BitVector const& probGreater0States,
- double const& prob0Value,
- double const& precision,
- bool relative
- );
-
- template bool checkAndFixScheduler<double>(storm::solver::GameSolver<double> const& solver,
- std::vector<double> const& x,
- std::vector<double> const& b,
- storm::storage::TotalScheduler& player1Scheduler,
- storm::storage::TotalScheduler& player2Scheduler,
- storm::storage::BitVector const& targetChoices,
- storm::storage::SparseMatrix<double>& inducedA,
- std::vector<double>& inducedB,
- storm::storage::BitVector& probGreater0States
- );
-
- template bool checkAndFixScheduler<double>(storm::storage::SparseMatrix<double> const& A,
- std::vector<double> const& x,
- std::vector<double> const& b,
- storm::storage::TotalScheduler& scheduler,
- storm::storage::BitVector const& targetChoices,
- double const& precision,
- bool relative,
- storm::storage::SparseMatrix<double>& inducedA,
- std::vector<double>& inducedB,
- storm::storage::BitVector& probGreater0States
- );
-
- }
- }
-}
diff --git a/src/storm/utility/policyguessing.h b/src/storm/utility/policyguessing.h
deleted file mode 100644
index 29a2d0ca0..000000000
--- a/src/storm/utility/policyguessing.h
+++ /dev/null
@@ -1,254 +0,0 @@
-/*
- * File: Regions.h
- * Author: Tim Quatmann
- *
- * Created on November 16, 2015,
- *
- * This file provides functions to apply a solver on a nondeterministic model or a two player game.
- * However, schedulers are used to compute an initial guess which will (hopefully) speed up the value iteration techniques.
- */
-
-
-#ifndef STORM_UTILITY_POLICYGUESSING_H
-#define STORM_UTILITY_POLICYGUESSING_H
-
-#include "storm/solver/GameSolver.h"
-#include "storm/solver/MinMaxLinearEquationSolver.h"
-#include "storm/solver/OptimizationDirection.h"
-#include "storm/utility/vector.h"
-#include "storm/storage/BitVector.h"
-#include "storm/storage/sparse/StateType.h"
-#include "storm/storage/SparseMatrix.h"
-#include "storm/storage/TotalScheduler.h"
-
-namespace storm {
- namespace utility{
- namespace policyguessing {
-
- /*!
- * invokes the given game solver.
- *
- * The given schedulers for player 1 and player 2 will serve as initial guess.
- * A linear equation system defined by the induced Matrix A and vector b is solved before
- * solving the actual game.
- * Note that, depending on the schedulers, the qualitative properties of the graph defined by A
- * might be different to the original graph of the game.
- * To ensure a unique solution, we need to filter out the "prob0"-states.
- * To identify these states and set the result for them correctly, it is necessary to know whether rewards or probabilities are to be computed
- *
- * @param solver the solver to be invoked
- * @param player1Goal Sets whether player 1 wants to minimize or maximize.
- * @param player2Goal Sets whether player 2 wants to minimize or maximize.
- * @param x The initial guess of the solution.
- * @param b The vector to add after matrix-vector multiplication.
- * @param player1Scheduler A Scheduler that selects rows in every rowgroup of player1. This will be used as an initial guess
- * @param player2Scheduler A Scheduler that selects rows in every rowgroup of player2. This will be used as an initial guess
- * @param targetChoices marks the choices in the player2 matrix that have a positive probability to lead to a target state
- * @param prob0Value the value that, after Scheduler instantiation, is assigned to the states that have probability zero to reach a target
- * @return The solution vector in the form of the vector x as well as the two schedulers.
- */
- template<typename ValueType>
- void solveGame( storm::solver::GameSolver<ValueType>& solver,
- std::vector<ValueType>& x,
- std::vector<ValueType> const& b,
- OptimizationDirection player1Goal,
- OptimizationDirection player2Goal,
- storm::storage::TotalScheduler& player1Scheduler,
- storm::storage::TotalScheduler& player2Scheduler,
- storm::storage::BitVector const& targetChoices,
- ValueType const& prob0Value
- );
-
- /*!
- * invokes the given MinMaxLinearEquationSolver.
- *
- * The given Scheduler will serve as an initial guess.
- * A linear equation system defined by the induced Matrix A and vector b is solved before
- * solving the actual MinMax equation system.
- * Note that, depending on the Scheduler, the qualitative properties of the graph defined by A
- * might be different to the original graph.
- * To ensure a unique solution, we need to filter out the "prob0"-states.
- * To identify these states and set the result for them correctly, it is necessary to know whether rewards or probabilities are to be computed
- *
- * @param solver the solver that contains the matrix
- * @param A The matrix itself
- * @param x The initial guess of the solution.
- * @param b The vector to add after matrix-vector multiplication.
- * @param goal Sets whether we want to minimize or maximize.
- * @param Scheduler A Scheduler that selects rows in every rowgroup.
- * @param targetChoices marks the rows in the matrix that have a positive probability to lead to a target state
- * @param prob0Value the value that is assigned to the states that have probability zero to reach a target
- * @return The solution vector in the form of the vector x.
- */
- template<typename ValueType>
- void solveMinMaxLinearEquationSystem( storm::solver::MinMaxLinearEquationSolver<ValueType>& solver,
- storm::storage::SparseMatrix<ValueType> const& A,
- std::vector<ValueType>& x,
- std::vector<ValueType> const& b,
- OptimizationDirection goal,
- storm::storage::TotalScheduler& Scheduler,
- storm::storage::BitVector const& targetChoices,
- ValueType const& prob0Value
- );
-
- /*!
- * Constructs the equation system defined by the matrix inducedA and vector inducedB that result from applying
- * the given schedulers to the matrices of the two players and the given b.
- *
- * Note that, depending on the schedulers, the qualitative properties of the graph defined by inducedA
- * might be different to the original graph.
- *
- * @param solver the solver that contains the two player matrices
- * @param b The vector in which to select the entries of the right hand side
- * @param player1Scheduler A Scheduler that selects rows in every rowgroup of player1.
- * @param player2Scheduler A Scheduler that selects rows in every rowgroup of player2.
- * @param targetChoices marks the choices in the player2 matrix that have a positive probability to lead to a target state
- * @param inducedA the Matrix for the resulting equation system
- * @param inducedB the Vector for the resulting equation system
- * @param probGreater0States marks the states which have a positive probability to lead to a target state
- * @return Induced A, b and targets
- */
- template<typename ValueType>
- void getInducedEquationSystem(storm::solver::GameSolver<ValueType> const& solver,
- std::vector<ValueType> const& b,
- storm::storage::TotalScheduler const& player1Scheduler,
- storm::storage::TotalScheduler const& player2Scheduler,
- storm::storage::BitVector const& targetChoices,
- storm::storage::SparseMatrix<ValueType>& inducedA,
- std::vector<ValueType>& inducedB,
- storm::storage::BitVector& probGreater0States
- );
-
- /*!
- * Constructs the equation system defined by the matrix inducedA and vector inducedB that result from applying
- * the given Scheduler to the matrix from the given solver and the given b.
- *
- * Note that, depending on the schedulers, the qualitative properties of the graph defined by inducedA
- * might be different to the original graph.
- *
- * @param A the matrix
- * @param b The vector in which to select the entries of the right hand side
- * @param Scheduler A Scheduler that selects rows in every rowgroup.
- * @param targetChoices marks the choices in the player2 matrix that have a positive probability to lead to a target state
- * @param inducedA the Matrix for the resulting equation system
- * @param inducedB the Vector for the resulting equation system
- * @param probGreater0States marks the states which have a positive probability to lead to a target state
- * @return Induced A, b and targets
- */
- template<typename ValueType>
- void getInducedEquationSystem(storm::storage::SparseMatrix<ValueType> const& A,
- std::vector<ValueType> const& b,
- storm::storage::TotalScheduler const& scheduler,
- storm::storage::BitVector const& targetChoices,
- storm::storage::SparseMatrix<ValueType>& inducedA,
- std::vector<ValueType>& inducedB,
- storm::storage::BitVector& probGreater0States
- );
-
- /*!
- * Solves the given equation system.
- *
- * It is not assumed that qualitative properties of the Graph defined by A have been checked, yet.
- * However, actual target states are already filtered out.
- * To ensure a unique solution, we also need to filter out the "prob0"-states.
- *
- * If the result does not satisfy "Ax+b = x (modulo precision)", the solver is executed
- * again with increased precision.
- *
- * @param A the matrix of the equation system
- * @param x The initial guess of the solution.
- * @param b The vector of the equation system
- * @param targetChoices marks the rows in the matrix that have a positive probability to lead to a target state
- * @param prob0Value the value that is assigned to the states that have probability zero to reach a target
- * @param const& precision The precision to be used by the solver
- * @param relative sets whether to consider relative errors
- * @return The solution vector in the form of the vector x.
- */
- template<typename ValueType>
- void solveLinearEquationSystem(storm::storage::SparseMatrix<ValueType>const& A,
- std::vector<ValueType>& x,
- std::vector<ValueType> const& b,
- storm::storage::BitVector const& probGreater0States,
- ValueType const& prob0Value,
- ValueType const& precision,
- bool relative
- );
-
- /*!
- * Checks if the given schedulers make choices that lead to states from which no target state is reachable ("prob0"-states).
- * This can happen when value iteration is applied and there are multiple choices with the same value
- * (e.g. a state that allows to chose a selfloop with probability one)
- *
- * If the schedulers are changed, they are updated accordingly (as well as the given inducedA, inducedB and probGreater0States)
- *
- * @param solver the solver that contains the two player matrices
- * @param x the solution vector (the result from value iteration)
- * @param b The vector in which to select the entries of the right hand side
- * @param player1Scheduler A Scheduler that selects rows in every rowgroup of player1.
- * @param player2Scheduler A Scheduler that selects rows in every rowgroup of player2.
- * @param targetChoices marks the choices in the player2 matrix that have a positive probability to lead to a target state
- * @param inducedA the Matrix for the equation system
- * @param inducedB the Vector for the equation system
- * @param probGreater0States marks the states which have a positive probability to lead to a target state
- * @return true iff there are no more prob0-states. Also changes the given schedulers accordingly
- */
- template<typename ValueType>
- bool checkAndFixScheduler(storm::solver::GameSolver<ValueType> const& solver,
- std::vector<ValueType> const& x,
- std::vector<ValueType> const& b,
- storm::storage::TotalScheduler& player1Scheduler,
- storm::storage::TotalScheduler& player2Scheduler,
- storm::storage::BitVector const& targetChoices,
- storm::storage::SparseMatrix<ValueType>& inducedA,
- std::vector<ValueType>& inducedB,
- storm::storage::BitVector& probGreater0States
- );
-
- /*!
- * Checks if the given schedulers make choices that lead to states from which no target state is reachable ("prob0"-states).
- * This can happen when value iteration is applied and there are multiple choices with the same value
- * (e.g. a state that allows to chose a selfloop with probability one)
- *
- * If the schedulers are changed, they are updated accordingly (as well as the given inducedA, inducedB and probGreater0States)
- *
- * @param A the matrix
- * @param x the solution vector (the result from value iteration)
- * @param b The vector in which to select the entries of the right hand side
- * @param Scheduler A Scheduler that selects rows in every rowgroup.
- * @param targetChoices marks the choices in the player2 matrix that have a positive probability to lead to a target state
- * @param inducedA the Matrix for the equation system
- * @param probGreater0States marks the states which have a positive probability to lead to a target state
- * @return true iff there are no more prob0-states. Also changes the given schedulers accordingly
- */
- template<typename ValueType>
- bool checkAndFixScheduler(storm::storage::SparseMatrix<ValueType> const& A,
- std::vector<ValueType> const& x,
- std::vector<ValueType> const& b,
- storm::storage::TotalScheduler& Scheduler,
- storm::storage::BitVector const& targetChoices,
- ValueType const& precision,
- bool relative,
- storm::storage::SparseMatrix<ValueType>& inducedA,
- std::vector<ValueType>& inducedB,
- storm::storage::BitVector& probGreater0States
- );
-
- //little helper function
- template<typename ValueType>
- bool rowLeadsToTarget(uint_fast64_t row,
- storm::storage::SparseMatrix<ValueType> const& matrix,
- storm::storage::BitVector const& targetChoices,
- storm::storage::BitVector const& probGreater0States){
- if(targetChoices.get(row)) return true;
- for(auto const& successor : matrix.getRow(row)){
- if(probGreater0States.get(successor.getColumn())) return true;
- }
- return false;
- }
- }
- }
-}
-
-
-#endif /* STORM_UTILITY_REGIONS_H */
-