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