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