1(*  Title:      HOL/HOLCF/IOA/ABP/Env.thy
2    Author:     Olaf M��ller
3*)
4
5section \<open>The environment\<close>
6
7theory Env
8imports IOA.IOA Action
9begin
10
11type_synonym
12  'm env_state = bool   \<comment> \<open>give next bit to system\<close>
13
14definition
15  env_asig :: "'m action signature" where
16  "env_asig == ({Next},
17                 UN m. {S_msg(m)},
18                 {})"
19
20definition
21  env_trans :: "('m action, 'm env_state)transition set" where
22  "env_trans =
23   {tr. let s = fst(tr);
24            t = snd(snd(tr))
25        in case fst(snd(tr))
26        of
27        Next       => t=True |
28        S_msg(m)   => s=True & t=False |
29        R_msg(m)   => False |
30        S_pkt(pkt) => False |
31        R_pkt(pkt) => False |
32        S_ack(b)   => False |
33        R_ack(b)   => False}"
34
35definition
36  env_ioa :: "('m action, 'm env_state)ioa" where
37  "env_ioa = (env_asig, {True}, env_trans,{},{})"
38
39axiomatization
40  "next" :: "'m env_state => bool"
41
42end
43