MyMonadicSMemory (transformers.States.MyMonadicSMemory)

module Containers = Gillian.Utils.Containers

module DR = Gillian.Monadic.Delayed_result

module Recovery_tactic = Gillian.General.Recovery_tactic

module type S = sig ... end

module Defaults : sig ... end

module type ID = sig ... end

A custom Init Data module; agnostic of the data format. Comes with a callback, that is called whenever memory is initialised with some init data.

module DummyID : ID with type t = unit

module Make
  (Mem : S)
  (ID : ID) : 
  Gillian.Monadic.MonadicSMemory.S with type init_data = ID.t

Functor to convert composable, typed state models into Gillian monadic state models