type origin = Memory | Buffer
type event = Idle | Drain of int * int * int64
  | Issue of int * int * Syntax.instruction * origin option
type t = {
  pc : int array;
  regs : int64 array array;
  memory : int64 array;
  buffers : (int * int64) list array;
  critical : bool array;
}
val initial : Syntax.t -> t
val step : Syntax.t -> Syntax.model -> Syntax.location list -> t -> int -> (t * event) option
val replay : Syntax.t -> Syntax.model -> Syntax.location list -> int array -> t array * event array
val observations : t -> int64 list
val bad : Syntax.t -> t -> bool
val reachable : Syntax.t -> Syntax.model -> Syntax.location list -> int -> bool * int
val reschedule : Syntax.t -> Syntax.location list -> int array -> int array
type graph = { states : t array; parents : (int * int) array; edges : int; violations : int list }
val explore : ?limit:int -> ?visit:(t -> int -> unit) -> Syntax.t ->
  Syntax.model -> Syntax.location list -> graph
val counterexample : graph -> int array option