SMTMinimalLabelSetGenerator

Warning

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

class SMTMinimalLabelSetGenerator[ValueType]

Highlevel Counterexample Generator with SMT as backend

Template arguments:

• ValueType (type)

Available specializations:

• SMTMinimalLabelSetGenerator[float]

Members

static SMTMinimalLabelSetGenerator.compute_counterexample_label_set(

env,

stats: stormpy.developer.SMTMinimalLabelSetGeneratorStats[float],

symbolic_model: stormpy.io.SymbolicModelDescription,

model: stormpy.models.SparseModel[float],

counterex_input,

dont_care_labels: stormpy.developer.FlatSet,

options: stormpy.developer.SMTMinimalLabelSetGeneratorOptions[float],

) → list[stormpy.developer.FlatSet]

Compute counterexample

static SMTMinimalLabelSetGenerator.precompute(

env,

symbolic_model: stormpy.io.SymbolicModelDescription,

model: stormpy.models.SparseModel[float],

formula: stormpy.logic.Formula,

)

Precompute input for counterexample generation