Module Flags.IVC
Inductive Validity Cores
type minimize_mode
=[
|
`DO_NOT_MINIMIZE
|
`VALID_LUSTRE
|
`CONCISE
]
type ivc_element
=[
|
`NODE_CALL
|
`CONTRACT_ITEM
|
`EQUATION
|
`ASSERTION
|
`ANNOTATIONS
]
val ivc_all : unit -> bool
val ivc_category : unit -> ivc_element list
Specify on which elements we want to minimize
val ivc_must_set : unit -> bool
If true, compute the MUST set first and compute the IVCs starting from it
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 minimize_program : unit -> minimize_mode
Generate a minimize lustre program