BisimulationOptions¶

class BisimulationOptions(self: stormpy.transformations.BisimulationOptions)¶

Bases: pybind11_object

Options for bisimulation on sparse models

Create default options

property action_sensitive¶: Whether matching choices must occur at identical positions

property bisimulation_type¶: Type of bisimulation

property create_quotient_choice_mapping¶: Whether to create a mapping from quotient to original choices

property prefer_signature_refinement¶: Whether to prefer signature-based over splitter-based refinement

property preserve_all_rewards¶: Whether to preserve all reward models. If None, then all rewards are preserved iff no formula is given

property preserve_choice_labels¶: Whether to preserve choice labels

property preserve_choice_origins¶: Whether to preserve choice origins

property state_label_preservation¶: Which state labels to preserve

property tolerance¶: Maximum permitted numerical deviation in values (probabilities, rates, rewards) between the original and quotient model