Module Property

type prop_status =
  1. | PropUnknown
    (*

    Status of property is unknown

    *)
  2. | PropKTrue of int
    (*

    Property is true for at least k steps

    *)
  3. | PropInvariant of Certificate.t
    (*

    Property is true in all reachable states

    *)
  4. | PropFalse of (StateVar.t * Model.value list) list
    (*

    Property is false at some step

    *)

Current status of a property

type prop_bound =
  1. | From of int
  2. | Within of int
  3. | At of int
  4. | FromWithin of int * int
type prop_kind =
  1. | Invariant
  2. | Reachable of prop_bound option
type t = {
  1. prop_name : string;
    (*

    Identifier for the property

    *)
  2. prop_source : prop_source;
    (*

    Source of the property

    *)
  3. prop_kind : prop_kind;
    (*

    Kind of property (do we wish to prove it invariant or reachable)

    *)
  4. prop_term : Term.t;
    (*

    Term with variables at offsets prop_base and prop_base - 1

    *)
  5. prop_expr : string option;
  6. mutable prop_status : prop_status;
    (*

    Current status

    *)
}

A property of a transition system

and generated_source =
  1. | Contract
  2. | Body
and prop_source =
  1. | PropAnnot of Lib.position
    (*

    Property is from an annotation

    *)
  2. | Generated of Lib.position option * StateVar.t list * generated_source
    (*

    Property was generated, for example, from a subrange constraint

    *)
  3. | Instantiated of Scope.t * Lib.position * t
    (*

    Property is an instance of a property in a called node.

    Reference the instantiated property by the scope of the subsystem and the name of the property

    *)
  4. | Assumption of Lib.position * Scope.t * Lib.position
    (*

    Contract assumption that a caller has to prove.

    Reference the assumption by its position, the scope of the subsystem, and the position of the node call

    *)
  5. | Guarantee of Lib.position * Scope.t
    (*

    Contract guarantees.

    *)
  6. | GuaranteeOneModeActive of Lib.position * Scope.t
    (*

    Contract: at least one mode active.

    *)
  7. | GuaranteeModeImplication of Lib.position * Scope.t
    (*

    Contract: mode implication.

    *)
  8. | NonVacuityCheck of Lib.position * Scope.t
    (*

    Non-vacuity check

    *)
  9. | TerminationCheck of Lib.position
    (*

    Termination check

    *)
  10. | Candidate of prop_source option
    (*

    User supplied candidate invariant

    *)

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 is_candidate : t -> bool

Returns true iff the input property is a candidate property

val is_real : t -> bool

Returns true iff the input property is not a candidate property

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 pp_print_generated_source : Stdlib.Format.formatter -> generated_source -> unit
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
val get_prop_original_source : t -> prop_source
val get_prop_term : t -> Term.t
val get_pos_from_prop_source : prop_source -> Lib.position option