stamina::core::StaminaModelChecker Class Reference

Public Member Functions
	StaminaModelChecker (std::shared_ptr< storm::prism::Program > modulesFile=nullptr, std::shared_ptr< std::vector< storm::jani::Property > > propertiesVector=nullptr)
	~StaminaModelChecker ()
void	initialize (std::shared_ptr< storm::prism::Program > modulesFile=nullptr, std::shared_ptr< std::vector< storm::jani::Property > > propertiesVector=nullptr)
std::unique_ptr< storm::modelchecker::CheckResult >	modelCheckProperty (storm::jani::Property propMin, storm::jani::Property propMax, storm::prism::Program const &modulesFile)

Constructor & Destructor Documentation

StaminaModelChecker()

stamina::core::StaminaModelChecker::StaminaModelChecker	(	std::shared_ptr< storm::prism::Program >	modulesFile = nullptr,
		std::shared_ptr< std::vector< storm::jani::Property > >	propertiesVector = nullptr
	)

Constructor for StaminaModelChecker

Parameters

modulesFile	Pointer to the Modules file
propertiesVector	Pointer to the Properties vector

~StaminaModelChecker()

stamina::core::StaminaModelChecker::~StaminaModelChecker

(

)

Standard destructor

Member Function Documentation

initialize()

void stamina::core::StaminaModelChecker::initialize	(	std::shared_ptr< storm::prism::Program >	modulesFile = nullptr,
		std::shared_ptr< std::vector< storm::jani::Property > >	propertiesVector = nullptr
	)

Initializes the StaminaModelChecker class

Parameters

propertiesVector

A vector to the list of JANI properties

modelCheckProperty()

std::unique_ptr< storm::modelchecker::CheckResult > stamina::core::StaminaModelChecker::modelCheckProperty	(	storm::jani::Property	propMin,
		storm::jani::Property	propMax,
		storm::prism::Program const &	modulesFile
	)

Model checks a specific property

Parameters

prop	Property to check
modulesFile	The modules file to work with

Returns

A pointer to the result of the model checking

---

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

• /home/josh/Documents/Work/stamina-cplusplus/src/stamina/core/StaminaModelChecker.h
• /home/josh/Documents/Work/stamina-cplusplus/src/stamina/core/StaminaModelChecker.cpp