create_filter

create_filter(

model,

expression: Expression,

) → SymbolicQualitativeCheckResult

Create a filter selecting the states of a symbolic model satisfying the given expression.

The filter can be applied to a model checking result via result.filter(filter).

Parameters:

• model – The symbolic model.

• expression – Boolean expression over the model variables.

Returns:

Qualitative check result containing the states satisfying the expression.