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 -> 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, andl
is a post-fixpoint of the model's post image operator, andl
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, andl
is a post-fixpoint of the model's pre image operator, andl
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.