DFTTraceSimulator

Warning

The stormpy developer API is internal and can be subject to change.

class DFTTraceSimulator[ValueType](

dft,

state_generation_info: stormpy.dft.developer.DFTStateGenerationInfo,

generator: stormpy.dft.developer.RandomGenerator,

)

Simulator for DFT traces

Template arguments:

• ValueType (type)

Available specializations:

• DFTTraceSimulator[float]

• DFTTraceSimulator[stormpy.numbers.RationalFunction]

Construction

Create Simulator

The specialization can be inferred from the first positional constructor argument (alternatively, the dft keyword argument).

Members

DFTTraceSimulator.get_state(self: stormpy.dft.developer.DFTTraceSimulator[ValueType])

Get current state

DFTTraceSimulator.get_time(self: stormpy.dft.developer.DFTTraceSimulator[ValueType]) → float

Get total elapsed time so far

DFTTraceSimulator.random_step(

self: stormpy.dft.developer.DFTTraceSimulator[ValueType],

) → stormpy.dft.SimulationStepResult

Perform random simulation step.

DFTTraceSimulator.reset(self: stormpy.dft.developer.DFTTraceSimulator[ValueType]) → None

Reset to initial state

DFTTraceSimulator.reset_state(

self: stormpy.dft.developer.DFTTraceSimulator[ValueType],

state,

) → None

Reset to state

DFTTraceSimulator.simulate_trace(

self: stormpy.dft.developer.DFTTraceSimulator[ValueType],

timebound: SupportsFloat | SupportsIndex,

) → stormpy.dft.SimulationTraceResult

Simulate complete trace for given timebound

DFTTraceSimulator.step(

self: stormpy.dft.developer.DFTTraceSimulator[ValueType],

next_failure,

dependency_success: bool = True,

) → stormpy.dft.SimulationStepResult

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