1(*  Title:      HOL/HOLCF/IOA/NTP/Sender.thy
2    Author:     Tobias Nipkow & Konrad Slind
3*)
4
5section \<open>The implementation: sender\<close>
6
7theory Sender
8imports IOA.IOA Action
9begin
10
11type_synonym
12'm sender_state = "'m list * bool multiset * bool multiset * bool * bool"
13(*                messages   #sent           #received      header  mode *)
14
15definition sq :: "'m sender_state => 'm list" where "sq = fst"
16definition ssent :: "'m sender_state => bool multiset" where "ssent = fst \<circ> snd"
17definition srcvd :: "'m sender_state => bool multiset" where "srcvd = fst \<circ> snd \<circ> snd"
18definition sbit :: "'m sender_state => bool" where "sbit = fst \<circ> snd \<circ> snd \<circ> snd"
19definition ssending :: "'m sender_state => bool" where "ssending = snd \<circ> snd \<circ> snd \<circ> snd"
20
21definition
22  sender_asig :: "'m action signature" where
23  "sender_asig = ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),
24                   UN pkt. {S_pkt(pkt)},
25                   {C_m_s,C_r_s})"
26
27definition
28  sender_trans :: "('m action, 'm sender_state)transition set" where
29  "sender_trans =
30 {tr. let s = fst(tr);
31          t = snd(snd(tr))
32      in case fst(snd(tr))
33      of
34      S_msg(m) => sq(t)=sq(s)@[m]   \<and>
35                  ssent(t)=ssent(s) \<and>
36                  srcvd(t)=srcvd(s) \<and>
37                  sbit(t)=sbit(s)   \<and>
38                  ssending(t)=ssending(s) |
39      R_msg(m) => False |
40      S_pkt(pkt) => hdr(pkt) = sbit(s)      \<and>
41                       (\<exists>Q. sq(s) = (msg(pkt)#Q))  \<and>
42                       sq(t) = sq(s)           \<and>
43                       ssent(t) = addm (ssent s) (sbit s) \<and>
44                       srcvd(t) = srcvd(s) \<and>
45                       sbit(t) = sbit(s)   \<and>
46                       ssending(s)         \<and>
47                       ssending(t) |
48    R_pkt(pkt) => False |
49    S_ack(b)   => False |
50      R_ack(b) => sq(t)=sq(s)                  \<and>
51                     ssent(t)=ssent(s)            \<and>
52                     srcvd(t) = addm (srcvd s) b  \<and>
53                     sbit(t)=sbit(s)              \<and>
54                     ssending(t)=ssending(s) |
55      C_m_s => count (ssent s) (~sbit s) < count (srcvd s) (~sbit s) \<and>
56               sq(t)=sq(s)       \<and>
57               ssent(t)=ssent(s) \<and>
58               srcvd(t)=srcvd(s) \<and>
59               sbit(t)=sbit(s)   \<and>
60               ssending(s)       \<and>
61               ~ssending(t) |
62      C_m_r => False |
63      C_r_s => count (ssent s) (sbit s) <= count (srcvd s) (~sbit s) \<and>
64               sq(t)=tl(sq(s))      \<and>
65               ssent(t)=ssent(s)    \<and>
66               srcvd(t)=srcvd(s)    \<and>
67               sbit(t) = (~sbit(s)) \<and>
68               ~ssending(s)         \<and>
69               ssending(t) |
70      C_r_r(m) => False}"
71
72definition
73  sender_ioa :: "('m action, 'm sender_state)ioa" where
74  "sender_ioa =
75   (sender_asig, {([],{|},{|},False,True)}, sender_trans,{},{})"
76
77lemma in_sender_asig:
78  "S_msg(m) \<in> actions(sender_asig)"
79  "R_msg(m) \<notin> actions(sender_asig)"
80  "S_pkt(pkt) \<in> actions(sender_asig)"
81  "R_pkt(pkt) \<notin> actions(sender_asig)"
82  "S_ack(b) \<notin> actions(sender_asig)"
83  "R_ack(b) \<in> actions(sender_asig)"
84  "C_m_s \<in> actions(sender_asig)"
85  "C_m_r \<notin> actions(sender_asig)"
86  "C_r_s \<in> actions(sender_asig)"
87  "C_r_r(m) \<notin> actions(sender_asig)"
88  by (simp_all add: sender_asig_def actions_def asig_projections)
89
90lemmas sender_projections = sq_def ssent_def srcvd_def sbit_def ssending_def
91
92end
93