sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

removed obsolete policy guessing

tempestpy_adaptions
TimQu 8 years ago
parent
14e44e0165
commit
3686c42965
2 changed files with 0 additions and 678 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 424
      src/storm/utility/policyguessing.cpp
  2. 254
      src/storm/utility/policyguessing.h

424
src/storm/utility/policyguessing.cpp
View File

@ -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
);
}
}
}

254
src/storm/utility/policyguessing.h
View File

@ -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 */
Write Preview
Loading…
Cancel
Save