Module type Controller_itp.Scheduler

module type Scheduler = sig .. end

Any module of this signature should implement a scheduler, that allows the register functions to call, and call them depending on some time constraints: after a given delay, or simply when there is no more tasks with higher priority.

val blocking : bool

Set to true when the scheduler should wait for results of why3server (script), false otherwise (ITP which needs reactive scheduling)

val multiplier : int

Number of allowed task given to why3server is this number times the number of allowed proc on the machine.

val timeout : ms:int -> (unit -> bool) -> unit

timeout ~ms f registers the function f as a function to be called every ms milliseconds. The function is called repeatedly until it returns false. the ms delay is not strictly guaranteed: it is only a minimum delay between the end of the last call and the beginning of the next call. Several functions can be registered at the same time.

val idle : prio:int -> (unit -> bool) -> unit

idle prio f registers the function f as a function to be called whenever there is nothing else to do. Several functions can be registered at the same time. Several functions can be registered at the same time. Functions registered with higher priority will be called first.