Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
storm::analysis::AssumptionMaker< ValueType, ConstantType > Class Template Reference

#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 >, AssumptionStatuscreateAndCheckAssumptions (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 >, AssumptionStatuscreateAndCheckAssumptions (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.
 

Detailed Description

template<typename ValueType, typename ConstantType>
class storm::analysis::AssumptionMaker< ValueType, ConstantType >

Definition at line 15 of file AssumptionMaker.h.

Constructor & Destructor Documentation

◆ AssumptionMaker()

template<typename ValueType , typename ConstantType >
storm::analysis::AssumptionMaker< ValueType, ConstantType >::AssumptionMaker ( storage::SparseMatrix< ValueType >  matrix)

Constructs AssumptionMaker based on the matrix of the model.

Parameters
matrixThe matrix of the model.

Definition at line 6 of file AssumptionMaker.cpp.

Member Function Documentation

◆ createAndCheckAssumptions() [1/2]

template<typename ValueType , typename ConstantType >
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.

Parameters
val1First state number.
val2Second state number.
orderThe order on which the assumptions are checked.
regionThe region for the parameters.
Returns
Map with at most three assumptions, and the validation.

Definition at line 15 of file AssumptionMaker.cpp.

◆ createAndCheckAssumptions() [2/2]

template<typename ValueType , typename ConstantType >
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.

◆ initializeCheckingOnSamples()

template<typename ValueType , typename ConstantType >
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.

Parameters
formulaThe formula to compute the samples for.
modelThe considered model.
regionThe region of the model's parameters.
numberOfSamplesNumber of sample points.

Definition at line 71 of file AssumptionMaker.cpp.

◆ setSampleValues()

template<typename ValueType , typename ConstantType >
void storm::analysis::AssumptionMaker< ValueType, ConstantType >::setSampleValues ( std::vector< std::vector< ConstantType > > const &  samples)

Sets the sample values to the given vector.

Parameters
samplesThe new value for samples.

Definition at line 78 of file AssumptionMaker.cpp.


The documentation for this class was generated from the following files: