24 trans_of ::"('action,'state)ioa => ('action,'state)transition set" |
26 trans_of ::"('action,'state)ioa => ('action,'state)transition set" |
25 IOA ::"('action,'state)ioa => bool" |
27 IOA ::"('action,'state)ioa => bool" |
26 |
28 |
27 (* Executions, schedules, and traces *) |
29 (* Executions, schedules, and traces *) |
28 |
30 |
29 is_execution_fragment, |
31 is_execution_fragment ::"[('action,'state)ioa, ('action,'state)execution] => bool" |
30 has_execution ::"[('action,'state)ioa, ('action,'state)execution] => bool" |
32 has_execution ::"[('action,'state)ioa, ('action,'state)execution] => bool" |
31 executions :: "('action,'state)ioa => ('action,'state)execution set" |
33 executions :: "('action,'state)ioa => ('action,'state)execution set" |
32 mk_trace :: "[('action,'state)ioa, 'action oseq] => 'action oseq" |
34 mk_trace :: "[('action,'state)ioa, 'action oseq] => 'action oseq" |
33 reachable :: "[('action,'state)ioa, 'state] => bool" |
35 reachable :: "[('action,'state)ioa, 'state] => bool" |
34 invariant :: "[('action,'state)ioa, 'state=>bool] => bool" |
36 invariant :: "[('action,'state)ioa, 'state=>bool] => bool" |
60 (* Instantiation of abstract IOA by concrete actions *) |
62 (* Instantiation of abstract IOA by concrete actions *) |
61 rename:: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa" |
63 rename:: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa" |
62 |
64 |
63 defs |
65 defs |
64 |
66 |
65 state_trans_def |
67 state_trans_def: |
66 "state_trans asig R == |
68 "state_trans asig R == |
67 (!triple. triple:R --> fst(snd(triple)):actions(asig)) & |
69 (!triple. triple:R --> fst(snd(triple)):actions(asig)) & |
68 (!a. (a:inputs(asig)) --> (!s1. ? s2. (s1,a,s2):R))" |
70 (!a. (a:inputs(asig)) --> (!s1. ? s2. (s1,a,s2):R))" |
69 |
71 |
70 |
72 |
71 asig_of_def "asig_of == fst" |
73 asig_of_def: "asig_of == fst" |
72 starts_of_def "starts_of == (fst o snd)" |
74 starts_of_def: "starts_of == (fst o snd)" |
73 trans_of_def "trans_of == (snd o snd)" |
75 trans_of_def: "trans_of == (snd o snd)" |
74 |
76 |
75 ioa_def |
77 ioa_def: |
76 "IOA(ioa) == (is_asig(asig_of(ioa)) & |
78 "IOA(ioa) == (is_asig(asig_of(ioa)) & |
77 (~ starts_of(ioa) = {}) & |
79 (~ starts_of(ioa) = {}) & |
78 state_trans (asig_of ioa) (trans_of ioa))" |
80 state_trans (asig_of ioa) (trans_of ioa))" |
79 |
81 |
80 |
82 |
81 (* An execution fragment is modelled with a pair of sequences: |
83 (* An execution fragment is modelled with a pair of sequences: |
82 * the first is the action options, the second the state sequence. |
84 * the first is the action options, the second the state sequence. |
83 * Finite executions have None actions from some point on. |
85 * Finite executions have None actions from some point on. |
84 *******) |
86 *******) |
85 is_execution_fragment_def |
87 is_execution_fragment_def: |
86 "is_execution_fragment A ex == |
88 "is_execution_fragment A ex == |
87 let act = fst(ex); state = snd(ex) |
89 let act = fst(ex); state = snd(ex) |
88 in !n a. (act(n)=None --> state(Suc(n)) = state(n)) & |
90 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))" |
91 (act(n)=Some(a) --> (state(n),a,state(Suc(n))):trans_of(A))" |
90 |
92 |
91 |
93 |
92 executions_def |
94 executions_def: |
93 "executions(ioa) == {e. snd e 0:starts_of(ioa) & |
95 "executions(ioa) == {e. snd e 0:starts_of(ioa) & |
94 is_execution_fragment ioa e}" |
96 is_execution_fragment ioa e}" |
95 |
97 |
96 |
98 |
97 reachable_def |
99 reachable_def: |
98 "reachable ioa s == (? ex:executions(ioa). ? n. (snd ex n) = s)" |
100 "reachable ioa s == (? ex:executions(ioa). ? n. (snd ex n) = s)" |
99 |
101 |
100 |
102 |
101 invariant_def "invariant A P == (!s. reachable A s --> P(s))" |
103 invariant_def: "invariant A P == (!s. reachable A s --> P(s))" |
102 |
104 |
103 |
105 |
104 (* Restrict the trace to those members of the set s *) |
106 (* Restrict the trace to those members of the set s *) |
105 filter_oseq_def |
107 filter_oseq_def: |
106 "filter_oseq p s == |
108 "filter_oseq p s == |
107 (%i. case s(i) |
109 (%i. case s(i) |
108 of None => None |
110 of None => None |
109 | Some(x) => if p x then Some x else None)" |
111 | Some(x) => if p x then Some x else None)" |
110 |
112 |
111 |
113 |
112 mk_trace_def |
114 mk_trace_def: |
113 "mk_trace(ioa) == filter_oseq(%a. a:externals(asig_of(ioa)))" |
115 "mk_trace(ioa) == filter_oseq(%a. a:externals(asig_of(ioa)))" |
114 |
116 |
115 |
117 |
116 (* Does an ioa have an execution with the given trace *) |
118 (* Does an ioa have an execution with the given trace *) |
117 has_trace_def |
119 has_trace_def: |
118 "has_trace ioa b == |
120 "has_trace ioa b == |
119 (? ex:executions(ioa). b = mk_trace ioa (fst ex))" |
121 (? ex:executions(ioa). b = mk_trace ioa (fst ex))" |
120 |
122 |
121 normal_form_def |
123 normal_form_def: |
122 "NF(tr) == @nf. ? f. mono(f) & (!i. nf(i)=tr(f(i))) & |
124 "NF(tr) == @nf. ? f. mono(f) & (!i. nf(i)=tr(f(i))) & |
123 (!j. j ~: range(f) --> nf(j)= None) & |
125 (!j. j ~: range(f) --> nf(j)= None) & |
124 (!i. nf(i)=None --> (nf (Suc i)) = None) " |
126 (!i. nf(i)=None --> (nf (Suc i)) = None) " |
125 |
127 |
126 (* All the traces of an ioa *) |
128 (* All the traces of an ioa *) |
127 |
129 |
128 traces_def |
130 traces_def: |
129 "traces(ioa) == {trace. ? tr. trace=NF(tr) & has_trace ioa tr}" |
131 "traces(ioa) == {trace. ? tr. trace=NF(tr) & has_trace ioa tr}" |
130 |
132 |
131 (* |
133 (* |
132 traces_def |
134 traces_def: |
133 "traces(ioa) == {tr. has_trace ioa tr}" |
135 "traces(ioa) == {tr. has_trace ioa tr}" |
134 *) |
136 *) |
135 |
137 |
136 compat_asigs_def |
138 compat_asigs_def: |
137 "compat_asigs a1 a2 == |
139 "compat_asigs a1 a2 == |
138 (((outputs(a1) Int outputs(a2)) = {}) & |
140 (((outputs(a1) Int outputs(a2)) = {}) & |
139 ((internals(a1) Int actions(a2)) = {}) & |
141 ((internals(a1) Int actions(a2)) = {}) & |
140 ((internals(a2) Int actions(a1)) = {}))" |
142 ((internals(a2) Int actions(a1)) = {}))" |
141 |
143 |
142 |
144 |
143 compat_ioas_def |
145 compat_ioas_def: |
144 "compat_ioas ioa1 ioa2 == compat_asigs (asig_of(ioa1)) (asig_of(ioa2))" |
146 "compat_ioas ioa1 ioa2 == compat_asigs (asig_of(ioa1)) (asig_of(ioa2))" |
145 |
147 |
146 |
148 |
147 asig_comp_def |
149 asig_comp_def: |
148 "asig_comp a1 a2 == |
150 "asig_comp a1 a2 == |
149 (((inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)), |
151 (((inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)), |
150 (outputs(a1) Un outputs(a2)), |
152 (outputs(a1) Un outputs(a2)), |
151 (internals(a1) Un internals(a2))))" |
153 (internals(a1) Un internals(a2))))" |
152 |
154 |
153 |
155 |
154 par_def |
156 par_def: |
155 "(ioa1 || ioa2) == |
157 "(ioa1 || ioa2) == |
156 (asig_comp (asig_of ioa1) (asig_of ioa2), |
158 (asig_comp (asig_of ioa1) (asig_of ioa2), |
157 {pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)}, |
159 {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)) |
160 {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))) & |
161 in (a:actions(asig_of(ioa1)) | a:actions(asig_of(ioa2))) & |
160 (if a:actions(asig_of(ioa1)) then |
162 (if a:actions(asig_of(ioa1)) then |
161 (fst(s),a,fst(t)):trans_of(ioa1) |
163 (fst(s),a,fst(t)):trans_of(ioa1) |
162 else fst(t) = fst(s)) |
164 else fst(t) = fst(s)) |
163 & |
165 & |
164 (if a:actions(asig_of(ioa2)) then |
166 (if a:actions(asig_of(ioa2)) then |
165 (snd(s),a,snd(t)):trans_of(ioa2) |
167 (snd(s),a,snd(t)):trans_of(ioa2) |
166 else snd(t) = snd(s))})" |
168 else snd(t) = snd(s))})" |
167 |
169 |
168 |
170 |
169 restrict_asig_def |
171 restrict_asig_def: |
170 "restrict_asig asig actns == |
172 "restrict_asig asig actns == |
171 (inputs(asig) Int actns, outputs(asig) Int actns, |
173 (inputs(asig) Int actns, outputs(asig) Int actns, |
172 internals(asig) Un (externals(asig) - actns))" |
174 internals(asig) Un (externals(asig) - actns))" |
173 |
175 |
174 |
176 |
175 restrict_def |
177 restrict_def: |
176 "restrict ioa actns == |
178 "restrict ioa actns == |
177 (restrict_asig (asig_of ioa) actns, starts_of(ioa), trans_of(ioa))" |
179 (restrict_asig (asig_of ioa) actns, starts_of(ioa), trans_of(ioa))" |
178 |
180 |
179 |
181 |
180 ioa_implements_def |
182 ioa_implements_def: |
181 "ioa_implements ioa1 ioa2 == |
183 "ioa_implements ioa1 ioa2 == |
182 ((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) & |
184 ((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) & |
183 (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2))) & |
185 (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2))) & |
184 traces(ioa1) <= traces(ioa2))" |
186 traces(ioa1) <= traces(ioa2))" |
185 |
187 |
186 rename_def |
188 rename_def: |
187 "rename ioa ren == |
189 "rename ioa ren == |
188 (({b. ? x. Some(x)= ren(b) & x : inputs(asig_of(ioa))}, |
190 (({b. ? x. Some(x)= ren(b) & x : inputs(asig_of(ioa))}, |
189 {b. ? x. Some(x)= ren(b) & x : outputs(asig_of(ioa))}, |
191 {b. ? x. Some(x)= ren(b) & x : outputs(asig_of(ioa))}, |
190 {b. ? x. Some(x)= ren(b) & x : internals(asig_of(ioa))}), |
192 {b. ? x. Some(x)= ren(b) & x : internals(asig_of(ioa))}), |
191 starts_of(ioa) , |
193 starts_of(ioa) , |
192 {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) |
194 {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) |
193 in |
195 in |
194 ? x. Some(x) = ren(a) & (s,x,t):trans_of(ioa)})" |
196 ? x. Some(x) = ren(a) & (s,x,t):trans_of(ioa)})" |
195 |
197 |
196 end |
198 ML {* use_legacy_bindings (the_context ()) *} |
|
199 |
|
200 end |