src/HOL/TLA/Memory/MemoryParameters.thy
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 6255 db63752140c7
child 9517 f58863b1406a
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
wenzelm@3807
     1
(*
wenzelm@3807
     2
    File:        MemoryParameters.thy
wenzelm@3807
     3
    Author:      Stephan Merz
wenzelm@3807
     4
    Copyright:   1997 University of Munich
wenzelm@3807
     5
wenzelm@3807
     6
    Theory Name: MemoryParameters
wenzelm@3807
     7
    Logic Image: TLA
wenzelm@3807
     8
wenzelm@3807
     9
    RPC-Memory example: Memory parameters
wenzelm@3807
    10
*)
wenzelm@3807
    11
berghofe@5184
    12
MemoryParameters = Datatype + RPCMemoryParams +
wenzelm@3807
    13
wenzelm@6255
    14
(* the memory operations *)
wenzelm@6255
    15
(***
wenzelm@3807
    16
datatype  Rd = read
wenzelm@3807
    17
datatype  Wr = write
wenzelm@6255
    18
***)
wenzelm@3807
    19
wenzelm@6255
    20
datatype memOp = read Locs | write Locs Vals
wenzelm@6255
    21
wenzelm@6255
    22
(***
wenzelm@3807
    23
types
wenzelm@3807
    24
  (* legal arguments for the memory *)
wenzelm@3807
    25
  memArgType = "(Rd * Locs) + (Wr * Locs * Vals)"
wenzelm@6255
    26
***)
wenzelm@3807
    27
wenzelm@3807
    28
consts
wenzelm@3807
    29
  (* memory locations and contents *)
wenzelm@6255
    30
  MemLoc         :: Locs set
wenzelm@6255
    31
  MemVal         :: Vals set
wenzelm@3807
    32
wenzelm@3807
    33
  (* some particular values *)
wenzelm@3807
    34
  OK             :: "Vals"
wenzelm@3807
    35
  BadArg         :: "Vals"
wenzelm@3807
    36
  MemFailure     :: "Vals"
wenzelm@3807
    37
  NotAResult     :: "Vals"  (* defined here for simplicity *)
wenzelm@3807
    38
  
wenzelm@3807
    39
  (* the initial value stored in each memory cell *)
wenzelm@3807
    40
  InitVal        :: "Vals"
wenzelm@3807
    41
wenzelm@3807
    42
rules
wenzelm@3807
    43
  (* basic assumptions about the above constants and predicates *)
wenzelm@6255
    44
  BadArgNoMemVal    "BadArg ~: MemVal"
wenzelm@6255
    45
  MemFailNoMemVal   "MemFailure ~: MemVal"
wenzelm@6255
    46
  InitValMemVal     "InitVal : MemVal"
wenzelm@6255
    47
  NotAResultNotVal  "NotAResult ~: MemVal"
wenzelm@3807
    48
  NotAResultNotOK   "NotAResult ~= OK"
wenzelm@3807
    49
  NotAResultNotBA   "NotAResult ~= BadArg"
wenzelm@3807
    50
  NotAResultNotMF   "NotAResult ~= MemFailure"
wenzelm@3807
    51
end