|
1 (* Title: HOLCF/IOA/meta_theory/Traces.thy |
|
2 ID: |
|
3 Author: Olaf M"uller |
|
4 Copyright 1996 TU Muenchen |
|
5 |
|
6 Executions and Traces of I/O automata in HOLCF. |
|
7 *) |
|
8 |
|
9 |
|
10 Traces = Automata + Sequence + |
|
11 |
|
12 default term |
|
13 |
|
14 types |
|
15 ('a,'s)pairs = "('a * 's) Seq" |
|
16 ('a,'s)execution = "'s * ('a,'s)pairs" |
|
17 'a trace = "'a Seq" |
|
18 |
|
19 consts |
|
20 |
|
21 (* Executions *) |
|
22 is_ex_fr ::"('a,'s)ioa => ('a,'s)pairs -> ('s => tr)" |
|
23 is_execution_fragment, |
|
24 has_execution ::"[('a,'s)ioa, ('a,'s)execution] => bool" |
|
25 executions :: "('a,'s)ioa => ('a,'s)execution set" |
|
26 |
|
27 (* Schedules and traces *) |
|
28 filter_act ::"('a,'s)pairs -> 'a trace" |
|
29 has_schedule, |
|
30 has_trace :: "[('a,'s)ioa, 'a trace] => bool" |
|
31 schedules, |
|
32 traces :: "('a,'s)ioa => 'a trace set" |
|
33 |
|
34 mk_trace :: "('a,'s)ioa => ('a,'s)pairs -> 'a trace" |
|
35 |
|
36 (* Notion of implementation *) |
|
37 "=<|" :: "[('a,'s1)ioa, ('a,'s2)ioa] => bool" (infixr 12) |
|
38 |
|
39 (* |
|
40 (* FIX: introduce good symbol *) |
|
41 syntax (symbols) |
|
42 |
|
43 "op <<|" ::"[('a,'s1)ioa, ('a,'s2)ioa] => bool" (infixr "\\<parallel>" 10) |
|
44 *) |
|
45 |
|
46 |
|
47 defs |
|
48 |
|
49 |
|
50 (* ------------------- Executions ------------------------------ *) |
|
51 |
|
52 |
|
53 is_execution_fragment_def |
|
54 "is_execution_fragment A ex == ((is_ex_fr A`(snd ex)) (fst ex) ~= FF)" |
|
55 |
|
56 is_ex_fr_def |
|
57 "is_ex_fr A ==(fix`(LAM h ex. (%s. case ex of |
|
58 nil => TT |
|
59 | x##xs => (flift1 |
|
60 (%p.Def ((s,p):trans_of A) andalso (h`xs) (snd p)) |
|
61 `x) |
|
62 )))" |
|
63 |
|
64 executions_def |
|
65 "executions ioa == {e. ((fst e) : starts_of(ioa)) & |
|
66 is_execution_fragment ioa e}" |
|
67 |
|
68 |
|
69 (* ------------------- Schedules ------------------------------ *) |
|
70 |
|
71 |
|
72 filter_act_def |
|
73 "filter_act == Map fst" |
|
74 |
|
75 has_schedule_def |
|
76 "has_schedule ioa sch == |
|
77 (? ex:executions ioa. sch = filter_act`(snd ex))" |
|
78 |
|
79 schedules_def |
|
80 "schedules ioa == {sch. has_schedule ioa sch}" |
|
81 |
|
82 |
|
83 (* ------------------- Traces ------------------------------ *) |
|
84 |
|
85 has_trace_def |
|
86 "has_trace ioa tr == |
|
87 (? sch:schedules ioa. tr = Filter (%a.a:ext(ioa))`sch)" |
|
88 |
|
89 traces_def |
|
90 "traces ioa == {tr. has_trace ioa tr}" |
|
91 |
|
92 |
|
93 mk_trace_def |
|
94 "mk_trace ioa == LAM tr. |
|
95 Filter (%a.a:ext(ioa))`(filter_act`tr)" |
|
96 |
|
97 |
|
98 (* ------------------- Implementation ------------------------------ *) |
|
99 |
|
100 ioa_implements_def |
|
101 "ioa1 =<| ioa2 == |
|
102 (((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) & |
|
103 (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2)))) & |
|
104 traces(ioa1) <= traces(ioa2))" |
|
105 |
|
106 |
|
107 end |