src/HOL/TLA/Buffer/Buffer.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:        Buffer.thy
     3     Author:      Stephan Merz
     4     Copyright:   1997 University of Munich
     5 
     6    Theory Name: Buffer
     7    Logic Image: TLA
     8 
     9    A simple FIFO buffer (synchronous communication, interleaving)
    10 *)
    11 
    12 Buffer = TLA +
    13 
    14 consts
    15   (* actions *)
    16   BInit     :: "'a stfun => 'a list stfun => 'a stfun => stpred"
    17   Enq       :: "'a stfun => 'a list stfun => 'a stfun => action"
    18   Deq       :: "'a stfun => 'a list stfun => 'a stfun => action"
    19   Next      :: "'a stfun => 'a list stfun => 'a stfun => action"
    20 
    21   (* temporal formulas *)
    22   IBuffer   :: "'a stfun => 'a list stfun => 'a stfun => temporal"
    23   Buffer    :: "'a stfun => 'a stfun => temporal"
    24 
    25 rules
    26   BInit_def   "BInit ic q oc    == PRED q = #[]"
    27   Enq_def     "Enq ic q oc      == ACT (ic$ ~= $ic) 
    28                                      & (q$ = $q @ [ ic$ ]) 
    29                                      & (oc$ = $oc)"
    30   Deq_def     "Deq ic q oc      == ACT ($q ~= #[])
    31                                      & (oc$ = hd< $q >)
    32                                      & (q$ = tl< $q >)
    33                                      & (ic$ = $ic)"
    34   Next_def    "Next ic q oc     == ACT (Enq ic q oc | Deq ic q oc)"
    35   IBuffer_def "IBuffer ic q oc  == TEMP Init (BInit ic q oc)
    36                                       & [][Next ic q oc]_(ic,q,oc)
    37                                       & WF(Deq ic q oc)_(ic,q,oc)"
    38   Buffer_def  "Buffer ic oc     == TEMP (EEX q. IBuffer ic q oc)"
    39 end
    40 
    41 
    42