145 fun is_many_smsg :: "t_smsg \<Rightarrow> bool" |
145 fun is_many_smsg :: "t_smsg \<Rightarrow> bool" |
146 where |
146 where |
147 "is_many_smsg (Created,sec,tag) = True" |
147 "is_many_smsg (Created,sec,tag) = True" |
148 | "is_many_smsg _ = False" |
148 | "is_many_smsg _ = False" |
149 |
149 |
|
150 (* wrong def |
150 fun is_many_smsgq :: "t_smsgq \<Rightarrow> bool" |
151 fun is_many_smsgq :: "t_smsgq \<Rightarrow> bool" |
151 where |
152 where |
152 "is_many_smsgq (Created,sec,sms) = (True \<and> (\<forall> sm \<in> (set sms). is_many_smsg sm))" |
153 "is_many_smsgq (Created,sec,sms) = (True \<and> (\<forall> sm \<in> (set sms). is_many_smsg sm))" |
153 | "is_many_smsgq _ = False" |
154 | "is_many_smsgq _ = False" |
|
155 *) |
|
156 |
|
157 fun is_many_smsgq :: "t_smsgq \<Rightarrow> bool" |
|
158 where |
|
159 "is_many_smsgq (Created,sec,sms) = True" |
|
160 | "is_many_smsgq _ = False" |
154 |
161 |
155 fun is_many_sshm :: "t_sshm \<Rightarrow> bool" |
162 fun is_many_sshm :: "t_sshm \<Rightarrow> bool" |
156 where |
163 where |
157 "is_many_sshm (Created, sec) = True" |
164 "is_many_sshm (Created, sec) = True" |
158 | "is_many_sshm _ = False" |
165 | "is_many_sshm _ = False" |
159 |
|
160 (* |
|
161 fun is_init_sobj :: "t_sobject \<Rightarrow> bool" |
|
162 where |
|
163 "is_init_sobj (S_proc (popt, sec, fds, shms) tag) = (popt \<noteq> None)" |
|
164 | "is_init_sobj (S_file sf tag) = (is_init_sfile sf)" |
|
165 | "is_init_sobj (S_dir sf tag) = (is_init_sfile sf)" |
|
166 | "is_init_sobj (S_msg" *) |
|
167 |
166 |
168 fun is_many :: "t_sobject \<Rightarrow> bool" |
167 fun is_many :: "t_sobject \<Rightarrow> bool" |
169 where |
168 where |
170 "is_many (S_proc sp tag) = is_many_sproc sp" |
169 "is_many (S_proc sp tag) = is_many_sproc sp" |
171 | "is_many (S_file sfs tag) = (\<forall> sf \<in> sfs. is_many_sfile sf)" |
170 | "is_many (S_file sfs tag) = (\<forall> sf \<in> sfs. is_many_sfile sf)" |
172 | "is_many (S_dir sf ) = is_many_sfile sf" |
171 | "is_many (S_dir sf ) = is_many_sfile sf" |
173 | "is_many (S_msgq sq ) = is_many_smsgq sq" |
172 | "is_many (S_msgq sq ) = is_many_smsgq sq" |
174 | "is_many (S_shm sh ) = is_many_sshm sh" |
173 | "is_many (S_shm sh ) = is_many_sshm sh" |
|
174 |
|
175 fun is_init_smsgq :: "t_smsgq \<Rightarrow> bool" |
|
176 where |
|
177 "is_init_smsgq (Init q,sec,sms) = True" |
|
178 | "is_init_smsgq _ = False" |
|
179 |
|
180 fun is_init_sshm :: "t_sshm \<Rightarrow> bool" |
|
181 where |
|
182 "is_init_sshm (Init h,sec) = True" |
|
183 | "is_init_sshm _ = False" |
|
184 |
|
185 fun is_init_sobj :: "t_sobject \<Rightarrow> bool" |
|
186 where |
|
187 "is_init_sobj (S_proc sp tag ) = is_init_sproc sp" |
|
188 | "is_init_sobj (S_file sfs tag) = (\<exists> sf \<in> sfs. is_init_sfile sf)" |
|
189 | "is_init_sobj (S_dir sf ) = is_init_sfile sf" |
|
190 | "is_init_sobj (S_msgq sq ) = is_init_smsgq sq" |
|
191 | "is_init_sobj (S_shm sh ) = is_init_sshm sh" |
175 |
192 |
176 (* |
193 (* |
177 fun update_ss_sp:: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state" |
194 fun update_ss_sp:: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state" |
178 where |
195 where |
179 "update_ss_sp ss (S_proc sp tag) (S_proc sp' tag') = |
196 "update_ss_sp ss (S_proc sp tag) (S_proc sp' tag') = |