SMTMinimalLabelSetGeneratorOptions

Warning

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

class SMTMinimalLabelSetGeneratorOptions[ValueType](check_threshold_feasible: bool = False)

Options for highlevel counterexample generation

Template arguments:

• ValueType (type)

Available specializations:

• SMTMinimalLabelSetGeneratorOptions[float]

Construction

The default specialization is SMTMinimalLabelSetGeneratorOptions[float].

Members

property SMTMinimalLabelSetGeneratorOptions.add_backward_implication_cuts

property SMTMinimalLabelSetGeneratorOptions.check_threshold_feasible

property SMTMinimalLabelSetGeneratorOptions.continue_after_first_counterexample_until

property SMTMinimalLabelSetGeneratorOptions.encode_reachability

property SMTMinimalLabelSetGeneratorOptions.maximum_counterexamples

property SMTMinimalLabelSetGeneratorOptions.maximum_extra_iterations

property SMTMinimalLabelSetGeneratorOptions.silent

property SMTMinimalLabelSetGeneratorOptions.use_dynamic_constraints