Module type TestgenStrategies.Sig

module type Sig = sig .. end
Signature for test generation strategies. The idea is let the strategy work on the solver (work function) using the actions on the solver given by an actions record. Function work returns false if it is ot done, i.e. the system should be unrolled and work called again.

type data 
Type for the data of the strategy.
val prefix : string
Prefix which should be unique to a strategy. The supervisor should check that no two strategy have the same prefix to avoid test-case filename collisions.
val name : string
Name of the strategy, for logging.
val out_dir : string
val no_stuttering : bool
Returns true if the strategy requires succeeding input tuples to be different.
val abstract_subsystems : bool
Returns true if the strategy requires subsystems to be abstracted.
val mk_context : TestgenLib.sys ->
(TestgenLib.actlit -> unit) ->
(?eq:bool -> (TestgenLib.actlit * TestgenLib.term) list -> unit) ->
(TestgenLib.actlit list -> TestgenLib.term list -> TestgenLib.values option) ->
(string -> unit) -> data TestgenStrategies.context
Creates a context for this strategy.
val work : data TestgenStrategies.context -> TestgenLib.k -> bool
Works on the k^th unrolling of the system. Returns false if the strategy is not done, i.e. its handler should unroll the system further and call this function again.

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