~james/reorder

reorder/src/engine.mli -rw-r--r-- 1.3 KiB
735c0c8f — james chore(import): snapshot james.dad.town/reorder at c27220bf810c 14 hours ago 
                                                                                
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33

type witness = {
  case : Syntax.t;
  model : Syntax.model;
  bound : int;
  fences : Syntax.location list;
  actors : int array;
}
type result = { witness : witness option; query : Solver.query }
type phase = Searching of int * Syntax.location list
  | Counterexample of witness | Excluded of int | Refining of int
  | Verified of Syntax.location list * int * int
type repair = {
  case : Syntax.t;
  fences : Syntax.location list;
  clauses : int list list;
  rounds : int;
  bound : int;
  states : int;
}
val check : ?timeout:int -> ?tick:(unit -> unit) -> ?bound:int ->
  ?fences:Syntax.location list -> ?folder:string -> ?fixed:int array ->
  Syntax.t -> Syntax.model -> result
val witness_sexp : witness -> Sexp.t
val load_witness : string -> witness
val replay : witness -> Machine.t array * Machine.event array
val save : string -> result -> unit
val repair : ?timeout:int -> ?tick:(unit -> unit) -> ?notify:(phase -> unit) ->
  Syntax.t -> string -> repair option
val load_repair : string -> repair
val certify : ?timeout:int -> ?tick:(unit -> unit) -> string -> repair
val audit : ?timeout:int -> ?tick:(unit -> unit) -> string -> string -> repair
val validate_schedule : ?timeout:int -> Syntax.t -> Syntax.location list -> int array -> unit
val outcomes : ?timeout:int -> ?tick:(unit -> unit) -> Syntax.t -> Syntax.model -> (int64 * int64) list