Stormpy.dft¶

class ApproximationHeuristic(self: stormpy.dft._dft.ApproximationHeuristic, value: SupportsInt)¶

Heuristic for selecting states to explore next

Members:

DEPTH

PROBABILITY

BOUNDDIFFERENCE

BOUNDDIFFERENCE = <ApproximationHeuristic.BOUNDDIFFERENCE: 2>¶

DEPTH = <ApproximationHeuristic.DEPTH: 0>¶

PROBABILITY = <ApproximationHeuristic.PROBABILITY: 1>¶

property name¶

property value¶

class DFTBE_double¶: Basic Event

class DFTBE_ratfunc¶: Basic Event

class DFTDependency_double¶

Dependency

property dependent_events¶: Dependent events

property trigger¶: Trigger event

class DFTDependency_ratfunc¶

Dependency

property dependent_events¶: Dependent events

property trigger¶: Trigger event

class DFTElementType(self: stormpy.dft._dft.DFTElementType, value: SupportsInt)¶

Members:

AND

VOT

PAND

POR

SPARE

PDEP

SEQ

MUTEX

AND = <DFTElementType.AND: 1>¶

BE = <DFTElementType.BE: 0>¶

MUTEX = <DFTElementType.MUTEX: 9>¶

OR = <DFTElementType.OR: 2>¶

PAND = <DFTElementType.PAND: 4>¶

PDEP = <DFTElementType.PDEP: 7>¶

POR = <DFTElementType.POR: 5>¶

SEQ = <DFTElementType.SEQ: 8>¶

SPARE = <DFTElementType.SPARE: 6>¶

VOT = <DFTElementType.VOT: 3>¶

property name¶

property value¶

class DFTElement_double¶

DFT element

property id¶: Id

property name¶: Name

property type¶: Type

class DFTElement_ratfunc¶

DFT element

property id¶: Id

property name¶: Name

property type¶: Type

class DFTInstantiator(self: stormpy.dft._dft.DFTInstantiator, dft: stormpy.dft._dft.DFT_ratfunc)¶

Instantiator for parametric DFT

Initialize with parametric DFT

instantiate(self: stormpy.dft._dft.DFTInstantiator, valuation: collections.abc.Mapping[stormpy.pycarl._pycarl_core.Variable, stormpy.pycarl.cln.Rational]) → stormpy.dft._dft.DFT_double¶: Instantiate parametric DFT and obtain concrete DFT

class DFTSimulator_double(self: stormpy.dft._dft.DFTSimulator_double, dft: stormpy.dft._dft.DFT_double, state_generation_info: stormpy.dft._dft.DFTStateInfo, generator: stormpy.dft._dft.RandomGenerator)¶

Simulator for DFT traces

Create Simulator

get_state(self: stormpy.dft._dft.DFTSimulator_double) → stormpy.dft._dft.DFTState_double¶: Get current state

get_time(self: stormpy.dft._dft.DFTSimulator_double) → float¶: Get total elapsed time so far

random_step(self: stormpy.dft._dft.DFTSimulator_double) → stormpy.dft._dft.SimulationStepResult¶: Perform random simulation step.

reset(self: stormpy.dft._dft.DFTSimulator_double) → None¶: Reset to initial state

reset_state(self: stormpy.dft._dft.DFTSimulator_double, state: stormpy.dft._dft.DFTState_double) → None¶: Reset to state

simulate_trace(self: stormpy.dft._dft.DFTSimulator_double, timebound: SupportsFloat) → stormpy.dft._dft.SimulationTraceResult¶: Simulate complete trace for given timebound

step(self: stormpy.dft._dft.DFTSimulator_double, next_failure: stormpy.dft._dft.FailableElement, dependency_success: bool = True) → stormpy.dft._dft.SimulationStepResult¶: Perform simulation step according to next_failure. For PDEPs, dependency_success determines whether the PDEP was successful or not.

class DFTSimulator_ratfunc(self: stormpy.dft._dft.DFTSimulator_ratfunc, dft: stormpy.dft._dft.DFT_ratfunc, state_generation_info: stormpy.dft._dft.DFTStateInfo, generator: stormpy.dft._dft.RandomGenerator)¶

Simulator for DFT traces

Create Simulator

get_state(self: stormpy.dft._dft.DFTSimulator_ratfunc) → stormpy.dft._dft.DFTState_ratfunc¶: Get current state

get_time(self: stormpy.dft._dft.DFTSimulator_ratfunc) → float¶: Get total elapsed time so far

random_step(self: stormpy.dft._dft.DFTSimulator_ratfunc) → stormpy.dft._dft.SimulationStepResult¶: Perform random simulation step.

reset(self: stormpy.dft._dft.DFTSimulator_ratfunc) → None¶: Reset to initial state

reset_state(self: stormpy.dft._dft.DFTSimulator_ratfunc, state: stormpy.dft._dft.DFTState_ratfunc) → None¶: Reset to state

simulate_trace(self: stormpy.dft._dft.DFTSimulator_ratfunc, timebound: SupportsFloat) → stormpy.dft._dft.SimulationTraceResult¶: Simulate complete trace for given timebound

step(self: stormpy.dft._dft.DFTSimulator_ratfunc, next_failure: stormpy.dft._dft.FailableElement, dependency_success: bool = True) → stormpy.dft._dft.SimulationStepResult¶: Perform simulation step according to next_failure. For PDEPs, dependency_success determines whether the PDEP was successful or not.

class DFTStateInfo¶: State Generation Info for DFT

class DFTState_double¶

DFT state

dontcare(self: stormpy.dft._dft.DFTState_double, id: SupportsInt) → bool¶: Is element Don’t Care

failable(self: stormpy.dft._dft.DFTState_double) → storm::dft::storage::FailableElements¶: Get failable elements

failed(self: stormpy.dft._dft.DFTState_double, id: SupportsInt) → bool¶: Is element failed

failsafe(self: stormpy.dft._dft.DFTState_double, id: SupportsInt) → bool¶: Is element fail-safe

invalid(self: stormpy.dft._dft.DFTState_double) → bool¶: Is state invalid

operational(self: stormpy.dft._dft.DFTState_double, id: SupportsInt) → bool¶: Is element operational

spare_uses(self: stormpy.dft._dft.DFTState_double, spare_id: SupportsInt) → int¶: Child currently used by a SPARE

to_string(self: stormpy.dft._dft.DFTState_double, dft: stormpy.dft._dft.DFT_double) → str¶: Print status

class DFTState_ratfunc¶

DFT state

dontcare(self: stormpy.dft._dft.DFTState_ratfunc, id: SupportsInt) → bool¶: Is element Don’t Care

failable(self: stormpy.dft._dft.DFTState_ratfunc) → storm::dft::storage::FailableElements¶: Get failable elements

failed(self: stormpy.dft._dft.DFTState_ratfunc, id: SupportsInt) → bool¶: Is element failed

failsafe(self: stormpy.dft._dft.DFTState_ratfunc, id: SupportsInt) → bool¶: Is element fail-safe

invalid(self: stormpy.dft._dft.DFTState_ratfunc) → bool¶: Is state invalid

operational(self: stormpy.dft._dft.DFTState_ratfunc, id: SupportsInt) → bool¶: Is element operational

spare_uses(self: stormpy.dft._dft.DFTState_ratfunc, spare_id: SupportsInt) → int¶: Child currently used by a SPARE

to_string(self: stormpy.dft._dft.DFTState_ratfunc, dft: stormpy.dft._dft.DFT_ratfunc) → str¶: Print status

class DFT_double¶

Dynamic Fault Tree

can_have_nondeterminism(self: stormpy.dft._dft.DFT_double) → bool¶: Whether the model can contain non-deterministic choices

get_element(self: stormpy.dft._dft.DFT_double, index: SupportsInt) → storm::dft::storage::elements::DFTElement<double>¶: Get DFT element at index

get_element_by_name(self: stormpy.dft._dft.DFT_double, name: str) → storm::dft::storage::elements::DFTElement<double>¶: Get DFT element by name

modules(self: stormpy.dft._dft.DFT_double) → storm::dft::storage::DftIndependentModule¶: Compute independent modules of DFT

nr_be(self: stormpy.dft._dft.DFT_double) → int¶: Number of basic elements

nr_dynamic(self: stormpy.dft._dft.DFT_double) → int¶: Number of dynamic elements

nr_elements(self: stormpy.dft._dft.DFT_double) → int¶: Total number of elements

set_relevant_events(self: stormpy.dft._dft.DFT_double, relevant_events: stormpy.dft._dft.RelevantEvents, allow_dc_for_revelant: bool) → None¶

state_generation_info(self: stormpy.dft._dft.DFT_double, symmetries: stormpy.dft._dft.DftSymmetries = <stormpy.dft._dft.DftSymmetries object at 0x7f4234e40ef0>) → storm::dft::storage::DFTStateGenerationInfo¶: Build state generation information

str_long(self: stormpy.dft._dft.DFT_double) → str¶

symmetries(self: stormpy.dft._dft.DFT_double) → stormpy.dft._dft.DftSymmetries¶: Compute symmetries in DFT

property top_level_element¶: Get top level element

class DFT_ratfunc¶

Dynamic Fault Tree

can_have_nondeterminism(self: stormpy.dft._dft.DFT_ratfunc) → bool¶: Whether the model can contain non-deterministic choices

get_element(self: stormpy.dft._dft.DFT_ratfunc, index: SupportsInt) → storm::dft::storage::elements::DFTElement<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::NotRelevant, carl::StdMultivariatePolynomialPolicies<0> > >, true> >¶: Get DFT element at index

get_element_by_name(self: stormpy.dft._dft.DFT_ratfunc, name: str) → storm::dft::storage::elements::DFTElement<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::NotRelevant, carl::StdMultivariatePolynomialPolicies<0> > >, true> >¶: Get DFT element by name

modules(self: stormpy.dft._dft.DFT_ratfunc) → storm::dft::storage::DftIndependentModule¶: Compute independent modules of DFT

nr_be(self: stormpy.dft._dft.DFT_ratfunc) → int¶: Number of basic elements

nr_dynamic(self: stormpy.dft._dft.DFT_ratfunc) → int¶: Number of dynamic elements

nr_elements(self: stormpy.dft._dft.DFT_ratfunc) → int¶: Total number of elements

set_relevant_events(self: stormpy.dft._dft.DFT_ratfunc, relevant_events: stormpy.dft._dft.RelevantEvents, allow_dc_for_revelant: bool) → None¶

state_generation_info(self: stormpy.dft._dft.DFT_ratfunc, symmetries: stormpy.dft._dft.DftSymmetries = <stormpy.dft._dft.DftSymmetries object at 0x7f4234e4cc70>) → storm::dft::storage::DFTStateGenerationInfo¶: Build state generation information

str_long(self: stormpy.dft._dft.DFT_ratfunc) → str¶

symmetries(self: stormpy.dft._dft.DFT_ratfunc) → stormpy.dft._dft.DftSymmetries¶: Compute symmetries in DFT

property top_level_element¶: Get top level element

class DftIndependentModule¶

Independent module in DFT

elements(self: stormpy.dft._dft.DftIndependentModule) → set[int]¶: Get elements of module (excluding submodules)

fully_static(self: stormpy.dft._dft.DftIndependentModule) → bool¶: Whether the module contains only static elements (also in submodules)

representative(self: stormpy.dft._dft.DftIndependentModule) → int¶: Get module representative

single_be(self: stormpy.dft._dft.DftIndependentModule) → bool¶: Whether the module consists of a single BE (trivial module)

static(self: stormpy.dft._dft.DftIndependentModule) → bool¶: Whether the module contains only static elements (except in submodules)

submodules(self: stormpy.dft._dft.DftIndependentModule) → set[stormpy.dft._dft.DftIndependentModule]¶: Get submodules

class DftSymmetries(self: stormpy.dft._dft.DftSymmetries)¶

Symmetries in DFT

Constructor for empty symmetry

get_group(self: stormpy.dft._dft.DftSymmetries, index: SupportsInt) → list[list[int]]¶: Get symmetry group

class ExplicitDFTModelBuilder_double(self: stormpy.dft._dft.ExplicitDFTModelBuilder_double, dft: storm::dft::storage::DFT<double>, symmetries: stormpy.dft._dft.DftSymmetries = <stormpy.dft._dft.DftSymmetries object at 0x7f423608ab30>)¶

Builder to generate explicit model from DFT

Constructor

build(self: stormpy.dft._dft.ExplicitDFTModelBuilder_double, iteration: typing.SupportsInt, approximation_threshold: typing.SupportsFloat = 0.0, approximation_heuristic: stormpy.dft._dft.ApproximationHeuristic = <ApproximationHeuristic.DEPTH: 0>) → None¶: Build state space of model

get_model(self: stormpy.dft._dft.ExplicitDFTModelBuilder_double) → stormpy.storage._storage._SparseModel¶: Get complete model

get_partial_model(self: stormpy.dft._dft.ExplicitDFTModelBuilder_double, lower_bound: bool, expected_time: bool) → stormpy.storage._storage._SparseModel¶: Get partial model

class ExplicitDFTModelBuilder_ratfunc(self: stormpy.dft._dft.ExplicitDFTModelBuilder_ratfunc, dft: storm::dft::storage::DFT<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::NotRelevant, carl::StdMultivariatePolynomialPolicies<0> > >, true> >, symmetries: stormpy.dft._dft.DftSymmetries = <stormpy.dft._dft.DftSymmetries object at 0x7f4235e3c4b0>)¶

Builder to generate explicit model from DFT

Constructor

build(self: stormpy.dft._dft.ExplicitDFTModelBuilder_ratfunc, iteration: typing.SupportsInt, approximation_threshold: typing.SupportsFloat = 0.0, approximation_heuristic: stormpy.dft._dft.ApproximationHeuristic = <ApproximationHeuristic.DEPTH: 0>) → None¶: Build state space of model

get_model(self: stormpy.dft._dft.ExplicitDFTModelBuilder_ratfunc) → stormpy.storage._storage._SparseParametricModel¶: Get complete model

get_partial_model(self: stormpy.dft._dft.ExplicitDFTModelBuilder_ratfunc, lower_bound: bool, expected_time: bool) → stormpy.storage._storage._SparseParametricModel¶: Get partial model

class FailableElement¶

Failable element

as_be_double(self: stormpy.dft._dft.FailableElement, dft: stormpy.dft._dft.DFT_double) → stormpy.dft._dft.DFTBE_double¶: Get BE which fails

as_be_ratfunc(self: stormpy.dft._dft.FailableElement, dft: stormpy.dft._dft.DFT_ratfunc) → stormpy.dft._dft.DFTBE_ratfunc¶: Get BE which fails

as_dependency_double(self: stormpy.dft._dft.FailableElement, dft: stormpy.dft._dft.DFT_double) → stormpy.dft._dft.DFTDependency_double¶: Get dependency which is triggered

as_dependency_ratfunc(self: stormpy.dft._dft.FailableElement, dft: stormpy.dft._dft.DFT_ratfunc) → stormpy.dft._dft.DFTDependency_ratfunc¶: Get dependency which is triggered

is_due_dependency(self: stormpy.dft._dft.FailableElement) → bool¶: Is failure due to dependency

class FailableElements¶: Failable elements in DFT state

class FailableIterator¶

class RandomGenerator¶

Random number generator

static create(seed: SupportsInt) → stormpy.dft._dft.RandomGenerator¶: Initialize random number generator

class RelevantEvents(self: stormpy.dft._dft.RelevantEvents)¶

Relevant events which should be observed

Create empty list of relevant events

is_relevant(self: stormpy.dft._dft.RelevantEvents, name: str) → bool¶: Check whether the given name is a relevant event

class SimulationStepResult(self: stormpy.dft._dft.SimulationStepResult, value: SupportsInt)¶

Members:

SUCCESSFUL

UNSUCCESSFUL

INVALID

INVALID = <SimulationStepResult.INVALID: 2>¶

SUCCESSFUL = <SimulationStepResult.SUCCESSFUL: 0>¶

UNSUCCESSFUL = <SimulationStepResult.UNSUCCESSFUL: 1>¶

property name¶

property value¶

class SimulationTraceResult(self: stormpy.dft._dft.SimulationTraceResult, value: SupportsInt)¶

Members:

SUCCESSFUL

UNSUCCESSFUL

INVALID

CONTINUE

CONTINUE = <SimulationTraceResult.CONTINUE: 3>¶

INVALID = <SimulationTraceResult.INVALID: 2>¶

SUCCESSFUL = <SimulationTraceResult.SUCCESSFUL: 0>¶

UNSUCCESSFUL = <SimulationTraceResult.UNSUCCESSFUL: 1>¶

property name¶

property value¶

analyze_dft(ft, properties, symred=True, allow_modularisation=False, relevant_events=<stormpy.dft._dft.RelevantEvents object>, allow_dc_for_relevant=False)¶

build_model(ft, symmetries=<stormpy.dft._dft.DftSymmetries object>, relevant_events=<stormpy.dft._dft.RelevantEvents object>, allow_dc_for_relevant=False)¶

compute_dependency_conflicts(ft, use_smt=False, solver_timeout=0)¶

compute_relevant_events(properties: collections.abc.Sequence[stormpy.logic._logic.Formula], additional_relevant_names: collections.abc.Sequence[str] = []) → stormpy.dft._dft.RelevantEvents¶: Compute relevant event ids from properties and additional relevant names

export_dft_json_file(dft: stormpy.dft._dft.DFT_double, path: str) → None¶: Export DFT to JSON file

export_dft_json_string(dft: stormpy.dft._dft.DFT_double) → str¶: Export DFT to JSON string

export_parametric_dft_json_file(dft: stormpy.dft._dft.DFT_ratfunc, path: str) → None¶: Export parametric DFT to JSON file

export_parametric_dft_json_string(dft: stormpy.dft._dft.DFT_ratfunc) → str¶: Export parametric DFT to JSON string

get_parameters(dft: storm::dft::storage::DFT<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::NotRelevant, carl::StdMultivariatePolynomialPolicies<0> > >, true> >) → set[stormpy.pycarl._pycarl_core.Variable]¶: Collect parameters in parametric DFT

has_potential_modeling_issues(ft)¶

is_well_formed(ft, check_valid_for_analysis=True)¶

load_dft_galileo_file(path: str) → stormpy.dft._dft.DFT_double¶: Load DFT from Galileo file

load_dft_json_file(path: str) → stormpy.dft._dft.DFT_double¶: Load DFT from JSON file

load_dft_json_string(json_string: str) → stormpy.dft._dft.DFT_double¶: Load DFT from JSON string

load_parametric_dft_galileo_file(path: str) → stormpy.dft._dft.DFT_ratfunc¶: Load parametric DFT from Galileo file

load_parametric_dft_json_file(path: str) → stormpy.dft._dft.DFT_ratfunc¶: Load parametric DFT from JSON file

load_parametric_dft_json_string(json_string: str) → stormpy.dft._dft.DFT_ratfunc¶: Load parametric DFT from JSON string

modules_json(dft)¶

Create JSON representation of DFT modules.

Parameters:: dft – DFT.
Returns:: JSON object containing all modules in a recursive hierarchy.

prepare_for_analysis(ft)¶

transform_dft(ft, unique_constant_be, binary_fdeps, exponential_distributions)¶