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.
__str__(self: stormpy.dft.dft.DFTElementType) -> str
__str__(self: handle) -> str
- property value¶
- 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
- 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: float) 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¶
Simulator for DFT traces
- 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: float) 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: 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 0x7f04ab9dcd70>) 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 0x7f04abbb5cb0>) 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 SimulationStepResult¶
Members:
SUCCESSFUL
UNSUCCESSFUL
INVALID
- INVALID = <SimulationStepResult.INVALID: 2>¶
- SUCCESSFUL = <SimulationStepResult.SUCCESSFUL: 0>¶
- UNSUCCESSFUL = <SimulationStepResult.UNSUCCESSFUL: 1>¶
- property name¶
- property value¶
- class SimulationTraceResult¶
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: 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)¶