@ -8,11 +8,14 @@
# ifndef GMMXXDTMCPRCTLMODELCHECKER_H_
# define GMMXXDTMCPRCTLMODELCHECKER_H_
# include "src/utility/vector.h"
# include <cmath>
# include "src/models/Dtmc.h"
# include "src/modelChecker/DtmcPrctlModelChecker.h"
# include "src/solver/GraphAnalyzer.h"
# include "src/utility/vector.h"
# include "src/utility/settings.h"
# include "gmm/gmm_matrix.h"
# include "gmm/gmm_iter_solvers.h"
@ -46,24 +49,23 @@ public:
mrmc : : storage : : SquareSparseMatrix < Type > tmpMatrix ( * this - > getModel ( ) . getTransitionProbabilityMatrix ( ) ) ;
/ / Make all rows absorbing that violate both sub - formulas or satisfy the second sub - formula .
tmpMatrix . makeRowsAbsorbing ( ( ~ * leftStates & * rightStates ) | * rightStates ) ;
tmpMatrix . makeRowsAbsorbing ( ~ ( * leftStates & * rightStates ) | * rightStates ) ;
/ / Transform the transition probability matrix to the gmm + + format to use its arithmetic .
gmm : : csr_matrix < doubl e> * gmmxxMatrix = tmpMatrix . toGMMXXSparseMatrix ( ) ;
gmm : : csr_matrix < Typ e> * gmmxxMatrix = tmpMatrix . toGMMXXSparseMatrix ( ) ;
/ / Create the vector with which to multiply .
std : : vector < Type > * result = new std : : vector < Type > ( this - > getModel ( ) . getNumberOfStates ( ) ) ;
mrmc : : utility : : setVectorValues ( result , * rightStates , static_cast < doubl e> ( 1.0 ) ) ;
mrmc : : utility : : setVectorValues ( result , * rightStates , static_cast < Typ e> ( 1.0 ) ) ;
/ / Now perform matrix - vector multiplication as long as we meet the bound of the formula .
for ( uint_fast64_t i = 0 ; i < formula . getBound ( ) ; + + i ) {
gmm : : mult ( * gmmxxMatrix , * result , * result ) ;
}
/ / Delete intermediate results .
/ / Delete intermediate results and return result .
delete leftStates ;
delete rightStates ;
return result ;
}
@ -72,19 +74,19 @@ public:
mrmc : : storage : : BitVector * nextStates = this - > checkStateFormula ( formula . getChild ( ) ) ;
/ / Transform the transition probability matrix to the gmm + + format to use its arithmetic .
gmm : : csr_matrix < doubl e> * gmmxxMatrix = this - > getModel ( ) . getTransitionProbabilityMatrix ( ) - > toGMMXXSparseMatrix ( ) ;
gmm : : csr_matrix < Typ e> * gmmxxMatrix = this - > getModel ( ) . getTransitionProbabilityMatrix ( ) - > toGMMXXSparseMatrix ( ) ;
/ / Create the vector with which to multiply and initialize it correctly .
std : : vector < Type > x ( this - > getModel ( ) . getNumberOfStates ( ) ) ;
mrmc : : utility : : setVectorValues ( & x , * nextStates , static_cast < doubl e> ( 1.0 ) ) ;
mrmc : : utility : : setVectorValues ( & x , * nextStates , static_cast < Typ e> ( 1.0 ) ) ;
/ / Delete not needed next states bit vector .
/ / Delete obsolete sub - result .
delete nextStates ;
/ / Create resulting vector .
std : : vector < Type > * result = new std : : vector < Type > ( this - > getModel ( ) . getNumberOfStates ( ) ) ;
/ / Perform the actual computation .
/ / Perform the actual computation , namely matrix - vector multiplication .
gmm : : mult ( * gmmxxMatrix , x , * result ) ;
/ / Delete temporary matrix and return result .
@ -101,9 +103,10 @@ public:
/ / all states that have probability 0 and 1 of satisfying the until - formula .
mrmc : : storage : : BitVector notExistsPhiUntilPsiStates ( this - > getModel ( ) . getNumberOfStates ( ) ) ;
mrmc : : storage : : BitVector alwaysPhiUntilPsiStates ( this - > getModel ( ) . getNumberOfStates ( ) ) ;
mrmc : : solver : : GraphAnalyzer : : getPhiUntilPsiStates < double > ( this - > getModel ( ) , * leftStates , * rightStates , & notExistsPhiUntilPsiStates , & alwaysPhiUntilPsiStates ) ;
mrmc : : solver : : GraphAnalyzer : : getPhiUntilPsiStates ( this - > getModel ( ) , * leftStates , * rightStates , & notExistsPhiUntilPsiStates , & alwaysPhiUntilPsiStates ) ;
notExistsPhiUntilPsiStates . complement ( ) ;
/ / Delete sub - results that are obsolete now .
delete leftStates ;
delete rightStates ;
@ -118,13 +121,14 @@ public:
/ / Only try to solve system if there are states for which the probability is unknown .
if ( maybeStates . getNumberOfSetBits ( ) > 0 ) {
/ / Now we can eliminate the rows and columns from the original transition probability matrix .
mrmc : : storage : : SquareSparseMatrix < doubl e> * submatrix = this - > getModel ( ) . getTransitionProbabilityMatrix ( ) - > getSubmatrix ( maybeStates ) ;
/ / Converting the matrix to the form needed for the equation system . That is , we go from
/ / x = A * x + b to ( I - A ) x = b .
mrmc : : storage : : SquareSparseMatrix < Typ e> * submatrix = this - > getModel ( ) . getTransitionProbabilityMatrix ( ) - > getSubmatrix ( maybeStates ) ;
/ / Converting the matrix from the fixpoint notation to the form needed for the equation
/ / system . That is , we go from x = A * x + b to ( I - A ) x = b .
submatrix - > convertToEquationSystem ( ) ;
/ / Transform the submatrix to the gmm + + format to use its solvers .
gmm : : csr_matrix < double > * gmmxxMatrix = submatrix - > toGMMXXSparseMatrix ( ) ;
gmm : : csr_matrix < Type > * gmmxxMatrix = submatrix - > toGMMXXSparseMatrix ( ) ;
delete submatrix ;
/ / Initialize the x vector with 0.5 for each element . This is the initial guess for
/ / the iterative solvers . It should be safe as for all ' maybe ' states we know that the
@ -133,19 +137,58 @@ public:
/ / 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 .
std : : vector < double > b ( maybeStates . getNumberOfSetBits ( ) ) ;
this - > getModel ( ) . getTransitionProbabilityMatrix ( ) - > getConstrainedRowCountVector ( maybeStates , alwaysPhiUntilPsiStates , & x ) ;
std : : vector < Type > b ( maybeStates . getNumberOfSetBits ( ) ) ;
this - > getModel ( ) . getTransitionProbabilityMatrix ( ) - > getConstrainedRowCountVector ( maybeStates , alwaysPhiUntilPsiStates , & b ) ;
/ / Get the settings object to customize linear solving .
mrmc : : settings : : Settings * s = mrmc : : settings : : instance ( ) ;
/ / Set up the precondition of the iterative solver .
gmm : : ilu_precond < gmm : : csr_matrix < double > > P ( * gmmxxMatrix ) ;
/ / Prepare an iteration object that determines the accuracy , maximum number of iterations
/ / and the like .
gmm : : iteration iter ( 0.000001 ) ;
gmm : : iteration iter ( s - > get < double > ( " precision " ) , 0 , s - > get < unsigned > ( " lemaxiter " ) ) ;
/ / Now do the actual solving .
LOG4CPLUS_INFO ( logger , " Starting iterative solver. " ) ;
gmm : : bicgstab ( * gmmxxMatrix , x , b , P , iter ) ;
LOG4CPLUS_INFO ( logger , " Iterative solver converged. " ) ;
const std : : string & precond = s - > getString ( " precond " ) ;
if ( s - > getString ( " lemethod " ) . compare ( " bicgstab " ) = = 0 ) {
if ( precond . compare ( " ilu " ) ) {
gmm : : bicgstab ( * gmmxxMatrix , x , b , gmm : : ilu_precond < gmm : : csr_matrix < Type > > ( * gmmxxMatrix ) , iter ) ;
} else if ( precond . compare ( " diagonal " ) = = 0 ) {
gmm : : bicgstab ( * gmmxxMatrix , x , b , gmm : : diagonal_precond < gmm : : csr_matrix < Type > > ( * gmmxxMatrix ) , iter ) ;
} else if ( precond . compare ( " ildlt " ) = = 0 ) {
gmm : : bicgstab ( * gmmxxMatrix , x , b , gmm : : ildlt_precond < gmm : : csr_matrix < Type > > ( * gmmxxMatrix ) , iter ) ;
} else if ( precond . compare ( " none " ) = = 0 ) {
gmm : : bicgstab ( * gmmxxMatrix , x , b , gmm : : identity_matrix ( ) , iter ) ;
}
/ / FIXME : gmres has been disabled , because it triggers gmm + + compilation errors
/* } else if (s->getString("lemethod").compare("gmres") == 0) {
if ( precond . compare ( " ilu " ) ) {
gmm : : gmres ( * gmmxxMatrix , x , b , gmm : : ilu_precond < gmm : : csr_matrix < Type > > ( * gmmxxMatrix ) , s - > get < unsigned > ( " restart " ) , iter ) ;
} else if ( precond . compare ( " diagonal " ) = = 0 ) {
gmm : : gmres ( * gmmxxMatrix , x , b , gmm : : diagonal_precond < gmm : : csr_matrix < Type > > ( * gmmxxMatrix ) , s - > get < unsigned > ( " restart " ) , iter ) ;
} else if ( precond . compare ( " ildlt " ) = = 0 ) {
gmm : : gmres ( * gmmxxMatrix , x , b , gmm : : ildlt_precond < gmm : : csr_matrix < Type > > ( * gmmxxMatrix ) , s - > get < unsigned > ( " restart " ) , iter ) ;
} else if ( precond . compare ( " none " ) = = 0 ) {
gmm : : gmres ( * gmmxxMatrix , x , b , gmm : : identity_matrix ( ) , s - > get < unsigned > ( " restart " ) , iter ) ;
} */
} else if ( s - > getString ( " lemethod " ) . compare ( " qmr " ) = = 0 ) {
if ( precond . compare ( " ilu " ) ) {
gmm : : qmr ( * gmmxxMatrix , x , b , gmm : : ilu_precond < gmm : : csr_matrix < Type > > ( * gmmxxMatrix ) , iter ) ;
} else if ( precond . compare ( " diagonal " ) = = 0 ) {
gmm : : qmr ( * gmmxxMatrix , x , b , gmm : : diagonal_precond < gmm : : csr_matrix < Type > > ( * gmmxxMatrix ) , iter ) ;
} else if ( precond . compare ( " ildlt " ) = = 0 ) {
gmm : : qmr ( * gmmxxMatrix , x , b , gmm : : ildlt_precond < gmm : : csr_matrix < Type > > ( * gmmxxMatrix ) , iter ) ;
} else if ( precond . compare ( " none " ) = = 0 ) {
gmm : : qmr ( * gmmxxMatrix , x , b , gmm : : identity_matrix ( ) , iter ) ;
}
}
/ / Check if the solver converged and issue a warning otherwise .
if ( iter . converged ( ) ) {
LOG4CPLUS_INFO ( logger , " Iterative solver converged after " < < iter . get_iteration ( ) < < " iterations. " ) ;
} else {
LOG4CPLUS_WARN ( logger , " Iterative solver did not converge. " ) ;
}
/ / Set values of resulting vector according to result .
mrmc : : utility : : setVectorValues < Type > ( result , maybeStates , x ) ;
@ -154,11 +197,59 @@ public:
delete gmmxxMatrix ;
}
mrmc : : utility : : setVectorValues < Type > ( result , notExistsPhiUntilPsiStates , static_cast < double > ( 0 ) ) ;
mrmc : : utility : : setVectorValues < Type > ( result , alwaysPhiUntilPsiStates , static_cast < double > ( 1.0 ) ) ;
/ / Set values of resulting vector that are known exactly .
mrmc : : utility : : setVectorValues < Type > ( result , notExistsPhiUntilPsiStates , static_cast < Type > ( 0 ) ) ;
mrmc : : utility : : setVectorValues < Type > ( result , alwaysPhiUntilPsiStates , static_cast < Type > ( 1.0 ) ) ;
return result ;
}
/*!
* Returns the name of this module .
* @ return The name of this module .
*/
static std : : string getModuleName ( ) {
return " gmm++ " ;
}
/*!
* Returns a trigger such that if the option " matrixlib " is set to " gmm++ " , this model checker
* is to be used .
* @ return An option trigger for this module .
*/
static std : : pair < std : : string , std : : string > getOptionTrigger ( ) {
return std : : pair < std : : string , std : : string > ( " matrixlib " , " gmm++ " ) ;
}
/*!
* Registers all options associated with the gmm + + matrix library .
*/
static void putOptions ( boost : : program_options : : options_description * desc ) {
desc - > add_options ( ) ( " lemethod " , boost : : program_options : : value < std : : string > ( ) - > default_value ( " bicgstab " ) - > notifier ( & validateLeMethod ) , " Sets the method used for linear equation solving. Must be in {bicgstab, qmr}. " ) ;
desc - > add_options ( ) ( " lemaxiter " , boost : : program_options : : value < unsigned > ( ) - > default_value ( 10000 ) , " Sets the maximal number of iterations for iterative linear equation solving. " ) ;
desc - > add_options ( ) ( " precision " , boost : : program_options : : value < double > ( ) - > default_value ( 10e-6 ) , " Sets the precision for iterative linear equation solving. " ) ;
desc - > add_options ( ) ( " precond " , boost : : program_options : : value < std : : string > ( ) - > default_value ( " ilu " ) - > notifier ( & validatePreconditioner ) , " Sets the preconditioning technique for linear equation solving. Must be in {ilu, diagonal, ildlt, none}. " ) ;
}
/*!
* Validates whether the given lemethod matches one of the available ones .
* Throws an exception of type InvalidSettings in case the selected method is illegal .
*/
static void validateLeMethod ( const std : : string & lemethod ) {
if ( lemethod . compare ( " bicgstab " ) ! = 0 & & lemethod . compare ( " qmr " ) ! = 0 ) {
throw exceptions : : InvalidSettings ( ) < < " Argument " < < lemethod < < " for option 'lemethod' is invalid. " ;
}
}
/*!
* Validates whether the given preconditioner matches one of the available ones .
* Throws an exception of type InvalidSettings in case the selected preconditioner is illegal .
*/
static void validatePreconditioner ( const std : : string & preconditioner ) {
if ( preconditioner . compare ( " ilu " ) ! = 0 & & preconditioner . compare ( " diagonal " ) ! = 0 & & preconditioner . compare ( " ildlt " ) & & preconditioner . compare ( " none " ) ! = 0 ) {
throw exceptions : : InvalidSettings ( ) < < " Argument " < < preconditioner < < " for option 'precond' is invalid. " ;
}
}
} ;
} / / namespace modelChecker