Functor Validator.Make


module Make: 
functor (A : Model.S) -> sig .. end
Functor providing inductive invariant checking and path feasibility checking functions for a given model.
Parameters:
A : Model.S


Invariant Checking



Potential invariants are represented as lists of symbolic states of the model. Such a list stands for the union of its elements. Thus if a location does not appear in the list, then its associated region is the empty region Region.bot.
val is_safe_fwd_invariant : A.State.t list -> bool
is_safe_fwd_invariant l returns true if l is a safe forward inductive invariant:
  • l contains all initial symbolic states of the model, and
  • l is a post-fixpoint of the model's post image operator, and
  • l is disjoint from all error symbolic states of the model.

val is_safe_bwd_invariant : A.State.t list -> bool
is_safe_bwd_invariant l returns true if l is a safe backward inductive invariant:
  • l contains all error symbolic states of the model, and
  • l is a post-fixpoint of the model's pre image operator, and
  • l is disjoint from all initial symbolic states of the model.


Path Feasibility Checking



A path is a list of contiguous transitions of the model's automaton. A path [t1; ...; tN] is feasible if we can insert (N+1) environments between the transitions of the path such that these environments respect the semantics of the commands labeling the transitions of the path.
val is_empty_path_feasible : unit -> bool
is_empty_path_feasible () returns true if there is a non empty intersection between initial and error symbolic states of the model.
val is_non_empty_path_fwd_feasible : A.Automaton.Transition.t list -> bool
is_non_empty_path_fwd_feasible p returns true if p is a non empty path that is feasible. Feasibility checking is performed with a forward post computation along the path.
val is_non_empty_path_bwd_feasible : A.Automaton.Transition.t list -> bool
is_non_empty_path_bwd_feasible p returns true if p is a non empty path that is feasible. Feasibility checking is performed with a backward pre computation along the path.