equal
deleted
inserted
replaced
|
1 (* Title: HOLCF/IOA/ABP/Impl.thy |
|
2 ID: $Id$ |
|
3 Author: Olaf Mueller |
|
4 Copyright 1995 TU Muenchen |
|
5 |
|
6 The environment |
|
7 *) |
|
8 |
|
9 Env = IOA + Action + |
|
10 |
|
11 types |
|
12 |
|
13 'm env_state = "bool" |
|
14 (* give next bit to system *) |
|
15 |
|
16 consts |
|
17 |
|
18 env_asig :: 'm action signature |
|
19 env_trans :: ('m action, 'm env_state)transition set |
|
20 env_ioa :: ('m action, 'm env_state)ioa |
|
21 next :: 'm env_state => bool |
|
22 |
|
23 defs |
|
24 |
|
25 env_asig_def |
|
26 "env_asig == ({Next}, |
|
27 UN m. {S_msg(m)}, |
|
28 {})" |
|
29 |
|
30 env_trans_def "env_trans == |
|
31 {tr. let s = fst(tr); |
|
32 t = snd(snd(tr)) |
|
33 in case fst(snd(tr)) |
|
34 of |
|
35 Next => t=True | |
|
36 S_msg(m) => s=True & t=False | |
|
37 R_msg(m) => False | |
|
38 S_pkt(pkt) => False | |
|
39 R_pkt(pkt) => False | |
|
40 S_ack(b) => False | |
|
41 R_ack(b) => False}" |
|
42 |
|
43 env_ioa_def "env_ioa == |
|
44 (env_asig, {True}, env_trans)" |
|
45 |
|
46 end |
|
47 |