products/sources/formale sprachen/Delphi/Bille 0.71/__history/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Mainboard.pas.~1029~   Sprache: Unknown

(*  Title:      HOL/TLA/Memory/MemClerkParameters.thy
    Author:     Stephan Merz, University of Munich
*)

section \<open>RPC-Memory example: Parameters of the memory clerk\<close>

theory MemClerkParameters
imports RPCParameters
begin

datatype mClkState = clkA | clkB

(* types sent on the clerk's send and receive channels are argument types
   of the memory and the RPC, respectively *)
type_synonym mClkSndArgType = "memOp"
type_synonym mClkRcvArgType = "rpcOp"

definition
  (* translate a memory call to an RPC call *)
  MClkRelayArg     :: "memOp \ rpcOp"
  where "MClkRelayArg marg = memcall marg"

definition
  (* translate RPC failures to memory failures *)
  MClkReplyVal     :: "Vals \ Vals"
  where "MClkReplyVal v = (if v = RPCFailure then MemFailure else v)"

end

[ Dauer der Verarbeitung: 0.0 Sekunden  (vorverarbeitet)  ]