Class StatisticalModelChecker

Class Documentation

class StatisticalModelChecker

Entry point for the statistical model checking pipeline. This class instantiates the model checking engine given the settings.

Public Functions

StatisticalModelChecker() = delete
StatisticalModelChecker(const storm::storage::SymbolicModelDescription &model, const storm::jani::Property &property, const settings::SmcSettings &settings)

Generate a new instance of the StatisticalModelChecker, using the provided settings to load the model and the property to verify.

Parameters:

  • model –

  • property –

  • settings –

~StatisticalModelChecker()
void printProperty() const

Print the loaded property in a human readable format.

void check()

Perform the model checking operation and store the result internally.

template<typename ResultType>
ResultType getResult() const

Get the computed result.

Template Parameters:

ResultType – The type of result to retrieve (i.e. double for probabilities and rewards and bool for conditions)

Returns:

The computed result, according to the ResultType template parameter