Module `Flags.MCS`

Minimal Cut Sets

type mcs_element = [ | `NODE_CALL | `CONTRACT_ITEM | `EQUATION | `ASSERTION | `ANNOTATIONS ]

val compute_mcs : unit -> bool: Enable computation of Minimal Cut Sets

val mcs_all : unit -> bool: Specify whether all the Minimal Cut Sets must be computed or just one

val mcs_category : unit -> mcs_element list: Specify on which elements we want to minimize

val mcs_max_cardinality : unit -> int: Only search for MCSs of cardinality lower or equal to this parameter

val print_mcs : unit -> bool: Print the model elements of the computed MCS

val print_mcs_compl : unit -> bool: Print the model elements NOT in the computed MCS

val print_mcs_legacy : unit -> bool: Print the MCS using the legacy format

val print_mcs_counterexample : unit -> bool: Print the counterexample found for each MCS

val mcs_only_main_node : unit -> bool: If true, compute MCS over elements of the main node only

val mcs_per_property : unit -> bool: If true, MCSs will be computed for each properties separately