src/HOL/TLA/Memory/MemClerk.thy
author wenzelm
Fri Oct 05 23:58:52 2001 +0200 (2001-10-05)
changeset 11703 6e5de8d4290a
parent 9517 f58863b1406a
child 17309 c43ed29bd197
permissions -rw-r--r--
tuned;
     1 (*
     2     File:        MemClerk.thy
     3     Author:      Stephan Merz
     4     Copyright:   1997 University of Munich
     5 
     6     Theory Name: MemClerk
     7     Logic Image: TLA
     8 
     9     RPC-Memory example: specification of the memory clerk.
    10 *)
    11 
    12 MemClerk = Memory + RPC + MemClerkParameters +
    13 
    14 types
    15   (* The clerk takes the same arguments as the memory and sends requests to the RPC *)
    16   mClkSndChType = "memChType"
    17   mClkRcvChType = "rpcSndChType"
    18   mClkStType    = "(PrIds => mClkState) stfun"
    19 
    20 constdefs
    21   (* state predicates *)
    22   MClkInit      :: "mClkRcvChType => mClkStType => PrIds => stpred"
    23      "MClkInit rcv cst p == PRED (cst!p = #clkA  &  ~Calling rcv p)"
    24 
    25   (* actions *)
    26   MClkFwd       :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action"
    27      "MClkFwd send rcv cst p == ACT
    28                            $Calling send p
    29                          & $(cst!p) = #clkA
    30                          & Call rcv p MClkRelayArg<arg<send!p>>
    31                          & (cst!p)$ = #clkB
    32                          & unchanged (rtrner send!p)"
    33 
    34   MClkRetry     :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action"
    35      "MClkRetry send rcv cst p == ACT
    36                            $(cst!p) = #clkB
    37                          & res<$(rcv!p)> = #RPCFailure
    38                          & Call rcv p MClkRelayArg<arg<send!p>>
    39                          & unchanged (cst!p, rtrner send!p)"
    40 
    41   MClkReply     :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action"
    42      "MClkReply send rcv cst p == ACT
    43                            ~$Calling rcv p
    44                          & $(cst!p) = #clkB
    45                          & Return send p MClkReplyVal<res<rcv!p>>
    46                          & (cst!p)$ = #clkA
    47                          & unchanged (caller rcv!p)"
    48 
    49   MClkNext      :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action"
    50       "MClkNext send rcv cst p == ACT
    51                         (  MClkFwd send rcv cst p
    52                          | MClkRetry send rcv cst p
    53                          | MClkReply send rcv cst p)"
    54 
    55 
    56   (* temporal *)
    57   MClkIPSpec    :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => temporal"
    58       "MClkIPSpec send rcv cst p == TEMP
    59                            Init MClkInit rcv cst p
    60                          & [][ MClkNext send rcv cst p ]_(cst!p, rtrner send!p, caller rcv!p)
    61                          & WF(MClkFwd send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p)
    62                          & SF(MClkReply send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p)"
    63 
    64   MClkISpec     :: "mClkSndChType => mClkRcvChType => mClkStType => temporal"
    65       "MClkISpec send rcv cst == TEMP (ALL p. MClkIPSpec send rcv cst p)"
    66 
    67 end