| author | paulson |
| Wed, 06 May 1998 13:01:30 +0200 | |
| changeset 4898 | 68fd1a2b8b7b |
| parent 3522 | a34c20f4bf44 |
| child 6468 | a7b1669f5365 |
| permissions | -rw-r--r-- |
|
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
1 |
(* Title: HOLCF/IOA/ABP/Receiver.thy |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
2 |
ID: $Id$ |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
3 |
Author: Olaf Mueller |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
4 |
Copyright 1995 TU Muenchen |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
5 |
|
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
6 |
The implementation: receiver |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
7 |
*) |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
8 |
|
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
9 |
Receiver = List + IOA + Action + Lemmas + |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
10 |
|
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
11 |
types |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
12 |
|
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
13 |
'm receiver_state |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
14 |
= "'m list * bool" |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
15 |
(* messages mode *) |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
16 |
|
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
17 |
consts |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
18 |
|
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
19 |
receiver_asig :: 'm action signature |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
20 |
receiver_trans:: ('m action, 'm receiver_state)transition set
|
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
21 |
receiver_ioa :: ('m action, 'm receiver_state)ioa
|
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
22 |
rq :: 'm receiver_state => 'm list |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
23 |
rbit :: 'm receiver_state => bool |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
24 |
|
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
25 |
defs |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
26 |
|
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
27 |
rq_def "rq == fst" |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
28 |
rbit_def "rbit == snd" |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
29 |
|
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
30 |
receiver_asig_def "receiver_asig == |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
31 |
(UN pkt. {R_pkt(pkt)},
|
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
32 |
(UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),
|
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
33 |
{})"
|
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
34 |
|
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
35 |
receiver_trans_def "receiver_trans == |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
36 |
{tr. let s = fst(tr);
|
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
37 |
t = snd(snd(tr)) |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
38 |
in |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
39 |
case fst(snd(tr)) |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
40 |
of |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
41 |
Next => False | |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
42 |
S_msg(m) => False | |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
43 |
R_msg(m) => (rq(s) ~= []) & |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
44 |
m = hd(rq(s)) & |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
45 |
rq(t) = tl(rq(s)) & |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
46 |
rbit(t)=rbit(s) | |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
47 |
S_pkt(pkt) => False | |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
48 |
R_pkt(pkt) => if (hdr(pkt) ~= rbit(s))&rq(s)=[] then |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
49 |
rq(t) = (rq(s)@[msg(pkt)]) &rbit(t) = (~rbit(s)) else |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
50 |
rq(t) =rq(s) & rbit(t)=rbit(s) | |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
51 |
S_ack(b) => b = rbit(s) & |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
52 |
rq(t) = rq(s) & |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
53 |
rbit(t)=rbit(s) | |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
54 |
R_ack(b) => False}" |
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
55 |
|
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
56 |
receiver_ioa_def "receiver_ioa == |
| 3522 | 57 |
(receiver_asig, {([],False)}, receiver_trans,{},{})"
|
|
3072
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
58 |
|
|
a31419014be5
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
59 |
end |