|
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 + List + |
|
13 |
|
14 consts |
|
15 (* infix syntax for list operations *) |
|
16 "IntNil" :: 'w::world => 'a list (".[]") |
|
17 "IntCons" :: ['w::world => 'a, 'w => 'a list] => ('w => 'a list) ("(_ .#/ _)" [65,66] 65) |
|
18 "IntApp" :: ['w::world => 'a list, 'w => 'a list] => ('w => 'a list) ("(_ .@/ _)" [65,66] 65) |
|
19 |
|
20 (* actions *) |
|
21 BInit :: "'a stfun => 'a list stfun => 'a stfun => action" |
|
22 Enq :: "'a stfun => 'a list stfun => 'a stfun => action" |
|
23 Deq :: "'a stfun => 'a list stfun => 'a stfun => action" |
|
24 Next :: "'a stfun => 'a list stfun => 'a stfun => action" |
|
25 |
|
26 (* temporal formulas *) |
|
27 IBuffer :: "'a stfun => 'a list stfun => 'a stfun => temporal" |
|
28 Buffer :: "'a stfun => 'a stfun => temporal" |
|
29 |
|
30 syntax |
|
31 "@listInt" :: args => ('a list, 'w) term (".[(_)]") |
|
32 |
|
33 translations |
|
34 ".[]" == "con []" |
|
35 "x .# xs" == "lift2 (op #) x xs" |
|
36 "xs .@ ys" == "lift2 (op @) xs ys" |
|
37 ".[ x, xs ]" == "x .# .[xs]" |
|
38 ".[ x ]" == "x .# .[]" |
|
39 |
|
40 rules |
|
41 BInit_def "BInit ic q oc == $q .= .[]" |
|
42 Enq_def "Enq ic q oc == (ic$ .~= $ic) |
|
43 .& (q$ .= $q .@ .[ ic$ ]) |
|
44 .& (oc$ .= $oc)" |
|
45 Deq_def "Deq ic q oc == ($q .~= .[]) |
|
46 .& (oc$ .= hd[ $q ]) |
|
47 .& (q$ .= tl[ $q ]) |
|
48 .& (ic$ .= $ic)" |
|
49 Next_def "Next ic q oc == Enq ic q oc .| Deq ic q oc" |
|
50 IBuffer_def "IBuffer ic q oc == Init (BInit ic q oc) |
|
51 .& [][Next ic q oc]_<ic,q,oc> |
|
52 .& WF(Deq ic q oc)_<ic,q,oc>" |
|
53 Buffer_def "Buffer ic oc == EEX q. IBuffer ic q oc" |
|
54 end |
|
55 |
|
56 |
|
57 |