src/HOL/TLA/Memory/MemClerk.thy

A formalization of TLA in HOL -- by Stephan Merz;

(*
    File:        MemClerk.thy
    Author:      Stephan Merz
    Copyright:   1997 University of Munich

    Theory Name: MemClerk
    Logic Image: TLA

    RPC-Memory example: specification of the memory clerk.
*)

MemClerk = Memory + RPC + MemClerkParameters +

types
  (* The clerk takes the same arguments as the memory and sends requests to the RPC *)
  mClkSndChType = "memChType"
  mClkRcvChType = "rpcSndChType"
  mClkStType    = "(PrIds => mClkState) stfun"

consts
  (* state predicates *)
  MClkInit      :: "mClkRcvChType => mClkStType => PrIds => stpred"

  (* actions *)
  MClkFwd       :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action"
  MClkRetry     :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action"
  MClkReply     :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action"
  MClkNext      :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action"

  (* temporal *)
  MClkIPSpec    :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => temporal"
  MClkISpec     :: "mClkSndChType => mClkRcvChType => mClkStType => temporal"

rules
  MClkInit_def     "$(MClkInit rcv cst p) .=
                        ($(cst@p) .= #clkA  .&  .~ $(Calling rcv p))"

  MClkFwd_def      "MClkFwd send rcv cst p ==
                        $(Calling send p)
                        .& $(cst@p) .= #clkA
                        .& Call rcv p (MClkRelayArg[ arg[$(send@p)] ])
                        .& (cst@p)$ .= #clkB
                        .& unchanged (rtrner send @ p)"

  MClkRetry_def    "MClkRetry send rcv cst p ==
                        $(cst@p) .= #clkB
                        .& res[$(rcv@p)] .= #RPCFailure
                        .& Call rcv p (MClkRelayArg[ arg[$(send@p)] ])
                        .& unchanged <cst@p, rtrner send @ p>"

  MClkReply_def    "MClkReply send rcv cst p ==
                        .~ $(Calling rcv p)
                        .& $(cst@p) .= #clkB
                        .& Return send p (MClkReplyVal[ res[$(rcv@p)] ])
                        .& (cst@p)$ .= #clkA
                        .& unchanged (caller rcv @ p)"

  MClkNext_def     "MClkNext send rcv cst p ==
                        MClkFwd send rcv cst p
                        .| MClkRetry send rcv cst p
                        .| MClkReply send rcv cst p"

  MClkIPSpec_def   "MClkIPSpec send rcv cst p ==
                        Init($(MClkInit rcv cst p))
                        .& [][ MClkNext send rcv cst p ]_<cst@p, rtrner send @ p, caller rcv @ p>
                        .& WF(MClkFwd send rcv cst p)_<cst@p, rtrner send @ p, caller rcv @ p>
                        .& SF(MClkReply send rcv cst p)_<cst@p, rtrner send @ p, caller rcv @ p>"

  MClkISpec_def    "MClkISpec send rcv cst == RALL p. MClkIPSpec send rcv cst p"
end