Module TestgenLib

module TestgenLib: sig .. end
Turns an actlit uf in a term.

type sys = TransSys.t 
type svar = StateVar.t 
type actlit = UfSymbol.t 
type term = Term.t 
type model = Model.t 
type values = (Term.t * Term.t) list 
type k = Numeral.t 
val term_of : actlit -> term
Turns an actlit uf in a term.
val list_eq : 'a list -> 'a list -> bool
Compares two lists using physical equality.
type 'data context = {
   sys : sys;
   declare : actlit -> unit;
   actlit_implications : ?eq:bool -> (actlit * term) list -> unit;
   checksat_getvalues : actlit list -> term list -> values option;
   trace_comment : string -> unit;
   mutable data : 'data;
}
Gathers the contracts, the actions a strategy can perform on the underlying smt solver used for test generation, and some data a strategy generates tests from.
val mk_context : 'data ->
sys ->
(actlit -> unit) ->
(?eq:bool -> (actlit * term) list -> unit) ->
(actlit list -> term list -> values option) ->
(string -> unit) -> 'data context
Construction helper for context.
val declare : 'data context -> actlit -> unit
Calls the declare field of a context on its input list of actlit / term pair.
val activate : 'data context ->
?eq:bool -> (actlit * term) list -> unit
Calls the actlit_implications field of a context on its input list of actlit / term pair.
val get_values : 'data context ->
actlit list -> term list -> values option
Calls the checksat_getvalues field of a context on its input list of actlits.
val comment : 'data context -> string -> unit
Calls the trace_comment field of a context on its input string.
val cex_to_inputs_csv : Format.formatter ->
sys -> model -> k -> unit
Converts a model to the system's input values in csv.
val cex_to_outputs_csv : Format.formatter ->
sys -> model -> k -> unit
Converts a model to the system's output values in csv.
type contract_testcase = (k * svar list) list 
A contract test case is a list of numeral / term pairs such that
type contract_testcases = (actlit * k * contract_testcase) list 
A map from actlits to contract test cases.
val pp_print_contract_testcase : Format.formatter -> contract_testcase -> unit
Pretty prints a test case.
val pp_print_contract_testcase_named : sys -> Format.formatter -> contract_testcase -> unit
Pretty prints a test case with the name of the modes it triggers.
val pp_print_contract_testcases : Format.formatter -> contract_testcases -> unit
Pretty prints a list of test cases.
val pp_print_contract_testcases_named : sys -> Format.formatter -> contract_testcases -> unit
Pretty prints a list of test cases with the name of the modes they trigger.
val description_of_contract_testcase : sys ->
actlit * k * contract_testcase ->
string list
Constructs the text description of a test case.
type tree = 
| Branch of (string list * tree) list
| Leaf of string list list
Tree structure to display the tree of activable modes.
val pp_print_tree : Format.formatter -> tree -> unit
Pretty printer for the tree structure.
val testcases_to_tree : sys -> contract_testcases -> tree
Converts some test cases to a tree.
val unroll_test_case : contract_testcase ->
k -> contract_testcase -> contract_testcase
Constructs the explicit unrolling of a test case.
val extend_contract_testcases : contract_testcases context ->
k -> contract_testcases
Extends some test cases: creates the new test cases made of the input ones extended with one transition to whatever mode they can activate.

The input is a context, where the data is the tree of activable modes in k transitions from the initial state. A test case is a path in this tree. This function considers each test case and checks which modes it can reach in one transition. A new test case is created for each mode each test case can reach.

val testcase_gen : string ->
string ->
(string -> string -> string -> string list -> 'a) ->
contract_testcases context ->
(actlit list -> model option) -> unit
Generates the actual test cases in csv using a get-model function. Arguments: