src/HOL/TLA/Buffer/DBuffer.thy
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 6255 db63752140c7
child 17309 c43ed29bd197
permissions -rw-r--r--
import -> imports
     1 (*
     2     File:        DBuffer.thy
     3     Author:      Stephan Merz
     4     Copyright:   1997 University of Munich
     5 
     6    Theory Name: DBuffer
     7    Logic Image: TLA
     8 
     9    Two FIFO buffers in a row, with interleaving assumption.
    10 *)
    11 
    12 DBuffer = Buffer +
    13 
    14 consts
    15   (* implementation variables *)
    16   inp, mid, out  :: nat stfun
    17   q1, q2, qc     :: nat list stfun
    18 
    19   DBInit                         :: stpred
    20   DBEnq, DBDeq, DBPass, DBNext   :: action
    21   DBuffer                        :: temporal
    22 
    23 rules
    24   DB_base        "basevars (inp,mid,out,q1,q2)"
    25 
    26   (* the concatenation of the two buffers *)
    27   qc_def         "PRED qc == PRED (q2 @ q1)"
    28 
    29   DBInit_def     "DBInit   == PRED (BInit inp q1 mid  &  BInit mid q2 out)"
    30   DBEnq_def      "DBEnq    == ACT  Enq inp q1 mid  &  unchanged (q2,out)"
    31   DBDeq_def      "DBDeq    == ACT  Deq mid q2 out  &  unchanged (inp,q1)"
    32   DBPass_def     "DBPass   == ACT  Deq inp q1 mid
    33                                  & (q2$ = $q2 @ [ mid$ ])
    34                                  & (out$ = $out)"
    35   DBNext_def     "DBNext   == ACT  (DBEnq | DBDeq | DBPass)"
    36   DBuffer_def    "DBuffer  == TEMP Init DBInit
    37                                  & [][DBNext]_(inp,mid,out,q1,q2)
    38                                  & WF(DBDeq)_(inp,mid,out,q1,q2)
    39                                  & WF(DBPass)_(inp,mid,out,q1,q2)"
    40 
    41 end