| author | huffman |
| Sat, 27 Nov 2010 16:08:10 -0800 | |
| changeset 41022 | 0437dbc127b3 |
| parent 35174 | src/HOLCF/IOA/ABP/Env.thy@e15040ae75d7 |
| child 41193 | b8703f63bfb2 |
| permissions | -rw-r--r-- |
| mueller@3072 | 1 |
(* Title: HOLCF/IOA/ABP/Impl.thy |
| wenzelm@12218 | 2 |
Author: Olaf Müller |
| mueller@3072 | 3 |
*) |
| mueller@3072 | 4 |
|
| wenzelm@17244 | 5 |
header {* The environment *}
|
| wenzelm@17244 | 6 |
|
| wenzelm@17244 | 7 |
theory Env |
| wenzelm@17244 | 8 |
imports IOA Action |
| wenzelm@17244 | 9 |
begin |
| mueller@3072 | 10 |
|
| mueller@3072 | 11 |
types |
| wenzelm@17244 | 12 |
'm env_state = bool -- {* give next bit to system *}
|
| mueller@3072 | 13 |
|
| wenzelm@25131 | 14 |
definition |
| wenzelm@25131 | 15 |
env_asig :: "'m action signature" where |
| wenzelm@25131 | 16 |
"env_asig == ({Next},
|
| wenzelm@25131 | 17 |
UN m. {S_msg(m)},
|
| wenzelm@25131 | 18 |
{})"
|
| wenzelm@17244 | 19 |
|
| wenzelm@25131 | 20 |
definition |
| wenzelm@25131 | 21 |
env_trans :: "('m action, 'm env_state)transition set" where
|
| wenzelm@25131 | 22 |
"env_trans = |
| wenzelm@25131 | 23 |
{tr. let s = fst(tr);
|
| wenzelm@25131 | 24 |
t = snd(snd(tr)) |
| wenzelm@25131 | 25 |
in case fst(snd(tr)) |
| wenzelm@25131 | 26 |
of |
| wenzelm@25131 | 27 |
Next => t=True | |
| wenzelm@25131 | 28 |
S_msg(m) => s=True & t=False | |
| wenzelm@25131 | 29 |
R_msg(m) => False | |
| wenzelm@25131 | 30 |
S_pkt(pkt) => False | |
| wenzelm@25131 | 31 |
R_pkt(pkt) => False | |
| wenzelm@25131 | 32 |
S_ack(b) => False | |
| wenzelm@25131 | 33 |
R_ack(b) => False}" |
| wenzelm@17244 | 34 |
|
| wenzelm@25131 | 35 |
definition |
| wenzelm@25131 | 36 |
env_ioa :: "('m action, 'm env_state)ioa" where
|
| wenzelm@25131 | 37 |
"env_ioa = (env_asig, {True}, env_trans,{},{})"
|
| mueller@3072 | 38 |
|
| wenzelm@25131 | 39 |
axiomatization |
| wenzelm@25131 | 40 |
"next" :: "'m env_state => bool" |
| mueller@3072 | 41 |
|
| mueller@3072 | 42 |
end |