author | mueller |
Mon, 12 Jan 1998 17:48:23 +0100 | |
changeset 4559 | 8e604d885b54 |
parent 3842 | b55686a7b22c |
child 5976 | 44290b71a85f |
permissions | -rw-r--r-- |
3071 | 1 |
(* Title: HOLCF/IOA/meta_theory/Traces.thy |
3275 | 2 |
ID: $Id$ |
3071 | 3 |
Author: Olaf M"uller |
4 |
Copyright 1996 TU Muenchen |
|
5 |
||
6 |
Executions and Traces of I/O automata in HOLCF. |
|
7 |
*) |
|
8 |
||
9 |
||
3275 | 10 |
Traces = Sequence + Automata + |
3071 | 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" |
|
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 |
(* FIX: introduce good symbol *) |
|
71 |
syntax (symbols) |
|
72 |
||
73 |
"op <<|" ::"[('a,'s1)ioa, ('a,'s2)ioa] => bool" (infixr "\\<parallel>" 10) |
|
74 |
*) |
|
75 |
||
76 |
||
77 |
defs |
|
78 |
||
79 |
||
80 |
(* ------------------- Executions ------------------------------ *) |
|
81 |
||
82 |
||
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
83 |
is_exec_frag_def |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
84 |
"is_exec_frag A ex == ((is_exec_fragC A`(snd ex)) (fst ex) ~= FF)" |
3071 | 85 |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
86 |
|
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
87 |
is_exec_fragC_def |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
88 |
"is_exec_fragC A ==(fix`(LAM h ex. (%s. case ex of |
3071 | 89 |
nil => TT |
90 |
| x##xs => (flift1 |
|
3842 | 91 |
(%p. Def ((s,p):trans_of A) andalso (h`xs) (snd p)) |
3071 | 92 |
`x) |
93 |
)))" |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
94 |
|
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
95 |
|
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
96 |
|
3071 | 97 |
executions_def |
98 |
"executions ioa == {e. ((fst e) : starts_of(ioa)) & |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
99 |
is_exec_frag ioa e}" |
3071 | 100 |
|
101 |
||
102 |
(* ------------------- Schedules ------------------------------ *) |
|
103 |
||
104 |
||
105 |
filter_act_def |
|
106 |
"filter_act == Map fst" |
|
107 |
||
108 |
has_schedule_def |
|
109 |
"has_schedule ioa sch == |
|
110 |
(? ex:executions ioa. sch = filter_act`(snd ex))" |
|
111 |
||
112 |
schedules_def |
|
113 |
"schedules ioa == {sch. has_schedule ioa sch}" |
|
114 |
||
115 |
||
116 |
(* ------------------- Traces ------------------------------ *) |
|
117 |
||
118 |
has_trace_def |
|
119 |
"has_trace ioa tr == |
|
3842 | 120 |
(? sch:schedules ioa. tr = Filter (%a. a:ext(ioa))`sch)" |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
121 |
|
3071 | 122 |
traces_def |
123 |
"traces ioa == {tr. has_trace ioa tr}" |
|
124 |
||
125 |
||
126 |
mk_trace_def |
|
127 |
"mk_trace ioa == LAM tr. |
|
3842 | 128 |
Filter (%a. a:ext(ioa))`(filter_act`tr)" |
3071 | 129 |
|
130 |
||
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
131 |
(* ------------------- Fair Traces ------------------------------ *) |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
132 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
133 |
laststate_def |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
134 |
"laststate ex == case Last`(snd ex) of |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
135 |
Undef => fst ex |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
136 |
| Def at => snd at" |
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 |
inf_often_def |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
139 |
"inf_often P s == Infinite (Filter P`s)" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
140 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
141 |
(* filtering P yields a finite or partial sequence *) |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
142 |
fin_often_def |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
143 |
"fin_often P s == ~inf_often P s" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
144 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
145 |
(* 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
|
146 |
else branch prohibits it. However they can be sfair in the case when all W |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
147 |
are only finitely often enabled: FIX Is this the right model? *) |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
148 |
wfair_ex_def |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
149 |
"wfair_ex A ex == ! W : wfair_of A. |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
150 |
if Finite (snd ex) |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
151 |
then ~Enabled A W (laststate ex) |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
152 |
else is_wfair A W ex" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
153 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
154 |
is_wfair_def |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
155 |
"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
|
156 |
| inf_often (%x.~Enabled A W (snd x)) (snd 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 |
sfair_ex_def |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
159 |
"sfair_ex A ex == ! W : sfair_of A. |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
160 |
if Finite (snd ex) |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
161 |
then ~Enabled A W (laststate ex) |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
162 |
else is_sfair A W ex" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
163 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
164 |
is_sfair_def |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
165 |
"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
|
166 |
| fin_often (%x. Enabled A W (snd x)) (snd 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 |
fair_ex_def |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
169 |
"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
|
170 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
171 |
fairexecutions_def |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
172 |
"fairexecutions A == {ex. ex:executions A & fair_ex A ex}" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
173 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
174 |
fairtraces_def |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
175 |
"fairtraces A == {mk_trace A`(snd ex) | ex. ex:fairexecutions A}" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
176 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
177 |
|
3071 | 178 |
(* ------------------- Implementation ------------------------------ *) |
179 |
||
180 |
ioa_implements_def |
|
181 |
"ioa1 =<| ioa2 == |
|
182 |
(((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) & |
|
183 |
(outputs(asig_of(ioa1)) = outputs(asig_of(ioa2)))) & |
|
184 |
traces(ioa1) <= traces(ioa2))" |
|
185 |
||
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
186 |
fair_implements_def |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
187 |
"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
|
188 |
fairtraces(C) <= fairtraces(A)" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3842
diff
changeset
|
189 |
|
3521 | 190 |
(* ------------------- Modules ------------------------------ *) |
191 |
||
192 |
Execs_def |
|
193 |
"Execs A == (executions A, asig_of A)" |
|
194 |
||
195 |
Scheds_def |
|
196 |
"Scheds A == (schedules A, asig_of A)" |
|
197 |
||
198 |
Traces_def |
|
199 |
"Traces A == (traces A,asig_of A)" |
|
200 |
||
3071 | 201 |
|
202 |
end |