equal
deleted
inserted
replaced
165 | "is_init_sobj (S_dir sf tag) = (is_init_sfile sf)" |
165 | "is_init_sobj (S_dir sf tag) = (is_init_sfile sf)" |
166 | "is_init_sobj (S_msg" *) |
166 | "is_init_sobj (S_msg" *) |
167 |
167 |
168 fun is_many :: "t_sobject \<Rightarrow> bool" |
168 fun is_many :: "t_sobject \<Rightarrow> bool" |
169 where |
169 where |
170 "is_many (S_proc (Many, sec, fds, shms) tag) = True" |
170 "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)" |
171 | "is_many (S_file sfs tag) = (\<forall> sf \<in> sfs. is_many_sfile sf)" |
172 | "is_many (S_dir sf ) = is_many_sfile sf" |
172 | "is_many (S_dir sf ) = is_many_sfile sf" |
173 | "is_many (S_msgq sq ) = is_many_smsgq sq" |
173 | "is_many (S_msgq sq ) = is_many_smsgq sq" |
174 | "is_many (S_shm sh ) = is_many_sshm sh" |
174 | "is_many (S_shm sh ) = is_many_sshm sh" |
|
175 | "is_many _ = False" |
175 |
176 |
176 (* |
177 (* |
177 fun update_ss_sp:: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state" |
178 fun update_ss_sp:: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state" |
178 where |
179 where |
179 "update_ss_sp ss (S_proc sp tag) (S_proc sp' tag') = |
180 "update_ss_sp ss (S_proc sp tag) (S_proc sp' tag') = |