author | kleing |
Mon, 21 Jun 2004 10:25:57 +0200 | |
changeset 14981 | e73f8140af78 |
parent 12919 | d6a0d168291e |
child 17233 | 41eee2e7b465 |
permissions | -rw-r--r-- |
3071 | 1 |
(* Title: HOLCF/IOA/meta_theory/Automata.thy |
3275 | 2 |
ID: $Id$ |
12218 | 3 |
Author: Olaf Müller, Konrad Slind, Tobias Nipkow |
3071 | 4 |
|
5 |
The I/O automata of Lynch and Tuttle in HOLCF. |
|
6 |
*) |
|
7 |
||
8 |
||
12919 | 9 |
Automata = Asig + |
3071 | 10 |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12218
diff
changeset
|
11 |
default type |
3071 | 12 |
|
13 |
types |
|
14 |
('a,'s)transition = "'s * 'a * 's" |
|
3521 | 15 |
('a,'s)ioa = "'a signature * 's set * ('a,'s)transition set * |
16 |
(('a set) set) * (('a set) set)" |
|
3071 | 17 |
|
18 |
consts |
|
19 |
||
20 |
(* IO automata *) |
|
3521 | 21 |
|
22 |
asig_of ::"('a,'s)ioa => 'a signature" |
|
23 |
starts_of ::"('a,'s)ioa => 's set" |
|
24 |
trans_of ::"('a,'s)ioa => ('a,'s)transition set" |
|
25 |
wfair_of ::"('a,'s)ioa => ('a set) set" |
|
26 |
sfair_of ::"('a,'s)ioa => ('a set) set" |
|
27 |
||
28 |
is_asig_of ::"('a,'s)ioa => bool" |
|
29 |
is_starts_of ::"('a,'s)ioa => bool" |
|
30 |
is_trans_of ::"('a,'s)ioa => bool" |
|
31 |
input_enabled ::"('a,'s)ioa => bool" |
|
32 |
IOA ::"('a,'s)ioa => bool" |
|
3071 | 33 |
|
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
34 |
(* constraints for fair IOA *) |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
35 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
36 |
fairIOA ::"('a,'s)ioa => bool" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
37 |
input_resistant::"('a,'s)ioa => bool" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
38 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
39 |
(* enabledness of actions and action sets *) |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
40 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
41 |
enabled ::"('a,'s)ioa => 'a => 's => bool" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
42 |
Enabled ::"('a,'s)ioa => 'a set => 's => bool" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
43 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
44 |
(* action set keeps enabled until probably disabled by itself *) |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
45 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
46 |
en_persistent :: "('a,'s)ioa => 'a set => bool" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
47 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
48 |
(* post_conditions for actions and action sets *) |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
49 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
50 |
was_enabled ::"('a,'s)ioa => 'a => 's => bool" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
51 |
set_was_enabled ::"('a,'s)ioa => 'a set => 's => bool" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
52 |
|
3071 | 53 |
(* reachability and invariants *) |
54 |
reachable :: "('a,'s)ioa => 's set" |
|
55 |
invariant :: "[('a,'s)ioa, 's=>bool] => bool" |
|
56 |
||
57 |
(* binary composition of action signatures and automata *) |
|
58 |
asig_comp ::"['a signature, 'a signature] => 'a signature" |
|
3521 | 59 |
compatible ::"[('a,'s)ioa, ('a,'t)ioa] => bool" |
3071 | 60 |
"||" ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa" (infixr 10) |
61 |
||
3521 | 62 |
(* hiding and restricting *) |
63 |
hide_asig :: "['a signature, 'a set] => 'a signature" |
|
64 |
hide :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa" |
|
3071 | 65 |
restrict_asig :: "['a signature, 'a set] => 'a signature" |
66 |
restrict :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa" |
|
67 |
||
68 |
(* renaming *) |
|
3521 | 69 |
rename_set :: "'a set => ('c => 'a option) => 'c set" |
70 |
rename :: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa" |
|
3071 | 71 |
|
72 |
||
73 |
syntax |
|
74 |
||
75 |
"_trans_of" :: "'s => 'a => ('a,'s)ioa => 's => bool" ("_ -_--_-> _" [81,81,81,81] 100) |
|
76 |
"reachable" :: "[('a,'s)ioa, 's] => bool" |
|
77 |
"act" :: "('a,'s)ioa => 'a set" |
|
78 |
"ext" :: "('a,'s)ioa => 'a set" |
|
79 |
"int" :: "('a,'s)ioa => 'a set" |
|
80 |
"inp" :: "('a,'s)ioa => 'a set" |
|
81 |
"out" :: "('a,'s)ioa => 'a set" |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
82 |
"local" :: "('a,'s)ioa => 'a set" |
3071 | 83 |
|
84 |
||
12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
7661
diff
changeset
|
85 |
syntax (xsymbols) |
3071 | 86 |
|
87 |
"_trans_of" :: "'s => 'a => ('a,'s)ioa => 's => bool" |
|
12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
7661
diff
changeset
|
88 |
("_ \\<midarrow>_\\<midarrow>_\\<longrightarrow> _" [81,81,81,81] 100) |
3071 | 89 |
"op ||" ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa" (infixr "\\<parallel>" 10) |
90 |
||
91 |
||
92 |
inductive "reachable C" |
|
93 |
intrs |
|
94 |
reachable_0 "s:(starts_of C) ==> s : reachable C" |
|
95 |
reachable_n "[|s:reachable C; (s,a,t):trans_of C|] ==> t:reachable C" |
|
96 |
||
97 |
||
98 |
translations |
|
99 |
"s -a--A-> t" == "(s,a,t):trans_of A" |
|
100 |
"reachable A s" == "s:reachable A" |
|
101 |
"act A" == "actions (asig_of A)" |
|
102 |
"ext A" == "externals (asig_of A)" |
|
103 |
"int A" == "internals (asig_of A)" |
|
104 |
"inp A" == "inputs (asig_of A)" |
|
105 |
"out A" == "outputs (asig_of A)" |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
106 |
"local A" == "locals (asig_of A)" |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
107 |
|
3071 | 108 |
|
109 |
||
110 |
defs |
|
111 |
||
112 |
(* --------------------------------- IOA ---------------------------------*) |
|
113 |
||
114 |
||
115 |
||
116 |
asig_of_def "asig_of == fst" |
|
117 |
starts_of_def "starts_of == (fst o snd)" |
|
3521 | 118 |
trans_of_def "trans_of == (fst o snd o snd)" |
119 |
wfair_of_def "wfair_of == (fst o snd o snd o snd)" |
|
120 |
sfair_of_def "sfair_of == (snd o snd o snd o snd)" |
|
121 |
||
122 |
is_asig_of_def |
|
123 |
"is_asig_of A == is_asig (asig_of A)" |
|
124 |
||
125 |
is_starts_of_def |
|
126 |
"is_starts_of A == (~ starts_of A = {})" |
|
127 |
||
128 |
is_trans_of_def |
|
129 |
"is_trans_of A == |
|
130 |
(!triple. triple:(trans_of A) --> fst(snd(triple)):actions(asig_of A))" |
|
131 |
||
132 |
input_enabled_def |
|
133 |
"input_enabled A == |
|
134 |
(!a. (a:inputs(asig_of A)) --> (!s1. ? s2. (s1,a,s2):(trans_of A)))" |
|
135 |
||
3071 | 136 |
|
137 |
ioa_def |
|
3521 | 138 |
"IOA A == (is_asig_of A & |
139 |
is_starts_of A & |
|
140 |
is_trans_of A & |
|
141 |
input_enabled A)" |
|
3071 | 142 |
|
143 |
||
144 |
invariant_def "invariant A P == (!s. reachable A s --> P(s))" |
|
145 |
||
146 |
||
147 |
(* ------------------------- parallel composition --------------------------*) |
|
148 |
||
149 |
||
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
150 |
compatible_def |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
151 |
"compatible A B == |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
152 |
(((out A Int out B) = {}) & |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
153 |
((int A Int act B) = {}) & |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
154 |
((int B Int act A) = {}))" |
3071 | 155 |
|
156 |
asig_comp_def |
|
157 |
"asig_comp a1 a2 == |
|
158 |
(((inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)), |
|
159 |
(outputs(a1) Un outputs(a2)), |
|
160 |
(internals(a1) Un internals(a2))))" |
|
161 |
||
162 |
par_def |
|
3521 | 163 |
"(A || B) == |
164 |
(asig_comp (asig_of A) (asig_of B), |
|
165 |
{pr. fst(pr):starts_of(A) & snd(pr):starts_of(B)}, |
|
3071 | 166 |
{tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) |
3521 | 167 |
in (a:act A | a:act B) & |
168 |
(if a:act A then |
|
169 |
(fst(s),a,fst(t)):trans_of(A) |
|
3071 | 170 |
else fst(t) = fst(s)) |
171 |
& |
|
3521 | 172 |
(if a:act B then |
173 |
(snd(s),a,snd(t)):trans_of(B) |
|
174 |
else snd(t) = snd(s))}, |
|
175 |
wfair_of A Un wfair_of B, |
|
176 |
sfair_of A Un sfair_of B)" |
|
177 |
||
3071 | 178 |
|
179 |
(* ------------------------ hiding -------------------------------------------- *) |
|
180 |
||
181 |
restrict_asig_def |
|
182 |
"restrict_asig asig actns == |
|
3521 | 183 |
(inputs(asig) Int actns, |
184 |
outputs(asig) Int actns, |
|
3071 | 185 |
internals(asig) Un (externals(asig) - actns))" |
186 |
||
3521 | 187 |
(* Notice that for wfair_of and sfair_of nothing has to be changed, as |
188 |
changes from the outputs to the internals does not touch the locals as |
|
189 |
a whole, which is of importance for fairness only *) |
|
3071 | 190 |
|
191 |
restrict_def |
|
3521 | 192 |
"restrict A actns == |
193 |
(restrict_asig (asig_of A) actns, |
|
194 |
starts_of A, |
|
195 |
trans_of A, |
|
196 |
wfair_of A, |
|
197 |
sfair_of A)" |
|
198 |
||
199 |
hide_asig_def |
|
200 |
"hide_asig asig actns == |
|
201 |
(inputs(asig) - actns, |
|
202 |
outputs(asig) - actns, |
|
203 |
internals(asig) Un actns)" |
|
204 |
||
205 |
hide_def |
|
206 |
"hide A actns == |
|
207 |
(hide_asig (asig_of A) actns, |
|
208 |
starts_of A, |
|
209 |
trans_of A, |
|
210 |
wfair_of A, |
|
211 |
sfair_of A)" |
|
3071 | 212 |
|
213 |
(* ------------------------- renaming ------------------------------------------- *) |
|
214 |
||
3521 | 215 |
rename_set_def |
7661 | 216 |
"rename_set A ren == {b. ? x. Some x = ren b & x : A}" |
3521 | 217 |
|
3071 | 218 |
rename_def |
219 |
"rename ioa ren == |
|
3521 | 220 |
((rename_set (inp ioa) ren, |
221 |
rename_set (out ioa) ren, |
|
222 |
rename_set (int ioa) ren), |
|
223 |
starts_of ioa, |
|
3071 | 224 |
{tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) |
225 |
in |
|
3521 | 226 |
? x. Some(x) = ren(a) & (s,x,t):trans_of ioa}, |
227 |
{rename_set s ren | s. s: wfair_of ioa}, |
|
228 |
{rename_set s ren | s. s: sfair_of ioa})" |
|
3071 | 229 |
|
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
230 |
(* ------------------------- fairness ----------------------------- *) |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
231 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
232 |
fairIOA_def |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
233 |
"fairIOA A == (! S : wfair_of A. S<= local A) & |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
234 |
(! S : sfair_of A. S<= local A)" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
235 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
236 |
input_resistant_def |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
237 |
"input_resistant A == ! W : sfair_of A. ! s a t. |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
238 |
reachable A s & reachable A t & a:inp A & |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
239 |
Enabled A W s & s -a--A-> t |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
240 |
--> Enabled A W t" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
241 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
242 |
enabled_def |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
243 |
"enabled A a s == ? t. s-a--A-> t" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
244 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
245 |
Enabled_def |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
246 |
"Enabled A W s == ? w:W. enabled A w s" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
247 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
248 |
en_persistent_def |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
249 |
"en_persistent A W == ! s a t. Enabled A W s & |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
250 |
a ~:W & |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
251 |
s -a--A-> t |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
252 |
--> Enabled A W t" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
253 |
was_enabled_def |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
254 |
"was_enabled A a t == ? s. s-a--A-> t" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
255 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
256 |
set_was_enabled_def |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
257 |
"set_was_enabled A W t == ? w:W. was_enabled A w t" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3521
diff
changeset
|
258 |
|
3071 | 259 |
|
260 |
end |
|
261 |