Module Property

module Property: sig .. end
Current status of a property

type prop_status = 
| PropUnknown
| PropKTrue of int
| PropInvariant of Certificate.t
| PropFalse of (StateVar.t * Model.value list) list
type t = {
   prop_name : string;
   prop_source : prop_source;
   prop_term : Term.t;
   mutable prop_status : prop_status;
}
A property of a transition system
type 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 pp_print_prop_source : Format.formatter -> prop_source -> unit
Pretty-prints a property source.
val pp_print_prop_status : Format.formatter -> prop_status -> unit
Pretty-prints a property status.
val pp_print_prop_quiet : Format.formatter -> t -> unit
Pretty-prints a property (name and source only).
val pp_print_property : 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 length_of_cex : (StateVar.t * Model.value list) list -> int
val get_prop_status : t -> prop_status