Module Forward (.ml)

module Forward: sig .. end

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 (Types.SAtom.t * Ast.transition_info * Variable.subst * Types.SAtom.t) 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 replay_history : Ast.t_system ->
       Node.t ->
       (Types.SAtom.t * Ast.transition_info * Variable.subst * Types.SAtom.t) list
       option

Replays the history of a faulty node and returns (possibly) an error trace

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