@ -84,45 +84,38 @@ namespace storm {
}
template < typename ValueType >
void StandardMinMaxLinearEquationSolver < ValueType > : : solveEquations ( OptimizationDirection dir , std : : vector < ValueType > & x , std : : vector < ValueType > const & b , std : : vector < ValueType > * multiplyResult , std : : vector < ValueType > * newX ) const {
void StandardMinMaxLinearEquationSolver < ValueType > : : solveEquations ( OptimizationDirection dir , std : : vector < ValueType > & x , std : : vector < ValueType > const & b ) const {
switch ( this - > getSettings ( ) . getSolutionMethod ( ) ) {
case StandardMinMaxLinearEquationSolverSettings < ValueType > : : SolutionMethod : : ValueIteration : solveEquationsValueIteration ( dir , x , b , multiplyResult , newX ) ; break ;
case StandardMinMaxLinearEquationSolverSettings < ValueType > : : SolutionMethod : : PolicyIteration : solveEquationsPolicyIteration ( dir , x , b , multiplyResult , newX ) ; break ;
case StandardMinMaxLinearEquationSolverSettings < ValueType > : : SolutionMethod : : ValueIteration : solveEquationsValueIteration ( dir , x , b ) ; break ;
case StandardMinMaxLinearEquationSolverSettings < ValueType > : : SolutionMethod : : PolicyIteration : solveEquationsPolicyIteration ( dir , x , b ) ; break ;
}
}
template < typename ValueType >
void StandardMinMaxLinearEquationSolver < ValueType > : : solveEquationsPolicyIteration ( OptimizationDirection dir , std : : vector < ValueType > & x , std : : vector < ValueType > const & b , std : : vector < ValueType > * multiplyResult , std : : vector < ValueType > * newX ) const {
// Create scratch memory if none was provided.
bool multiplyResultMemoryProvided = multiplyResult ! = nullptr ;
if ( multiplyResult = = nullptr ) {
multiplyResult = new std : : vector < ValueType > ( this - > A . getRowCount ( ) ) ;
}
void StandardMinMaxLinearEquationSolver < ValueType > : : solveEquationsPolicyIteration ( OptimizationDirection dir , std : : vector < ValueType > & x , std : : vector < ValueType > const & b ) const {
// Create the initial scheduler.
std : : vector < storm : : storage : : sparse : : state_type > scheduler ( this - > A . getRowGroupCount ( ) ) ;
// Create a vector for storing the right-hand side of the inner equation system.
std : : vector < ValueType > subB ( this - > A . getRowGroupCount ( ) ) ;
// Create a vector that the inner equation solver can use as scratch memory.
std : : vector < ValueType > deterministicMultiplyResult ( this - > A . getRowGroupCount ( ) ) ;
// Resolve the nondeterminism according to the current scheduler.
storm : : storage : : SparseMatrix < ValueType > submatrix = this - > A . selectRowsFromRowGroups ( scheduler , true ) ;
submatrix . convertToEquationSystem ( ) ;
storm : : utility : : vector : : selectVectorValues < ValueType > ( subB , scheduler , this - > A . getRowGroupIndices ( ) , b ) ;
// Create a solver that we will use throughout the procedure. We will modify the matrix in each iteration.
auto solver = linearEquationSolverFactory - > create ( std : : move ( submatrix ) ) ;
solver - > allocateAuxMemory ( LinearEquationSolverOperation : : SolveEquations ) ;
Status status = Status : : InProgress ;
uint64_t iterations = 0 ;
do {
// Resolve the nondeterminism according to the current scheduler.
storm : : storage : : SparseMatrix < ValueType > submatrix = this - > A . selectRowsFromRowGroups ( scheduler , true ) ;
submatrix . convertToEquationSystem ( ) ;
storm : : utility : : vector : : selectVectorValues < ValueType > ( subB , scheduler , this - > A . getRowGroupIndices ( ) , b ) ;
// Solve the equation system for the 'DTMC'.
// FIXME: we need to remove the 0- and 1- states to make the solution unique.
// HOWEVER: if we start with a valid scheduler, then we will never get an illegal one, because staying
// within illegal MECs will never strictly improve the value. Is this true?
auto solver = linearEquationSolverFactory - > create ( std : : move ( submatrix ) ) ;
solver - > solveEquations ( x , subB , & deterministicMultiplyResult ) ;
solver - > solveEquations ( x , subB ) ;
// Go through the multiplication result and see whether we can improve any of the choices.
bool schedulerImproved = false ;
@ -151,6 +144,12 @@ namespace storm {
// If the scheduler did not improve, we are done.
if ( ! schedulerImproved ) {
status = Status : : Converged ;
} else {
// Update the scheduler and the solver.
submatrix = this - > A . selectRowsFromRowGroups ( scheduler , true ) ;
submatrix . convertToEquationSystem ( ) ;
storm : : utility : : vector : : selectVectorValues < ValueType > ( subB , scheduler , this - > A . getRowGroupIndices ( ) , b ) ;
solver - > setMatrix ( std : : move ( submatrix ) ) ;
}
// Update environment variables.
@ -164,10 +163,6 @@ namespace storm {
if ( this - > isTrackSchedulerSet ( ) ) {
this - > scheduler = std : : make_unique < storm : : storage : : TotalScheduler > ( std : : move ( scheduler ) ) ;
}
if ( ! multiplyResultMemoryProvided ) {
delete multiplyResult ;
}
}
template < typename ValueType >
@ -186,22 +181,15 @@ namespace storm {
}
template < typename ValueType >
void StandardMinMaxLinearEquationSolver < ValueType > : : solveEquationsValueIteration ( OptimizationDirection dir , std : : vector < ValueType > & x , std : : vector < ValueType > const & b , std : : vector < ValueType > * multiplyResult , std : : vector < ValueType > * newX ) const {
void StandardMinMaxLinearEquationSolver < ValueType > : : solveEquationsValueIteration ( OptimizationDirection dir , std : : vector < ValueType > & x , std : : vector < ValueType > const & b ) const {
std : : unique_ptr < storm : : solver : : LinearEquationSolver < ValueType > > solver = linearEquationSolverFactory - > create ( A ) ;
// Create scratch memory if none was provided.
bool multiplyResultMemoryProvided = multiplyResult ! = nullptr ;
if ( multiplyResult = = nullptr ) {
multiplyResult = new std : : vector < ValueType > ( this - > A . getRowCount ( ) ) ;
}
std : : vector < ValueType > * currentX = & x ;
bool xMemoryProvided = newX ! = nullptr ;
if ( newX = = nullptr ) {
newX = new std : : vector < ValueType > ( x . size ( ) ) ;
bool allocatedAuxMemory = ! this - > hasAuxMemory ( MinMaxLinearEquationSolverOperation : : SolveEquations ) ;
if ( allocatedAuxMemory ) {
this - > allocateAuxMemory ( MinMaxLinearEquationSolverOperation : : SolveEquations ) ;
}
// Keep track of which of the vectors for x is the auxiliary copy.
std : : vector < ValueType > * copyX = newX ;
std : : vector < ValueType > * currentX = & x ;
std : : vector < ValueType > * newX = auxiliarySolvingVectorMemory . get ( ) ;
// Proceed with the iterations as long as the method did not converge or reach the maximum number of iterations.
uint64_t iterations = 0 ;
@ -209,10 +197,10 @@ namespace storm {
Status status = Status : : InProgress ;
while ( status = = Status : : InProgress ) {
// Compute x' = A*x + b.
solver - > multiply ( * currentX , * multiplyResult , & b ) ;
solver - > multiply ( * currentX , & b , * auxiliarySolvingMultiplyMemory ) ;
// Reduce the vector x' by applying min/max for all non-deterministic choices.
storm : : utility : : vector : : reduceVectorMinOrMax ( dir , * multiplyResult , * newX , this - > A . getRowGroupIndices ( ) ) ;
storm : : utility : : vector : : reduceVectorMinOrMax ( dir , * auxiliarySolvingMultiplyMemory , * newX , this - > A . getRowGroupIndices ( ) ) ;
// Determine whether the method converged.
if ( storm : : utility : : vector : : equalModuloPrecision < ValueType > ( * currentX , * newX , this - > getSettings ( ) . getPrecision ( ) , this - > getSettings ( ) . getRelativeTerminationCriterion ( ) ) ) {
@ -229,10 +217,10 @@ namespace storm {
// If we performed an odd number of iterations, we need to swap the x and currentX, because the newest result
// is currently stored in currentX, but x is the output vector.
if ( currentX = = copyX ) {
if ( currentX = = auxiliarySolvingVectorMemory . get ( ) ) {
std : : swap ( x , * currentX ) ;
}
// If requested, we store the scheduler for retrieval.
if ( this - > isTrackSchedulerSet ( ) ) {
if ( iterations = = 0 ) { //may happen due to custom termination condition. Then we need to compute x'= A*x+b
@ -243,36 +231,33 @@ namespace storm {
storm : : utility : : vector : : reduceVectorMinOrMax ( dir , * multiplyResult , x , this - > A . getRowGroupIndices ( ) , & choices ) ;
this - > scheduler = std : : make_unique < storm : : storage : : TotalScheduler > ( std : : move ( choices ) ) ;
}
// Dispose of allocated scratch memory.
if ( ! xMemoryProvided ) {
delete copyX ;
}
if ( ! multiplyResultMemoryProvided ) {
delete multiplyResult ;
// If we allocated auxiliary memory, we need to dispose of it now.
if ( allocatedAuxMemory ) {
this - > deallocateAuxMemory ( MinMaxLinearEquationSolverOperation : : SolveEquations ) ;
}
}
template < typename ValueType >
void StandardMinMaxLinearEquationSolver < ValueType > : : multiply ( OptimizationDirection dir , std : : vector < ValueType > & x , std : : vector < ValueType > * b , uint_fast64_t n , std : : vector < ValueType > * multiplyResult ) const {
std : : unique_ptr < storm : : solver : : LinearEquationSolver < ValueType > > solver = linearEquationSolverFactory - > create ( A ) ;
// If scratch memory was not provided, we create it.
bool multiplyResultMemoryProvided = multiplyResult ! = nullptr ;
if ( ! multiplyResult ) {
multiplyResult = new std : : vector < ValueType > ( this - > A . getRowCount ( ) ) ;
void StandardMinMaxLinearEquationSolver < ValueType > : : repeatedMultiply ( OptimizationDirection dir , std : : vector < ValueType > & x , std : : vector < ValueType > * b , uint_fast64_t n ) const {
bool allocatedAuxMemory = ! this - > hasAuxMemory ( MinMaxLinearEquationSolverOperation : : MultiplyRepeatedly ) ;
if ( allocatedAuxMemory ) {
this - > allocateAuxMemory ( MinMaxLinearEquationSolverOperation : : MultiplyRepeatedly ) ;
}
std : : unique_ptr < storm : : solver : : LinearEquationSolver < ValueType > > solver = linearEquationSolverFactory - > create ( A ) ;
for ( uint64_t i = 0 ; i < n ; + + i ) {
solver - > multiply ( x , * multiplyResult , b ) ;
solver - > multiply ( x , b , * auxiliaryRepeatedMultiplyMemory ) ;
// Reduce the vector x' by applying min/max for all non-deterministic choices as given by the topmost
// element of the min/max operator stack.
storm : : utility : : vector : : reduceVectorMinOrMax ( dir , * multiplyResult , x , this - > A . getRowGroupIndices ( ) ) ;
storm : : utility : : vector : : reduceVectorMinOrMax ( dir , * auxiliaryRepeatedMultiplyMemory , x , this - > A . getRowGroupIndices ( ) ) ;
}
if ( ! multiplyResultMemoryProvided ) {
delete multiplyResult ;
// If we allocated auxiliary memory, we need to dispose of it now.
if ( allocatedAuxMemory ) {
this - > deallocateAuxMemory ( MinMaxLinearEquationSolverOperation : : MultiplyRepeatedly ) ;
}
}
@ -309,6 +294,73 @@ namespace storm {
return settings ;
}
template < typename ValueType >
bool StandardMinMaxLinearEquationSolver < ValueType > : : allocateAuxMemory ( MinMaxLinearEquationSolverOperation operation ) const {
bool result = false ;
if ( operation = = MinMaxLinearEquationSolverOperation : : SolveEquations ) {
if ( this - > getSettings ( ) . getSolutionMethod ( ) = = StandardMinMaxLinearEquationSolverSettings < ValueType > : : SolutionMethod : : ValueIteration ) {
if ( ! auxiliarySolvingMultiplyMemory ) {
result = true ;
auxiliarySolvingMultiplyMemory = std : : make_unique < std : : vector < ValueType > > ( this - > A . getRowCount ( ) ) ;
}
if ( ! auxiliarySolvingVectorMemory ) {
result = true ;
auxiliarySolvingVectorMemory = std : : make_unique < std : : vector < ValueType > > ( this - > A . getRowGroupCount ( ) ) ;
}
} else if ( this - > getSettings ( ) . getSolutionMethod ( ) = = StandardMinMaxLinearEquationSolverSettings < ValueType > : : SolutionMethod : : PolicyIteration ) {
// Nothing to do in this case.
} else {
STORM_LOG_ASSERT ( false , " Cannot allocate aux storage for this method. " ) ;
}
} else {
if ( ! auxiliaryRepeatedMultiplyMemory ) {
result = true ;
auxiliaryRepeatedMultiplyMemory = std : : make_unique < std : : vector < ValueType > > ( this - > A . getRowCount ( ) ) ;
}
}
return result ;
}
template < typename ValueType >
bool StandardMinMaxLinearEquationSolver < ValueType > : : deallocateAuxMemory ( MinMaxLinearEquationSolverOperation operation ) const {
bool result = false ;
if ( operation = = MinMaxLinearEquationSolverOperation : : SolveEquations ) {
if ( this - > getSettings ( ) . getSolutionMethod ( ) = = StandardMinMaxLinearEquationSolverSettings < ValueType > : : SolutionMethod : : ValueIteration ) {
if ( auxiliarySolvingMultiplyMemory ) {
result = true ;
auxiliarySolvingMultiplyMemory . reset ( ) ;
}
if ( auxiliarySolvingVectorMemory ) {
result = true ;
auxiliarySolvingVectorMemory . reset ( ) ;
}
} else if ( this - > getSettings ( ) . getSolutionMethod ( ) = = StandardMinMaxLinearEquationSolverSettings < ValueType > : : SolutionMethod : : PolicyIteration ) {
// Nothing to do in this case.
} else {
STORM_LOG_ASSERT ( false , " Cannot allocate aux storage for this method. " ) ;
}
} else {
if ( auxiliaryRepeatedMultiplyMemory ) {
result = true ;
auxiliaryRepeatedMultiplyMemory . reset ( ) ;
}
}
return result ;
}
template < typename ValueType >
bool StandardMinMaxLinearEquationSolver < ValueType > : : hasAuxMemory ( MinMaxLinearEquationSolverOperation operation ) const {
if ( operation = = MinMaxLinearEquationSolverOperation : : SolveEquations ) {
if ( this - > getSettings ( ) . getSolutionMethod ( ) = = StandardMinMaxLinearEquationSolverSettings < ValueType > : : SolutionMethod : : ValueIteration ) {
return auxiliarySolvingMultiplyMemory & & auxiliarySolvingVectorMemory ;
} else {
return false ;
}
} else {
return static_cast < bool > ( auxiliaryRepeatedMultiplyMemory ) ;
}
}
template < typename ValueType >
StandardMinMaxLinearEquationSolverFactory < ValueType > : : StandardMinMaxLinearEquationSolverFactory ( bool trackScheduler ) : MinMaxLinearEquationSolverFactory < ValueType > ( trackScheduler ) , linearEquationSolverFactory ( nullptr ) {
// Intentionally left empty.
TimQu
9 years ago