Module Enumerative (.ml)

module Enumerative: sig .. end

Enumerative forward search

val search : Variable.t list -> Ast.t_system -> unit

search procs init performs enumerative forward search. States are stored in an internal hash-table.

val resume_search_from : Variable.t list -> Ast.t_system -> unit

val replay_trace_and_expand : Variable.t list -> Ast.t_system -> Node.t -> unit

val smallest_to_resist_on_trace : Node.t list -> Node.t list

Given a list of candidate approximations (and their permutations), checks if one is satisfiable on the finite model constructed by search.

Exported functions to construct enumeration based oracles

type env

The type of environments for enumerative explorations

type state = private int array

The type of states, we allow states to be constructed from the outside by calling the function new_undef_state.

val print_state : env -> Format.formatter -> state -> unit

Printing a state. It is decoded to an SAtom in a very inefficient manner. This function should only be used for debugging.

val empty_env : env

A dummy empty environment.

val mk_env : int -> Ast.t_system -> env

mk_env nb sys creates an environment for the enumerative exploration of the transition system sys with a fixed number nb of processes.

val int_of_term : env -> Types.term -> int

Encoding of a term in the enumerative environment.

val next_id : env -> int

Returns the next free integer that is not used for encoding terms.

val new_undef_state : env -> state

Returns a new uninitialized state from an enumertive environment

val empty_state : state

A dummy empty state.

val register_state : env -> state -> unit

val size_of_env : env -> int

Returns the (heuristically) computed size of tables needed for the exploration.

val no_scan_states : env -> unit

Prevent the GC from scanning the list of states stored in the environemnt as it is going to be kept in memory all the time. Call this function once the exploration is finished.

val print_last : env -> unit

Oracle interface

see Oracle.S

include Oracle.S