type instruction =
  | Store of int * int64 | Load of int * int | Fence
  | Move of int * int64 | Branch of int * int64 * int
  | Enter | Leave | Exchange of int * int * int64

type goal = Overlap | Outcome of {
  registers : (int * int * int64) list;
  memory : (int * int64) list;
  drained : bool;
}

type model = Sc | Tso
type location = int * int
type t = {
  name : string;
  names : string array;
  bound : int;
  threads : instruction array array;
  candidates : location list;
  goal : goal;
}

val validate : t -> unit
val decode : Sexp.t -> t
val encode : t -> Sexp.t
val load : string -> t
val instruction : instruction -> Sexp.t
val location : Sexp.t -> location
val model : string -> model
val model_name : model -> string