1 (* Title: HOL/IOA/meta_theory/IOA.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow & Konrad Slind |
|
4 Copyright 1994 TU Muenchen |
|
5 |
|
6 The I/O automata of Lynch and Tuttle. |
|
7 *) |
|
8 |
|
9 IOA = Asig + Option + |
|
10 |
|
11 types |
|
12 'a seq = "nat => 'a" |
|
13 'a oseq = "nat => 'a option" |
|
14 ('a,'b)execution = "'a oseq * 'b seq" |
|
15 ('a,'s)transition = "('s * 'a * 's)" |
|
16 ('a,'s)ioa = "'a signature * 's set * ('a,'s)transition set" |
|
17 |
|
18 consts |
|
19 |
|
20 (* IO automata *) |
|
21 state_trans::"['action signature, ('action,'state)transition set] => bool" |
|
22 asig_of ::"('action,'state)ioa => 'action signature" |
|
23 starts_of ::"('action,'state)ioa => 'state set" |
|
24 trans_of ::"('action,'state)ioa => ('action,'state)transition set" |
|
25 IOA ::"('action,'state)ioa => bool" |
|
26 |
|
27 (* Executions, schedules, and traces *) |
|
28 |
|
29 is_execution_fragment, |
|
30 has_execution ::"[('action,'state)ioa, ('action,'state)execution] => bool" |
|
31 executions :: "('action,'state)ioa => ('action,'state)execution set" |
|
32 mk_trace :: "[('action,'state)ioa, 'action oseq] => 'action oseq" |
|
33 reachable :: "[('action,'state)ioa, 'state] => bool" |
|
34 invariant :: "[('action,'state)ioa, 'state=>bool] => bool" |
|
35 has_trace :: "[('action,'state)ioa, 'action oseq] => bool" |
|
36 traces :: "('action,'state)ioa => 'action oseq set" |
|
37 NF :: "'a oseq => 'a oseq" |
|
38 |
|
39 (* Composition of action signatures and automata *) |
|
40 compatible_asigs ::"('a => 'action signature) => bool" |
|
41 asig_composition ::"('a => 'action signature) => 'action signature" |
|
42 compatible_ioas ::"('a => ('action,'state)ioa) => bool" |
|
43 ioa_composition ::"('a => ('action, 'state)ioa) =>('action,'a => 'state)ioa" |
|
44 |
|
45 (* binary composition of action signatures and automata *) |
|
46 compat_asigs ::"['action signature, 'action signature] => bool" |
|
47 asig_comp ::"['action signature, 'action signature] => 'action signature" |
|
48 compat_ioas ::"[('action,'s)ioa, ('action,'t)ioa] => bool" |
|
49 "||" ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa" (infixr 10) |
|
50 |
|
51 (* Filtering and hiding *) |
|
52 filter_oseq :: "('a => bool) => 'a oseq => 'a oseq" |
|
53 |
|
54 restrict_asig :: "['a signature, 'a set] => 'a signature" |
|
55 restrict :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa" |
|
56 |
|
57 (* Notions of correctness *) |
|
58 ioa_implements :: "[('action,'state1)ioa, ('action,'state2)ioa] => bool" |
|
59 |
|
60 (* Instantiation of abstract IOA by concrete actions *) |
|
61 rename:: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa" |
|
62 |
|
63 defs |
|
64 |
|
65 state_trans_def |
|
66 "state_trans asig R == |
|
67 (!triple. triple:R --> fst(snd(triple)):actions(asig)) & |
|
68 (!a. (a:inputs(asig)) --> (!s1. ? s2. (s1,a,s2):R))" |
|
69 |
|
70 |
|
71 asig_of_def "asig_of == fst" |
|
72 starts_of_def "starts_of == (fst o snd)" |
|
73 trans_of_def "trans_of == (snd o snd)" |
|
74 |
|
75 ioa_def |
|
76 "IOA(ioa) == (is_asig(asig_of(ioa)) & |
|
77 (~ starts_of(ioa) = {}) & |
|
78 state_trans (asig_of ioa) (trans_of ioa))" |
|
79 |
|
80 |
|
81 (* An execution fragment is modelled with a pair of sequences: |
|
82 * the first is the action options, the second the state sequence. |
|
83 * Finite executions have None actions from some point on. |
|
84 *******) |
|
85 is_execution_fragment_def |
|
86 "is_execution_fragment A ex == |
|
87 let act = fst(ex); state = snd(ex) |
|
88 in !n a. (act(n)=None --> state(Suc(n)) = state(n)) & |
|
89 (act(n)=Some(a) --> (state(n),a,state(Suc(n))):trans_of(A))" |
|
90 |
|
91 |
|
92 executions_def |
|
93 "executions(ioa) == {e. snd e 0:starts_of(ioa) & |
|
94 is_execution_fragment ioa e}" |
|
95 |
|
96 |
|
97 reachable_def |
|
98 "reachable ioa s == (? ex:executions(ioa). ? n. (snd ex n) = s)" |
|
99 |
|
100 |
|
101 invariant_def "invariant A P == (!s. reachable A s --> P(s))" |
|
102 |
|
103 |
|
104 (* Restrict the trace to those members of the set s *) |
|
105 filter_oseq_def |
|
106 "filter_oseq p s == |
|
107 (%i.case s(i) |
|
108 of None => None |
|
109 | Some(x) => if p x then Some x else None)" |
|
110 |
|
111 |
|
112 mk_trace_def |
|
113 "mk_trace(ioa) == filter_oseq(%a.a:externals(asig_of(ioa)))" |
|
114 |
|
115 |
|
116 (* Does an ioa have an execution with the given trace *) |
|
117 has_trace_def |
|
118 "has_trace ioa b == |
|
119 (? ex:executions(ioa). b = mk_trace ioa (fst ex))" |
|
120 |
|
121 normal_form_def |
|
122 "NF(tr) == @nf. ? f. mono(f) & (!i. nf(i)=tr(f(i))) & |
|
123 (!j. j ~: range(f) --> nf(j)= None) & |
|
124 (!i. nf(i)=None --> (nf (Suc i)) = None) " |
|
125 |
|
126 (* All the traces of an ioa *) |
|
127 |
|
128 traces_def |
|
129 "traces(ioa) == {trace. ? tr. trace=NF(tr) & has_trace ioa tr}" |
|
130 |
|
131 (* |
|
132 traces_def |
|
133 "traces(ioa) == {tr. has_trace ioa tr}" |
|
134 *) |
|
135 |
|
136 compat_asigs_def |
|
137 "compat_asigs a1 a2 == |
|
138 (((outputs(a1) Int outputs(a2)) = {}) & |
|
139 ((internals(a1) Int actions(a2)) = {}) & |
|
140 ((internals(a2) Int actions(a1)) = {}))" |
|
141 |
|
142 |
|
143 compat_ioas_def |
|
144 "compat_ioas ioa1 ioa2 == compat_asigs (asig_of(ioa1)) (asig_of(ioa2))" |
|
145 |
|
146 |
|
147 asig_comp_def |
|
148 "asig_comp a1 a2 == |
|
149 (((inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)), |
|
150 (outputs(a1) Un outputs(a2)), |
|
151 (internals(a1) Un internals(a2))))" |
|
152 |
|
153 |
|
154 par_def |
|
155 "(ioa1 || ioa2) == |
|
156 (asig_comp (asig_of ioa1) (asig_of ioa2), |
|
157 {pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)}, |
|
158 {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) |
|
159 in (a:actions(asig_of(ioa1)) | a:actions(asig_of(ioa2))) & |
|
160 (if a:actions(asig_of(ioa1)) then |
|
161 (fst(s),a,fst(t)):trans_of(ioa1) |
|
162 else fst(t) = fst(s)) |
|
163 & |
|
164 (if a:actions(asig_of(ioa2)) then |
|
165 (snd(s),a,snd(t)):trans_of(ioa2) |
|
166 else snd(t) = snd(s))})" |
|
167 |
|
168 |
|
169 restrict_asig_def |
|
170 "restrict_asig asig actns == |
|
171 (inputs(asig) Int actns, outputs(asig) Int actns, |
|
172 internals(asig) Un (externals(asig) - actns))" |
|
173 |
|
174 |
|
175 restrict_def |
|
176 "restrict ioa actns == |
|
177 (restrict_asig (asig_of ioa) actns, starts_of(ioa), trans_of(ioa))" |
|
178 |
|
179 |
|
180 ioa_implements_def |
|
181 "ioa_implements 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 |
|
186 rename_def |
|
187 "rename ioa ren == |
|
188 (({b. ? x. Some(x)= ren(b) & x : inputs(asig_of(ioa))}, |
|
189 {b. ? x. Some(x)= ren(b) & x : outputs(asig_of(ioa))}, |
|
190 {b. ? x. Some(x)= ren(b) & x : internals(asig_of(ioa))}), |
|
191 starts_of(ioa) , |
|
192 {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) |
|
193 in |
|
194 ? x. Some(x) = ren(a) & (s,x,t):trans_of(ioa)})" |
|
195 |
|
196 end |
|