Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Public Member Functions | Protected Attributes | List of all members
storm::modelchecker::SparseInstantiationModelChecker< SparseModelType, ConstantType > Class Template Referenceabstract

Class to efficiently check a formula on a parametric model with different parameter instantiations. More...

#include <SparseInstantiationModelChecker.h>

Inheritance diagram for storm::modelchecker::SparseInstantiationModelChecker< SparseModelType, ConstantType >:
Inheritance graph
[legend]

Public Member Functions

 SparseInstantiationModelChecker (SparseModelType const &parametricModel)
 
virtual ~SparseInstantiationModelChecker ()=default
 
void specifyFormula (CheckTask< storm::logic::Formula, typename SparseModelType::ValueType > const &checkTask)
 
virtual std::unique_ptr< CheckResult > check (Environment const &env, storm::utility::parametric::Valuation< typename SparseModelType::ValueType > const &valuation)=0
 
virtual bool isWellDefined (storm::utility::parametric::Valuation< typename SparseModelType::ValueType > const &valuation)=0
 Checks if the given valuation is valid for the current model.
 
void setInstantiationsAreGraphPreserving (bool value)
 
bool getInstantiationsAreGraphPreserving () const
 
SparseModelType const & getOriginalModel () const
 

Protected Attributes

SparseModelType const & parametricModel
 
std::unique_ptr< CheckTask< storm::logic::Formula, ConstantType > > currentCheckTask
 

Detailed Description

template<typename SparseModelType, typename ConstantType>
class storm::modelchecker::SparseInstantiationModelChecker< SparseModelType, ConstantType >

Class to efficiently check a formula on a parametric model with different parameter instantiations.

Definition at line 19 of file SparseInstantiationModelChecker.h.

Constructor & Destructor Documentation

◆ SparseInstantiationModelChecker()

template<typename SparseModelType , typename ConstantType >
storm::modelchecker::SparseInstantiationModelChecker< SparseModelType, ConstantType >::SparseInstantiationModelChecker ( SparseModelType const &  parametricModel)

Definition at line 15 of file SparseInstantiationModelChecker.cpp.

◆ ~SparseInstantiationModelChecker()

template<typename SparseModelType , typename ConstantType >
virtual storm::modelchecker::SparseInstantiationModelChecker< SparseModelType, ConstantType >::~SparseInstantiationModelChecker ( )
virtualdefault

Member Function Documentation

◆ check()

template<typename SparseModelType , typename ConstantType >
virtual std::unique_ptr< CheckResult > storm::modelchecker::SparseInstantiationModelChecker< SparseModelType, ConstantType >::check ( Environment const &  env,
storm::utility::parametric::Valuation< typename SparseModelType::ValueType > const &  valuation 
)
pure virtual

Implemented in storm::modelchecker::SparseCtmcInstantiationModelChecker< SparseModelType, ConstantType >, storm::modelchecker::SparseDtmcInstantiationModelChecker< SparseModelType, ConstantType >, and storm::modelchecker::SparseMdpInstantiationModelChecker< SparseModelType, ConstantType >.

◆ getInstantiationsAreGraphPreserving()

template<typename SparseModelType , typename ConstantType >
bool storm::modelchecker::SparseInstantiationModelChecker< SparseModelType, ConstantType >::getInstantiationsAreGraphPreserving ( ) const

Definition at line 34 of file SparseInstantiationModelChecker.cpp.

◆ getOriginalModel()

template<typename SparseModelType , typename ConstantType >
SparseModelType const & storm::modelchecker::SparseInstantiationModelChecker< SparseModelType, ConstantType >::getOriginalModel ( ) const

Definition at line 39 of file SparseInstantiationModelChecker.cpp.

◆ isWellDefined()

template<typename SparseModelType , typename ConstantType >
virtual bool storm::modelchecker::SparseInstantiationModelChecker< SparseModelType, ConstantType >::isWellDefined ( storm::utility::parametric::Valuation< typename SparseModelType::ValueType > const &  valuation)
pure virtual

Checks if the given valuation is valid for the current model.

Currently used before checking whether the center of the model is SAT / UNSAT in PLA. So we'll use the model instantiator to instantiate the model anyway, but we currently don't re-use the result.

Parameters
valuationThe valuation to check.
Returns
true if the valuation is well-defined, false otherwise.

Implemented in storm::modelchecker::SparseCtmcInstantiationModelChecker< SparseModelType, ConstantType >, storm::modelchecker::SparseDtmcInstantiationModelChecker< SparseModelType, ConstantType >, and storm::modelchecker::SparseMdpInstantiationModelChecker< SparseModelType, ConstantType >.

◆ setInstantiationsAreGraphPreserving()

template<typename SparseModelType , typename ConstantType >
void storm::modelchecker::SparseInstantiationModelChecker< SparseModelType, ConstantType >::setInstantiationsAreGraphPreserving ( bool  value)

Definition at line 29 of file SparseInstantiationModelChecker.cpp.

◆ specifyFormula()

template<typename SparseModelType , typename ConstantType >
void storm::modelchecker::SparseInstantiationModelChecker< SparseModelType, ConstantType >::specifyFormula ( CheckTask< storm::logic::Formula, typename SparseModelType::ValueType > const &  checkTask)

Definition at line 21 of file SparseInstantiationModelChecker.cpp.

Member Data Documentation

◆ currentCheckTask

template<typename SparseModelType , typename ConstantType >
std::unique_ptr<CheckTask<storm::logic::Formula, ConstantType> > storm::modelchecker::SparseInstantiationModelChecker< SparseModelType, ConstantType >::currentCheckTask
protected

Definition at line 49 of file SparseInstantiationModelChecker.h.

◆ parametricModel

template<typename SparseModelType , typename ConstantType >
SparseModelType const& storm::modelchecker::SparseInstantiationModelChecker< SparseModelType, ConstantType >::parametricModel
protected

Definition at line 48 of file SparseInstantiationModelChecker.h.

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