storm::modelchecker::SparseInstantiationModelChecker< SparseModelType, ConstantType > Class Template Reference

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 >:

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 12 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 31 of file SparseInstantiationModelChecker.cpp.

getOriginalModel()

template<typename SparseModelType, typename ConstantType>

SparseModelType const & storm::modelchecker::SparseInstantiationModelChecker< SparseModelType, ConstantType >::getOriginalModel

(

)

const

Definition at line 36 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

valuation

The 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 26 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 18 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:

• src/storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.h
• src/storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.cpp