|
1051
|
1 |
(* Title: HOL/IOA/NTP/Receiver.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow & Konrad Slind
|
|
|
4 |
Copyright 1994 TU Muenchen
|
|
|
5 |
|
|
|
6 |
The implementation: receiver
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
Receiver = List + IOA + Action + Multiset +
|
|
|
10 |
|
|
|
11 |
types
|
|
|
12 |
|
|
|
13 |
'm receiver_state
|
|
|
14 |
= "'m list * bool multiset * 'm packet multiset * bool * bool"
|
|
|
15 |
(* messages #replies #received header 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 |
rsent :: "'m receiver_state => bool multiset"
|
|
|
24 |
rrcvd :: "'m receiver_state => 'm packet multiset"
|
|
|
25 |
rbit :: "'m receiver_state => bool"
|
|
|
26 |
rsending :: "'m receiver_state => bool"
|
|
|
27 |
|
|
|
28 |
defs
|
|
|
29 |
|
|
|
30 |
rq_def "rq == fst"
|
|
|
31 |
rsent_def "rsent == fst o snd"
|
|
|
32 |
rrcvd_def "rrcvd == fst o snd o snd"
|
|
|
33 |
rbit_def "rbit == fst o snd o snd o snd"
|
|
|
34 |
rsending_def "rsending == snd o snd o snd o snd"
|
|
|
35 |
|
|
|
36 |
receiver_asig_def "receiver_asig == \
|
|
|
37 |
\ (UN pkt. {R_pkt(pkt)}, \
|
|
|
38 |
\ (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}), \
|
|
|
39 |
\ insert C_m_r (UN m. {C_r_r(m)}))"
|
|
|
40 |
|
|
|
41 |
receiver_trans_def "receiver_trans == \
|
|
|
42 |
\ {tr. let s = fst(tr); \
|
|
|
43 |
\ t = snd(snd(tr)) \
|
|
|
44 |
\ in \
|
|
|
45 |
\ case fst(snd(tr)) \
|
|
|
46 |
\ of \
|
|
|
47 |
\ S_msg(m) => False | \
|
|
|
48 |
\ R_msg(m) => rq(s) = (m # rq(t)) & \
|
|
|
49 |
\ rsent(t)=rsent(s) & \
|
|
|
50 |
\ rrcvd(t)=rrcvd(s) & \
|
|
|
51 |
\ rbit(t)=rbit(s) & \
|
|
|
52 |
\ rsending(t)=rsending(s) | \
|
|
|
53 |
\ S_pkt(pkt) => False | \
|
|
|
54 |
\ R_pkt(pkt) => rq(t) = rq(s) & \
|
|
|
55 |
\ rsent(t) = rsent(s) & \
|
|
|
56 |
\ rrcvd(t) = addm (rrcvd s) pkt & \
|
|
|
57 |
\ rbit(t) = rbit(s) & \
|
|
|
58 |
\ rsending(t) = rsending(s) | \
|
|
|
59 |
\ S_ack(b) => b = rbit(s) & \
|
|
|
60 |
\ rq(t) = rq(s) & \
|
|
|
61 |
\ rsent(t) = addm (rsent s) (rbit s) & \
|
|
|
62 |
\ rrcvd(t) = rrcvd(s) & \
|
|
|
63 |
\ rbit(t)=rbit(s) & \
|
|
|
64 |
\ rsending(s) & \
|
|
|
65 |
\ rsending(t) | \
|
|
|
66 |
\ R_ack(b) => False | \
|
|
|
67 |
\ C_m_s => False | \
|
|
|
68 |
\ C_m_r => count (rsent s) (~rbit s) < countm (rrcvd s) (%y.hdr(y)=rbit(s)) & \
|
|
|
69 |
\ rq(t) = rq(s) & \
|
|
|
70 |
\ rsent(t)=rsent(s) & \
|
|
|
71 |
\ rrcvd(t)=rrcvd(s) & \
|
|
|
72 |
\ rbit(t)=rbit(s) & \
|
|
|
73 |
\ rsending(s) & \
|
|
|
74 |
\ ~rsending(t) | \
|
|
|
75 |
\ C_r_s => False | \
|
|
|
76 |
\ C_r_r(m) => count (rsent s) (rbit s) <= countm (rrcvd s) (%y.hdr(y)=rbit(s)) & \
|
|
|
77 |
\ count (rsent s) (~rbit s) < count (rrcvd s) (rbit(s),m) & \
|
|
|
78 |
\ rq(t) = rq(s)@[m] & \
|
|
|
79 |
\ rsent(t)=rsent(s) & \
|
|
|
80 |
\ rrcvd(t)=rrcvd(s) & \
|
|
|
81 |
\ rbit(t) = (~rbit(s)) & \
|
|
|
82 |
\ ~rsending(s) & \
|
|
|
83 |
\ rsending(t)}"
|
|
|
84 |
|
|
|
85 |
|
|
|
86 |
receiver_ioa_def "receiver_ioa == \
|
|
|
87 |
\ (receiver_asig, {([],{|},{|},False,False)}, receiver_trans)"
|
|
|
88 |
|
|
|
89 |
end
|