prophesy.modelcheckers package¶

Module contents¶

Interfaces¶

prophesy.modelcheckers.pmc module¶

class BisimulationType(value)¶

Bases: enum.Enum

Bisimulation type (None, Strong, Weak).

none = 0¶

strong = 1¶

weak = 2¶

class ProbabilisticModelChecker¶

Bases: prophesy.sampling.sampler.Sampler

An abstraction of probabilistic model checkers for concrete systems.

abstract display_model()¶: Display the model. :return:

abstract has_built_model()¶

load_model(model_description, constants={})¶

Parameters

model_description –
constants –

Returns

abstract load_model_from_drn(drnfile, constants={})¶

abstract load_model_from_prismfile(prismfile, constants={})¶: Load model from given Prism file. :param prismfile: Prism file. :param constants: List of constants and their values.

abstract name()¶: Get name of model checker. :return: A string with the name of the model checker.

abstract set_bisimulation_type(bisimulationType)¶: Set bisimulation type. :param bisimulationType: Bisimulation type (None, Strong, Weak).

abstract set_pctl_formula(formula)¶: Set PCTL formula to check. :param formula: PCTL formula

abstract usage_stats()¶

abstract version()¶: Get version of model checker. :return: A string with the version of the model checker.

prophesy.modelcheckers.ppmc module¶

class ParametricProbabilisticModelChecker¶

Bases: prophesy.modelcheckers.pmc.ProbabilisticModelChecker

An abstraction of probabilistic model checkers for parametric systems.

abstract check_hyperrectangle(parameters, hyperrectangle, threshold, above_threshold)¶

Check if the given hypothesis holds in the given hyperrectangle. :param parameters: A dictionary of variable name to its interval. :param hyperrectangle: Hyperrectangle. :param threshold: A value indicating the threshold, that is, a value expected to be

above or below each value in the hyperrectangle.

Parameters: above_threshold – Whether the rectangle is expected to be above or below the given threshold.
Returns: True iff the hypothesis holds.

abstract get_parameter_constraints()¶

For the model and the parameters at hand, get the constraints under which they induce a welldefined model

Returns: Two list of constraints, one with the welldefinedness constraints, one with the graph preservation constraints.

abstract get_rational_function()¶: Compute rational function representing model checking result. :return: A rational function in prophesy format.

Implementations¶

prophesy.modelcheckers.storm module¶

class StormModelChecker(main_location=None, parameter_location=None)¶

Bases: prophesy.modelcheckers.ppmc.ParametricProbabilisticModelChecker

Class wrapping the storm model checker CLI.

check_hyperrectangle(parameters, hyperrectangle, threshold, safe)¶

above or below each value in the hyperrectangle.

Parameters: above_threshold – Whether the rectangle is expected to be above or below the given threshold.
Returns: True iff the hypothesis holds.

get_parameter_constraints()¶

For the model and the parameters at hand, get the constraints under which they induce a welldefined model

Returns: Two list of constraints, one with the welldefinedness constraints, one with the graph preservation constraints.

get_rational_function()¶: Compute rational function representing model checking result. :return: A rational function in prophesy format.

has_built_model()¶

load_model_from_drn(drnfile, constants={})¶

load_model_from_prismfile(prismfile, constants={})¶: Load model from given Prism file. :param prismfile: Prism file. :param constants: List of constants and their values.

name()¶: Get name of model checker. :return: A string with the name of the model checker.

perform_sampling(sample_points, surely_welldefined=False)¶

Given some parameter instantiations, perform sampling on these instantiations.

Parameters: samplepoints – An iterable yielding parameter instantiations
Returns: A collection with the results of these samples
Return type: InstantiationResultDict

set_bisimulation_type(t)¶: Set bisimulation type. :param bisimulationType: Bisimulation type (None, Strong, Weak).

set_pctl_formula(formula)¶: Set PCTL formula to check. :param formula: PCTL formula

version()¶: Get version of model checker. :return: A string with the version of the model checker.

prophesy.modelcheckers.stormpy module¶

class StormpyModelChecker¶

Bases: prophesy.modelcheckers.ppmc.ParametricProbabilisticModelChecker

Class wrapping the stormpy bindings.

bound_value_in_hyperrectangle(parameters, hyperrectangle, direction, all_states=False, generate_split_estimates=False)¶

Parameters

parameters – The parameters
hyperrectangle – The hyperrectangle for the parameters
direction –
all_states – Should the value be computed for all states

Returns

check_hyperrectangle(parameters, hyperrectangle, threshold, above_threshold, only_check_hypothesis=True)¶

above or below each value in the hyperrectangle.

Parameters: above_threshold – Whether the rectangle is expected to be above or below the given threshold.
Returns: True iff the hypothesis holds.

display_model()¶: Display the model. :return:

get_model()¶: Get model. If model is not built before, first build the model and (optionally) perform bisimulation. :return: Model.

get_model_instantiation_checker()¶

get_model_instantiator()¶: Return model instantiator. :return: Model instantiator.

get_parameter_constraints()¶

For the model and the parameters at hand, get the constraints under which they induce a welldefined model

Returns: Two list of constraints, one with the welldefinedness constraints, one with the graph preservation constraints.

get_parameter_mapping(prophesy_parameters, from_storm=False)¶: Get a mapping from prophesy parameters to model parameters in stormpy (or the other way around).

get_parameters()¶

get_pla_checker(threshold, splitting_assistance=False, allow_simplifications=True)¶: Return model checker for PLA. :param threshold: Threshold in formula. :param splitting_assistance: Should splitting assistance be turned on (induces a mild performance penalty) :param allow_simplifications: Allow model simplifications in the checker (prevents using solutions for all states, induces an overhead on simplified models) :return: PLA model checker.

get_rational_function()¶: Compute rational function representing model checking result. :return: A rational function in prophesy format.

has_built_model()¶

property instantiated_model_checking_time¶

load_model_from_drn(drnfile, constants={})¶

load_model_from_prismfile(prism_file, constants={})¶: Load model from given Prism file. :param prismfile: Prism file. :param constants: List of constants and their values.

mc_single_point(parameter_instantiation, parameter_mapping=None)¶

property model_building_time¶

name()¶: Get name of model checker. :return: A string with the name of the model checker.

property nr_regions_checked¶

property nr_samples_checked¶

property nr_states¶

property nr_states_before_bisim¶

property nr_transitions¶

property nr_transitions_before_bisim¶

perform_sampling(sample_points, surely_welldefined=False)¶

Given some parameter instantiations, perform sampling on these instantiations.

Parameters: samplepoints – An iterable yielding parameter instantiations
Returns: A collection with the results of these samples
Return type: InstantiationResultDict

prob01_states()¶

property region_model_checking_time¶

rew0_states()¶

sample_single_point(parameter_instantiation, parameter_mapping)¶

set_bisimulation_type(bisimulation_type)¶: Set bisimulation type. :param bisimulationType: Bisimulation type (None, Strong, Weak).

set_pctl_formula(formula)¶: Set PCTL formula to check. :param formula: PCTL formula

set_welldefined_checker(checker)¶

usage_stats()¶

version()¶: Get version of model checker. :return: A string with the version of the model checker.

prophesy.modelcheckers.param module¶

class ParamParametricModelChecker¶

Bases: prophesy.modelcheckers.ppmc.ParametricProbabilisticModelChecker

Class wrapping the param model checker CLI.

check_hyperrectangle(parameters, hyperrectangle, threshold, above_threshold)¶

above or below each value in the hyperrectangle.

Parameters: above_threshold – Whether the rectangle is expected to be above or below the given threshold.
Returns: True iff the hypothesis holds.

get_parameter_constraints()¶

For the model and the parameters at hand, get the constraints under which they induce a welldefined model

Returns: Two list of constraints, one with the welldefinedness constraints, one with the graph preservation constraints.

get_rational_function()¶: Compute rational function representing model checking result. :return: A rational function in prophesy format.

load_model_from_prismfile(prismfile, constants)¶: Load model from given Prism file. :param prismfile: Prism file. :param constants: List of constants and their values.

name()¶: Get name of model checker. :return: A string with the name of the model checker.

perform_sampling(samplepoints)¶

Given some parameter instantiations, perform sampling on these instantiations.

Parameters: samplepoints – An iterable yielding parameter instantiations
Returns: A collection with the results of these samples
Return type: InstantiationResultDict

set_bisimulation_type(BisimulationType)¶: Set bisimulation type. :param bisimulationType: Bisimulation type (None, Strong, Weak).

set_pctl_formula(formula)¶: Set PCTL formula to check. :param formula: PCTL formula

version()¶: Get version of model checker. :return: A string with the version of the model checker.

prophesy.modelcheckers.prism module¶

class PrismModelChecker(location=None)¶

Bases: prophesy.modelcheckers.ppmc.ParametricProbabilisticModelChecker

Class wrapping the prism model checker CLI.

check_hyperrectangle(parameters, hyperrectangle, threshold, above_threshold)¶

above or below each value in the hyperrectangle.

Parameters: above_threshold – Whether the rectangle is expected to be above or below the given threshold.
Returns: True iff the hypothesis holds.

get_parameter_constraints()¶

For the model and the parameters at hand, get the constraints under which they induce a welldefined model

Returns: Two list of constraints, one with the welldefinedness constraints, one with the graph preservation constraints.

get_rational_function()¶: Compute rational function representing model checking result. :return: A rational function in prophesy format.

load_model_from_drn(drnfile, constants={})¶

load_model_from_prismfile(prismfile, constants={})¶: Load model from given Prism file. :param prismfile: Prism file. :param constants: List of constants and their values.

name()¶: Get name of model checker. :return: A string with the name of the model checker.

perform_sampling(samplepoints, surely_welldefined=False)¶

Given some parameter instantiations, perform sampling on these instantiations.

Parameters: samplepoints – An iterable yielding parameter instantiations
Returns: A collection with the results of these samples
Return type: InstantiationResultDict

perform_uniform_sampling(parameters, region, samples_per_dimension)¶

Samples a uniform grid of points.

Given a list of intervals (i.e., the first and last point; for each dimension, in order) and the number of samples per dimension, a uniformly-spaced grid of points (the cartesian product) is sampled.

Parameters

parameters – Parameters together with their region.
samples_per_dimension – In how many points should the region be divided.

sample_single_point(parameter_instantiation, result_path=None, pctl_path=None)¶

set_bisimulation_type(bisimulationType)¶: Set bisimulation type. :param bisimulationType: Bisimulation type (None, Strong, Weak).

set_pctl_formula(formula)¶: Set PCTL formula to check. :param formula: PCTL formula

version()¶: Get version of model checker. :return: A string with the version of the model checker.