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