|
1050
|
1 |
(* Title: HOL/IOA/ABP/Receiver.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow & Olaf Mueller
|
|
|
4 |
Copyright 1995 TU Muenchen
|
|
|
5 |
|
|
|
6 |
The implementation: receiver
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
Receiver = List + IOA + Action + Lemmas +
|
|
|
10 |
|
|
|
11 |
types
|
|
|
12 |
|
|
|
13 |
'm receiver_state
|
|
|
14 |
= "'m list * bool"
|
|
|
15 |
(* messages mode *)
|
|
|
16 |
|
|
|
17 |
consts
|
|
|
18 |
|
|
|
19 |
receiver_asig :: "'m action signature"
|
|
|
20 |
receiver_trans:: "('m action, 'm receiver_state)transition set"
|
|
|
21 |
receiver_ioa :: "('m action, 'm receiver_state)ioa"
|
|
|
22 |
rq :: "'m receiver_state => 'm list"
|
|
|
23 |
rbit :: "'m receiver_state => bool"
|
|
|
24 |
|
|
|
25 |
defs
|
|
|
26 |
|
|
|
27 |
rq_def "rq == fst"
|
|
|
28 |
rbit_def "rbit == snd"
|
|
|
29 |
|
|
|
30 |
receiver_asig_def "receiver_asig == \
|
|
|
31 |
\ (UN pkt. {R_pkt(pkt)}, \
|
|
|
32 |
\ (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}), \
|
|
|
33 |
\ {})"
|
|
|
34 |
|
|
|
35 |
receiver_trans_def "receiver_trans == \
|
|
|
36 |
\ {tr. let s = fst(tr); \
|
|
|
37 |
\ t = snd(snd(tr)) \
|
|
|
38 |
\ in \
|
|
|
39 |
\ case fst(snd(tr)) \
|
|
|
40 |
\ of \
|
|
|
41 |
\ Next => False | \
|
|
|
42 |
\ S_msg(m) => False | \
|
|
|
43 |
\ R_msg(m) => (rq(s) ~= []) & \
|
|
|
44 |
\ m = hd(rq(s)) & \
|
|
|
45 |
\ rq(t) = tl(rq(s)) & \
|
|
|
46 |
\ rbit(t)=rbit(s) | \
|
|
|
47 |
\ S_pkt(pkt) => False | \
|
|
|
48 |
\ R_pkt(pkt) => if (hdr(pkt) ~= rbit(s))&rq(s)=[] then \
|
|
|
49 |
\ rq(t) = (rq(s)@[msg(pkt)]) &rbit(t) = (~rbit(s)) else \
|
|
|
50 |
\ rq(t) =rq(s) & rbit(t)=rbit(s) | \
|
|
|
51 |
\ S_ack(b) => b = rbit(s) & \
|
|
|
52 |
\ rq(t) = rq(s) & \
|
|
|
53 |
\ rbit(t)=rbit(s) | \
|
|
|
54 |
\ R_ack(b) => False}"
|
|
|
55 |
|
|
|
56 |
receiver_ioa_def "receiver_ioa == \
|
|
|
57 |
\ (receiver_asig, {([],False)}, receiver_trans)"
|
|
|
58 |
|
|
|
59 |
end
|