|
1 (* Title: HOLCF/IOA/TrivEx.thy |
|
2 ID: $Id$ |
|
3 Author: Olaf Mueller |
|
4 Copyright 1995 TU Muenchen |
|
5 |
|
6 Trivial Abstraction Example with fairness |
|
7 *) |
|
8 |
|
9 TrivEx2 = Abstraction + IOA + |
|
10 |
|
11 datatype action = INC |
|
12 |
|
13 consts |
|
14 |
|
15 C_asig :: "action signature" |
|
16 C_trans :: (action, nat)transition set |
|
17 C_ioa :: (action, nat)ioa |
|
18 C_live_ioa :: (action, nat)live_ioa |
|
19 |
|
20 A_asig :: "action signature" |
|
21 A_trans :: (action, bool)transition set |
|
22 A_ioa :: (action, bool)ioa |
|
23 A_live_ioa :: (action, bool)live_ioa |
|
24 |
|
25 h_abs :: "nat => bool" |
|
26 |
|
27 defs |
|
28 |
|
29 C_asig_def |
|
30 "C_asig == ({},{INC},{})" |
|
31 |
|
32 C_trans_def "C_trans == |
|
33 {tr. let s = fst(tr); |
|
34 t = snd(snd(tr)) |
|
35 in case fst(snd(tr)) |
|
36 of |
|
37 INC => t = Suc(s)}" |
|
38 |
|
39 C_ioa_def "C_ioa == |
|
40 (C_asig, {0}, C_trans,{},{})" |
|
41 |
|
42 C_live_ioa_def |
|
43 "C_live_ioa == (C_ioa, WF C_ioa {INC})" |
|
44 |
|
45 A_asig_def |
|
46 "A_asig == ({},{INC},{})" |
|
47 |
|
48 A_trans_def "A_trans == |
|
49 {tr. let s = fst(tr); |
|
50 t = snd(snd(tr)) |
|
51 in case fst(snd(tr)) |
|
52 of |
|
53 INC => t = True}" |
|
54 |
|
55 A_ioa_def "A_ioa == |
|
56 (A_asig, {False}, A_trans,{},{})" |
|
57 |
|
58 A_live_ioa_def |
|
59 "A_live_ioa == (A_ioa, WF A_ioa {INC})" |
|
60 |
|
61 |
|
62 |
|
63 h_abs_def |
|
64 "h_abs n == n~=0" |
|
65 |
|
66 rules |
|
67 |
|
68 MC_result |
|
69 "validLIOA (A_ioa,WF A_ioa {INC}) (<>[] <%(b,a,c). b>)" |
|
70 |
|
71 end |