author | wenzelm |
Sat, 01 Dec 2001 18:52:32 +0100 | |
changeset 12338 | de0f4a63baa5 |
parent 12218 | 6597093b77e7 |
child 14981 | e73f8140af78 |
permissions | -rw-r--r-- |
3071 | 1 |
(* Title: HOLCF/IOA/meta_theory/Traces.thy |
3275 | 2 |
ID: $Id$ |
12218 | 3 |
Author: Olaf Müller |
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
3071 | 5 |
|
6 |
Executions and Traces of I/O automata in HOLCF. |
|
7 |
*) |
|
8 |
||
9 |
||
3275 | 10 |
Traces = Sequence + Automata + |
3071 | 11 |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12218
diff
changeset
|
12 |
default type |
3071 | 13 |
|
14 |
types |
|
15 |
('a,'s)pairs = "('a * 's) Seq" |
|
16 |
('a,'s)execution = "'s * ('a,'s)pairs" |
|
17 |
'a trace = "'a Seq" |
|
3521 | 18 |
|
19 |
('a,'s)execution_module = "('a,'s)execution set * 'a signature" |
|
20 |
'a schedule_module = "'a trace set * 'a signature" |
|
21 |
'a trace_module = "'a trace set * 'a signature" |
|
3071 | 22 |
|
23 |
consts |
|
24 |
||
25 |
(* Executions *) |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
26 |
|
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
27 |
is_exec_fragC ::"('a,'s)ioa => ('a,'s)pairs -> 's => tr" |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
28 |
is_exec_frag, |
3071 | 29 |
has_execution ::"[('a,'s)ioa, ('a,'s)execution] => bool" |
30 |
executions :: "('a,'s)ioa => ('a,'s)execution set" |
|
31 |
||
32 |
(* Schedules and traces *) |
|
33 |
filter_act ::"('a,'s)pairs -> 'a trace" |
|
34 |
has_schedule, |
|
35 |
has_trace :: "[('a,'s)ioa, 'a trace] => bool" |
|
36 |
schedules, |
|
37 |
traces :: "('a,'s)ioa => 'a trace set" |
|
38 |
mk_trace :: "('a,'s)ioa => ('a,'s)pairs -> 'a trace" |
|
39 |
||
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
40 |
laststate ::"('a,'s)execution => 's" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
41 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
42 |
(* A predicate holds infinitely (finitely) often in a sequence *) |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
43 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
44 |
inf_often ::"('a => bool) => 'a Seq => bool" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
45 |
fin_often ::"('a => bool) => 'a Seq => bool" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
46 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
47 |
(* fairness of executions *) |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
48 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
49 |
wfair_ex ::"('a,'s)ioa => ('a,'s)execution => bool" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
50 |
sfair_ex ::"('a,'s)ioa => ('a,'s)execution => bool" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
51 |
is_wfair ::"('a,'s)ioa => 'a set => ('a,'s)execution => bool" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
52 |
is_sfair ::"('a,'s)ioa => 'a set => ('a,'s)execution => bool" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
53 |
fair_ex ::"('a,'s)ioa => ('a,'s)execution => bool" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
54 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
55 |
(* fair behavior sets *) |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
56 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
57 |
fairexecutions ::"('a,'s)ioa => ('a,'s)execution set" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
58 |
fairtraces ::"('a,'s)ioa => 'a trace set" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
59 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
60 |
(* Notions of implementation *) |
3071 | 61 |
"=<|" :: "[('a,'s1)ioa, ('a,'s2)ioa] => bool" (infixr 12) |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
62 |
fair_implements :: "('a,'s1)ioa => ('a,'s2)ioa => bool" |
3071 | 63 |
|
3521 | 64 |
(* Execution, schedule and trace modules *) |
65 |
Execs :: "('a,'s)ioa => ('a,'s)execution_module" |
|
66 |
Scheds :: "('a,'s)ioa => 'a schedule_module" |
|
67 |
Traces :: "('a,'s)ioa => 'a trace_module" |
|
68 |
||
3071 | 69 |
|
70 |
defs |
|
71 |
||
72 |
||
73 |
(* ------------------- Executions ------------------------------ *) |
|
74 |
||
75 |
||
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
76 |
is_exec_frag_def |
10835 | 77 |
"is_exec_frag A ex == ((is_exec_fragC A$(snd ex)) (fst ex) ~= FF)" |
3071 | 78 |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
79 |
|
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
80 |
is_exec_fragC_def |
10835 | 81 |
"is_exec_fragC A ==(fix$(LAM h ex. (%s. case ex of |
3071 | 82 |
nil => TT |
83 |
| x##xs => (flift1 |
|
10835 | 84 |
(%p. Def ((s,p):trans_of A) andalso (h$xs) (snd p)) |
85 |
$x) |
|
3071 | 86 |
)))" |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
87 |
|
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
88 |
|
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
89 |
|
3071 | 90 |
executions_def |
91 |
"executions ioa == {e. ((fst e) : starts_of(ioa)) & |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
92 |
is_exec_frag ioa e}" |
3071 | 93 |
|
94 |
||
95 |
(* ------------------- Schedules ------------------------------ *) |
|
96 |
||
97 |
||
98 |
filter_act_def |
|
99 |
"filter_act == Map fst" |
|
100 |
||
101 |
has_schedule_def |
|
102 |
"has_schedule ioa sch == |
|
10835 | 103 |
(? ex:executions ioa. sch = filter_act$(snd ex))" |
3071 | 104 |
|
105 |
schedules_def |
|
106 |
"schedules ioa == {sch. has_schedule ioa sch}" |
|
107 |
||
108 |
||
109 |
(* ------------------- Traces ------------------------------ *) |
|
110 |
||
111 |
has_trace_def |
|
112 |
"has_trace ioa tr == |
|
10835 | 113 |
(? sch:schedules ioa. tr = Filter (%a. a:ext(ioa))$sch)" |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
114 |
|
3071 | 115 |
traces_def |
116 |
"traces ioa == {tr. has_trace ioa tr}" |
|
117 |
||
118 |
||
119 |
mk_trace_def |
|
120 |
"mk_trace ioa == LAM tr. |
|
10835 | 121 |
Filter (%a. a:ext(ioa))$(filter_act$tr)" |
3071 | 122 |
|
123 |
||
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
124 |
(* ------------------- Fair Traces ------------------------------ *) |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
125 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
126 |
laststate_def |
10835 | 127 |
"laststate ex == case Last$(snd ex) of |
12028 | 128 |
UU => fst ex |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
129 |
| Def at => snd at" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
130 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
131 |
inf_often_def |
10835 | 132 |
"inf_often P s == Infinite (Filter P$s)" |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
133 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
134 |
(* filtering P yields a finite or partial sequence *) |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
135 |
fin_often_def |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
136 |
"fin_often P s == ~inf_often P s" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
137 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
138 |
(* Note that partial execs cannot be wfair as the inf_often predicate in the |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
139 |
else branch prohibits it. However they can be sfair in the case when all W |
5976 | 140 |
are only finitely often enabled: Is this the right model? |
141 |
See LiveIOA for solution conforming with the literature and superseding this one *) |
|
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
142 |
wfair_ex_def |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
143 |
"wfair_ex A ex == ! W : wfair_of A. |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
144 |
if Finite (snd ex) |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
145 |
then ~Enabled A W (laststate ex) |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
146 |
else is_wfair A W ex" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
147 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
148 |
is_wfair_def |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
149 |
"is_wfair A W ex == (inf_often (%x. fst x:W) (snd ex) |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
150 |
| inf_often (%x.~Enabled A W (snd x)) (snd ex))" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
151 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
152 |
sfair_ex_def |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
153 |
"sfair_ex A ex == ! W : sfair_of A. |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
154 |
if Finite (snd ex) |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
155 |
then ~Enabled A W (laststate ex) |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
156 |
else is_sfair A W ex" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
157 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
158 |
is_sfair_def |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
159 |
"is_sfair A W ex == (inf_often (%x. fst x:W) (snd ex) |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
160 |
| fin_often (%x. Enabled A W (snd x)) (snd ex))" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
161 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
162 |
fair_ex_def |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
163 |
"fair_ex A ex == wfair_ex A ex & sfair_ex A ex" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
164 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
165 |
fairexecutions_def |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
166 |
"fairexecutions A == {ex. ex:executions A & fair_ex A ex}" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
167 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
168 |
fairtraces_def |
10835 | 169 |
"fairtraces A == {mk_trace A$(snd ex) | ex. ex:fairexecutions A}" |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
170 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
171 |
|
3071 | 172 |
(* ------------------- Implementation ------------------------------ *) |
173 |
||
174 |
ioa_implements_def |
|
175 |
"ioa1 =<| ioa2 == |
|
176 |
(((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) & |
|
177 |
(outputs(asig_of(ioa1)) = outputs(asig_of(ioa2)))) & |
|
178 |
traces(ioa1) <= traces(ioa2))" |
|
179 |
||
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
180 |
fair_implements_def |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
181 |
"fair_implements C A == inp(C) = inp(A) & out(C)=out(A) & |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
182 |
fairtraces(C) <= fairtraces(A)" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
183 |
|
3521 | 184 |
(* ------------------- Modules ------------------------------ *) |
185 |
||
186 |
Execs_def |
|
187 |
"Execs A == (executions A, asig_of A)" |
|
188 |
||
189 |
Scheds_def |
|
190 |
"Scheds A == (schedules A, asig_of A)" |
|
191 |
||
192 |
Traces_def |
|
193 |
"Traces A == (traces A,asig_of A)" |
|
194 |
||
3071 | 195 |
|
196 |
end |