Module `Property`

type prop_status = | PropUnknown | PropKTrue of int | PropInvariant of Certificate.t | PropFalse of (StateVar.t * Model.value list) list: Current status of a property

type t = { prop_name : string; prop_source : prop_source; prop_term : Term.t; mutable prop_status : prop_status; }: A property of a transition system

and prop_source = | PropAnnot of Lib.position | Generated of StateVar.t list | Instantiated of Scope.t * t | Assumption of Lib.position * string list | Guarantee of Lib.position * Scope.t | GuaranteeOneModeActive of Lib.position * Scope.t | GuaranteeModeImplication of Lib.position * Scope.t | Candidate of prop_source option: Source of a property

val copy : t -> t
val pp_print_prop_source : Stdlib.Format.formatter -> prop_source -> unit: Pretty-prints a property source.

val pp_print_prop_status : Stdlib.Format.formatter -> prop_status -> unit: Pretty-prints a property status.

val pp_print_prop_quiet : Stdlib.Format.formatter -> t -> unit: Pretty-prints a property (name and source only).

val pp_print_property : Stdlib.Format.formatter -> t -> unit: Pretty-prints a property.

val prop_status_known : prop_status -> bool: Return true if the status of the property is known

val set_prop_status : t -> prop_status -> unit
val set_prop_invariant : t -> Certificate.t -> unit
val set_prop_ktrue : t -> int -> unit
val set_prop_false : t -> (StateVar.t * Model.value list) list -> unit
val set_prop_unknown : t -> unit
val length_of_cex : (StateVar.t * Model.value list) list -> int
val get_prop_status : t -> prop_status