Stormpy.dft

class DFT

Dynamic Fault Tree

can_have_nondeterminism(self: stormpy.dft.dft.DFT) bool

Whether the model can contain non-deterministic choices

get_element(self: stormpy.dft.dft.DFT, index: int) stormpy.dft.dft.DFTElement

Get DFT element at index

get_element_by_name(self: stormpy.dft.dft.DFT, name: str) stormpy.dft.dft.DFTElement

Get DFT element by name

modularisation(self: stormpy.dft.dft.DFT) List[stormpy.dft.dft.DFT]

Split DFT into independent modules

nr_be(self: stormpy.dft.dft.DFT) int

Number of basic elements

nr_dynamic(self: stormpy.dft.dft.DFT) int

Number of dynamic elements

nr_elements(self: stormpy.dft.dft.DFT) int

Total number of elements

symmetries(self: stormpy.dft.dft.DFT) storm::storage::DFTIndependentSymmetries

Compute symmetries in DFT

property top_level_element

Get top level element

class DFTElement

DFT element

property id

Id

property name

Name

class DFTSymmetries

Symmetries in DFT

property groups

Symmetry groups

class ParametricDFT

Parametric DFT

can_have_nondeterminism(self: stormpy.dft.dft.ParametricDFT) bool

Whether the model can contain non-deterministic choices

get_element(self: stormpy.dft.dft.ParametricDFT, index: int) stormpy.dft.dft.ParametricDFTElement

Get DFT element at index

get_element_by_name(self: stormpy.dft.dft.ParametricDFT, name: str) stormpy.dft.dft.ParametricDFTElement

Get DFT element by name

modularisation(self: stormpy.dft.dft.ParametricDFT) List[stormpy.dft.dft.ParametricDFT]

Split DFT into independent modules

nr_be(self: stormpy.dft.dft.ParametricDFT) int

Number of basic elements

nr_dynamic(self: stormpy.dft.dft.ParametricDFT) int

Number of dynamic elements

nr_elements(self: stormpy.dft.dft.ParametricDFT) int

Total number of elements

symmetries(self: stormpy.dft.dft.ParametricDFT) storm::storage::DFTIndependentSymmetries

Compute symmetries in DFT

property top_level_element

Get top level element

class ParametricDFTElement

Parametric DFT element

property id

Id

property name

Name

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

analyze_dft(dft: stormpy.dft.dft.DFT, properties: List[stormpy.logic.logic.Formula], symred: bool=True, allow_modularisation: bool=False, relevant_events: stormpy.dft.dft.RelevantEvents=<stormpy.dft.dft.RelevantEvents object at 0x7f930be028f0>, allow_dc_for_relevant: bool=False) List[float]

Analyze the DFT

compute_dependency_conflicts(dft: stormpy.dft.dft.DFT, use_smt: bool = False, solver_timeout: float = 0) bool

Set conflicts between FDEPs. Is used in analysis.

compute_relevant_events(dft: stormpy.dft.dft.DFT, 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, path: str) None

Export DFT to JSON file

export_dft_json_string(dft: stormpy.dft.dft.DFT) str

Export DFT to JSON string

is_well_formed(dft: stormpy.dft.dft.DFT, check_valid_for_analysis: bool = True) Tuple[bool, str]

Check whether DFT is well-formed.

load_dft_galileo_file(path: str) stormpy.dft.dft.DFT

Load DFT from Galileo file

load_dft_json_file(path: str) stormpy.dft.dft.DFT

Load DFT from JSON file

load_dft_json_string(json_string: str) stormpy.dft.dft.DFT

Load DFT from JSON string

transform_dft(dft: stormpy.dft.dft.DFT, unique_constant_be: bool, binary_fdeps: bool) stormpy.dft.dft.DFT

Apply transformations on DFT