- Generated by
1.9.8
|
Storm 1.11.1.1
A Modern Probabilistic Model Checker
|
#include <GradientDescentInstantiationSearcher.h>
Classes | |
| struct | VisualizationPoint |
| A point in the Gradient Descent walk, recorded if recordRun is set to true in the constructor (false by default). More... | |
Public Member Functions | |
| GradientDescentInstantiationSearcher (storm::models::sparse::Dtmc< FunctionType > const &model, GradientDescentMethod method=GradientDescentMethod::ADAM, ConstantType learningRate=0.1, ConstantType averageDecay=0.9, ConstantType squaredAverageDecay=0.999, uint_fast64_t miniBatchSize=32, ConstantType terminationEpsilon=1e-6, std::optional< std::map< typename utility::parametric::VariableType< FunctionType >::type, typename utility::parametric::CoefficientType< FunctionType >::type > > startPoint=std::nullopt, GradientDescentConstraintMethod constraintMethod=GradientDescentConstraintMethod::PROJECT_WITH_GRADIENT, std::optional< storage::ParameterRegion< FunctionType > > region=std::nullopt, bool recordRun=false) | |
| The GradientDescentInstantiationSearcher can find extrema and feasible instantiations in pMCs, for either rewards or probabilities. | |
| void | setup (Environment const &env, std::shared_ptr< storm::pars::FeasibilitySynthesisTask const > const &task) |
| This will setup the matrices used for computing the derivatives by constructing the SparseDerivativeInstantiationModelChecker. | |
| std::pair< std::map< typename utility::parametric::VariableType< FunctionType >::type, typename utility::parametric::CoefficientType< FunctionType >::type >, ConstantType > | gradientDescent () |
| Perform Gradient Descent. | |
| void | printRunAsJson () |
| Print the previously done run as JSON. | |
| std::vector< VisualizationPoint > | getVisualizationWalk () |
| Get the visualization walk that is recorded if recordRun is set to true in the constructor (false by default). | |
Definition at line 22 of file GradientDescentInstantiationSearcher.h.
|
inline |
The GradientDescentInstantiationSearcher can find extrema and feasible instantiations in pMCs, for either rewards or probabilities.
Internally uses the SparseDerivativeInstantiationModelChecker to evaluate derivatives at instantiations.
| env | The environment. Always pass the same environment to the gradientDescent call! |
| model | The Dtmc to optimize. |
| method | The method of gradient descent that is used. |
| learningRate | The learning rate of the Gradient Descent. |
| averageDecay | Decay of ADAM's decaying average. |
| squaredAverageDecay | Decay of ADAM's squared decaying average. |
| miniBatchSize | Size of a minibatch. |
| terminationEpsilon | A value step smaller than this is considered a "tiny step", after a number of these the algorithm will terminate. |
| startPoint | Start point of the search (default: all parameters set to 0.5) |
| recordRun | Records the run into a global variable, which can be converted into JSON using the printRunAsJson function |
| region | If constraintMethod is PROJECT_WITH_GRADIENT or PROJECT, the region of the search. If this is not set the region will be the graph-preseving region. |
Definition at line 43 of file GradientDescentInstantiationSearcher.h.
| std::vector< typename GradientDescentInstantiationSearcher< FunctionType, ConstantType >::VisualizationPoint > storm::derivative::GradientDescentInstantiationSearcher< FunctionType, ConstantType >::getVisualizationWalk | ( | ) |
Get the visualization walk that is recorded if recordRun is set to true in the constructor (false by default).
Definition at line 538 of file GradientDescentInstantiationSearcher.cpp.
| std::pair< std::map< VariableType< FunctionType >, CoefficientType< FunctionType > >, ConstantType > storm::derivative::GradientDescentInstantiationSearcher< FunctionType, ConstantType >::gradientDescent | ( | ) |
Perform Gradient Descent.
Definition at line 388 of file GradientDescentInstantiationSearcher.cpp.
| void storm::derivative::GradientDescentInstantiationSearcher< FunctionType, ConstantType >::printRunAsJson | ( | ) |
Print the previously done run as JSON.
This run can be retrieved using getVisualizationWalk.
Definition at line 517 of file GradientDescentInstantiationSearcher.cpp.
|
inline |
This will setup the matrices used for computing the derivatives by constructing the SparseDerivativeInstantiationModelChecker.
Note this consumes a substantial amount of memory, if the model is big and there's a large number of parameters.
| env | The environment. We need this because we need to know what kind of equation solver we are dealing with. |
| task | The FeasibilitySynthesisTask. |
Definition at line 141 of file GradientDescentInstantiationSearcher.h.
1.9.8