1(*  Title:      HOL/HOLCF/IOA/ABP/Spec.thy
2    Author:     Olaf M��ller
3*)
4
5section \<open>The specification of reliable transmission\<close>
6
7theory Spec
8imports IOA.IOA Action
9begin
10
11definition
12  spec_sig :: "'m action signature" where
13  sig_def: "spec_sig = (UN m.{S_msg(m)},
14                       UN m.{R_msg(m)} Un {Next},
15                       {})"
16
17definition
18  spec_trans :: "('m action, 'm list)transition set" where
19  trans_def: "spec_trans =
20   {tr. let s = fst(tr);
21            t = snd(snd(tr))
22        in
23        case fst(snd(tr))
24        of
25        Next =>  t=s |           \<comment> \<open>Note that there is condition as in Sender\<close>
26        S_msg(m) => t = s@[m]  |
27        R_msg(m) => s = (m#t)  |
28        S_pkt(pkt) => False |
29        R_pkt(pkt) => False |
30        S_ack(b) => False |
31        R_ack(b) => False}"
32
33definition
34  spec_ioa :: "('m action, 'm list)ioa" where
35  ioa_def: "spec_ioa = (spec_sig, {[]}, spec_trans, {}, {})"
36
37end
38