|
3807
|
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 |
|
|
6255
|
12 |
Buffer = TLA +
|
|
3807
|
13 |
|
|
|
14 |
consts
|
|
|
15 |
(* actions *)
|
|
6255
|
16 |
BInit :: "'a stfun => 'a list stfun => 'a stfun => stpred"
|
|
3807
|
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
|
|
6255
|
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)"
|
|
3807
|
39 |
end
|
|
|
40 |
|
|
|
41 |
|
|
|
42 |
|