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 implementation |
|
7 *) |
|
8 |
|
9 Impl_finite = Sender + Receiver + Abschannel_finite + |
|
10 |
|
11 types |
|
12 |
|
13 'm impl_fin_state |
|
14 = "'m sender_state * 'm receiver_state * 'm packet list * bool list" |
|
15 (* sender_state * receiver_state * srch_state * rsch_state *) |
|
16 |
|
17 constdefs |
|
18 |
|
19 impl_fin_ioa :: ('m action, 'm impl_fin_state)ioa |
|
20 "impl_fin_ioa == (sender_ioa || receiver_ioa || srch_fin_ioa || |
|
21 rsch_fin_ioa)" |
|
22 |
|
23 sen_fin :: 'm impl_fin_state => 'm sender_state |
|
24 "sen_fin == fst" |
|
25 |
|
26 rec_fin :: 'm impl_fin_state => 'm receiver_state |
|
27 "rec_fin == fst o snd" |
|
28 |
|
29 srch_fin :: 'm impl_fin_state => 'm packet list |
|
30 "srch_fin == fst o snd o snd" |
|
31 |
|
32 rsch_fin :: 'm impl_fin_state => bool list |
|
33 "rsch_fin == snd o snd o snd" |
|
34 |
|
35 end |
|
36 |