Module Flags.IVC

Inductive Validity Cores

type minimize_mode = [
  1. | `DO_NOT_MINIMIZE
  2. | `VALID_LUSTRE
  3. | `CONCISE
]
type ivc_element = [
  1. | `NODE_CALL
  2. | `CONTRACT_ITEM
  3. | `EQUATION
  4. | `ASSERTION
  5. | `ANNOTATIONS
]
val compute_ivc : unit -> bool

Enable computation of Inductive Validity Cores

val ivc_all : unit -> bool
val ivc_category : unit -> ivc_element list

Specify on which elements we want to minimize

val print_ivc : unit -> bool

Print the model elements of the computed IVC

val print_ivc_compl : unit -> bool

Print the model elements NOT in the computed IVC

val ivc_approximate : unit -> bool

If true, compute an approximation of a MIVC

val ivc_must_set : unit -> bool

If true, compute the MUST set first and compute the IVCs starting from it

val ivc_smallest_first : unit -> bool

If true, compute a smallest IVC first

val ivc_only_main_node : unit -> bool

If true, compute IVC over elements of the main node only

val ivc_precomputed_mcs : unit -> int

Parameter k of the UMIVC algorithm. Correspond to the parameter 'k' of the implementation UMIVC. In particular, the value 0 implements the MARCO algorithm, and the value -1 (infinity) implements the CAMUS algorithm.

val ivc_per_property : unit -> bool

If true, IVCs will be computed for each properties separately

val minimize_program : unit -> minimize_mode

Generate a minimize lustre program

val minimized_program_dir : unit -> string

The directory where minimized programs should be saved

val ivc_uc_timeout : unit -> int

Timeout for unsat core computation

val ivc_disable_must_opt : unit -> bool

DEBUG flag: disable the must-set optimisation (ignored if ivc_must_set is true)