Stormpy.dft

class ApproximationHeuristic

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

Members:

BE

AND

OR

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>
name()

__str__(*args, **kwargs) Overloaded function.

  1. __str__(self: stormpy.dft.dft.DFTElementType) -> str

  2. __str__(self: handle) -> str

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

Instantiator for parametric DFT

instantiate(self: stormpy.dft.dft.DFTInstantiator, valuation: Dict[pycarl.core.Variable, pycarl.cln.cln.Rational]) stormpy.dft.dft.DFT_double

Instantiate parametric DFT and obtain concrete DFT

class DFTSimulator_double

Simulator for DFT traces

current(self: stormpy.dft.dft.DFTSimulator_double) stormpy.dft.dft.DFTState_double

Get current state

random_step(self: stormpy.dft.dft.DFTSimulator_double) Tuple[stormpy.dft.dft.SimulationResult, float]

Perform random simulation step. Returns a tuple of the simulation result and the time which progressed during this step.

reset(self: stormpy.dft.dft.DFTSimulator_double) None

Reset to initial state

simulate_trace(self: stormpy.dft.dft.DFTSimulator_double, timebound: float) stormpy.dft.dft.SimulationResult

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.SimulationResult

Perform simulation step according to next_failure. For PDEPs, dependency_success determines whether the PDEP was successful or not.

class DFTSimulator_ratfunc

Simulator for DFT traces

current(self: stormpy.dft.dft.DFTSimulator_ratfunc) stormpy.dft.dft.DFTState_ratfunc

Get current state

random_step(self: stormpy.dft.dft.DFTSimulator_ratfunc) Tuple[stormpy.dft.dft.SimulationResult, float]

Perform random simulation step. Returns a tuple of the simulation result and the time which progressed during this step.

reset(self: stormpy.dft.dft.DFTSimulator_ratfunc) None

Reset to initial state

simulate_trace(self: stormpy.dft.dft.DFTSimulator_ratfunc, timebound: float) stormpy.dft.dft.SimulationResult

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.SimulationResult

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: int) 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: int) bool

Is element failed

failsafe(self: stormpy.dft.dft.DFTState_double, id: int) bool

Is element fail-safe

invalid(self: stormpy.dft.dft.DFTState_double) bool

Is state invalid

operational(self: stormpy.dft.dft.DFTState_double, id: int) bool

Is element operational

spare_uses(self: stormpy.dft.dft.DFTState_double, spare_id: int) 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: int) 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: int) bool

Is element failed

failsafe(self: stormpy.dft.dft.DFTState_ratfunc, id: int) bool

Is element fail-safe

invalid(self: stormpy.dft.dft.DFTState_ratfunc) bool

Is state invalid

operational(self: stormpy.dft.dft.DFTState_ratfunc, id: int) bool

Is element operational

spare_uses(self: stormpy.dft.dft.DFTState_ratfunc, spare_id: int) 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: int) 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 0x7f35a8df6bb0>) 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: int) 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 0x7f35a8df7af0>) 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

Symmetries in DFT

get_group(self: stormpy.dft.dft.DftSymmetries, index: int) List[List[int]]

Get symmetry group

class ExplicitDFTModelBuilder_double

Builder to generate explicit model from DFT

build(self: stormpy.dft.dft.ExplicitDFTModelBuilder_double, iteration: int, approximation_threshold: float = 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

Builder to generate explicit model from DFT

build(self: stormpy.dft.dft.ExplicitDFTModelBuilder_ratfunc, iteration: int, approximation_threshold: float = 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: int) stormpy.dft.dft.RandomGenerator

Initialize random number generator

class RelevantEvents

Relevant events which should be observed

is_relevant(self: stormpy.dft.dft.RelevantEvents, name: str) bool

Check whether the given name is a relevant event

class SimulationResult

Members:

SUCCESSFUL

UNSUCCESSFUL

INVAlID

INVAlID = <SimulationResult.INVAlID: 2>
SUCCESSFUL = <SimulationResult.SUCCESSFUL: 0>
UNSUCCESSFUL = <SimulationResult.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: List[stormpy.logic.logic.Formula], additional_relevant_names: List[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[pycarl.core.Variable]

Collect parameters in parametric DFT

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)