Index

A

accept_region() (HyperRectangleRegions method) (RegionGenerator method) add_variable() (IsatSolver method) (SmtlibSolver method) (SMTSolver method) analyse_region() (RegionChecker method) (SmtRegionChecker method) analysis_time (GenerationRecord property)

Answer (class in prophesy.smt.smt) area (GenerationRecord property) assert_constraint() (IsatSolver method) (SmtlibSolver method) (SMTSolver method) assert_guarded_constraint() (IsatSolver method) (SmtlibSolver method) (SMTSolver method)

B

bad_regions (GenerationRecord property) BisimulationType (class in prophesy.modelcheckers.pmc)

Bool (VariableDomain attribute) bound_value_in_hyperrectangle() (StormpyModelChecker method) BoundType (class in prophesy.data.interval)

C

center() (HyperRectangle method) (Interval method) check() (IsatSolver method) (SmtlibSolver method) (SMTSolver method) check_existence() (Configuration method) check_filepath_for_reading() (in module prophesy.util) check_hyperrectangle() (ParametricProbabilisticModelChecker method) (ParamParametricModelChecker method) (PrismModelChecker method) (StormModelChecker method) (StormpyModelChecker method) check_region() (HyperRectangleRegions method) check_tools() (ProphesyConfig method) close() (HyperRectangle method) (Interval method) closed (BoundType attribute) Configuration (class in prophesy.util)

ConfigurationError Constants (class in prophesy.data.constant) constraint_to_interval() (in module prophesy.data.interval) CONSTRAINTS (ProphesyConfig attribute) contains() (HyperRectangle method) (Interval method) contains_nondeterministic_model() (DrnFile method) (PrismFile method) Context (class in prophesy.regions.region_smtchecker) copy() (InstantiationResultDict method) CounterExample (RegionCheckResult attribute) covered_area (GenerationRecord property) covered_safe_area (GenerationRecord property) create_cartesian_product() (in module prophesy.data.range) create_embedded_closed_interval() (in module prophesy.data.interval) create_range_from_interval() (in module prophesy.data.range) CTMC (ModelType attribute) cube() (HyperRectangle class method)

D

DEPENDENCIES (ModulesConfig attribute) dimension() (HyperRectangle method) (Point method), [1] DimensionNotSupportedError DIRECTORIES (ProphesyConfig attribute)

display_model() (ProbabilisticModelChecker method) (StormpyModelChecker method) distance() (ParameterInstantiation method) (Point method), [1] DrnFile (class in prophesy.input.modelfile) DTMC (ModelType attribute)

E

empty() (HyperRectangle method) (Interval method) encoding_timer (SmtRegionChecker property)

ensure_dir_exists() (in module prophesy.util) export_results() (RegionGenerator method) export_stats() (RegionGenerator method) EXTERNAL_TOOLS (ProphesyConfig attribute)

F

fail_region() (HyperRectangleRegions method) (RegionGenerator method) find() (FixedDenomFloatApproximation method) fix_guard() (SmtlibSolver method) fix_guards() (SMTSolver method) FixedDenomFloatApproximation (class in prophesy.data.nice_approximation) flip_green_red (Plot attribute)

from_extremal_points() (HyperRectangle class method) from_file() (IsatSolver method) (SmtlibSolver method) (SMTSolver method) from_point() (InstantiationResult class method) (ParameterInstantiation class method) from_region_string() (HyperRectangle class method)

G

generate_constraints() (RegionGenerator method) generate_header() (RegionGenerator method) generate_stats() (RegionGenerator method) generation_time (GenerationRecord property) GenerationRecord (class in prophesy.regions.region_generation) GEQ (InexactRelation attribute) get() (Configuration method) (PctlFile method), [1] get_all() (Configuration method) get_boolean() (Configuration method) get_float() (Configuration method) get_instantiation_point() (InstantiationResult method) get_int() (Configuration method) get_intermediate_dir() (ProphesyConfig method) get_isat() (ProphesyConfig method) get_model() (SmtlibSolver method) (StormpyModelChecker method) get_model_instantiation_checker() (StormpyModelChecker method) get_model_instantiator() (StormpyModelChecker method) get_nr_formulas() (PctlFile method), [1] get_param() (ProphesyConfig method) get_parameter() (ParameterOrder method) get_parameter_bounds() (ParameterOrder method) get_parameter_constraints() (ParametricProbabilisticModelChecker method) (ParamParametricModelChecker method) (PrismModelChecker method) (StormModelChecker method) (StormpyModelChecker method)

get_parameter_mapping() (StormpyModelChecker method) get_parameters() (InstantiationResult method) (ParameterInstantiation method) (StormpyModelChecker method) get_pla_checker() (StormpyModelChecker method) get_plots_dir() (ProphesyConfig method) get_point() (ParameterInstantiation method) get_prism() (ProphesyConfig method) get_rational_function() (ParametricProbabilisticModelChecker method) (ParamParametricModelChecker method) (PrismModelChecker method) (StormModelChecker method) (StormpyModelChecker method) get_sampling_epsilon() (ProphesyConfig method) get_sampling_min_distance() (ProphesyConfig method) get_smt_memout() (ProphesyConfig method) get_smt_timeout() (ProphesyConfig method) get_storm() (ProphesyConfig method) get_storm_pars() (ProphesyConfig method) get_tool() (ProphesyConfig method) get_vertex() (HyperRectangle method) get_yices() (ProphesyConfig method) get_z3() (ProphesyConfig method) getAvailableParametricMCs() (ProphesyConfig method) getAvailableProbMCs() (ProphesyConfig method) getAvailableSamplers() (ProphesyConfig method) getAvailableSMTSolvers() (ProphesyConfig method) getSection() (ProphesyConfig method) GREATER (InexactRelation attribute)

H

has_built_model() (ProbabilisticModelChecker method) (StormModelChecker method) (StormpyModelChecker method) has_gurobipy() (ProphesyConfig method) has_pycarl_parser() (ModulesConfig method)

has_stormpy() (ModulesConfig method) (ProphesyConfig method) Homogenous (RegionCheckResult attribute) HyperRectangle (class in prophesy.data.hyperrectangle) HyperRectangleRegions (class in prophesy.regions.region_quads)

I

ignore_region() (HyperRectangleRegions method) (RegionGenerator method) InexactInstantiationResult (class in prophesy.data.samples) InexactRelation (class in prophesy.data.samples) Inhomogenous (RegionCheckResult attribute) initialize() (RegionChecker method) (SmtRegionChecker method) instantiate() (ParameterOrder method) instantiated_model_checking_time (StormpyModelChecker property) InstantiationResult (class in prophesy.data.samples) InstantiationResultDict (class in prophesy.data.samples)

InstantiationResultFlag (class in prophesy.data.samples) Int (VariableDomain attribute) intersect() (HyperRectangle method) (Interval method) Interval (class in prophesy.data.interval) is_bounded() (Interval method) is_closed() (HyperRectangle method) (Interval method) is_continuous_time() (ModelType method) is_module_available() (ModulesConfig method) IsatSolver (class in prophesy.smt.isat) iteration_time (GenerationRecord property)

K

killed (Answer attribute)

L

left_bound() (Interval method) left_bound_type() (Interval method) LEQ (InexactRelation attribute) LESS (InexactRelation attribute) LinearRefinement (class in prophesy.sampling.sampling_linear) load_configuration() (in module prophesy.config) load_model() (ProbabilisticModelChecker method) load_model_from_drn() (PrismModelChecker method) (ProbabilisticModelChecker method) (StormModelChecker method) (StormpyModelChecker method)

load_model_from_prismfile() (ParamParametricModelChecker method) (PrismModelChecker method) (ProbabilisticModelChecker method) (StormModelChecker method) (StormpyModelChecker method)

M

MA (ModelType attribute) make_intervals_closed() (ParameterOrder method) make_intervals_open() (ParameterOrder method) make_temporary_copy() (PrismFile method) mc_single_point() (StormpyModelChecker method) MDP (ModelType attribute) memout (Answer attribute) model_building_time (StormpyModelChecker property) model_is_nondeterministic() (in module prophesy.data.model_type) ModelInput (class in prophesy.input.modelfile) ModelType (class in prophesy.data.model_type) module prophesy.config prophesy.data.constant prophesy.data.constraint prophesy.data.hyperrectangle prophesy.data.interval prophesy.data.model_type prophesy.data.nice_approximation prophesy.data.parameter prophesy.data.point, [1] prophesy.data.range prophesy.data.samples prophesy.exceptions.configuration_error prophesy.exceptions.dimension_not_supported_error prophesy.exceptions.module_error prophesy.exceptions.not_enough_information_error prophesy.input.modelfile prophesy.input.pctlfile, [1] prophesy.input.samplefile prophesy.input.solutionfunctionfile prophesy.modelcheckers prophesy.modelcheckers.param prophesy.modelcheckers.pmc prophesy.modelcheckers.ppmc prophesy.modelcheckers.prism prophesy.modelcheckers.storm prophesy.modelcheckers.stormpy prophesy.output.plot prophesy.regions prophesy.regions.region_checker prophesy.regions.region_generation prophesy.regions.region_quads prophesy.regions.region_smtchecker prophesy.sampling.sample_generator prophesy.sampling.sampler prophesy.sampling.sampler_ratfunc prophesy.sampling.sampling prophesy.sampling.sampling_linear prophesy.sampling.sampling_uniform prophesy.smt prophesy.smt.isat prophesy.smt.smt prophesy.smt.smtlib prophesy.smt.YicesCli_solver prophesy.smt.Z3cli_solver prophesy.util

ModuleError ModulesConfig (class in prophesy.config) Monotonicity (class in prophesy.data.parameter)

N

name() (IsatSolver method) (ParamParametricModelChecker method) (PrismModelChecker method) (ProbabilisticModelChecker method) (SmtlibSolver method) (SMTSolver method) (StormModelChecker method) (StormpyModelChecker method) (YicesCLISolver method) (Z3CliSolver method) negated() (BoundType method) NEGATIVE (Monotonicity attribute) NEITHER (Monotonicity attribute) next_region() (HyperRectangleRegions method) (RegionGenerator method)

non_empty_intersection() (HyperRectangle method) none (BisimulationType attribute) NOT_WELLDEFINED (InstantiationResultFlag attribute) NotEnoughInformationError nr_parameters() (PrismFile method) nr_regions_checked (StormpyModelChecker property) nr_samples_checked (StormpyModelChecker property) nr_states (StormpyModelChecker property) nr_states_before_bisim (StormpyModelChecker property) nr_transitions (StormpyModelChecker property) nr_transitions_before_bisim (StormpyModelChecker property) numerical_distance() (ParameterInstantiation method) (Point method), [1]

O

open (BoundType attribute) open() (Interval method)

open_file() (in module prophesy.util) open_model_file() (in module prophesy.input.modelfile) over_approximates() (SmtRegionChecker method)

P

Parameter (class in prophesy.data.parameter) ParameterInstantiation (class in prophesy.data.samples) ParameterOrder (class in prophesy.data.parameter) ParametricProbabilisticModelChecker (class in prophesy.modelcheckers.ppmc) ParametricResult (class in prophesy.input.solutionfunctionfile) ParamParametricModelChecker (class in prophesy.modelcheckers.param) parse_constants_string() (in module prophesy.data.constant) parse_smt_command() (in module prophesy.smt.smtlib) parse_smt_expr() (in module prophesy.smt.smtlib) PctlFile (class in prophesy.input.pctlfile), [1] perform_sampling() (ParamParametricModelChecker method) (PrismModelChecker method) (RatFuncSampling method) (Sampler method) (StormModelChecker method) (StormpyModelChecker method) perform_uniform_sampling() (PrismModelChecker method) (Sampler method) Plot (class in prophesy.output.plot) plot_candidate() (HyperRectangleRegions method) (RegionGenerator method) plot_poly() (Plot static method) plot_results() (Plot static method) (RegionGenerator method) plot_samples() (in module prophesy.output.plot) Point (class in prophesy.data.point), [1] pop() (IsatSolver method) (SmtlibSolver method) (SMTSolver method) POSITIVE (Monotonicity attribute) print_calls() (IsatSolver method) (SmtlibSolver method) PrismFile (class in prophesy.input.modelfile) PrismModelChecker (class in prophesy.modelcheckers.prism) prob01_states() (StormpyModelChecker method) ProbabilisticModelChecker (class in prophesy.modelcheckers.pmc) projection() (Point method), [1] prophesy.config module prophesy.data.constant module prophesy.data.constraint module prophesy.data.hyperrectangle module prophesy.data.interval module prophesy.data.model_type module prophesy.data.nice_approximation module prophesy.data.parameter module prophesy.data.point module, [1] prophesy.data.range module prophesy.data.samples module prophesy.exceptions.configuration_error module prophesy.exceptions.dimension_not_supported_error module prophesy.exceptions.module_error module

prophesy.exceptions.not_enough_information_error module prophesy.input.modelfile module prophesy.input.pctlfile module, [1] prophesy.input.samplefile module prophesy.input.solutionfunctionfile module prophesy.modelcheckers module prophesy.modelcheckers.param module prophesy.modelcheckers.pmc module prophesy.modelcheckers.ppmc module prophesy.modelcheckers.prism module prophesy.modelcheckers.storm module prophesy.modelcheckers.stormpy module prophesy.output.plot module prophesy.regions module prophesy.regions.region_checker module prophesy.regions.region_generation module prophesy.regions.region_quads module prophesy.regions.region_smtchecker module prophesy.sampling.sample_generator module prophesy.sampling.sampler module prophesy.sampling.sampler_ratfunc module prophesy.sampling.sampling module prophesy.sampling.sampling_linear module prophesy.sampling.sampling_uniform module prophesy.smt module prophesy.smt.isat module prophesy.smt.smt module prophesy.smt.smtlib module prophesy.smt.YicesCli_solver module prophesy.smt.Z3cli_solver module prophesy.util module ProphesyConfig (class in prophesy.config) push() (IsatSolver method) (SmtlibSolver method) (SMTSolver method)

R

Range (class in prophesy.data.range) RatFuncSampling (class in prophesy.sampling.sampler_ratfunc) read_param_result() (in module prophesy.input.solutionfunctionfile) read_pstorm_result() (in module prophesy.input.solutionfunctionfile) read_samples_file() (in module prophesy.input.samplefile) Real (VariableDomain attribute) record_accepted() (RegionGenerator method) record_border() (RegionGenerator method) record_cex() (RegionGenerator method) record_contains_border() (RegionGenerator method) record_illdefined() (RegionGenerator method) record_results() (RegionGenerator method) record_unknown() (RegionGenerator method) refine_region() (HyperRectangleRegions method) refine_samples() (in module prophesy.sampling.sampling) Refined (RegionCheckResult attribute)

region (GenerationRecord property) region_from_polygon() (in module prophesy.data.constraint) region_model_checking_time (StormpyModelChecker property) RegionChecker (class in prophesy.regions.region_checker) RegionCheckResult (class in prophesy.regions.region_checker) RegionGenerator (class in prophesy.regions.region_generation) reject_region() (HyperRectangleRegions method) (RegionGenerator method) remove_parameter() (ParameterOrder method) replace_parameter_keyword() (PrismFile method) result (GenerationRecord property) rew0_states() (StormpyModelChecker method) right_bound() (Interval method) right_bound_type() (Interval method) run() (IsatSolver method) (SmtlibSolver method) run_tool() (in module prophesy.util)

S

safe (GenerationRecord property) safe_area (GenerationRecord property) safe_regions (GenerationRecord property) sample_single_point() (PrismModelChecker method) (StormpyModelChecker method) SampleGenerator (class in prophesy.sampling.sample_generator) Sampler (class in prophesy.sampling.sampler) SAMPLING (ProphesyConfig attribute) sat (Answer attribute) Satisfied (RegionCheckResult attribute) set() (Configuration method) set_bisimulation_type() (ParamParametricModelChecker method) (PrismModelChecker method) (ProbabilisticModelChecker method) (StormModelChecker method) (StormpyModelChecker method) set_guard() (IsatSolver method) (SmtlibSolver method) (SMTSolver method) set_pctl_formula() (ParamParametricModelChecker method) (PrismModelChecker method) (ProbabilisticModelChecker method) (StormModelChecker method) (StormpyModelChecker method) set_region() (GenerationRecord method) set_regions() (GenerationRecord method) set_result() (GenerationRecord method) set_welldefined_checker() (StormpyModelChecker method) setminus() (HyperRectangle method) (Interval method) size() (HyperRectangle method)

SMT (ProphesyConfig attribute) SmtlibSolver (class in prophesy.smt.smtlib) SmtRegionChecker (class in prophesy.regions.region_smtchecker) SMTSolver (class in prophesy.smt.smt) solver_timer (SmtRegionChecker property) split() (InstantiationResultDict method) (Interval method) split_by_growing_rectangles() (HyperRectangleRegions static method) split_in_every_dimension() (HyperRectangle method) split_in_single_dimension() (HyperRectangle method) split_uniformly_in_every_dimension() (HyperRectangleRegions static method) Splitted (RegionCheckResult attribute) start_analysis() (RegionGenerator method) start_analysis_timer() (GenerationRecord method) start_generation() (RegionGenerator method) start_generation_timer() (GenerationRecord method) start_iteration() (RegionGenerator method) start_iteration_timer() (GenerationRecord method) stop() (IsatSolver method) (SmtlibSolver method) stop_analysis() (RegionGenerator method) stop_analysis_timer() (GenerationRecord method) stop_generation() (RegionGenerator method) stop_generation_timer() (GenerationRecord method) stop_iteration() (RegionGenerator method) stop_iteration_timer() (GenerationRecord method) StormModelChecker (class in prophesy.modelcheckers.storm) StormpyModelChecker (class in prophesy.modelcheckers.stormpy) string_to_interval() (in module prophesy.data.interval) strong (BisimulationType attribute) supports_only_closed_regions() (RegionChecker method)

T

timeout (Answer attribute) to_file() (IsatSolver method) (SmtlibSolver method) (SMTSolver method) to_float() (Point method), [1]

to_formula() (HyperRectangle method) (ParameterInstantiation method) to_key_value_string() (Constants method) to_nice_rationals() (Point method), [1] to_region_string() (HyperRectangle method)

U

uniform_samples() (in module prophesy.sampling.sampling) UniformSampleGenerator (class in prophesy.sampling.sampling_uniform) unknown (Answer attribute) UNKNOWN (Monotonicity attribute) Unknown (RegionCheckResult attribute)

unsat (Answer attribute) update_configuration_file() (Configuration method) update_variables() (ParameterOrder method) usage_stats() (ProbabilisticModelChecker method) (StormpyModelChecker method)

V

values() (Range method) VariableDomain (class in prophesy.smt.smt) version() (IsatSolver method) (ParamParametricModelChecker method) (PrismModelChecker method) (ProbabilisticModelChecker method) (SmtlibSolver method) (SMTSolver method) (StormModelChecker method) (StormpyModelChecker method)

vertices() (HyperRectangle method)

W

weak (BisimulationType attribute) weighed_interpolation() (in module prophesy.data.samples) well_defined (InstantiationResult property) which() (in module prophesy.util)

width() (Interval method) write_pstorm_result() (in module prophesy.input.solutionfunctionfile) write_samples_file() (in module prophesy.input.samplefile) write_string_to_file() (in module prophesy.util) write_string_to_tmpfile() (in module prophesy.util)

Y

YicesCLISolver (class in prophesy.smt.YicesCli_solver)

Z

Z3CliSolver (class in prophesy.smt.Z3cli_solver)