perform_prob01_min

Warning

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

perform_prob01_min(

model: stormpy.developer.storage._storage._SparseNondeterministicModel_Double,

phi_states: stormpy.datastructures.BitVector,

psi_states: stormpy.datastructures.BitVector,

) → tuple[stormpy.datastructures.BitVector, stormpy.datastructures.BitVector]

perform_prob01_min(

model: stormpy.developer.storage._storage._SparseNondeterministicModel_Rational,

phi_states: stormpy.datastructures.BitVector,

psi_states: stormpy.datastructures.BitVector,

) → tuple[stormpy.datastructures.BitVector, stormpy.datastructures.BitVector]

perform_prob01_min(

model: stormpy.developer.storage._storage._SparseNondeterministicModel_RationalFunction,

phi_states: stormpy.datastructures.BitVector,

psi_states: stormpy.datastructures.BitVector,

) → tuple[stormpy.datastructures.BitVector, stormpy.datastructures.BitVector]

Compute states with minimal probability 0 and 1 of satisfying phi until psi

Compute states with minimal probability 0 and 1 of satisfying phi until psi

Compute states with minimal probability 0 and 1 of satisfying phi until psi