Module Forward (.ml)

module Forward: sig .. end
Symbolic forward exploration


Symbolic forward exploration
module HSA: Hashtbl.S  with type key = SAtom.t
module MA: Map.S  with type key = Atom.t
type inst_trans = {
   i_reqs : Types.SAtom.t;
   i_udnfs : Types.SAtom.t list list;
   i_actions : Types.SAtom.t;
   i_touched_terms : Types.Term.Set.t;
}
the type of instantiated transitions
type possible_result = 
| Reach of (Ast.transition_info * Variable.subst) list
| Spurious of Ast.trace
| Unreach
val all_var_terms : Variable.t list -> Ast.t_system -> Types.Term.Set.t
val search : Hstring.t list -> Ast.t_system -> unit HSA.t
val search_stateless : Hstring.t list ->
Ast.t_system -> (Types.SAtom.t * Types.Term.Set.t) MA.t
val instantiate_transitions : Variable.t list ->
Variable.t list -> Ast.transition list -> inst_trans list
instantiate transitions with a list of possible parameters
val abstract_others : Types.SAtom.t -> Hstring.t list -> Types.SAtom.t
val reachable_on_trace_from_init : Ast.t_system -> Node.t -> Ast.trace -> possible_result
val spurious : Node.t -> bool
check if the history of a node is spurious
val spurious_error_trace : Ast.t_system -> Node.t -> bool
check if an error trace is spurious
val spurious_due_to_cfm : Ast.t_system -> Node.t -> bool
check if an error trace is spurious due to the Crash Failure Model
val conflicting_from_trace : Ast.t_system -> Ast.trace -> Types.SAtom.t list
check if an error trace is spurious due to the Crash Failure Model
val uguard_dnf : Variable.subst ->
Variable.t list ->
Variable.t list ->
(Variable.t * Types.SAtom.t list) list -> Types.SAtom.t list list
put a universal guard in disjunctive normal form