Functor Validator.Make
module Make:Functor providing inductive invariant checking and path feasibility checking functions for a given model.
| Parameters: |
|
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 -> boolis_safe_fwd_invariant l returns true if l is a safe forward inductive
invariant:
lcontains all initial symbolic states of the model, andlis a post-fixpoint of the model's post image operator, andlis disjoint from all error symbolic states of the model.
val is_safe_bwd_invariant : A.State.t list -> boolis_safe_bwd_invariant l returns true if l is a safe backward inductive
invariant:
lcontains all error symbolic states of the model, andlis a post-fixpoint of the model's pre image operator, andlis 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 -> boolis_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 -> boolis_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 -> boolis_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.