Flags.Contracts
val compositional : unit -> bool
Compositional analysis.
val translate_contracts : unit -> string option
Translate contracts.
val check_modes : unit -> bool
Check modes.
val check_environment : unit -> bool
Check realizability of node environments.
val check_implem : unit -> bool
val contract_gen : unit -> bool
Contract generation.
val contract_gen_depth : unit -> int
Contract generation: max depth.
val assumption_gen : unit -> bool
Assumption generation.
val two_state_assumption : unit -> bool
val assumption_gen_iter : unit -> int
Assumption generation: generalization iterations
val refinement : unit -> bool
Activate refinement.
val print_deadlock : unit -> bool
Print deadlocking trace and a conflict
val dump_deadlock : unit -> bool
Dump deadlocking trace to a file *
val check_contract_is_sat : unit -> bool
Check whether a unrealizable contract is satisfiable
val print_viable_states : unit -> bool