710 | _ \<Rightarrow> None)" |
710 | _ \<Rightarrow> None)" |
711 |
711 |
712 |
712 |
713 definition cpfd2sfds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sfd set" |
713 definition cpfd2sfds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sfd set" |
714 where |
714 where |
715 "cpfd2sfds s p \<equiv> {sfd. \<exists> fd sfd f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd}" |
715 "cpfd2sfds s p \<equiv> {sfd. \<exists> fd f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd}" |
716 |
716 |
717 definition ch2sshm :: "t_state \<Rightarrow> t_shm \<Rightarrow> t_sshm option" |
717 definition ch2sshm :: "t_state \<Rightarrow> t_shm \<Rightarrow> t_sshm option" |
718 where |
718 where |
719 "ch2sshm s h \<equiv> (case (sectxt_of_obj s (O_shm h)) of |
719 "ch2sshm s h \<equiv> (case (sectxt_of_obj s (O_shm h)) of |
720 Some sec \<Rightarrow> |
720 Some sec \<Rightarrow> |
721 Some (if (\<not> deleted (O_shm h) s \<and> h \<in> init_shms) then Init h else Created, sec) |
721 Some (if (\<not> deleted (O_shm h) s \<and> h \<in> init_shms) then Init h else Created, sec) |
722 | _ \<Rightarrow> None)" |
722 | _ \<Rightarrow> None)" |
723 |
723 |
724 definition cph2spshs :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc_sshm set" |
724 definition cph2spshs :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc_sshm set" |
725 where |
725 where |
726 "cph2spshs s p \<equiv> {(sh, flag) | sh flag h. (p, flag) \<in> procs_of_shm s h \<and> ch2sshm s h = Some sh}" |
726 "cph2spshs s p \<equiv> {(sh, flag). \<exists> h. (p, flag) \<in> procs_of_shm s h \<and> ch2sshm s h = Some sh}" |
727 |
727 |
728 definition cp2sproc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc option" |
728 definition cp2sproc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc option" |
729 where |
729 where |
730 "cp2sproc s p \<equiv> (case (sectxt_of_obj s (O_proc p)) of |
730 "cp2sproc s p \<equiv> (case (sectxt_of_obj s (O_proc p)) of |
731 Some sec \<Rightarrow> |
731 Some sec \<Rightarrow> |