Storm
A Modern Probabilistic Model Checker
|
#include <AssumptionMaker.h>
Public Member Functions | |
AssumptionMaker (storage::SparseMatrix< ValueType > matrix) | |
Constructs AssumptionMaker based on the matrix of the model. | |
std::map< std::shared_ptr< expressions::BinaryRelationExpression >, AssumptionStatus > | createAndCheckAssumptions (uint_fast64_t val1, uint_fast64_t val2, std::shared_ptr< Order > order, storage::ParameterRegion< ValueType > region) const |
Creates assumptions, and checks them, only VALID and UNKNOWN assumptions are returned. | |
std::map< std::shared_ptr< expressions::BinaryRelationExpression >, AssumptionStatus > | createAndCheckAssumptions (uint_fast64_t val1, uint_fast64_t val2, std::shared_ptr< Order > order, storage::ParameterRegion< ValueType > region, std::vector< ConstantType > const minValues, std::vector< ConstantType > const maxValue) const |
void | initializeCheckingOnSamples (std::shared_ptr< logic::Formula const > formula, std::shared_ptr< models::sparse::Dtmc< ValueType > > model, storage::ParameterRegion< ValueType > region, uint_fast64_t numberOfSamples) |
Initializes the given number of sample points for a given model, formula and region. | |
void | setSampleValues (std::vector< std::vector< ConstantType > > const &samples) |
Sets the sample values to the given vector. | |
Definition at line 15 of file AssumptionMaker.h.
storm::analysis::AssumptionMaker< ValueType, ConstantType >::AssumptionMaker | ( | storage::SparseMatrix< ValueType > | matrix | ) |
Constructs AssumptionMaker based on the matrix of the model.
matrix | The matrix of the model. |
Definition at line 6 of file AssumptionMaker.cpp.
std::map< std::shared_ptr< expressions::BinaryRelationExpression >, AssumptionStatus > storm::analysis::AssumptionMaker< ValueType, ConstantType >::createAndCheckAssumptions | ( | uint_fast64_t | val1, |
uint_fast64_t | val2, | ||
std::shared_ptr< Order > | order, | ||
storage::ParameterRegion< ValueType > | region | ||
) | const |
Creates assumptions, and checks them, only VALID and UNKNOWN assumptions are returned.
If one assumption is VALID, this assumption will be returned as only assumption. Possible results: AssumptionStatus::VALID, AssumptionStatus::UNKNOWN.
val1 | First state number. |
val2 | Second state number. |
order | The order on which the assumptions are checked. |
region | The region for the parameters. |
Definition at line 15 of file AssumptionMaker.cpp.
std::map< std::shared_ptr< expressions::BinaryRelationExpression >, AssumptionStatus > storm::analysis::AssumptionMaker< ValueType, ConstantType >::createAndCheckAssumptions | ( | uint_fast64_t | val1, |
uint_fast64_t | val2, | ||
std::shared_ptr< Order > | order, | ||
storage::ParameterRegion< ValueType > | region, | ||
std::vector< ConstantType > const | minValues, | ||
std::vector< ConstantType > const | maxValue | ||
) | const |
Definition at line 23 of file AssumptionMaker.cpp.
void storm::analysis::AssumptionMaker< ValueType, ConstantType >::initializeCheckingOnSamples | ( | std::shared_ptr< logic::Formula const > | formula, |
std::shared_ptr< models::sparse::Dtmc< ValueType > > | model, | ||
storage::ParameterRegion< ValueType > | region, | ||
uint_fast64_t | numberOfSamples | ||
) |
Initializes the given number of sample points for a given model, formula and region.
formula | The formula to compute the samples for. |
model | The considered model. |
region | The region of the model's parameters. |
numberOfSamples | Number of sample points. |
Definition at line 71 of file AssumptionMaker.cpp.
void storm::analysis::AssumptionMaker< ValueType, ConstantType >::setSampleValues | ( | std::vector< std::vector< ConstantType > > const & | samples | ) |
Sets the sample values to the given vector.
samples | The new value for samples. |
Definition at line 78 of file AssumptionMaker.cpp.